1852 {
1853 assert(a.is_bool() && b.is_bool());
1855 }
1856 inline expr
implies(expr
const & a,
bool b) {
return implies(a, a.ctx().bool_val(b)); }
1857 inline expr
implies(
bool a, expr
const & b) {
return implies(b.ctx().bool_val(a), b); }
1858
1859
1861 inline expr
pw(expr
const & a,
int b) {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
1862 inline expr
pw(
int a, expr
const & b) {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
1863
1864 inline expr
mod(expr
const& a, expr
const& b) {
1865 if (a.is_bv()) {
1867 }
1868 else {
1870 }
1871 }
1872 inline expr
mod(expr
const & a,
int b) {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
1873 inline expr
mod(
int a, expr
const & b) {
return mod(b.ctx().num_val(a, b.get_sort()), b); }
1874
1875 inline expr
operator%(expr
const& a, expr
const& b) {
return mod(a, b); }
1876 inline expr
operator%(expr
const& a,
int b) {
return mod(a, b); }
1877 inline expr
operator%(
int a, expr
const& b) {
return mod(a, b); }
1878
1879
1880 inline expr
rem(expr
const& a, expr
const& b) {
1881 if (a.is_fpa() && b.is_fpa()) {
1883 } else {
1885 }
1886 }
1887 inline expr
rem(expr
const & a,
int b) {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
1888 inline expr
rem(
int a, expr
const & b) {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
1889
1890#undef _Z3_MK_BIN_
1891
1892#define _Z3_MK_UN_(a, mkun) \
1893 Z3_ast r = mkun(a.ctx(), a); \
1894 a.check_error(); \
1895 return expr(a.ctx(), r); \
1896
1897
1899 inline expr
complex(expr
const& re, expr
const& im) {
1902 re.check_error();
1903 return expr(re.ctx(), r);
1904 }
1905
1908 z.check_error();
1909 return expr(z.ctx(), r);
1910 }
1911
1914 z.check_error();
1915 return expr(z.ctx(), r);
1916 }
1917
1919
1921
1922#undef _Z3_MK_UN_
1923
1924 inline expr
operator&&(expr
const & a, expr
const & b) {
1926 assert(a.is_bool() && b.is_bool());
1927 Z3_ast args[2] = { a, b };
1929 a.check_error();
1930 return expr(a.ctx(), r);
1931 }
1932
1935
1936 inline expr
operator||(expr
const & a, expr
const & b) {
1938 assert(a.is_bool() && b.is_bool());
1939 Z3_ast args[2] = { a, b };
1941 a.check_error();
1942 return expr(a.ctx(), r);
1943 }
1944
1946
1948
1949 inline expr
operator==(expr
const & a, expr
const & b) {
1952 a.check_error();
1953 return expr(a.ctx(), r);
1954 }
1955 inline expr
operator==(expr
const & a,
int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa() || a.is_finite_field());
return a == a.ctx().num_val(b, a.get_sort()); }
1956 inline expr
operator==(
int a, expr
const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa() || b.is_finite_field());
return b.ctx().num_val(a, b.get_sort()) == b; }
1957 inline expr
operator==(expr
const & a,
double b) { assert(a.is_fpa());
return a == a.ctx().fpa_val(b); }
1958 inline expr
operator==(
double a, expr
const & b) { assert(b.is_fpa());
return b.ctx().fpa_val(a) == b; }
1959
1960 inline expr
operator!=(expr
const & a, expr
const & b) {
1962 Z3_ast args[2] = { a, b };
1964 a.check_error();
1965 return expr(a.ctx(), r);
1966 }
1967 inline expr
operator!=(expr
const & a,
int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa() || a.is_finite_field());
return a != a.ctx().num_val(b, a.get_sort()); }
1968 inline expr
operator!=(
int a, expr
const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa() || b.is_finite_field());
return b.ctx().num_val(a, b.get_sort()) != b; }
1969 inline expr
operator!=(expr
const & a,
double b) { assert(a.is_fpa());
return a != a.ctx().fpa_val(b); }
1970 inline expr
operator!=(
double a, expr
const & b) { assert(b.is_fpa());
return b.ctx().fpa_val(a) != b; }
1971
1972 inline expr
operator+(expr
const & a, expr
const & b) {
1975 if (a.is_arith() && b.is_arith()) {
1976 Z3_ast args[2] = { a, b };
1978 }
1979 else if (a.is_finite_field() && b.is_finite_field()) {
1980 Z3_ast args[2] = { a, b };
1982 }
1983 else if (a.is_bv() && b.is_bv()) {
1985 }
1986 else if (a.is_seq() && b.is_seq()) {
1988 }
1989 else if (a.is_re() && b.is_re()) {
1990 Z3_ast _args[2] = { a, b };
1992 }
1993 else if (a.is_fpa() && b.is_fpa()) {
1994 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1995 }
1996 else {
1997
1998 assert(false);
1999 }
2000 a.check_error();
2001 return expr(a.ctx(), r);
2002 }
2003 inline expr
operator+(expr
const & a,
int b) {
return a + a.
ctx().
num_val(b, a.get_sort()); }
2004 inline expr
operator+(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) + b; }
2005
2006 inline expr
operator*(expr
const & a, expr
const & b) {
2009 if (a.is_arith() && b.is_arith()) {
2010 Z3_ast args[2] = { a, b };
2012 }
2013 else if (a.is_finite_field() && b.is_finite_field()) {
2014 Z3_ast args[2] = { a, b };
2016 }
2017 else if (a.is_bv() && b.is_bv()) {
2019 }
2020 else if (a.is_fpa() && b.is_fpa()) {
2021 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2022 }
2023 else {
2024
2025 assert(false);
2026 }
2027 a.check_error();
2028 return expr(a.ctx(), r);
2029 }
2030 inline expr
operator*(expr
const & a,
int b) {
return a * a.
ctx().
num_val(b, a.get_sort()); }
2031 inline expr
operator*(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) * b; }
2032
2033
2034 inline expr
operator>=(expr
const & a, expr
const & b) {
2037 if (a.is_arith() && b.is_arith()) {
2039 }
2040 else if (a.is_bv() && b.is_bv()) {
2042 }
2043 else if (a.is_fpa() && b.is_fpa()) {
2045 }
2046 else {
2047
2048 assert(false);
2049 }
2050 a.check_error();
2051 return expr(a.ctx(), r);
2052 }
2053
2054 inline expr
operator/(expr
const & a, expr
const & b) {
2057 if (a.is_arith() && b.is_arith()) {
2059 }
2060 else if (a.is_bv() && b.is_bv()) {
2062 }
2063 else if (a.is_fpa() && b.is_fpa()) {
2064 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2065 }
2066 else {
2067
2068 assert(false);
2069 }
2070 a.check_error();
2071 return expr(a.ctx(), r);
2072 }
2073 inline expr
operator/(expr
const & a,
int b) {
return a / a.
ctx().
num_val(b, a.get_sort()); }
2074 inline expr
operator/(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) / b; }
2075
2078 if (a.is_arith()) {
2080 }
2081 else if (a.is_finite_field()) { r =
Z3_mk_ff_neg(a.ctx(), a); }
2082 else if (a.is_bv()) {
2084 }
2085 else if (a.is_fpa()) {
2087 }
2088 else {
2089
2090 assert(false);
2091 }
2092 a.check_error();
2093 return expr(a.ctx(), r);
2094 }
2095
2096 inline expr
operator-(expr
const & a, expr
const & b) {
2098 if (a.is_finite_field() && b.is_finite_field()) return a + -b;
2100 if (a.is_arith() && b.is_arith()) {
2101 Z3_ast args[2] = { a, b };
2103 }
2104 else if (a.is_bv() && b.is_bv()) {
2106 }
2107 else if (a.is_fpa() && b.is_fpa()) {
2108 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
2109 }
2110 else {
2111
2112 assert(false);
2113 }
2114 a.check_error();
2115 return expr(a.ctx(), r);
2116 }
2117 inline expr
operator-(expr
const & a,
int b) {
return a - a.
ctx().
num_val(b, a.get_sort()); }
2118 inline expr
operator-(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) - b; }
2119
2120 inline expr
operator<=(expr
const & a, expr
const & b) {
2123 if (a.is_arith() && b.is_arith()) {
2125 }
2126 else if (a.is_bv() && b.is_bv()) {
2128 }
2129 else if (a.is_fpa() && b.is_fpa()) {
2131 }
2132 else {
2133
2134 assert(false);
2135 }
2136 a.check_error();
2137 return expr(a.ctx(), r);
2138 }
2139 inline expr
operator<=(expr
const & a,
int b) {
return a <= a.
ctx().
num_val(b, a.get_sort()); }
2140 inline expr
operator<=(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) <= b; }
2141
2142 inline expr
operator>=(expr
const & a,
int b) {
return a >= a.
ctx().
num_val(b, a.get_sort()); }
2143 inline expr
operator>=(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) >= b; }
2144
2145 inline expr
operator<(expr
const & a, expr
const & b) {
2148 if (a.is_arith() && b.is_arith()) {
2150 }
2151 else if (a.is_bv() && b.is_bv()) {
2153 }
2154 else if (a.is_fpa() && b.is_fpa()) {
2156 }
2157 else {
2158
2159 assert(false);
2160 }
2161 a.check_error();
2162 return expr(a.ctx(), r);
2163 }
2164 inline expr
operator<(expr
const & a,
int b) {
return a < a.
ctx().
num_val(b, a.get_sort()); }
2165 inline expr
operator<(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) < b; }
2166
2167 inline expr
operator>(expr
const & a, expr
const & b) {
2170 if (a.is_arith() && b.is_arith()) {
2172 }
2173 else if (a.is_bv() && b.is_bv()) {
2175 }
2176 else if (a.is_fpa() && b.is_fpa()) {
2178 }
2179 else {
2180
2181 assert(false);
2182 }
2183 a.check_error();
2184 return expr(a.ctx(), r);
2185 }
2186 inline expr
operator>(expr
const & a,
int b) {
return a > a.
ctx().
num_val(b, a.get_sort()); }
2187 inline expr
operator>(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) > b; }
2188
2189 inline expr
operator&(expr
const & a, expr
const & b) {
if (a.is_bool())
return a && b;
check_context(a, b);
Z3_ast r =
Z3_mk_bvand(a.ctx(), a, b); a.check_error();
return expr(a.ctx(), r); }
2190 inline expr
operator&(expr
const & a,
int b) {
return a & a.
ctx().
num_val(b, a.get_sort()); }
2191 inline expr
operator&(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) & b; }
2192
2194 inline expr
operator^(expr
const & a,
int b) {
return a ^ a.
ctx().
num_val(b, a.get_sort()); }
2195 inline expr
operator^(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) ^ b; }
2196
2197 inline expr
operator|(expr
const & a, expr
const & b) {
if (a.is_bool())
return a || b;
check_context(a, b);
Z3_ast r =
Z3_mk_bvor(a.ctx(), a, b); a.check_error();
return expr(a.ctx(), r); }
2198 inline expr
operator|(expr
const & a,
int b) {
return a | a.
ctx().
num_val(b, a.get_sort()); }
2199 inline expr
operator|(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) | b; }
2200
2201 inline expr
nand(expr
const& a, expr
const& b) {
if (a.is_bool())
return !(a && b);
check_context(a, b);
Z3_ast r =
Z3_mk_bvnand(a.ctx(), a, b); a.check_error();
return expr(a.ctx(), r); }
2202 inline expr
nor(expr
const& a, expr
const& b) {
if (a.is_bool())
return !(a || b);
check_context(a, b);
Z3_ast r =
Z3_mk_bvnor(a.ctx(), a, b); a.check_error();
return expr(a.ctx(), r); }
2203 inline expr
xnor(expr
const& a, expr
const& b) {
if (a.is_bool())
return !(a ^ b);
check_context(a, b);
Z3_ast r =
Z3_mk_bvxnor(a.ctx(), a, b); a.check_error();
return expr(a.ctx(), r); }
2204 inline expr
min(expr
const& a, expr
const& b) {
2207 if (a.is_arith()) {
2209 }
2210 else if (a.is_bv()) {
2212 }
2213 else {
2214 assert(a.is_fpa());
2216 }
2217 a.check_error();
2218 return expr(a.ctx(), r);
2219 }
2220 inline expr
max(expr
const& a, expr
const& b) {
2223 if (a.is_arith()) {
2225 }
2226 else if (a.is_bv()) {
2228 }
2229 else {
2230 assert(a.is_fpa());
2232 }
2233 a.check_error();
2234 return expr(a.ctx(), r);
2235 }
2236 inline expr
bvredor(expr
const & a) {
2237 assert(a.is_bv());
2239 a.check_error();
2240 return expr(a.ctx(), r);
2241 }
2242 inline expr
bvredand(expr
const & a) {
2243 assert(a.is_bv());
2245 a.check_error();
2246 return expr(a.ctx(), r);
2247 }
2248 inline expr
abs(expr
const & a) {
2250 if (a.is_int()) {
2251 expr zero = a.ctx().int_val(0);
2252 expr ge = a >= zero;
2253 expr na = -a;
2255 }
2256 else if (a.is_real()) {
2257 expr zero = a.ctx().real_val(0);
2258 expr ge = a >= zero;
2259 expr na = -a;
2261 }
2262 else {
2264 }
2265 a.check_error();
2266 return expr(a.ctx(), r);
2267 }
2268 inline expr
sqrt(expr
const & a, expr
const& rm) {
2270 assert(a.is_fpa());
2272 a.check_error();
2273 return expr(a.ctx(), r);
2274 }
2275 inline expr
fp_eq(expr
const & a, expr
const & b) {
2277 assert(a.is_fpa());
2279 a.check_error();
2280 return expr(a.ctx(), r);
2281 }
2283
2284 inline expr
fma(expr
const& a, expr
const& b, expr
const& c, expr
const& rm) {
2286 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2288 a.check_error();
2289 return expr(a.ctx(), r);
2290 }
2291
2292 inline expr
fpa_fp(expr
const& sgn, expr
const& exp, expr
const& sig) {
2294 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2296 sgn.check_error();
2297 return expr(sgn.ctx(), r);
2298 }
2299
2300 inline expr
fpa_to_sbv(expr
const& t,
unsigned sz) {
2301 assert(t.is_fpa());
2303 t.check_error();
2304 return expr(t.ctx(), r);
2305 }
2306
2307 inline expr
fpa_to_ubv(expr
const& t,
unsigned sz) {
2308 assert(t.is_fpa());
2310 t.check_error();
2311 return expr(t.ctx(), r);
2312 }
2313
2314 inline expr
sbv_to_fpa(expr
const& t, sort s) {
2315 assert(t.is_bv());
2317 t.check_error();
2318 return expr(t.ctx(), r);
2319 }
2320
2321 inline expr
ubv_to_fpa(expr
const& t, sort s) {
2322 assert(t.is_bv());
2324 t.check_error();
2325 return expr(t.ctx(), r);
2326 }
2327
2328 inline expr
fpa_to_fpa(expr
const& t, sort s) {
2329 assert(t.is_fpa());
2331 t.check_error();
2332 return expr(t.ctx(), r);
2333 }
2334
2336 assert(t.is_fpa());
2338 t.check_error();
2339 return expr(t.ctx(), r);
2340 }
2341
2347 inline expr
ite(expr
const & c, expr
const & t, expr
const & e) {
2349 assert(c.is_bool());
2351 c.check_error();
2352 return expr(c.ctx(), r);
2353 }
2354
2355
2360 inline expr
to_expr(context & c, Z3_ast a) {
2366 return expr(c, a);
2367 }
2368
2369 inline sort
to_sort(context & c, Z3_sort s) {
2371 return sort(c, s);
2372 }
2373
2374 inline func_decl
to_func_decl(context & c, Z3_func_decl f) {
2376 return func_decl(c, f);
2377 }
2378
2382 inline expr
sle(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsle(a.ctx(), a, b)); }
2383 inline expr
sle(expr
const & a,
int b) {
return sle(a, a.ctx().num_val(b, a.get_sort())); }
2384 inline expr
sle(
int a, expr
const & b) {
return sle(b.ctx().num_val(a, b.get_sort()), b); }
2388 inline expr
slt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvslt(a.ctx(), a, b)); }
2389 inline expr
slt(expr
const & a,
int b) {
return slt(a, a.ctx().num_val(b, a.get_sort())); }
2390 inline expr
slt(
int a, expr
const & b) {
return slt(b.ctx().num_val(a, b.get_sort()), b); }
2394 inline expr
sge(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsge(a.ctx(), a, b)); }
2395 inline expr
sge(expr
const & a,
int b) {
return sge(a, a.ctx().num_val(b, a.get_sort())); }
2396 inline expr
sge(
int a, expr
const & b) {
return sge(b.ctx().num_val(a, b.get_sort()), b); }
2400 inline expr
sgt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsgt(a.ctx(), a, b)); }
2401 inline expr
sgt(expr
const & a,
int b) {
return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2402 inline expr
sgt(
int a, expr
const & b) {
return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2403
2404
2408 inline expr
ule(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvule(a.ctx(), a, b)); }
2409 inline expr
ule(expr
const & a,
int b) {
return ule(a, a.ctx().num_val(b, a.get_sort())); }
2410 inline expr
ule(
int a, expr
const & b) {
return ule(b.ctx().num_val(a, b.get_sort()), b); }
2414 inline expr
ult(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvult(a.ctx(), a, b)); }
2415 inline expr
ult(expr
const & a,
int b) {
return ult(a, a.ctx().num_val(b, a.get_sort())); }
2416 inline expr
ult(
int a, expr
const & b) {
return ult(b.ctx().num_val(a, b.get_sort()), b); }
2420 inline expr
uge(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvuge(a.ctx(), a, b)); }
2421 inline expr
uge(expr
const & a,
int b) {
return uge(a, a.ctx().num_val(b, a.get_sort())); }
2422 inline expr
uge(
int a, expr
const & b) {
return uge(b.ctx().num_val(a, b.get_sort()), b); }
2426 inline expr
ugt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvugt(a.ctx(), a, b)); }
2427 inline expr
ugt(expr
const & a,
int b) {
return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2428 inline expr
ugt(
int a, expr
const & b) {
return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2429
2434 inline expr
sdiv(expr
const & a,
int b) {
return sdiv(a, a.ctx().num_val(b, a.get_sort())); }
2435 inline expr
sdiv(
int a, expr
const & b) {
return sdiv(b.ctx().num_val(a, b.get_sort()), b); }
2436
2441 inline expr
udiv(expr
const & a,
int b) {
return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2442 inline expr
udiv(
int a, expr
const & b) {
return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2443
2448 inline expr
srem(expr
const & a,
int b) {
return srem(a, a.ctx().num_val(b, a.get_sort())); }
2449 inline expr
srem(
int a, expr
const & b) {
return srem(b.ctx().num_val(a, b.get_sort()), b); }
2450
2455 inline expr
smod(expr
const & a,
int b) {
return smod(a, a.ctx().num_val(b, a.get_sort())); }
2456 inline expr
smod(
int a, expr
const & b) {
return smod(b.ctx().num_val(a, b.get_sort()), b); }
2457
2462 inline expr
urem(expr
const & a,
int b) {
return urem(a, a.ctx().num_val(b, a.get_sort())); }
2463 inline expr
urem(
int a, expr
const & b) {
return urem(b.ctx().num_val(a, b.get_sort()), b); }
2464
2468 inline expr
shl(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvshl(a.ctx(), a, b)); }
2469 inline expr
shl(expr
const & a,
int b) {
return shl(a, a.ctx().num_val(b, a.get_sort())); }
2470 inline expr
shl(
int a, expr
const & b) {
return shl(b.ctx().num_val(a, b.get_sort()), b); }
2471
2476 inline expr
lshr(expr
const & a,
int b) {
return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2477 inline expr
lshr(
int a, expr
const & b) {
return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2478
2483 inline expr
ashr(expr
const & a,
int b) {
return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2484 inline expr
ashr(
int a, expr
const & b) {
return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2485
2490
2494 inline expr
bv2int(expr
const& a,
bool is_signed) {
Z3_ast r =
Z3_mk_bv2int(a.ctx(), a, is_signed); a.check_error();
return expr(a.ctx(), r); }
2495 inline expr
int2bv(
unsigned n, expr
const& a) {
Z3_ast r =
Z3_mk_int2bv(a.ctx(), n, a); a.check_error();
return expr(a.ctx(), r); }
2496
2502 }
2505 }
2508 }
2511 }
2514 }
2517 }
2520 }
2523 }
2524
2525
2530
2531 inline func_decl
linear_order(sort
const& a,
unsigned index) {
2533 }
2534 inline func_decl
partial_order(sort
const& a,
unsigned index) {
2536 }
2539 }
2540 inline func_decl
tree_order(sort
const& a,
unsigned index) {
2542 }
2543
2553 p.check_error();
2555 }
2556
2557 template<> class cast_ast<ast> {
2558 public:
2559 ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2560 };
2561
2562 template<> class cast_ast<expr> {
2563 public:
2564 expr operator()(context & c, Z3_ast a) {
2569 return expr(c, a);
2570 }
2571 };
2572
2573 template<> class cast_ast<sort> {
2574 public:
2575 sort operator()(context & c, Z3_ast a) {
2577 return sort(c,
reinterpret_cast<Z3_sort>(a));
2578 }
2579 };
2580
2581 template<> class cast_ast<func_decl> {
2582 public:
2583 func_decl operator()(context & c, Z3_ast a) {
2585 return func_decl(c,
reinterpret_cast<Z3_func_decl>(a));
2586 }
2587 };
2588
2589 template<typename T>
2590 template<typename T2>
2591 array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2592 for (unsigned i = 0; i < m_size; ++i) {
2593 m_array[i] = v[i];
2594 }
2595 }
2596
2597
2598
2599 inline expr
forall(expr
const & x, expr
const & b) {
2603 }
2604 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & b) {
2608 }
2609 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2613 }
2614 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2618 }
2619 inline expr
forall(expr_vector
const & xs, expr
const & b) {
2620 array<Z3_app> vars(xs);
2621 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2622 }
2623 inline expr
exists(expr
const & x, expr
const & b) {
2627 }
2628 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & b) {
2632 }
2633 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2637 }
2638 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2642 }
2643 inline expr
exists(expr_vector
const & xs, expr
const & b) {
2644 array<Z3_app> vars(xs);
2645 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, vars.size(), vars.ptr(), 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2646 }
2647 inline expr
lambda(expr
const & x, expr
const & b) {
2651 }
2652 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & b) {
2656 }
2657 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2661 }
2662 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2666 }
2667 inline expr
lambda(expr_vector
const & xs, expr
const & b) {
2668 array<Z3_app> vars(xs);
2670 }
2671
2672 inline expr
pble(expr_vector
const& es,
int const* coeffs,
int bound) {
2673 assert(es.size() > 0);
2674 context& ctx = es[0u].ctx();
2675 array<Z3_ast> _es(es);
2677 ctx.check_error();
2678 return expr(ctx, r);
2679 }
2680 inline expr
pbge(expr_vector
const& es,
int const* coeffs,
int bound) {
2681 assert(es.size() > 0);
2682 context& ctx = es[0u].ctx();
2683 array<Z3_ast> _es(es);
2685 ctx.check_error();
2686 return expr(ctx, r);
2687 }
2688 inline expr
pbeq(expr_vector
const& es,
int const* coeffs,
int bound) {
2689 assert(es.size() > 0);
2690 context& ctx = es[0u].ctx();
2691 array<Z3_ast> _es(es);
2693 ctx.check_error();
2694 return expr(ctx, r);
2695 }
2696 inline expr
atmost(expr_vector
const& es,
unsigned bound) {
2697 assert(es.size() > 0);
2698 context& ctx = es[0u].ctx();
2699 array<Z3_ast> _es(es);
2701 ctx.check_error();
2702 return expr(ctx, r);
2703 }
2704 inline expr
atleast(expr_vector
const& es,
unsigned bound) {
2705 assert(es.size() > 0);
2706 context& ctx = es[0u].ctx();
2707 array<Z3_ast> _es(es);
2709 ctx.check_error();
2710 return expr(ctx, r);
2711 }
2712 inline expr
sum(expr_vector
const& args) {
2713 assert(args.size() > 0);
2714 context& ctx = args[0u].ctx();
2715 array<Z3_ast> _args(args);
2717 ctx.check_error();
2718 return expr(ctx, r);
2719 }
2720
2721 inline expr
distinct(expr_vector
const& args) {
2722 assert(args.size() > 0);
2723 context& ctx = args[0u].ctx();
2724 array<Z3_ast> _args(args);
2726 ctx.check_error();
2727 return expr(ctx, r);
2728 }
2729
2730 inline expr
concat(expr
const& a, expr
const& b) {
2734 Z3_ast _args[2] = { a, b };
2736 }
2738 Z3_ast _args[2] = { a, b };
2740 }
2741 else {
2743 }
2744 a.ctx().check_error();
2745 return expr(a.ctx(), r);
2746 }
2747
2748 inline expr
concat(expr_vector
const& args) {
2750 assert(args.size() > 0);
2751 if (args.size() == 1) {
2752 return args[0u];
2753 }
2754 context& ctx = args[0u].ctx();
2755 array<Z3_ast> _args(args);
2758 }
2761 }
2762 else {
2763 r = _args[args.size()-1];
2764 for (unsigned i = args.size()-1; i > 0; ) {
2765 --i;
2767 ctx.check_error();
2768 }
2769 }
2770 ctx.check_error();
2771 return expr(ctx, r);
2772 }
2773
2774 inline expr
map(expr
const& f, expr
const& list) {
2775 context& ctx = f.
ctx();
2777 ctx.check_error();
2778 return expr(ctx, r);
2779 }
2780
2781 inline expr
mapi(expr
const& f, expr
const& i, expr
const& list) {
2782 context& ctx = f.
ctx();
2784 ctx.check_error();
2785 return expr(ctx, r);
2786 }
2787
2788 inline expr
foldl(expr
const& f, expr
const& a, expr
const& list) {
2789 context& ctx = f.
ctx();
2791 ctx.check_error();
2792 return expr(ctx, r);
2793 }
2794
2795 inline expr
foldli(expr
const& f, expr
const& i, expr
const& a, expr
const& list) {
2796 context& ctx = f.
ctx();
2798 ctx.check_error();
2799 return expr(ctx, r);
2800 }
2801
2802 inline expr
mk_or(expr_vector
const& args) {
2803 array<Z3_ast> _args(args);
2805 args.check_error();
2806 return expr(args.ctx(), r);
2807 }
2808 inline expr
mk_and(expr_vector
const& args) {
2809 array<Z3_ast> _args(args);
2811 args.check_error();
2812 return expr(args.ctx(), r);
2813 }
2814 inline expr
mk_xor(expr_vector
const& args) {
2815 if (args.empty())
2817 expr r = args[0u];
2818 for (unsigned i = 1; i < args.size(); ++i)
2819 r = r ^ args[i];
2820 return r;
2821 }
2822
2823
2824 class func_entry : public object {
2826 void init(Z3_func_entry e) {
2827 m_entry = e;
2829 }
2830 public:
2831 func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2832 func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2835 func_entry & operator=(func_entry const & s) {
2838 object::operator=(s);
2839 m_entry = s.m_entry;
2840 return *this;
2841 }
2845 };
2846
2847 class func_interp : public object {
2849 void init(Z3_func_interp e) {
2850 m_interp = e;
2852 }
2853 public:
2854 func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2855 func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2858 func_interp & operator=(func_interp const & s) {
2861 object::operator=(s);
2862 m_interp = s.m_interp;
2863 return *this;
2864 }
2868 void add_entry(expr_vector const& args, expr& value) {
2870 check_error();
2871 }
2872 void set_else(expr& value) {
2874 check_error();
2875 }
2876 };
2877
2878 class model : public object {
2880 void init(Z3_model m) {
2881 m_model = m;
2883 }
2884 public:
2885 struct translate {};
2886 model(context & c):object(c) { init(
Z3_mk_model(c)); }
2887 model(context & c, Z3_model m):object(c) { init(m); }
2888 model(model const & s):object(s) { init(s.m_model); }
2889 model(model& src, context& dst, translate) : object(dst) { init(
Z3_model_translate(src.ctx(), src, dst)); }
2891 operator Z3_model()
const {
return m_model; }
2892 model & operator=(model const & s) {
2895 object::operator=(s);
2896 m_model = s.m_model;
2897 return *this;
2898 }
2899
2900 expr eval(expr const & n, bool model_completion=false) const {
2903 bool status =
Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2904 check_error();
2905 if (status == false && ctx().enable_exceptions())
2906 Z3_THROW(exception(
"failed to evaluate expression"));
2907 return expr(ctx(), r);
2908 }
2909
2914 unsigned size() const { return num_consts() + num_funcs(); }
2915 func_decl operator[](int i) const {
2916 assert(0 <= i);
2917 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2918 }
2919
2920
2921
2922
2923 expr get_const_interp(func_decl c) const {
2926 check_error();
2927 return expr(ctx(), r);
2928 }
2929 func_interp get_func_interp(func_decl f) const {
2932 check_error();
2933 return func_interp(ctx(), r);
2934 }
2935
2936
2937
2938 bool has_interp(func_decl f) const {
2941 }
2942
2943 func_interp add_func_interp(func_decl& f, expr& else_val) {
2945 check_error();
2946 return func_interp(ctx(), r);
2947 }
2948
2949 void add_const_interp(func_decl& f, expr& value) {
2951 check_error();
2952 }
2953
2954 unsigned num_sorts() const {
2956 check_error();
2957 return r;
2958 }
2959
2964 sort get_sort(unsigned i) const {
2966 check_error();
2967 return sort(ctx(), s);
2968 }
2969
2973 check_error();
2975 }
2976
2977 friend std::ostream &
operator<<(std::ostream & out, model
const & m);
2978
2979 std::string to_string()
const {
return m_model ? std::string(
Z3_model_to_string(ctx(), m_model)) :
"null"; }
2980 };
2981
2982 inline expr
qe_lite(expr_vector
const& vars, expr
const& body) {
2984 Z3_ast r = Z3_qe_lite(body.ctx(), vars, body);
2985 body.check_error();
2986 return expr(body.ctx(), r);
2987 }
2988
2989 inline std::vector<Z3_app>
to_apps(expr_vector
const& bounds) {
2990 std::vector<Z3_app> apps;
2991 for (unsigned i = 0; i < bounds.size(); ++i) {
2992 if (!
Z3_is_app(bounds.ctx(), bounds[i]))
2993 Z3_THROW(exception(
"model projection bounds must be applications"));
2994 apps.push_back(
Z3_to_app(bounds.ctx(), bounds[i]));
2995 }
2996 return apps;
2997 }
2998
2999 inline expr
qe_model_project(model
const& m, expr_vector
const& bounds, expr
const& body) {
3001 std::vector<Z3_app> apps =
to_apps(bounds);
3002 Z3_ast r = Z3_qe_model_project(m.ctx(), m, bounds.size(), apps.data(), body);
3003 m.check_error();
3004 return expr(m.ctx(), r);
3005 }
3006
3010 inline expr
qe_model_project_skolem(model
const& m, expr_vector
const& bounds, expr
const& body, ast_map& map) {
3012 std::vector<Z3_app> apps =
to_apps(bounds);
3013 Z3_ast r = Z3_qe_model_project_skolem(m.ctx(), m, bounds.size(), apps.data(), body, map);
3014 m.check_error();
3015 return expr(m.ctx(), r);
3016 }
3017
3023 std::vector<Z3_app> apps =
to_apps(bounds);
3024 Z3_ast r = Z3_qe_model_project_with_witness(m.ctx(), m, bounds.size(), apps.data(), body, map);
3025 m.check_error();
3026 return expr(m.ctx(), r);
3027 }
3028
3029 inline std::ostream &
operator<<(std::ostream & out, model
const & m) {
return out << m.to_string(); }
3030
3031 class stats : public object {
3033 void init(Z3_stats e) {
3034 m_stats = e;
3036 }
3037 public:
3038 stats(context & c):object(c), m_stats(0) {}
3039 stats(context & c, Z3_stats e):object(c) { init(e); }
3040 stats(stats const & s):object(s) { init(s.m_stats); }
3042 operator Z3_stats()
const {
return m_stats; }
3043 stats & operator=(stats const & s) {
3046 object::operator=(s);
3047 m_stats = s.m_stats;
3048 return *this;
3049 }
3050 unsigned size()
const {
return Z3_stats_size(ctx(), m_stats); }
3052 bool is_uint(
unsigned i)
const {
bool r =
Z3_stats_is_uint(ctx(), m_stats, i); check_error();
return r; }
3053 bool is_double(
unsigned i)
const {
bool r =
Z3_stats_is_double(ctx(), m_stats, i); check_error();
return r; }
3054 unsigned uint_value(
unsigned i)
const {
unsigned r =
Z3_stats_get_uint_value(ctx(), m_stats, i); check_error();
return r; }
3055 double double_value(
unsigned i)
const {
double r =
Z3_stats_get_double_value(ctx(), m_stats, i); check_error();
return r; }
3056 friend std::ostream &
operator<<(std::ostream & out, stats
const & s);
3057 };
3059
3060
3061 inline std::ostream &
operator<<(std::ostream & out, check_result r) {
3062 if (r == unsat) out << "unsat";
3063 else if (r == sat) out << "sat";
3064 else out << "unknown";
3065 return out;
3066 }
3067
3078 class parameter {
3080 func_decl m_decl;
3081 unsigned m_index;
3082 context& ctx() const { return m_decl.ctx(); }
3083 void check_error() const { ctx().check_error(); }
3084 public:
3085 parameter(func_decl const& d, unsigned idx) : m_decl(d), m_index(idx) {
3086 if (ctx().enable_exceptions() && idx >= d.num_parameters())
3087 Z3_THROW(exception(
"parameter index is out of bounds"));
3089 }
3090 parameter(expr const& e, unsigned idx) : m_decl(e.decl()), m_index(idx) {
3091 if (ctx().enable_exceptions() && idx >= m_decl.num_parameters())
3092 Z3_THROW(exception(
"parameter index is out of bounds"));
3094 }
3103 };
3104
3105
3106 class solver : public object {
3108 void init(Z3_solver s) {
3109 m_solver = s;
3110 if (s)
3112 }
3113 public:
3114 struct simple {};
3115 struct translate {};
3116 solver(context & c):object(c) { init(
Z3_mk_solver(c)); check_error(); }
3118 solver(context & c, Z3_solver s):object(c) { init(s); }
3119 solver(context & c,
char const * logic):object(c) { init(
Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
3120 solver(context & c, solver
const& src, translate): object(c) {
Z3_solver s =
Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
3121 solver(solver const & s):object(s) { init(s.m_solver); }
3122 solver(solver const& s, simplifier const& simp);
3124 operator Z3_solver()
const {
return m_solver; }
3125 solver & operator=(solver const & s) {
3128 object::operator=(s);
3129 m_solver = s.m_solver;
3130 return *this;
3131 }
3133 void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
3134 void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
3135 void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
3136 void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
3137 void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
3149 void pop(
unsigned n = 1) {
Z3_solver_pop(ctx(), m_solver, n); check_error(); }
3151 void add(expr
const & e) { assert(e.is_bool());
Z3_solver_assert(ctx(), m_solver, e); check_error(); }
3152 void add(expr const & e, expr const & p) {
3153 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
3155 check_error();
3156 }
3157 void add(expr const & e, char const * p) {
3158 add(e, ctx().bool_const(p));
3159 }
3160 void add(expr_vector const& v) {
3162 for (unsigned i = 0; i < v.size(); ++i)
3163 add(v[i]);
3164 }
3165 void from_file(
char const* file) {
Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
3166 void from_string(
char const* s) {
Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
3167
3169 check_result check(
unsigned n, expr *
const assumptions) {
3170 array<Z3_ast> _assumptions(n);
3171 for (unsigned i = 0; i < n; ++i) {
3173 _assumptions[i] = assumptions[i];
3174 }
3176 check_error();
3178 }
3180 unsigned n = assumptions.size();
3181 array<Z3_ast> _assumptions(n);
3182 for (unsigned i = 0; i < n; ++i) {
3184 _assumptions[i] = assumptions[i];
3185 }
3187 check_error();
3189 }
3191 check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
3193 check_error();
3195 }
3203 expr_vector trail(array<unsigned>& levels)
const {
3205 check_error();
3207 unsigned sz = result.size();
3208 levels.resize(sz);
3210 check_error();
3211 return result;
3212 }
3213 expr congruence_root(expr const& t) const {
3216 check_error();
3217 return expr(ctx(), r);
3218 }
3219 expr congruence_next(expr const& t) const {
3222 check_error();
3223 return expr(ctx(), r);
3224 }
3225 expr congruence_explain(expr const& a, expr const& b) const {
3229 check_error();
3230 return expr(ctx(), r);
3231 }
3232 void set_initial_value(expr const& var, expr const& value) {
3234 check_error();
3235 }
3236 void set_initial_value(expr const& var, int i) {
3237 set_initial_value(var, ctx().num_val(i, var.get_sort()));
3238 }
3239 void set_initial_value(expr const& var, bool b) {
3240 set_initial_value(var, ctx().bool_val(b));
3241 }
3242
3243 void solve_for(expr_vector const& vars, expr_vector& terms, expr_vector& guards) {
3244
3246 for (unsigned i = 0; i < vars.size(); ++i) {
3248 variables.push_back(vars[i]);
3249 }
3250
3254 check_error();
3255 }
3256
3257 void import_model_converter(solver const& src) {
3260 check_error();
3261 }
3262
3264 friend std::ostream &
operator<<(std::ostream & out, solver
const & s);
3265
3266 std::string to_smt2(char const* status = "unknown") {
3267 array<Z3_ast> es(assertions());
3268 Z3_ast const* fmls = es.ptr();
3270 unsigned sz = es.size();
3271 if (sz > 0) {
3272 --sz;
3273 fml = fmls[sz];
3274 }
3275 else {
3276 fml = ctx().bool_val(true);
3277 }
3279 ctx(),
3280 "", "", status, "",
3281 sz,
3282 fmls,
3283 fml));
3284 }
3285
3286 std::string dimacs(
bool include_names =
true)
const {
return std::string(
Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
3287
3289
3290
3291 expr_vector cube(expr_vector& vars,
unsigned cutoff) {
3293 check_error();
3295 }
3296
3297 class cube_iterator {
3298 solver& m_solver;
3299 unsigned& m_cutoff;
3302 bool m_end;
3303 bool m_empty;
3304
3305 void inc() {
3306 assert(!m_end && !m_empty);
3307 m_cube = m_solver.cube(m_vars, m_cutoff);
3308 m_cutoff = 0xFFFFFFFF;
3309 if (m_cube.size() == 1 && m_cube[0u].is_false()) {
3311 m_end = true;
3312 }
3313 else if (m_cube.empty()) {
3314 m_empty = true;
3315 }
3316 }
3317 public:
3318 cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
3319 m_solver(s),
3320 m_cutoff(cutoff),
3321 m_vars(vars),
3322 m_cube(s.ctx()),
3323 m_end(end),
3324 m_empty(false) {
3325 if (!m_end) {
3326 inc();
3327 }
3328 }
3329
3330 cube_iterator& operator++() {
3331 assert(!m_end);
3332 if (m_empty) {
3333 m_end = true;
3334 }
3335 else {
3336 inc();
3337 }
3338 return *this;
3339 }
3340 cube_iterator operator++(int) { assert(false); return *this; }
3343
3344 bool operator==(cube_iterator
const& other)
const noexcept {
3345 return other.m_end == m_end;
3346 }
3347 bool operator!=(cube_iterator
const& other)
const noexcept {
3348 return other.m_end != m_end;
3349 }
3350
3351 };
3352
3353 class cube_generator {
3354 solver& m_solver;
3355 unsigned m_cutoff;
3358 public:
3359 cube_generator(solver& s):
3360 m_solver(s),
3361 m_cutoff(0xFFFFFFFF),
3362 m_default_vars(s.ctx()),
3363 m_vars(m_default_vars)
3364 {}
3365
3366 cube_generator(solver& s, expr_vector& vars):
3367 m_solver(s),
3368 m_cutoff(0xFFFFFFFF),
3369 m_default_vars(s.ctx()),
3370 m_vars(vars)
3371 {}
3372
3373 cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
3374 cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
3375 void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
3376 };
3377
3378 cube_generator cubes() { return cube_generator(*this); }
3379 cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
3380
3381 };
3383
3384 class goal : public object {
3385 Z3_goal m_goal;
3386 void init(Z3_goal s) {
3387 m_goal = s;
3389 }
3390 public:
3391 goal(context & c,
bool models=
true,
bool unsat_cores=
false,
bool proofs=
false):object(c) { init(
Z3_mk_goal(c, models, unsat_cores, proofs)); }
3392 goal(context & c, Z3_goal s):object(c) { init(s); }
3393 goal(goal const & s):object(s) { init(s.m_goal); }
3395 operator Z3_goal() const { return m_goal; }
3396 goal & operator=(goal const & s) {
3399 object::operator=(s);
3400 m_goal = s.m_goal;
3401 return *this;
3402 }
3404 void add(expr_vector
const& v) {
check_context(*
this, v);
for (
unsigned i = 0; i < v.size(); ++i) add(v[i]); }
3405 unsigned size()
const {
return Z3_goal_size(ctx(), m_goal); }
3406 expr operator[](
int i)
const { assert(0 <= i);
Z3_ast r =
Z3_goal_formula(ctx(), m_goal, i); check_error();
return expr(ctx(), r); }
3409 unsigned depth()
const {
return Z3_goal_depth(ctx(), m_goal); }
3414 model convert_model(model const & m) const {
3417 check_error();
3418 return model(ctx(), new_m);
3419 }
3420 model get_model() const {
3422 check_error();
3423 return model(ctx(), new_m);
3424 }
3425 expr as_expr() const {
3426 unsigned n = size();
3427 if (n == 0)
3428 return ctx().bool_val(true);
3429 else if (n == 1)
3430 return operator[](0u);
3431 else {
3432 array<Z3_ast> args(n);
3433 for (unsigned i = 0; i < n; ++i)
3434 args[i] = operator[](i);
3435 return expr(ctx(),
Z3_mk_and(ctx(), n, args.ptr()));
3436 }
3437 }
3438 std::string dimacs(
bool include_names =
true)
const {
return std::string(
Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
3439 friend std::ostream &
operator<<(std::ostream & out, goal
const & g);
3440 };
3442
3443 class apply_result : public object {
3444 Z3_apply_result m_apply_result;
3445 void init(Z3_apply_result s) {
3446 m_apply_result = s;
3448 }
3449 public:
3450 apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
3451 apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
3453 operator Z3_apply_result() const { return m_apply_result; }
3454 apply_result & operator=(apply_result const & s) {
3457 object::operator=(s);
3458 m_apply_result = s.m_apply_result;
3459 return *this;
3460 }
3462 goal operator[](
int i)
const { assert(0 <= i); Z3_goal r =
Z3_apply_result_get_subgoal(ctx(), m_apply_result, i); check_error();
return goal(ctx(), r); }
3463 friend std::ostream &
operator<<(std::ostream & out, apply_result
const & r);
3464 };
3466
3467 class tactic : public object {
3468 Z3_tactic m_tactic;
3469 void init(Z3_tactic s) {
3470 m_tactic = s;
3472 }
3473 public:
3474 tactic(context & c,
char const * name):object(c) { Z3_tactic r =
Z3_mk_tactic(c, name); check_error(); init(r); }
3475 tactic(context & c, Z3_tactic s):object(c) { init(s); }
3476 tactic(tactic const & s):object(s) { init(s.m_tactic); }
3478 operator Z3_tactic() const { return m_tactic; }
3479 tactic & operator=(tactic const & s) {
3482 object::operator=(s);
3483 m_tactic = s.m_tactic;
3484 return *this;
3485 }
3487 apply_result apply(goal const & g) const {
3490 check_error();
3491 return apply_result(ctx(), r);
3492 }
3493 apply_result operator()(goal const & g) const {
3494 return apply(g);
3495 }
3496 std::string help()
const {
char const * r =
Z3_tactic_get_help(ctx(), m_tactic); check_error();
return r; }
3497 friend tactic
operator&(tactic
const & t1, tactic
const & t2);
3498 friend tactic
operator|(tactic
const & t1, tactic
const & t2);
3499 friend tactic
repeat(tactic
const & t,
unsigned max);
3500 friend tactic
with(tactic
const & t, params
const & p);
3501 friend tactic
try_for(tactic
const & t,
unsigned ms);
3502 friend tactic
par_or(
unsigned n, tactic
const* tactics);
3503 friend tactic
par_and_then(tactic
const& t1, tactic
const& t2);
3505 };
3506
3507 inline tactic
operator&(tactic
const & t1, tactic
const & t2) {
3510 t1.check_error();
3511 return tactic(t1.ctx(), r);
3512 }
3513
3514 inline tactic
operator|(tactic
const & t1, tactic
const & t2) {
3517 t1.check_error();
3518 return tactic(t1.ctx(), r);
3519 }
3520
3521 inline tactic
repeat(tactic
const & t,
unsigned max=UINT_MAX) {
3523 t.check_error();
3524 return tactic(t.ctx(), r);
3525 }
3526
3527 inline tactic
with(tactic
const & t, params
const & p) {
3529 t.check_error();
3530 return tactic(t.ctx(), r);
3531 }
3532 inline tactic
try_for(tactic
const & t,
unsigned ms) {
3534 t.check_error();
3535 return tactic(t.ctx(), r);
3536 }
3537 inline tactic
par_or(
unsigned n, tactic
const* tactics) {
3538 if (n == 0) {
3539 Z3_THROW(exception(
"a non-zero number of tactics need to be passed to par_or"));
3540 }
3541 array<Z3_tactic> buffer(n);
3542 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3543 return tactic(tactics[0u].ctx(),
Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3544 }
3545
3546 inline tactic
par_and_then(tactic
const & t1, tactic
const & t2) {
3549 t1.check_error();
3550 return tactic(t1.ctx(), r);
3551 }
3552
3553 class simplifier : public object {
3554 Z3_simplifier m_simplifier;
3555 void init(Z3_simplifier s) {
3556 m_simplifier = s;
3558 }
3559 public:
3560 simplifier(context & c,
char const * name):object(c) { Z3_simplifier r =
Z3_mk_simplifier(c, name); check_error(); init(r); }
3561 simplifier(context & c, Z3_simplifier s):object(c) { init(s); }
3562 simplifier(simplifier const & s):object(s) { init(s.m_simplifier); }
3564 operator Z3_simplifier() const { return m_simplifier; }
3565 simplifier & operator=(simplifier const & s) {
3568 object::operator=(s);
3569 m_simplifier = s.m_simplifier;
3570 return *this;
3571 }
3572 std::string help()
const {
char const * r =
Z3_simplifier_get_help(ctx(), m_simplifier); check_error();
return r; }
3573 friend simplifier
operator&(simplifier
const & t1, simplifier
const & t2);
3574 friend simplifier
with(simplifier
const & t, params
const & p);
3576 };
3577
3578 inline solver::solver(solver
const& s, simplifier
const& simp):object(s) { init(
Z3_solver_add_simplifier(s.ctx(), s, simp)); }
3579
3580
3581 inline simplifier
operator&(simplifier
const & t1, simplifier
const & t2) {
3584 t1.check_error();
3585 return simplifier(t1.ctx(), r);
3586 }
3587
3588 inline simplifier
with(simplifier
const & t, params
const & p) {
3590 t.check_error();
3591 return simplifier(t.ctx(), r);
3592 }
3593
3594 class probe : public object {
3595 Z3_probe m_probe;
3596 void init(Z3_probe s) {
3597 m_probe = s;
3599 }
3600 public:
3601 probe(context & c,
char const * name):object(c) { Z3_probe r =
Z3_mk_probe(c, name); check_error(); init(r); }
3602 probe(context & c,
double val):object(c) { Z3_probe r =
Z3_probe_const(c, val); check_error(); init(r); }
3603 probe(context & c, Z3_probe s):object(c) { init(s); }
3604 probe(probe const & s):object(s) { init(s.m_probe); }
3606 operator Z3_probe() const { return m_probe; }
3607 probe & operator=(probe const & s) {
3610 object::operator=(s);
3611 m_probe = s.m_probe;
3612 return *this;
3613 }
3614 double apply(goal
const & g)
const {
double r =
Z3_probe_apply(ctx(), m_probe, g); check_error();
return r; }
3615 double operator()(goal const & g) const { return apply(g); }
3616 friend probe
operator<=(probe
const & p1, probe
const & p2);
3617 friend probe
operator<=(probe
const & p1,
double p2);
3618 friend probe
operator<=(
double p1, probe
const & p2);
3619 friend probe
operator>=(probe
const & p1, probe
const & p2);
3620 friend probe
operator>=(probe
const & p1,
double p2);
3621 friend probe
operator>=(
double p1, probe
const & p2);
3622 friend probe
operator<(probe
const & p1, probe
const & p2);
3623 friend probe
operator<(probe
const & p1,
double p2);
3624 friend probe
operator<(
double p1, probe
const & p2);
3625 friend probe
operator>(probe
const & p1, probe
const & p2);
3626 friend probe
operator>(probe
const & p1,
double p2);
3627 friend probe
operator>(
double p1, probe
const & p2);
3628 friend probe
operator==(probe
const & p1, probe
const & p2);
3629 friend probe
operator==(probe
const & p1,
double p2);
3630 friend probe
operator==(
double p1, probe
const & p2);
3631 friend probe
operator&&(probe
const & p1, probe
const & p2);
3632 friend probe
operator||(probe
const & p1, probe
const & p2);
3633 friend probe
operator!(probe
const & p);
3634 };
3635
3636 inline probe
operator<=(probe
const & p1, probe
const & p2) {
3638 }
3639 inline probe
operator<=(probe
const & p1,
double p2) {
return p1 <= probe(p1.ctx(), p2); }
3640 inline probe
operator<=(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) <= p2; }
3641 inline probe
operator>=(probe
const & p1, probe
const & p2) {
3643 }
3644 inline probe
operator>=(probe
const & p1,
double p2) {
return p1 >= probe(p1.ctx(), p2); }
3645 inline probe
operator>=(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) >= p2; }
3646 inline probe
operator<(probe
const & p1, probe
const & p2) {
3648 }
3649 inline probe
operator<(probe
const & p1,
double p2) {
return p1 < probe(p1.ctx(), p2); }
3650 inline probe
operator<(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) < p2; }
3651 inline probe
operator>(probe
const & p1, probe
const & p2) {
3653 }
3654 inline probe
operator>(probe
const & p1,
double p2) {
return p1 > probe(p1.ctx(), p2); }
3655 inline probe
operator>(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) > p2; }
3656 inline probe
operator==(probe
const & p1, probe
const & p2) {
3658 }
3659 inline probe
operator==(probe
const & p1,
double p2) {
return p1 == probe(p1.ctx(), p2); }
3660 inline probe
operator==(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) == p2; }
3661 inline probe
operator&&(probe
const & p1, probe
const & p2) {
3663 }
3664 inline probe
operator||(probe
const & p1, probe
const & p2) {
3666 }
3667 inline probe
operator!(probe
const & p) {
3668 Z3_probe r =
Z3_probe_not(p.ctx(), p); p.check_error();
return probe(p.ctx(), r);
3669 }
3670
3671 class optimize : public object {
3672 Z3_optimize m_opt;
3673
3674 public:
3675 struct translate {};
3676 class handle final {
3677 unsigned m_h;
3678 public:
3679 handle(unsigned h): m_h(h) {}
3680 unsigned h() const { return m_h; }
3681 };
3683 optimize(context & c, optimize const& src, translate): object(c) {
3685 check_error();
3686 m_opt = o;
3688 }
3689 optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3691 }
3692 optimize(context& c, optimize& src):object(c) {
3697 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3698 }
3699 optimize& operator=(optimize const& o) {
3702 m_opt = o.m_opt;
3703 object::operator=(o);
3704 return *this;
3705 }
3707 operator Z3_optimize() const { return m_opt; }
3708 void add(expr const& e) {
3709 assert(e.is_bool());
3711 }
3712 void add(expr_vector const& es) {
3713 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3714 }
3715 void add(expr const& e, expr const& t) {
3716 assert(e.is_bool());
3718 }
3719 void add(expr const& e, char const* p) {
3720 assert(e.is_bool());
3721 add(e, ctx().bool_const(p));
3722 }
3723 handle add_soft(expr const& e, unsigned weight) {
3724 assert(e.is_bool());
3725 auto str = std::to_string(weight);
3727 }
3728 handle add_soft(expr const& e, char const* weight) {
3729 assert(e.is_bool());
3731 }
3732 handle add(expr const& e, unsigned weight) {
3733 return add_soft(e, weight);
3734 }
3735 void set_initial_value(expr const& var, expr const& value) {
3737 check_error();
3738 }
3739 void set_initial_value(expr const& var, int i) {
3740 set_initial_value(var, ctx().num_val(i, var.get_sort()));
3741 }
3742 void set_initial_value(expr const& var, bool b) {
3743 set_initial_value(var, ctx().bool_val(b));
3744 }
3745
3746 handle maximize(expr const& e) {
3748 }
3749 handle minimize(expr const& e) {
3751 }
3752 void push() {
3754 }
3755 void pop() {
3757 }
3760 unsigned n = asms.size();
3761 array<Z3_ast> _asms(n);
3762 for (unsigned i = 0; i < n; ++i) {
3764 _asms[i] = asms[i];
3765 }
3767 check_error();
3769 }
3773 expr lower(handle const& h) {
3775 check_error();
3776 return expr(ctx(), r);
3777 }
3778 expr_vector lower_as_vector(handle
const& h)
const {
3780 check_error();
3782 }
3783 expr upper(handle const& h) {
3785 check_error();
3786 return expr(ctx(), r);
3787 }
3788 expr_vector upper_as_vector(handle
const& h)
const {
3790 check_error();
3792 }
3796 friend std::ostream &
operator<<(std::ostream & out, optimize
const & s);
3797 void from_file(
char const* filename) {
Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3798 void from_string(
char const* constraints) {
Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3799 std::string help()
const {
char const * r =
Z3_optimize_get_help(ctx(), m_opt); check_error();
return r; }
3800 };
3802
3803 class fixedpoint : public object {
3804 Z3_fixedpoint m_fp;
3805 public:
3809 fixedpoint & operator=(fixedpoint const & o) {
3812 m_fp = o.m_fp;
3813 object::operator=(o);
3814 return *this;
3815 }
3816 operator Z3_fixedpoint() const { return m_fp; }
3819 check_error();
3821 }
3824 check_error();
3826 }
3827 void add_rule(expr& rule, symbol
const& name) {
Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3828 void add_fact(func_decl& f,
unsigned * args) {
Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3831 array<Z3_func_decl> rs(relations);
3833 check_error();
3835 }
3840 expr get_cover_delta(int level, func_decl& p) {
3842 check_error();
3843 return expr(ctx(), r);
3844 }
3845 void add_cover(
int level, func_decl& p, expr& property) {
Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3854 std::string to_string(expr_vector const& queries) {
3855 array<Z3_ast> qs(queries);
3857 }
3858 };
3860
3861 inline tactic
fail_if(probe
const & p) {
3863 p.check_error();
3864 return tactic(p.ctx(), r);
3865 }
3866 inline tactic
when(probe
const & p, tactic
const & t) {
3869 t.check_error();
3870 return tactic(t.ctx(), r);
3871 }
3872 inline tactic
cond(probe
const & p, tactic
const & t1, tactic
const & t2) {
3875 t1.check_error();
3876 return tactic(t1.ctx(), r);
3877 }
3878
3879 inline symbol context::str_symbol(
char const * s) {
Z3_symbol r =
Z3_mk_string_symbol(m_ctx, s); check_error();
return symbol(*
this, r); }
3880 inline symbol context::int_symbol(
int n) {
Z3_symbol r =
Z3_mk_int_symbol(m_ctx, n); check_error();
return symbol(*
this, r); }
3881
3882 inline sort context::bool_sort() {
Z3_sort s =
Z3_mk_bool_sort(m_ctx); check_error();
return sort(*
this, s); }
3883 inline sort context::int_sort() {
Z3_sort s =
Z3_mk_int_sort(m_ctx); check_error();
return sort(*
this, s); }
3884 inline sort context::real_sort() {
Z3_sort s =
Z3_mk_real_sort(m_ctx); check_error();
return sort(*
this, s); }
3886 inline sort context::finite_field_sort(
char const* prime) {
Z3_sort s =
Z3_mk_finite_field_sort(m_ctx, prime); check_error();
return sort(*
this, s); }
3887 inline sort context::bv_sort(
unsigned sz) {
Z3_sort s =
Z3_mk_bv_sort(m_ctx, sz); check_error();
return sort(*
this, s); }
3889 inline sort context::char_sort() {
Z3_sort s =
Z3_mk_char_sort(m_ctx); check_error();
return sort(*
this, s); }
3890 inline sort context::seq_sort(sort& s) {
Z3_sort r =
Z3_mk_seq_sort(m_ctx, s); check_error();
return sort(*
this, r); }
3891 inline sort context::re_sort(sort& s) {
Z3_sort r =
Z3_mk_re_sort(m_ctx, s); check_error();
return sort(*
this, r); }
3893 inline sort context::fpa_sort(
unsigned ebits,
unsigned sbits) {
Z3_sort s =
Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error();
return sort(*
this, s); }
3894
3895 template<>
3896 inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3897
3898 template<>
3899 inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3900
3901 template<>
3902 inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3903
3904 template<>
3905 inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3906
3908
3909 inline sort context::array_sort(sort d, sort r) {
Z3_sort s =
Z3_mk_array_sort(m_ctx, d, r); check_error();
return sort(*
this, s); }
3910 inline sort context::array_sort(sort_vector const& d, sort r) {
3911 array<Z3_sort> dom(d);
3913 }
3914 inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3915 array<Z3_symbol> _enum_names(n);
3916 for (
unsigned i = 0; i < n; ++i) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3917 array<Z3_func_decl> _cs(n);
3918 array<Z3_func_decl> _ts(n);
3921 check_error();
3922 for (unsigned i = 0; i < n; ++i) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3923 return s;
3924 }
3925 inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3926 array<Z3_symbol> _names(n);
3927 array<Z3_sort> _sorts(n);
3928 for (
unsigned i = 0; i < n; ++i) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3929 array<Z3_func_decl> _projs(n);
3932 sort _ignore_s =
to_sort(*
this,
Z3_mk_tuple_sort(*
this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3933 check_error();
3934 for (unsigned i = 0; i < n; ++i) { projs.push_back(func_decl(*this, _projs[i])); }
3935 return func_decl(*this, tuple);
3936 }
3937
3938 class constructor_list {
3939 context& ctx;
3940 Z3_constructor_list clist;
3941 public:
3942 constructor_list(constructors const& cs);
3944 operator Z3_constructor_list() const { return clist; }
3945 };
3946
3947 class constructors {
3948 friend class constructor_list;
3949 context& ctx;
3950 std::vector<Z3_constructor> cons;
3951 std::vector<unsigned> num_fields;
3952 public:
3953 constructors(context& ctx): ctx(ctx) {}
3954
3955 ~constructors() {
3956 for (auto con : cons)
3958 }
3959
3960 void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
3961 array<unsigned> sort_refs(n);
3962 array<Z3_sort> sorts(n);
3963 array<Z3_symbol> _names(n);
3964 for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3965 cons.push_back(
Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3966 num_fields.push_back(n);
3967 }
3968
3969 Z3_constructor operator[](unsigned i) const { return cons[i]; }
3970
3971 unsigned size() const { return (unsigned)cons.size(); }
3972
3973 void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
3976 array<Z3_func_decl> accessors(num_fields[i]);
3977 accs.resize(0);
3979 cons[i],
3980 num_fields[i],
3981 &_constructor,
3982 &_test,
3983 accessors.ptr());
3984 constructor = func_decl(ctx, _constructor);
3985
3986 test = func_decl(ctx, _test);
3987 for (unsigned j = 0; j < num_fields[i]; ++j)
3988 accs.push_back(func_decl(ctx, accessors[j]));
3989 }
3990 };
3991
3992 inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) {
3993 array<Z3_constructor> cons(cs.size());
3994 for (unsigned i = 0; i < cs.size(); ++i)
3995 cons[i] = cs[i];
3997 }
3998
3999 inline sort context::datatype(symbol const& name, constructors const& cs) {
4000 array<Z3_constructor> _cs(cs.size());
4001 for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
4003 check_error();
4004 return sort(*this, s);
4005 }
4006
4007 inline sort context::datatype(symbol const &name, sort_vector const& params, constructors const &cs) {
4008 array<Z3_sort> _params(params);
4009 array<Z3_constructor> _cs(cs.size());
4010 for (unsigned i = 0; i < cs.size(); ++i)
4011 _cs[i] = cs[i];
4013 check_error();
4014 return sort(*this, s);
4015 }
4016
4018 unsigned n, symbol const* names,
4019 constructor_list *const* cons) {
4021 array<Z3_symbol> _names(n);
4022 array<Z3_sort> _sorts(n);
4023 array<Z3_constructor_list> _cons(n);
4024 for (unsigned i = 0; i < n; ++i)
4025 _names[i] = names[i], _cons[i] = *cons[i];
4027 for (unsigned i = 0; i < n; ++i)
4028 result.push_back(sort(*this, _sorts[i]));
4029 return result;
4030 }
4031
4032
4033 inline sort context::datatype_sort(symbol const& name) {
4035 check_error();
4036 return sort(*this, s);
4037 }
4038
4039 inline sort context::datatype_sort(symbol const& name, sort_vector const& params) {
4040 array<Z3_sort> _params(params);
4042 check_error();
4043 return sort(*this, s);
4044 }
4045
4046
4047 inline sort context::uninterpreted_sort(char const* name) {
4050 }
4051 inline sort context::uninterpreted_sort(symbol const& name) {
4053 }
4054
4055 inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
4056 array<Z3_sort> args(arity);
4057 for (unsigned i = 0; i < arity; ++i) {
4059 args[i] = domain[i];
4060 }
4062 check_error();
4063 return func_decl(*this, f);
4064 }
4065
4066 inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
4068 }
4069
4070 inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
4071 array<Z3_sort> args(domain.size());
4072 for (unsigned i = 0; i < domain.size(); ++i) {
4074 args[i] = domain[i];
4075 }
4077 check_error();
4078 return func_decl(*this, f);
4079 }
4080
4081 inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
4083 }
4084
4085
4086 inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
4090 check_error();
4091 return func_decl(*this, f);
4092 }
4093
4094 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
4098 check_error();
4099 return func_decl(*this, f);
4100 }
4101
4102 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
4104 Z3_sort args[3] = { d1, d2, d3 };
4106 check_error();
4107 return func_decl(*this, f);
4108 }
4109
4110 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
4112 Z3_sort args[4] = { d1, d2, d3, d4 };
4114 check_error();
4115 return func_decl(*this, f);
4116 }
4117
4118 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & d5, sort const & range) {
4120 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
4122 check_error();
4123 return func_decl(*this, f);
4124 }
4125
4126 inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
4127 array<Z3_sort> args(arity);
4128 for (unsigned i = 0; i < arity; ++i) {
4130 args[i] = domain[i];
4131 }
4133 check_error();
4134 return func_decl(*this, f);
4135
4136 }
4137
4138 inline func_decl context::recfun(symbol const & name, sort_vector const& domain, sort const & range) {
4140 array<Z3_sort> domain1(domain);
4142 check_error();
4143 return func_decl(*this, f);
4144 }
4145
4146 inline func_decl context::recfun(char const * name, sort_vector const& domain, sort const & range) {
4147 return recfun(str_symbol(name), domain, range);
4148
4149 }
4150
4151 inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
4152 return recfun(str_symbol(name), arity, domain, range);
4153 }
4154
4155 inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
4156 return recfun(str_symbol(name), 1, &d1, range);
4157 }
4158
4159 inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
4160 sort dom[2] = { d1, d2 };
4161 return recfun(str_symbol(name), 2, dom, range);
4162 }
4163
4164 inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
4166 array<Z3_ast> vars(args);
4168 }
4169
4170 inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
4172 array<Z3_sort> domain1(domain);
4174 check_error();
4175 return func_decl(*this, f);
4176 }
4177
4178 inline expr context::constant(symbol const & name, sort const & s) {
4180 check_error();
4181 return expr(*this, r);
4182 }
4183 inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
4184 inline expr context::variable(unsigned idx, sort const& s) {
4186 check_error();
4187 return expr(*this, r);
4188 }
4189 inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
4190 inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
4191 inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
4192 inline expr context::complex_const(char const * name) { return constant(name, complex_sort()); }
4193 inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
4194 inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
4195 inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
4196
4197 template<size_t precision>
4198 inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
4199
4200 inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
4201
4202 inline expr context::fpa_rounding_mode() {
4203 switch (m_rounding_mode) {
4209 }
4210 assert(false);
4212 }
4213
4214 inline expr context::bool_val(
bool b) {
return b ? expr(*
this,
Z3_mk_true(m_ctx)) : expr(*this,
Z3_mk_false(m_ctx)); }
4215
4216 inline expr context::int_val(
int n) {
Z3_ast r =
Z3_mk_int(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
4217 inline expr context::int_val(
unsigned n) {
Z3_ast r =
Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
4218 inline expr context::int_val(int64_t n) {
Z3_ast r =
Z3_mk_int64(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
4219 inline expr context::int_val(uint64_t n) {
Z3_ast r =
Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
4220 inline expr context::int_val(
char const * n) {
Z3_ast r =
Z3_mk_numeral(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
4221
4222 inline expr context::real_val(int64_t n, int64_t d) {
Z3_ast r =
Z3_mk_real_int64(m_ctx, n, d); check_error();
return expr(*
this, r); }
4223 inline expr context::real_val(
int n) {
Z3_ast r =
Z3_mk_int(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
4224 inline expr context::real_val(
unsigned n) {
Z3_ast r =
Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
4225 inline expr context::real_val(int64_t n) {
Z3_ast r =
Z3_mk_int64(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
4226 inline expr context::real_val(uint64_t n) {
Z3_ast r =
Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
4227 inline expr context::real_val(
char const * n) {
Z3_ast r =
Z3_mk_numeral(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
4228 inline expr context::complex_val(int re, int im) {
4229 expr r = real_val(re);
4230 expr i = real_val(im);
4232 }
4233 inline expr context::complex_val(char const* re, char const* im) {
4234 expr r = real_val(re);
4235 expr i = real_val(im);
4237 }
4238
4239 inline expr context::bv_val(
int n,
unsigned sz) { sort s = bv_sort(sz);
Z3_ast r =
Z3_mk_int(m_ctx, n, s); check_error();
return expr(*
this, r); }
4240 inline expr context::bv_val(
unsigned n,
unsigned sz) { sort s = bv_sort(sz);
Z3_ast r =
Z3_mk_unsigned_int(m_ctx, n, s); check_error();
return expr(*
this, r); }
4241 inline expr context::bv_val(int64_t n,
unsigned sz) { sort s = bv_sort(sz);
Z3_ast r =
Z3_mk_int64(m_ctx, n, s); check_error();
return expr(*
this, r); }
4242 inline expr context::bv_val(uint64_t n,
unsigned sz) { sort s = bv_sort(sz);
Z3_ast r =
Z3_mk_unsigned_int64(m_ctx, n, s); check_error();
return expr(*
this, r); }
4243 inline expr context::bv_val(
char const * n,
unsigned sz) { sort s = bv_sort(sz);
Z3_ast r =
Z3_mk_numeral(m_ctx, n, s); check_error();
return expr(*
this, r); }
4244 inline expr context::bv_val(unsigned n, bool const* bits) {
4245 array<bool> _bits(n);
4246 for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
4248 }
4249
4250 inline expr context::fpa_val(
double n) { sort s = fpa_sort<64>();
Z3_ast r =
Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error();
return expr(*
this, r); }
4251 inline expr context::fpa_val(
float n) { sort s = fpa_sort<32>();
Z3_ast r =
Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error();
return expr(*
this, r); }
4252 inline expr context::fpa_nan(sort
const & s) {
Z3_ast r =
Z3_mk_fpa_nan(m_ctx, s); check_error();
return expr(*
this, r); }
4253 inline expr context::fpa_inf(sort
const & s,
bool sgn) {
Z3_ast r =
Z3_mk_fpa_inf(m_ctx, s, sgn); check_error();
return expr(*
this, r); }
4254
4255 inline expr context::string_val(
char const* s,
unsigned n) {
Z3_ast r =
Z3_mk_lstring(m_ctx, n, s); check_error();
return expr(*
this, r); }
4256 inline expr context::string_val(
char const* s) {
Z3_ast r =
Z3_mk_string(m_ctx, s); check_error();
return expr(*
this, r); }
4257 inline expr context::string_val(std::string
const& s) {
Z3_ast r =
Z3_mk_string(m_ctx, s.c_str()); check_error();
return expr(*
this, r); }
4258 inline expr context::string_val(std::u32string
const& s) {
Z3_ast r =
Z3_mk_u32string(m_ctx, (
unsigned)s.size(), (
unsigned const*)s.c_str()); check_error();
return expr(*
this, r); }
4259
4260 inline expr context::num_val(
int n, sort
const & s) {
Z3_ast r =
Z3_mk_int(m_ctx, n, s); check_error();
return expr(*
this, r); }
4261
4262 inline expr func_decl::operator()(unsigned n, expr const * args) const {
4263 array<Z3_ast> _args(n);
4264 for (unsigned i = 0; i < n; ++i) {
4266 _args[i] = args[i];
4267 }
4269 check_error();
4270 return expr(ctx(), r);
4271
4272 }
4273 inline expr func_decl::operator()(expr_vector const& args) const {
4274 array<Z3_ast> _args(args.size());
4275 for (unsigned i = 0; i < args.size(); ++i) {
4277 _args[i] = args[i];
4278 }
4280 check_error();
4281 return expr(ctx(), r);
4282 }
4283 inline expr func_decl::operator()() const {
4285 ctx().check_error();
4286 return expr(ctx(), r);
4287 }
4288 inline expr func_decl::operator()(expr const & a) const {
4292 ctx().check_error();
4293 return expr(ctx(), r);
4294 }
4295 inline expr func_decl::operator()(int a) const {
4296 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
4298 ctx().check_error();
4299 return expr(ctx(), r);
4300 }
4301 inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
4303 Z3_ast args[2] = { a1, a2 };
4305 ctx().check_error();
4306 return expr(ctx(), r);
4307 }
4308 inline expr func_decl::operator()(expr const & a1, int a2) const {
4310 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
4312 ctx().check_error();
4313 return expr(ctx(), r);
4314 }
4315 inline expr func_decl::operator()(int a1, expr const & a2) const {
4317 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
4319 ctx().check_error();
4320 return expr(ctx(), r);
4321 }
4322 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
4324 Z3_ast args[3] = { a1, a2, a3 };
4326 ctx().check_error();
4327 return expr(ctx(), r);
4328 }
4329 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
4331 Z3_ast args[4] = { a1, a2, a3, a4 };
4333 ctx().check_error();
4334 return expr(ctx(), r);
4335 }
4336 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
4338 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
4340 ctx().check_error();
4341 return expr(ctx(), r);
4342 }
4343
4345
4346 inline func_decl
function(symbol
const & name,
unsigned arity, sort
const * domain, sort
const &
range) {
4348 }
4349 inline func_decl
function(
char const * name,
unsigned arity, sort
const * domain, sort
const &
range) {
4351 }
4352 inline func_decl
function(
char const * name, sort
const & domain, sort
const &
range) {
4354 }
4355 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const &
range) {
4357 }
4358 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const & d3, sort
const &
range) {
4360 }
4361 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const & d3, sort
const & d4, sort
const &
range) {
4363 }
4364 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const & d3, sort
const & d4, sort
const & d5, sort
const &
range) {
4366 }
4367 inline func_decl
function(
char const* name,
sort_vector const& domain, sort
const&
range) {
4369 }
4370 inline func_decl
function(std::string
const& name,
sort_vector const& domain, sort
const&
range) {
4372 }
4373
4374 inline func_decl
recfun(symbol
const & name,
unsigned arity, sort
const * domain, sort
const & range) {
4376 }
4377 inline func_decl
recfun(
char const * name,
unsigned arity, sort
const * domain, sort
const & range) {
4379 }
4380 inline func_decl
recfun(
char const * name, sort
const& d1, sort
const & range) {
4382 }
4383 inline func_decl
recfun(
char const * name, sort
const& d1, sort
const& d2, sort
const & range) {
4385 }
4386
4387 inline expr
select(expr
const & a, expr
const & i) {
4390 a.check_error();
4391 return expr(a.ctx(), r);
4392 }
4393 inline expr
select(expr
const & a,
int i) {
4394 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
4395 }
4396 inline expr
select(expr
const & a, expr_vector
const & i) {
4398 array<Z3_ast> idxs(i);
4400 a.check_error();
4401 return expr(a.ctx(), r);
4402 }
4403
4404 inline expr
store(expr
const & a, expr
const & i, expr
const & v) {
4407 a.check_error();
4408 return expr(a.ctx(), r);
4409 }
4410
4411 inline expr
store(expr
const & a,
int i, expr
const & v) {
return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
4412 inline expr
store(expr
const & a, expr i,
int v) {
return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
4413 inline expr
store(expr
const & a,
int i,
int v) {
4414 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
4415 }
4416 inline expr
store(expr
const & a, expr_vector
const & i, expr
const & v) {
4418 array<Z3_ast> idxs(i);
4420 a.check_error();
4421 return expr(a.ctx(), r);
4422 }
4423
4424 inline expr
as_array(func_decl & f) {
4426 f.check_error();
4427 return expr(f.ctx(), r);
4428 }
4429
4432 a.check_error();
4433 return expr(a.ctx(), r);
4434 }
4435
4436 inline expr
array_ext(expr
const & a, expr
const & b) {
4439 a.check_error();
4440 return expr(a.ctx(), r);
4441 }
4442
4443#define MK_EXPR1(_fn, _arg) \
4444 Z3_ast r = _fn(_arg.ctx(), _arg); \
4445 _arg.check_error(); \
4446 return expr(_arg.ctx(), r);
4447
4448#define MK_EXPR2(_fn, _arg1, _arg2) \
4449 check_context(_arg1, _arg2); \
4450 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
4451 _arg1.check_error(); \
4452 return expr(_arg1.ctx(), r);
4453
4454 inline expr
const_array(sort
const & d, expr
const & v) {
4456 }
4457
4460 }
4461
4462 inline expr
full_set(sort
const& s) {
4464 }
4465
4466 inline expr
set_add(expr
const& s, expr
const& e) {
4468 }
4469
4470 inline expr
set_del(expr
const& s, expr
const& e) {
4472 }
4473
4474 inline expr
set_union(expr
const& a, expr
const& b) {
4478 a.check_error();
4479 return expr(a.ctx(), r);
4480 }
4481
4486 a.check_error();
4487 return expr(a.ctx(), r);
4488 }
4489
4492 }
4493
4496 }
4497
4498 inline expr
set_member(expr
const& s, expr
const& e) {
4500 }
4501
4502 inline expr
set_subset(expr
const& a, expr
const& b) {
4504 }
4505
4506
4507
4510 s.check_error();
4511 return expr(s.ctx(), r);
4512 }
4513
4516 }
4517
4520 }
4521
4524 }
4525
4528 }
4529
4532 }
4533
4536 }
4537
4540 }
4541
4544 }
4545
4548 }
4549
4552 }
4553
4554
4555
4556
4557
4558 inline expr
empty(sort
const& s) {
4560 s.check_error();
4561 return expr(s.ctx(), r);
4562 }
4563 inline expr
suffixof(expr
const& a, expr
const& b) {
4566 a.check_error();
4567 return expr(a.ctx(), r);
4568 }
4569 inline expr
prefixof(expr
const& a, expr
const& b) {
4572 a.check_error();
4573 return expr(a.ctx(), r);
4574 }
4575 inline expr
indexof(expr
const& s, expr
const& substr, expr
const& offset) {
4578 s.check_error();
4579 return expr(s.ctx(), r);
4580 }
4581 inline expr
last_indexof(expr
const& s, expr
const& substr) {
4584 s.check_error();
4585 return expr(s.ctx(), r);
4586 }
4587 inline expr
to_re(expr
const& s) {
4589 }
4590 inline expr
in_re(expr
const& s, expr
const& re) {
4592 }
4593 inline expr
plus(expr
const& re) {
4595 }
4596 inline expr
option(expr
const& re) {
4598 }
4599 inline expr
star(expr
const& re) {
4601 }
4602 inline expr
re_empty(sort
const& s) {
4604 s.check_error();
4605 return expr(s.ctx(), r);
4606 }
4607 inline expr
re_full(sort
const& s) {
4609 s.check_error();
4610 return expr(s.ctx(), r);
4611 }
4613 assert(args.size() > 0);
4614 context& ctx = args[0u].ctx();
4615 array<Z3_ast> _args(args);
4617 ctx.check_error();
4618 return expr(ctx, r);
4619 }
4620 inline expr
re_diff(expr
const& a, expr
const& b) {
4622 context& ctx = a.ctx();
4624 ctx.check_error();
4625 return expr(ctx, r);
4626 }
4629 }
4630 inline expr
range(expr
const& lo, expr
const& hi) {
4633 lo.check_error();
4634 return expr(lo.ctx(), r);
4635 }
4636
4637
4638
4639
4640
4641 inline expr_vector context::parse_string(
char const* s) {
4643 check_error();
4645
4646 }
4647 inline expr_vector context::parse_file(
char const* s) {
4649 check_error();
4651 }
4652
4653 inline expr_vector context::parse_string(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls) {
4654 array<Z3_symbol> sort_names(sorts.size());
4655 array<Z3_symbol> decl_names(decls.size());
4656 array<Z3_sort> sorts1(sorts);
4657 array<Z3_func_decl> decls1(decls);
4658 for (unsigned i = 0; i < sorts.size(); ++i) {
4659 sort_names[i] = sorts[i].name();
4660 }
4661 for (unsigned i = 0; i < decls.size(); ++i) {
4662 decl_names[i] = decls[i].name();
4663 }
4664
4666 check_error();
4668 }
4669
4670 inline expr_vector context::parse_file(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls) {
4671 array<Z3_symbol> sort_names(sorts.size());
4672 array<Z3_symbol> decl_names(decls.size());
4673 array<Z3_sort> sorts1(sorts);
4674 array<Z3_func_decl> decls1(decls);
4675 for (unsigned i = 0; i < sorts.size(); ++i) {
4676 sort_names[i] = sorts[i].name();
4677 }
4678 for (unsigned i = 0; i < decls.size(); ++i) {
4679 decl_names[i] = decls[i].name();
4680 }
4682 check_error();
4684 }
4685
4687 assert(is_datatype());
4690 for (unsigned i = 0; i < n; ++i)
4692 return cs;
4693 }
4694
4696 assert(is_datatype());
4699 for (unsigned i = 0; i < n; ++i)
4701 return rs;
4702 }
4703
4706 assert(s.is_datatype());
4708 unsigned idx = 0;
4709 for (; idx < n; ++idx) {
4711 if (id() == f.id())
4712 break;
4713 }
4714 assert(idx < n);
4715 n = arity();
4717 for (unsigned i = 0; i < n; ++i)
4719 return as;
4720 }
4721
4722
4723 inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
4724 assert(src.size() == dst.size());
4725 array<Z3_ast> _src(src.size());
4726 array<Z3_ast> _dst(dst.size());
4727 for (unsigned i = 0; i < src.size(); ++i) {
4728 _src[i] = src[i];
4729 _dst[i] = dst[i];
4730 }
4732 check_error();
4733 return expr(ctx(), r);
4734 }
4735
4736 inline expr expr::substitute(expr_vector const& dst) {
4737 array<Z3_ast> _dst(dst.size());
4738 for (unsigned i = 0; i < dst.size(); ++i) {
4739 _dst[i] = dst[i];
4740 }
4742 check_error();
4743 return expr(ctx(), r);
4744 }
4745
4746 inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
4747 array<Z3_ast> _dst(dst.size());
4748 array<Z3_func_decl> _funs(funs.size());
4749 if (dst.size() != funs.size()) {
4750 Z3_THROW(exception(
"length of argument lists don't align"));
4751 return expr(ctx(), nullptr);
4752 }
4753 for (unsigned i = 0; i < dst.size(); ++i) {
4754 _dst[i] = dst[i];
4755 _funs[i] = funs[i];
4756 }
4758 check_error();
4759 return expr(ctx(), r);
4760 }
4761
4762 inline expr expr::update(expr_vector const& args) const {
4763 array<Z3_ast> _args(args.size());
4764 for (unsigned i = 0; i < args.size(); ++i) {
4765 _args[i] = args[i];
4766 }
4768 check_error();
4769 return expr(ctx(), r);
4770 }
4771
4772 inline expr expr::update_field(func_decl const& field_access, expr const& new_value) const {
4773 assert(is_datatype());
4775 check_error();
4776 return expr(ctx(), r);
4777 }
4778
4779 typedef std::function<void(expr
const& proof, std::vector<unsigned>
const& deps, expr_vector
const& clause)>
on_clause_eh_t;
4780
4781 class on_clause {
4782 context& c;
4784
4785 static void _on_clause_eh(
void* _ctx, Z3_ast _proof,
unsigned n,
unsigned const* dep, Z3_ast_vector _literals) {
4786 on_clause* ctx = static_cast<on_clause*>(_ctx);
4788 expr proof(ctx->c, _proof);
4789 std::vector<unsigned> deps;
4790 for (unsigned i = 0; i < n; ++i)
4791 deps.push_back(dep[i]);
4792 ctx->m_on_clause(proof, deps, lits);
4793 }
4794 public:
4795 on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {
4798 c.check_error();
4799 }
4800 };
4801
4802 class user_propagator_base {
4803
4804 typedef std::function<void(expr const&, expr const&)> fixed_eh_t;
4805 typedef std::function<void(void)> final_eh_t;
4806 typedef std::function<void(expr const&, expr const&)> eq_eh_t;
4807 typedef std::function<void(expr const&)> created_eh_t;
4808 typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
4809 typedef std::function<bool(expr const&, expr const&)> on_binding_eh_t;
4810
4811 final_eh_t m_final_eh;
4812 eq_eh_t m_eq_eh;
4813 fixed_eh_t m_fixed_eh;
4814 created_eh_t m_created_eh;
4815 decide_eh_t m_decide_eh;
4816 on_binding_eh_t m_on_binding_eh;
4817 solver* s;
4818 context* c;
4819 std::vector<z3::context*> subcontexts;
4820
4821 unsigned m_callbackNesting = 0;
4823
4824 struct scoped_cb {
4825 user_propagator_base& p;
4826 scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
4827 p.cb = cb;
4828 p.m_callbackNesting++;
4829 }
4830 ~scoped_cb() {
4831 if (--p.m_callbackNesting == 0)
4832 p.cb = nullptr;
4833 }
4834 };
4835
4836 static void push_eh(void* _p, Z3_solver_callback cb) {
4837 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4838 scoped_cb _cb(p, cb);
4839 static_cast<user_propagator_base*>(p)->push();
4840 }
4841
4842 static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
4843 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4844 scoped_cb _cb(p, cb);
4845 static_cast<user_propagator_base*>(_p)->pop(num_scopes);
4846 }
4847
4848 static void* fresh_eh(void* _p, Z3_context ctx) {
4849 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4850 context* c = new context(ctx);
4851 p->subcontexts.push_back(c);
4852 return p->fresh(*c);
4853 }
4854
4855 static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
4856 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4857 scoped_cb _cb(p, cb);
4858 expr value(p->ctx(), _value);
4859 expr var(p->ctx(), _var);
4860 p->m_fixed_eh(var, value);
4861 }
4862
4863 static void eq_eh(void* _p, Z3_solver_callback cb, Z3_ast _x, Z3_ast _y) {
4864 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4865 scoped_cb _cb(p, cb);
4866 expr x(p->ctx(), _x), y(p->ctx(), _y);
4867 p->m_eq_eh(x, y);
4868 }
4869
4870 static void final_eh(void* p, Z3_solver_callback cb) {
4871 scoped_cb _cb(p, cb);
4872 static_cast<user_propagator_base*>(p)->m_final_eh();
4873 }
4874
4875 static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e) {
4876 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4877 scoped_cb _cb(p, cb);
4878 expr e(p->ctx(), _e);
4879 p->m_created_eh(e);
4880 }
4881
4882 static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit, bool is_pos) {
4883 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4884 scoped_cb _cb(p, cb);
4885 expr val(p->ctx(), _val);
4886 p->m_decide_eh(val, bit, is_pos);
4887 }
4888
4889 static bool on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
4890 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4891 scoped_cb _cb(p, cb);
4892 expr q(p->ctx(), _q), inst(p->ctx(), _inst);
4893 return p->m_on_binding_eh(q, inst);
4894 }
4895
4896 public:
4897 user_propagator_base(context& c) : s(nullptr), c(&c) {}
4898
4899 user_propagator_base(solver* s): s(s), c(nullptr) {
4901 }
4902
4903 virtual void push() = 0;
4904 virtual void pop(unsigned num_scopes) = 0;
4905
4906 virtual ~user_propagator_base() {
4907 for (auto& subcontext : subcontexts) {
4908 subcontext->detach();
4909 delete subcontext;
4910 }
4911 }
4912
4913 context& ctx() {
4914 return c ? *c : s->ctx();
4915 }
4916
4925 virtual user_propagator_base* fresh(context& ctx) = 0;
4926
4933 void register_fixed(fixed_eh_t& f) {
4934 m_fixed_eh = f;
4935 if (s) {
4937 }
4938 }
4939
4940 void register_fixed() {
4941 m_fixed_eh = [this](expr const &id, expr const &e) {
4942 fixed(id, e);
4943 };
4944 if (s) {
4946 }
4947 }
4948
4949 void register_eq(eq_eh_t& f) {
4950 m_eq_eh = f;
4951 if (s) {
4953 }
4954 }
4955
4956 void register_eq() {
4957 m_eq_eh = [this](expr const& x, expr const& y) {
4959 };
4960 if (s) {
4962 }
4963 }
4964
4973 void register_final(final_eh_t& f) {
4974 m_final_eh = f;
4975 if (s) {
4977 }
4978 }
4979
4980 void register_final() {
4981 m_final_eh = [this]() {
4982 final();
4983 };
4984 if (s) {
4986 }
4987 }
4988
4989 void register_created(created_eh_t& c) {
4990 m_created_eh = c;
4991 if (s) {
4993 }
4994 }
4995
4996 void register_created() {
4997 m_created_eh = [this](expr const& e) {
4998 created(e);
4999 };
5000 if (s) {
5002 }
5003 }
5004
5005 void register_decide(decide_eh_t& c) {
5006 m_decide_eh = c;
5007 if (s) {
5009 }
5010 }
5011
5012 void register_decide() {
5013 m_decide_eh = [this](expr val, unsigned bit, bool is_pos) {
5014 decide(val, bit, is_pos);
5015 };
5016 if (s) {
5018 }
5019 }
5020
5021 void register_on_binding() {
5022 m_on_binding_eh = [this](expr const& q, expr const& inst) {
5023 return on_binding(q, inst);
5024 };
5025 if (s)
5027 }
5028
5029 virtual void fixed(expr const& , expr const& ) { }
5030
5031 virtual void eq(expr
const& , expr
const& ) { }
5032
5033 virtual void final() { }
5034
5035 virtual void created(expr const& ) {}
5036
5037 virtual void decide(expr const& , unsigned , bool ) {}
5038
5039 virtual bool on_binding(expr const& , expr const& ) { return true; }
5040
5041 bool next_split(expr
const& e,
unsigned idx,
Z3_lbool phase) {
5042 assert(cb);
5044 }
5045
5060 void add(expr const& e) {
5061 if (cb)
5063 else if (s)
5065 else
5066 assert(false);
5067 }
5068
5069 void conflict(expr_vector const& fixed) {
5070 assert(cb);
5071 expr conseq = ctx().bool_val(false);
5072 array<Z3_ast> _fixed(fixed);
5074 }
5075
5076 void conflict(expr_vector const& fixed, expr_vector const& lhs, expr_vector const& rhs) {
5077 assert(cb);
5078 assert(lhs.size() == rhs.size());
5079 expr conseq = ctx().bool_val(false);
5080 array<Z3_ast> _fixed(fixed);
5081 array<Z3_ast> _lhs(lhs);
5082 array<Z3_ast> _rhs(rhs);
5084 }
5085
5086 bool propagate(expr_vector const& fixed, expr const& conseq) {
5087 assert(cb);
5088 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
5089 array<Z3_ast> _fixed(fixed);
5091 }
5092
5093 bool propagate(expr_vector const& fixed,
5094 expr_vector const& lhs, expr_vector const& rhs,
5095 expr const& conseq) {
5096 assert(cb);
5097 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
5098 assert(lhs.size() == rhs.size());
5099 array<Z3_ast> _fixed(fixed);
5100 array<Z3_ast> _lhs(lhs);
5101 array<Z3_ast> _rhs(rhs);
5102
5104 }
5105 };
5106
5116 class rcf_num {
5118 Z3_rcf_num m_num;
5119
5121 if (m_ctx != other.m_ctx) {
5122 Z3_THROW(exception(
"rcf_num objects from different contexts"));
5123 }
5124 }
5125
5126 public:
5127 rcf_num(context& c, Z3_rcf_num n): m_ctx(c), m_num(n) {}
5128
5129 rcf_num(context& c, int val): m_ctx(c) {
5131 }
5132
5133 rcf_num(context& c, char const* val): m_ctx(c) {
5135 }
5136
5137 rcf_num(rcf_num const& other): m_ctx(other.m_ctx) {
5138
5141 }
5142
5143 rcf_num& operator=(rcf_num const& other) {
5144 if (this != &other) {
5146 m_ctx = other.m_ctx;
5149 }
5150 return *this;
5151 }
5152
5153 ~rcf_num() {
5155 }
5156
5157 operator Z3_rcf_num() const { return m_num; }
5159
5163 std::string to_string(bool compact = false) const {
5165 }
5166
5170 std::string to_decimal(unsigned precision = 10) const {
5172 }
5173
5174
5175 rcf_num
operator+(rcf_num
const& other)
const {
5177 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5179 }
5180
5181 rcf_num
operator-(rcf_num
const& other)
const {
5183 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5185 }
5186
5187 rcf_num
operator*(rcf_num
const& other)
const {
5189 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5191 }
5192
5193 rcf_num
operator/(rcf_num
const& other)
const {
5195 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5197 }
5198
5200 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5202 }
5203
5207 rcf_num power(unsigned k) const {
5208 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5210 }
5211
5215 rcf_num inv() const {
5216 return rcf_num(*const_cast<context*>(reinterpret_cast<context const*>(&m_ctx)),
5218 }
5219
5220
5221 bool operator<(rcf_num
const& other)
const {
5223 return Z3_rcf_lt(m_ctx, m_num, other.m_num);
5224 }
5225
5226 bool operator>(rcf_num
const& other)
const {
5228 return Z3_rcf_gt(m_ctx, m_num, other.m_num);
5229 }
5230
5231 bool operator<=(rcf_num
const& other)
const {
5233 return Z3_rcf_le(m_ctx, m_num, other.m_num);
5234 }
5235
5236 bool operator>=(rcf_num
const& other)
const {
5238 return Z3_rcf_ge(m_ctx, m_num, other.m_num);
5239 }
5240
5241 bool operator==(rcf_num
const& other)
const {
5243 return Z3_rcf_eq(m_ctx, m_num, other.m_num);
5244 }
5245
5246 bool operator!=(rcf_num
const& other)
const {
5248 return Z3_rcf_neq(m_ctx, m_num, other.m_num);
5249 }
5250
5251
5252 bool is_rational() const {
5254 }
5255
5256 bool is_algebraic() const {
5258 }
5259
5260 bool is_infinitesimal() const {
5262 }
5263
5264 bool is_transcendental() const {
5266 }
5267
5268 friend std::ostream&
operator<<(std::ostream& out, rcf_num
const& n) {
5269 return out << n.to_string();
5270 }
5271 };
5272
5276 inline rcf_num
rcf_pi(context& c) {
5278 }
5279
5283 inline rcf_num
rcf_e(context& c) {
5285 }
5286
5292 }
5293
5300 inline std::vector<rcf_num>
rcf_roots(context& c, std::vector<rcf_num>
const& coeffs) {
5301 if (coeffs.empty()) {
5302 Z3_THROW(exception(
"polynomial coefficients cannot be empty"));
5303 }
5304
5305 unsigned n = static_cast<unsigned>(coeffs.size());
5306 std::vector<Z3_rcf_num> a(n);
5307 std::vector<Z3_rcf_num> roots(n);
5308
5309 for (unsigned i = 0; i < n; ++i) {
5310 a[i] = coeffs[i];
5311 }
5312
5314
5315 std::vector<rcf_num> result;
5316 result.reserve(num_roots);
5317 for (unsigned i = 0; i < num_roots; ++i) {
5318 result.push_back(rcf_num(c, roots[i]));
5319 }
5320
5321 return result;
5322 }
5323
5324}
5325
5328#undef Z3_THROW
symbol str_symbol(char const *s)
Create a Z3 symbol based on the given string.
expr num_val(int n, sort const &s)
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl function(symbol const &name, unsigned arity, sort const *domain, sort const &range)
Z3_error_code check_error() const
Z3_ast Z3_API Z3_mk_exists_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Similar to Z3_mk_forall_const.
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh)
register a callback when the solver instantiates a quantifier. If the callback returns false,...
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o)
Return the set of asserted formulas on the optimization context.
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL,...
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_probe Z3_API Z3_probe_lt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned...
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
Z3_ast Z3_API Z3_mk_bvxnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise xnor.
Z3_parameter_kind Z3_API Z3_get_decl_parameter_kind(Z3_context c, Z3_func_decl d, unsigned idx)
Return the parameter type associated with a declaration.
bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s)
Check if s is a sequence sort.
Z3_ast Z3_API Z3_mk_bvnor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nor.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f)
Return the 'else' value of the given function interpretation.
Z3_ast Z3_API Z3_mk_bvsge(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than or equal to.
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a / b.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[])
Store in roots the roots of the polynomial a[n-1]*x^{n-1} + ... + a[0]. The output vector roots must ...
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:
Z3_probe Z3_API Z3_probe_eq(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned ...
Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o)
Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions ...
Z3_sort Z3_API Z3_mk_char_sort(Z3_context c)
Create a sort for unicode characters.
Z3_ast Z3_API Z3_mk_unsigned_int(Z3_context c, unsigned v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_ast Z3_API Z3_mk_bvsle(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than or equal to.
void Z3_API Z3_query_constructor(Z3_context c, Z3_constructor constr, unsigned num_fields, Z3_func_decl *constructor, Z3_func_decl *tester, Z3_func_decl accessors[])
Query constructor for declared functions.
void Z3_API Z3_optimize_set_initial_value(Z3_context c, Z3_optimize o, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_func_decl Z3_API Z3_get_decl_func_decl_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x)
Return the nonzero subresultants of p and q with respect to the "variable" x.
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
Z3_ast Z3_API Z3_mk_int(Z3_context c, int v, Z3_sort ty)
Create a numeral of an int, bit-vector, or finite-domain sort.
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val)
Return a RCF rational using the given string.
Z3_ast Z3_API Z3_mk_ff_neg(Z3_context c, Z3_ast a)
Additive inverse in a prime field.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o)
Retrieve the model for the last Z3_optimize_check.
Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort)
Create an empty finite set of the given sort.
void Z3_API Z3_apply_result_inc_ref(Z3_context c, Z3_apply_result r)
Increment the reference counter of the given Z3_apply_result object.
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvxor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise exclusive-or.
Z3_string Z3_API Z3_stats_to_string(Z3_context c, Z3_stats s)
Convert a statistics into a string.
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives....
Z3_ast Z3_API Z3_mk_le(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than or equal to.
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g)
Return true if the given goal contains the formula false.
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created.
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_mk_bvslt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed less than.
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the set difference of two finite sets.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a + b.
Z3_symbol Z3_API Z3_get_decl_symbol_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)
load solver assertions from a string.
Z3_ast Z3_API Z3_mk_unary_minus(Z3_context c, Z3_ast arg)
Create an AST node representing - arg.
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3_probe Z3_API Z3_probe_ge(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the...
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2)
Check if one finite set is a subset of another.
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point subtraction.
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a)
Add a new formula a to the given goal. The formula is split according to the following procedure that...
Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, Z3_symbol name, unsigned num_parameters, Z3_sort parameters[], unsigned num_constructors, Z3_constructor constructors[])
Create a parametric datatype with explicit type parameters.
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d)
Backtrack one level.
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
Z3_sort Z3_API Z3_mk_datatype(Z3_context c, Z3_symbol name, unsigned num_constructors, Z3_constructor constructors[])
Create datatype, such as lists, trees, records, enumerations or unions of records....
Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
Z3_ast Z3_API Z3_mk_bvmul(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement multiplication.
Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m)
Convert a model of the formulas of a goal to a model of an original goal. The model may be null,...
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr)
Reclaim memory allocated to constructor.
Z3_ast Z3_API Z3_mk_bvsgt(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed greater than.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a == b.
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t)
Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_s...
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
bool Z3_API Z3_stats_is_uint(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a unsigned integer.
bool Z3_API Z3_stats_is_double(Z3_context c, Z3_stats s, unsigned idx)
Return true if the given statistical data is a double.
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a < b.
Z3_ast Z3_API Z3_mk_mod(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 mod arg2.
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_ast Z3_API Z3_mk_ge(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than or equal to.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
bool Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback cb, unsigned num_fixed, Z3_ast const *fixed, unsigned num_eqs, Z3_ast const *eq_lhs, Z3_ast const *eq_rhs, Z3_ast conseq)
propagate a consequence based on fixed values and equalities. A client may invoke it during the pro...
Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector ...
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a)
Return the value 1/a.
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array)
Access the array default value. Produces the default range value, for arrays that can be represented ...
Z3_ast Z3_API Z3_datatype_update_field(Z3_context c, Z3_func_decl field_access, Z3_ast t, Z3_ast value)
Update record field with a value.
Z3_ast Z3_API Z3_mk_forall_const(Z3_context c, unsigned weight, unsigned num_bound, Z3_app const bound[], unsigned num_patterns, Z3_pattern const patterns[], Z3_ast body)
Create a universal quantifier using a list of constants that will form the set of bound variables.
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigns an interpretation to.
bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a > b.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Z3_param_descrs Z3_API Z3_tactic_get_param_descrs(Z3_context c, Z3_tactic t)
Return the parameter description set for the given tactic object.
Z3_sort Z3_API Z3_mk_tuple_sort(Z3_context c, Z3_symbol mk_tuple_name, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const field_sorts[], Z3_func_decl *mk_tuple_decl, Z3_func_decl proj_decl[])
Create a tuple type.
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e)
Increment the reference counter of the given Z3_func_entry object.
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a - b.
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2)
Maximum of floating-point numbers.
void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t)
Assert tracked hard constraint to the optimization context.
unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id)
Assert soft constraint to the optimization context.
Z3_app Z3_API Z3_to_app(Z3_context c, Z3_ast a)
Convert an ast into an APP_AST. This is just type casting.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a <= b.
Z3_ast Z3_API Z3_mk_bvshl(Z3_context c, Z3_ast t1, Z3_ast t2)
Shift left.
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set)
Filter a finite set using a predicate.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
Z3_ast Z3_API Z3_solver_congruence_next(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the next expression in the congruence class. The set of congruent siblings form a cyclic lis...
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g)
Return the number of formulas, subformulas and terms in the given goal.
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r)
Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
bool Z3_API Z3_rcf_is_infinitesimal(Z3_context c, Z3_rcf_num a)
Return true if a represents an infinitesimal.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i)
Array read. The argument a is the array and i is the index of the array that gets read.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check if an element is a member of a finite set.
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_ast Z3_API Z3_mk_u32string(Z3_context c, unsigned len, unsigned const chars[])
Create a string constant out of the string that is passed in It takes the length of the string as wel...
void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, Z3_func_decl r, unsigned num_args, unsigned args[])
Add a Database fact.
unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g)
Return the number of formulas in the given goal.
Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_symbol name, unsigned n, Z3_sort *domain, Z3_sort range)
void Z3_API Z3_stats_inc_ref(Z3_context c, Z3_stats s)
Increment the reference counter of the given statistics object.
Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs)
n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.
Z3_ast Z3_API Z3_mk_div(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 div arg2.
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d)
Increment the reference counter of the given optimize context.
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[])
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f)
Increment the reference counter of the given Z3_func_interp object.
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c)
Return a new infinitesimal that is smaller than all elements in the Z3 field.
Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the union of two finite sets.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g)
Increment the reference counter of the given goal.
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t)
Return number of constructors for datatype.
Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx)
Retrieve upper bound value or approximation for the i'th optimization objective.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than.
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
Z3_ast Z3_API Z3_mk_bvashr(Z3_context c, Z3_ast t1, Z3_ast t2)
Arithmetic shift right.
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)
Ad-hoc method for importing model conversion from solver.
bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a >= b.
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p)
Set parameters on optimization context, including parameters for the underlying SMT solver.
Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2)
Create the intersection of two finite sets.
Z3_ast Z3_API Z3_mk_bvor(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise or.
int Z3_API Z3_get_decl_int_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the integer value associated with an integer parameter.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th constructor.
Z3_lbool
Lifted Boolean type: false, undefined, true.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
void Z3_API Z3_solver_set_initial_value(Z3_context c, Z3_solver s, Z3_ast v, Z3_ast val)
provide an initialization hint to the solver. The initialization hint is used to calibrate an initial...
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d)
Create a backtracking point.
unsigned Z3_API Z3_stats_get_uint_value(Z3_context c, Z3_stats s, unsigned idx)
Return the unsigned value of the given statistical data.
void Z3_API Z3_probe_inc_ref(Z3_context c, Z3_probe p)
Increment the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point equality.
void Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
Z3_ast Z3_API Z3_mk_bvadd(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement addition.
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.
Z3_ast Z3_API Z3_solver_congruence_root(Z3_context c, Z3_solver s, Z3_ast a)
retrieve the congruence closure root of an expression. The root is retrieved relative to the state wh...
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
Z3_string Z3_API Z3_tactic_get_help(Z3_context c, Z3_tactic t)
Return a string containing a description of parameters accepted by the given tactic.
void Z3_API Z3_solver_propagate_final(Z3_context c, Z3_solver s, Z3_final_eh final_eh)
register a callback on final check. This provides freedom to the propagator to delay actions or imple...
Z3_parameter_kind
The different kinds of parameters that can be associated with function symbols.
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point greater than or equal.
void Z3_API Z3_solver_register_on_clause(Z3_context c, Z3_solver s, void *user_context, Z3_on_clause_eh on_clause_eh)
register a callback to that retrieves assumed, inferred and deleted clauses during search.
Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names)
Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF...
Z3_ast Z3_API Z3_mk_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create less than.
double Z3_API Z3_stats_get_double_value(Z3_context c, Z3_stats s, unsigned idx)
Return the double value of the given statistical data.
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a float.
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g)
Return the depth of the given goal. It tracks how many transformations were applied to it.
Z3_ast Z3_API Z3_update_term(Z3_context c, Z3_ast a, unsigned num_args, Z3_ast const args[])
Update the arguments of term a using the arguments args. The number of arguments num_args should coin...
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
Z3_ast Z3_API Z3_mk_bvnot(Z3_context c, Z3_ast t1)
Bitwise negation.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s)
Create a fold with index tracking of the function f over the sequence s with accumulator a starting a...
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
Z3_ast Z3_API Z3_mk_bvsub(Z3_context c, Z3_ast t1, Z3_ast t2)
Standard two's complement subtraction.
Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o)
Return objectives on the optimization context. If the objective function is a max-sat objective it is...
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of the first occurrence of substr in s starting from offset offset. If s does not contai...
Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 ^ arg2.
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.
Z3_ast Z3_API Z3_mk_ff_add(Z3_context c, unsigned n, Z3_ast const args[])
Sum at least two elements of the same prime field.
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g)
Erase all formulas from the given goal.
void Z3_API Z3_func_interp_dec_ref(Z3_context c, Z3_func_interp f)
Decrement the reference counter of the given Z3_func_interp object.
void Z3_API Z3_probe_dec_ref(Z3_context c, Z3_probe p)
Decrement the reference counter of the given probe.
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec)
Convert the RCF numeral into a string in decimal notation.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k)
Return the value a^k.
Z3_ast Z3_API Z3_solver_congruence_explain(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast b)
retrieve explanation for congruence.
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point remainder.
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_probe Z3_API Z3_probe_or(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
void Z3_API Z3_solver_propagate_init(Z3_context c, Z3_solver s, void *user_context, Z3_push_eh push_eh, Z3_pop_eh pop_eh, Z3_fresh_eh fresh_eh)
register a user-propagator with the solver.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
void Z3_API Z3_tactic_dec_ref(Z3_context c, Z3_tactic g)
Decrement the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_bvnand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise nand.
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a)
Assert hard constraint to the optimization context.
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s.
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_ast Z3_API Z3_mk_bv_numeral(Z3_context c, unsigned sz, bool const *bits)
create a bit-vector numeral from a vector of Booleans.
void Z3_API Z3_func_entry_dec_ref(Z3_context c, Z3_func_entry e)
Decrement the reference counter of the given Z3_func_entry object.
unsigned Z3_API Z3_stats_size(Z3_context c, Z3_stats s)
Return the number of statistical data in s.
Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o)
Print the current context as a string.
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2)
Minimum of floating-point numbers.
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s)
Create a map of the function f over the sequence s starting at index i.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer,...
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val)
Return a RCF small integer.
Z3_string Z3_API Z3_stats_get_key(Z3_context c, Z3_stats s, unsigned idx)
Return the key (a string) for a particular statistical data.
Z3_ast Z3_API Z3_mk_re_diff(Z3_context c, Z3_ast re1, Z3_ast re2)
Create the difference of regular expressions.
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate.
Z3_ast Z3_API Z3_mk_int64(Z3_context c, int64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_sort Z3_API Z3_mk_complex_sort(Z3_context c)
Create the Complex sort. Complex numbers are pairs of Reals.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point addition.
Z3_ast Z3_API Z3_mk_bvand(Z3_context c, Z3_ast t1, Z3_ast t2)
Bitwise and.
bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g)
Return true if the goal contains false, and it is precise or the product of an over approximation.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
Z3_ast Z3_API Z3_mk_bvsmod(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows divisor).
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_optimize Z3_API Z3_mk_optimize(Z3_context c)
Create a new optimize context.
bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a variable.
Z3_ast Z3_API Z3_substitute_funs(Z3_context c, Z3_ast a, unsigned num_funs, Z3_func_decl const from[], Z3_ast const to[])
Substitute functions in from with new expressions in to.
Z3_ast Z3_API Z3_func_entry_get_arg(Z3_context c, Z3_func_entry e, unsigned i)
Return an argument of a Z3_func_entry object.
Z3_ast Z3_API Z3_mk_eq(Z3_context c, Z3_ast l, Z3_ast r)
Create an AST node representing l = r.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d)
Decrement the reference counter of the given optimize context.
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, bool compact, bool html)
Convert the RCF numeral into a string.
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return true if a != b.
void Z3_API Z3_solver_solve_for(Z3_context c, Z3_solver s, Z3_ast_vector variables, Z3_ast_vector terms, Z3_ast_vector guards)
retrieve a 'solution' for variables as defined by equalities in maintained by solvers....
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_ff_mul(Z3_context c, unsigned n, Z3_ast const args[])
Multiply at least two elements of the same prime field.
void Z3_API Z3_rcf_del(Z3_context c, Z3_rcf_num a)
Delete a RCF numeral created using the RCF API.
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
Z3_sort Z3_API Z3_mk_finite_field_sort(Z3_context c, Z3_string prime)
Create a prime-field sort. Large moduli undergo probable-prime screening.
Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g)
Return the "precision" of the given goal. Goals can be transformed using over and under approximation...
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
double Z3_API Z3_get_decl_double_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the double value associated with an double parameter.
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than.
Z3_ast Z3_API Z3_mk_unsigned_int64(Z3_context c, uint64_t v, Z3_sort ty)
Create a numeral of a int, bit-vector, or finite-domain sort.
Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c)
Return Pi.
Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t)
Return a string containing a description of parameters accepted by optimize.
Z3_func_decl Z3_API Z3_get_datatype_sort_recognizer(Z3_context c, Z3_sort t, unsigned idx)
Return idx'th recognizer.
Z3_ast Z3_API Z3_mk_gt(Z3_context c, Z3_ast t1, Z3_ast t2)
Create greater than.
Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d)
Retrieve statistics information from the last call to Z3_optimize_check.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_probe Z3_API Z3_probe_gt(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is greater than the value retur...
Z3_ast Z3_API Z3_mk_complex(Z3_context c, Z3_ast re, Z3_ast im)
Create a complex number with the given real and imaginary components. Integer components are coerced ...
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_string Z3_API Z3_get_decl_rational_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the rational value, as a string, associated with a rational parameter.
unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a minimization constraint.
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.
bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Test if there exists an interpretation (i.e., assignment) for a in the model m.
void Z3_API Z3_tactic_inc_ref(Z3_context c, Z3_tactic t)
Increment the reference counter of the given tactic.
Z3_ast Z3_API Z3_mk_real_int64(Z3_context c, int64_t num, int64_t den)
Create a real from a fraction of int64.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr)
Return index of the last occurrence of substr in s. If s does not contain substr, then the value is -...
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
void Z3_API Z3_solver_propagate_eq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh)
register a callback on expression equalities.
Z3_ast Z3_API Z3_mk_string(Z3_context c, Z3_string s)
Create a string constant out of the string that is passed in The string may contain escape encoding f...
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
void Z3_API Z3_apply_result_dec_ref(Z3_context c, Z3_apply_result r)
Decrement the reference counter of the given Z3_apply_result object.
Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem)
Create a singleton finite set.
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t)
Add a maximization constraint.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i)
Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
Z3_probe Z3_API Z3_probe_le(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the va...
void Z3_API Z3_stats_dec_ref(Z3_context c, Z3_stats s)
Decrement the reference counter of the given statistics object.
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a)
Return the value -a.
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_func_entry Z3_API Z3_func_interp_get_entry(Z3_context c, Z3_func_interp f, unsigned i)
Return a "point" of the given function interpretation. It represents the value of f in a particular p...
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Z3_sort Z3_API Z3_get_decl_sort_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the sort value associated with a sort parameter.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2)
Floating-point less than or equal.
Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set)
Apply a function to all elements of a finite set.
void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh)
register a callback when a new expression with a registered function is used by the solver The regist...
bool Z3_API Z3_rcf_is_algebraic(Z3_context c, Z3_rcf_num a)
Return true if a represents an algebraic number.
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty)
Create a numeral of FloatingPoint sort from a double.
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point multiplication.
Z3_ast Z3_API Z3_mk_app(Z3_context c, Z3_func_decl d, unsigned num_args, Z3_ast const args[])
Create a constant or function application.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_ast Z3_API Z3_mk_bvneg(Z3_context c, Z3_ast t1)
Standard two's complement unary minus.
Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const *idxs, Z3_ast v)
n-ary Array update.
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query.
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id.
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
Z3_ast Z3_API Z3_mk_sub(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] - ... - args[num_args - 1].
Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort)
Create a finite set sort.
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
Z3_ast Z3_API Z3_mk_imag_part(Z3_context c, Z3_ast z)
Return the imaginary component of a Complex expression.
Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set)
Get the size (cardinality) of a finite set.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh)
register a callback when the solver decides to split on a registered expression. The callback may cha...
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
Z3_ast Z3_API Z3_mk_bvsdiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed division.
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high)
Create a finite set of integers in the range [low, high].
double Z3_API Z3_probe_apply(Z3_context c, Z3_probe p, Z3_goal g)
Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0....
bool Z3_API Z3_rcf_is_transcendental(Z3_context c, Z3_rcf_num a)
Return true if a represents a transcendental number.
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value)
Return the 'else' value of the given function interpretation.
void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g)
Decrement the reference counter of the given goal.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
void Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e)
register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Ve...
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_tactic Z3_API Z3_tactic_or_else(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 appl...
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2)
Floating-point division.
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t)
Floating-point square root.
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g)
Return true if the goal is empty, and it is precise or the product of a under approximation.
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.
void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s)
Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives....
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing.
Z3_ast Z3_API Z3_mk_rem(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create an AST node representing arg1 rem arg2.
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.
bool Z3_API Z3_rcf_is_rational(Z3_context c, Z3_rcf_num a)
Return true if a represents a rational number.
void Z3_API Z3_solver_propagate_fixed(Z3_context c, Z3_solver s, Z3_fixed_eh fixed_eh)
register a callback for when an expression is bound to a fixed value. The supported expression types ...
Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s)
Create a map of the function f over the sequence s.
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f)
Create array with the same interpretation as a function. The array satisfies the property (f x) = (se...
Z3_string Z3_API Z3_apply_result_to_string(Z3_context c, Z3_apply_result r)
Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s)
Create a fold of the function f over the sequence s with accumulator a.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Floating-point fused multiply-add.
Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c)
Return e (Euler's constant)
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast Z3_API Z3_mk_real_part(Z3_context c, Z3_ast z)
Return the real component of a Complex expression.
Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx)
Return a formula from the given goal.
Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[])
Check consistency and produce optimal values.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f)
Return the number of entries in the given function interpretation.
Z3_probe Z3_API Z3_probe_const(Z3_context x, double val)
Return a probe that always evaluates to val.
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c)
Create the RoundingMode sort.
Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g)
Convert a goal into a string.
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_tactic Z3_API Z3_tactic_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
Z3_optimize Z3_API Z3_optimize_translate(Z3_context c, Z3_optimize o, Z3_context target)
Copy an optimization context from a source to a target context.
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a)
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase)
Z3_probe Z3_API Z3_probe_and(Z3_context x, Z3_probe p1, Z3_probe p2)
Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s)
Check if s is a regular expression sort.
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for unicode strings.
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b)
Return the value a * b.
Z3_func_decl Z3_API Z3_get_datatype_sort_constructor_accessor(Z3_context c, Z3_sort t, unsigned idx_c, unsigned idx_a)
Return idx_a'th accessor for the idx_c'th constructor.
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
System.IntPtr Z3_ast_vector
System.IntPtr Z3_func_interp
System.IntPtr Z3_func_decl
System.IntPtr Z3_func_entry
System.IntPtr Z3_solver_callback
expr set_intersect(expr const &a, expr const &b)
expr re_intersect(expr_vector const &args)
expr store(expr const &a, expr const &i, expr const &v)
expr pw(expr const &a, expr const &b)
expr sbv_to_fpa(expr const &t, sort s)
expr bvneg_no_overflow(expr const &a)
expr finite_set_difference(expr const &a, expr const &b)
expr indexof(expr const &s, expr const &substr, expr const &offset)
tactic par_or(unsigned n, tactic const *tactics)
tactic par_and_then(tactic const &t1, tactic const &t2)
expr srem(expr const &a, expr const &b)
signed remainder operator for bitvectors
expr bvadd_no_underflow(expr const &a, expr const &b)
expr prefixof(expr const &a, expr const &b)
expr sum(expr_vector const &args)
expr ugt(expr const &a, expr const &b)
unsigned greater than operator for bitvectors.
expr operator/(expr const &a, expr const &b)
expr exists(expr const &x, expr const &b)
expr fp_eq(expr const &a, expr const &b)
func_decl tree_order(sort const &a, unsigned index)
expr concat(expr const &a, expr const &b)
expr bvmul_no_underflow(expr const &a, expr const &b)
expr lambda(expr const &x, expr const &b)
ast_vector_tpl< func_decl > func_decl_vector
expr fpa_to_fpa(expr const &t, sort s)
expr qe_model_project(model const &m, expr_vector const &bounds, expr const &body)
expr operator&&(expr const &a, expr const &b)
std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t
expr operator!=(expr const &a, expr const &b)
expr operator+(expr const &a, expr const &b)
expr set_complement(expr const &a)
func_decl recfun(symbol const &name, unsigned arity, sort const *domain, sort const &range)
expr const_array(sort const &d, expr const &v)
expr min(expr const &a, expr const &b)
expr set_difference(expr const &a, expr const &b)
expr forall(expr const &x, expr const &b)
expr array_default(expr const &a)
expr array_ext(expr const &a, expr const &b)
expr qe_lite(expr_vector const &vars, expr const &body)
expr operator>(expr const &a, expr const &b)
sort to_sort(context &c, Z3_sort s)
expr finite_set_map(expr const &f, expr const &s)
expr to_expr(context &c, Z3_ast a)
Wraps a Z3_ast as an expr object. It also checks for errors. This function allows the user to use the...
expr bv2int(expr const &a, bool is_signed)
bit-vector and integer conversions.
expr operator%(expr const &a, expr const &b)
expr operator~(expr const &a)
expr sle(expr const &a, expr const &b)
signed less than or equal to operator for bitvectors.
expr nor(expr const &a, expr const &b)
expr fpa_fp(expr const &sgn, expr const &exp, expr const &sig)
expr bvsub_no_underflow(expr const &a, expr const &b, bool is_signed)
expr finite_set_singleton(expr const &e)
expr mk_xor(expr_vector const &args)
expr lshr(expr const &a, expr const &b)
logic shift right operator for bitvectors
expr operator*(expr const &a, expr const &b)
expr nand(expr const &a, expr const &b)
expr fpa_to_ubv(expr const &t, unsigned sz)
expr bvredor(expr const &a)
ast_vector_tpl< sort > sort_vector
expr finite_set_subset(expr const &a, expr const &b)
func_decl piecewise_linear_order(sort const &a, unsigned index)
expr slt(expr const &a, expr const &b)
signed less than operator for bitvectors.
tactic when(probe const &p, tactic const &t)
expr last_indexof(expr const &s, expr const &substr)
expr int2bv(unsigned n, expr const &a)
expr max(expr const &a, expr const &b)
expr xnor(expr const &a, expr const &b)
expr udiv(expr const &a, expr const &b)
unsigned division operator for bitvectors.
expr pbge(expr_vector const &es, int const *coeffs, int bound)
expr round_fpa_to_closest_integer(expr const &t)
expr distinct(expr_vector const &args)
expr ashr(expr const &a, expr const &b)
arithmetic shift right operator for bitvectors
expr bvmul_no_overflow(expr const &a, expr const &b, bool is_signed)
expr bvsub_no_overflow(expr const &a, expr const &b)
expr star(expr const &re)
expr urem(expr const &a, expr const &b)
unsigned reminder operator for bitvectors
tactic repeat(tactic const &t, unsigned max=UINT_MAX)
expr mod(expr const &a, expr const &b)
expr fma(expr const &a, expr const &b, expr const &c, expr const &rm)
check_result to_check_result(Z3_lbool l)
expr mk_or(expr_vector const &args)
expr to_re(expr const &s)
void check_context(object const &a, object const &b)
expr_vector polynomial_subresultants(expr const &p, expr const &q, expr const &x)
Return the nonzero subresultants of p and q with respect to the "variable" x.
std::ostream & operator<<(std::ostream &out, exception const &e)
expr ule(expr const &a, expr const &b)
unsigned less than or equal to operator for bitvectors.
func_decl to_func_decl(context &c, Z3_func_decl f)
tactic with(tactic const &t, params const &p)
expr ite(expr const &c, expr const &t, expr const &e)
Create the if-then-else expression ite(c, t, e)
expr finite_set_filter(expr const &f, expr const &s)
expr ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
expr finite_set_union(expr const &a, expr const &b)
expr qe_model_project_skolem(model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
Project variables and write the introduced Skolem terms to map.
expr pbeq(expr_vector const &es, int const *coeffs, int bound)
expr operator^(expr const &a, expr const &b)
expr operator<=(expr const &a, expr const &b)
expr set_union(expr const &a, expr const &b)
expr imag_part(expr const &z)
expr operator>=(expr const &a, expr const &b)
func_decl linear_order(sort const &a, unsigned index)
expr sqrt(expr const &a, expr const &rm)
expr pble(expr_vector const &es, int const *coeffs, int bound)
expr operator==(expr const &a, expr const &b)
expr foldli(expr const &f, expr const &i, expr const &a, expr const &list)
expr full_set(sort const &s)
std::vector< rcf_num > rcf_roots(context &c, std::vector< rcf_num > const &coeffs)
Find roots of a polynomial with given coefficients.
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
expr implies(expr const &a, expr const &b)
expr finite_set_range(expr const &low, expr const &high)
expr empty_set(sort const &s)
expr complex(expr const &re, expr const &im)
Construct a Complex expression from Int or Real components.
expr in_re(expr const &s, expr const &re)
expr finite_set_member(expr const &e, expr const &s)
expr bvadd_no_overflow(expr const &a, expr const &b, bool is_signed)
bit-vector overflow/underflow checks
expr suffixof(expr const &a, expr const &b)
expr re_diff(expr const &a, expr const &b)
expr set_add(expr const &s, expr const &e)
rcf_num rcf_e(context &c)
Create an RCF numeral representing e (Euler's constant).
expr plus(expr const &re)
expr set_subset(expr const &a, expr const &b)
expr select(expr const &a, expr const &i)
forward declarations
expr bvredand(expr const &a)
expr operator&(expr const &a, expr const &b)
expr operator-(expr const &a)
expr set_member(expr const &s, expr const &e)
expr bvsdiv_no_overflow(expr const &a, expr const &b)
tactic try_for(tactic const &t, unsigned ms)
expr finite_set_size(expr const &s)
expr real_part(expr const &z)
expr sdiv(expr const &a, expr const &b)
signed division operator for bitvectors.
func_decl partial_order(sort const &a, unsigned index)
ast_vector_tpl< expr > expr_vector
expr rem(expr const &a, expr const &b)
expr sge(expr const &a, expr const &b)
signed greater than or equal to operator for bitvectors.
expr operator!(expr const &a)
expr re_empty(sort const &s)
expr foldl(expr const &f, expr const &a, expr const &list)
rcf_num rcf_pi(context &c)
Create an RCF numeral representing pi.
expr mk_and(expr_vector const &args)
expr finite_set_empty(sort const &s)
expr sext(expr const &a, unsigned i)
Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i,...
expr to_real(expr const &a)
expr shl(expr const &a, expr const &b)
shift left operator for bitvectors
std::vector< Z3_app > to_apps(expr_vector const &bounds)
expr operator||(expr const &a, expr const &b)
expr finite_set_intersect(expr const &a, expr const &b)
expr set_del(expr const &s, expr const &e)
expr ubv_to_fpa(expr const &t, sort s)
expr map(expr const &f, expr const &list)
tactic cond(probe const &p, tactic const &t1, tactic const &t2)
expr as_array(func_decl &f)
expr sgt(expr const &a, expr const &b)
signed greater than operator for bitvectors.
expr fpa_to_sbv(expr const &t, unsigned sz)
expr operator|(expr const &a, expr const &b)
expr atmost(expr_vector const &es, unsigned bound)
expr range(expr const &lo, expr const &hi)
expr zext(expr const &a, unsigned i)
Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i,...
expr atleast(expr_vector const &es, unsigned bound)
expr qe_model_project_with_witness(model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
Project variables and write the introduced witnesses to map.
expr uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
expr mapi(expr const &f, expr const &i, expr const &list)
expr operator<(expr const &a, expr const &b)
expr option(expr const &re)
expr re_full(sort const &s)
expr re_complement(expr const &a)
expr empty(sort const &s)
rcf_num rcf_infinitesimal(context &c)
Create an RCF numeral representing an infinitesimal.
tactic fail_if(probe const &p)
bool eq(AstRef a, AstRef b)
on_clause_eh(ctx, p, n, dep, clause)
#define _Z3_MK_BIN_(a, b, binop)
#define MK_EXPR1(_fn, _arg)
#define MK_EXPR2(_fn, _arg1, _arg2)
#define _Z3_MK_UN_(a, mkun)