1627 {
1628 assert(a.is_bool() && b.is_bool());
1630 }
1631 inline expr
implies(expr
const & a,
bool b) {
return implies(a, a.ctx().bool_val(b)); }
1632 inline expr
implies(
bool a, expr
const & b) {
return implies(b.ctx().bool_val(a), b); }
1633
1634
1636 inline expr
pw(expr
const & a,
int b) {
return pw(a, a.ctx().num_val(b, a.get_sort())); }
1637 inline expr
pw(
int a, expr
const & b) {
return pw(b.ctx().num_val(a, b.get_sort()), b); }
1638
1639 inline expr
mod(expr
const& a, expr
const& b) {
1640 if (a.is_bv()) {
1642 }
1643 else {
1645 }
1646 }
1647 inline expr
mod(expr
const & a,
int b) {
return mod(a, a.ctx().num_val(b, a.get_sort())); }
1648 inline expr
mod(
int a, expr
const & b) {
return mod(b.ctx().num_val(a, b.get_sort()), b); }
1649
1650 inline expr
operator%(expr
const& a, expr
const& b) {
return mod(a, b); }
1651 inline expr
operator%(expr
const& a,
int b) {
return mod(a, b); }
1652 inline expr
operator%(
int a, expr
const& b) {
return mod(a, b); }
1653
1654
1655 inline expr
rem(expr
const& a, expr
const& b) {
1656 if (a.is_fpa() && b.is_fpa()) {
1658 } else {
1660 }
1661 }
1662 inline expr
rem(expr
const & a,
int b) {
return rem(a, a.ctx().num_val(b, a.get_sort())); }
1663 inline expr
rem(
int a, expr
const & b) {
return rem(b.ctx().num_val(a, b.get_sort()), b); }
1664
1665#undef _Z3_MK_BIN_
1666
1667#define _Z3_MK_UN_(a, mkun) \
1668 Z3_ast r = mkun(a.ctx(), a); \
1669 a.check_error(); \
1670 return expr(a.ctx(), r); \
1671
1672
1674
1676
1677#undef _Z3_MK_UN_
1678
1679 inline expr
operator&&(expr
const & a, expr
const & b) {
1681 assert(a.is_bool() && b.is_bool());
1682 Z3_ast args[2] = { a, b };
1684 a.check_error();
1685 return expr(a.ctx(), r);
1686 }
1687
1690
1691 inline expr
operator||(expr
const & a, expr
const & b) {
1693 assert(a.is_bool() && b.is_bool());
1694 Z3_ast args[2] = { a, b };
1695 Z3_ast r =
Z3_mk_or(a.ctx(), 2, args);
1696 a.check_error();
1697 return expr(a.ctx(), r);
1698 }
1699
1701
1703
1704 inline expr
operator==(expr
const & a, expr
const & b) {
1706 Z3_ast r =
Z3_mk_eq(a.ctx(), a, b);
1707 a.check_error();
1708 return expr(a.ctx(), r);
1709 }
1710 inline expr
operator==(expr
const & a,
int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a == a.ctx().num_val(b, a.get_sort()); }
1711 inline expr
operator==(
int a, expr
const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) == b; }
1712 inline expr
operator==(expr
const & a,
double b) { assert(a.is_fpa());
return a == a.ctx().fpa_val(b); }
1713 inline expr
operator==(
double a, expr
const & b) { assert(b.is_fpa());
return b.ctx().fpa_val(a) == b; }
1714
1715 inline expr
operator!=(expr
const & a, expr
const & b) {
1717 Z3_ast args[2] = { a, b };
1719 a.check_error();
1720 return expr(a.ctx(), r);
1721 }
1722 inline expr
operator!=(expr
const & a,
int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa());
return a != a.ctx().num_val(b, a.get_sort()); }
1723 inline expr
operator!=(
int a, expr
const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa());
return b.ctx().num_val(a, b.get_sort()) != b; }
1724 inline expr
operator!=(expr
const & a,
double b) { assert(a.is_fpa());
return a != a.ctx().fpa_val(b); }
1725 inline expr
operator!=(
double a, expr
const & b) { assert(b.is_fpa());
return b.ctx().fpa_val(a) != b; }
1726
1727 inline expr
operator+(expr
const & a, expr
const & b) {
1729 Z3_ast r = 0;
1730 if (a.is_arith() && b.is_arith()) {
1731 Z3_ast args[2] = { a, b };
1733 }
1734 else if (a.is_bv() && b.is_bv()) {
1736 }
1737 else if (a.is_seq() && b.is_seq()) {
1739 }
1740 else if (a.is_re() && b.is_re()) {
1741 Z3_ast _args[2] = { a, b };
1743 }
1744 else if (a.is_fpa() && b.is_fpa()) {
1745 r =
Z3_mk_fpa_add(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1746 }
1747 else {
1748
1749 assert(false);
1750 }
1751 a.check_error();
1752 return expr(a.ctx(), r);
1753 }
1754 inline expr
operator+(expr
const & a,
int b) {
return a + a.
ctx().
num_val(b, a.get_sort()); }
1755 inline expr
operator+(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) + b; }
1756
1757 inline expr
operator*(expr
const & a, expr
const & b) {
1759 Z3_ast r = 0;
1760 if (a.is_arith() && b.is_arith()) {
1761 Z3_ast args[2] = { a, b };
1763 }
1764 else if (a.is_bv() && b.is_bv()) {
1766 }
1767 else if (a.is_fpa() && b.is_fpa()) {
1768 r =
Z3_mk_fpa_mul(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1769 }
1770 else {
1771
1772 assert(false);
1773 }
1774 a.check_error();
1775 return expr(a.ctx(), r);
1776 }
1777 inline expr
operator*(expr
const & a,
int b) {
return a * a.
ctx().
num_val(b, a.get_sort()); }
1778 inline expr
operator*(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) * b; }
1779
1780
1781 inline expr
operator>=(expr
const & a, expr
const & b) {
1783 Z3_ast r = 0;
1784 if (a.is_arith() && b.is_arith()) {
1786 }
1787 else if (a.is_bv() && b.is_bv()) {
1789 }
1790 else if (a.is_fpa() && b.is_fpa()) {
1792 }
1793 else {
1794
1795 assert(false);
1796 }
1797 a.check_error();
1798 return expr(a.ctx(), r);
1799 }
1800
1801 inline expr
operator/(expr
const & a, expr
const & b) {
1803 Z3_ast r = 0;
1804 if (a.is_arith() && b.is_arith()) {
1806 }
1807 else if (a.is_bv() && b.is_bv()) {
1809 }
1810 else if (a.is_fpa() && b.is_fpa()) {
1811 r =
Z3_mk_fpa_div(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1812 }
1813 else {
1814
1815 assert(false);
1816 }
1817 a.check_error();
1818 return expr(a.ctx(), r);
1819 }
1820 inline expr
operator/(expr
const & a,
int b) {
return a / a.
ctx().
num_val(b, a.get_sort()); }
1821 inline expr
operator/(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) / b; }
1822
1824 Z3_ast r = 0;
1825 if (a.is_arith()) {
1827 }
1828 else if (a.is_bv()) {
1830 }
1831 else if (a.is_fpa()) {
1833 }
1834 else {
1835
1836 assert(false);
1837 }
1838 a.check_error();
1839 return expr(a.ctx(), r);
1840 }
1841
1842 inline expr
operator-(expr
const & a, expr
const & b) {
1844 Z3_ast r = 0;
1845 if (a.is_arith() && b.is_arith()) {
1846 Z3_ast args[2] = { a, b };
1848 }
1849 else if (a.is_bv() && b.is_bv()) {
1851 }
1852 else if (a.is_fpa() && b.is_fpa()) {
1853 r =
Z3_mk_fpa_sub(a.ctx(), a.ctx().fpa_rounding_mode(), a, b);
1854 }
1855 else {
1856
1857 assert(false);
1858 }
1859 a.check_error();
1860 return expr(a.ctx(), r);
1861 }
1862 inline expr
operator-(expr
const & a,
int b) {
return a - a.
ctx().
num_val(b, a.get_sort()); }
1863 inline expr
operator-(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) - b; }
1864
1865 inline expr
operator<=(expr
const & a, expr
const & b) {
1867 Z3_ast r = 0;
1868 if (a.is_arith() && b.is_arith()) {
1870 }
1871 else if (a.is_bv() && b.is_bv()) {
1873 }
1874 else if (a.is_fpa() && b.is_fpa()) {
1876 }
1877 else {
1878
1879 assert(false);
1880 }
1881 a.check_error();
1882 return expr(a.ctx(), r);
1883 }
1884 inline expr
operator<=(expr
const & a,
int b) {
return a <= a.
ctx().
num_val(b, a.get_sort()); }
1885 inline expr
operator<=(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) <= b; }
1886
1887 inline expr
operator>=(expr
const & a,
int b) {
return a >= a.
ctx().
num_val(b, a.get_sort()); }
1888 inline expr
operator>=(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) >= b; }
1889
1890 inline expr
operator<(expr
const & a, expr
const & b) {
1892 Z3_ast r = 0;
1893 if (a.is_arith() && b.is_arith()) {
1895 }
1896 else if (a.is_bv() && b.is_bv()) {
1898 }
1899 else if (a.is_fpa() && b.is_fpa()) {
1901 }
1902 else {
1903
1904 assert(false);
1905 }
1906 a.check_error();
1907 return expr(a.ctx(), r);
1908 }
1909 inline expr
operator<(expr
const & a,
int b) {
return a < a.
ctx().
num_val(b, a.get_sort()); }
1910 inline expr
operator<(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) < b; }
1911
1912 inline expr
operator>(expr
const & a, expr
const & b) {
1914 Z3_ast r = 0;
1915 if (a.is_arith() && b.is_arith()) {
1917 }
1918 else if (a.is_bv() && b.is_bv()) {
1920 }
1921 else if (a.is_fpa() && b.is_fpa()) {
1923 }
1924 else {
1925
1926 assert(false);
1927 }
1928 a.check_error();
1929 return expr(a.ctx(), r);
1930 }
1931 inline expr
operator>(expr
const & a,
int b) {
return a > a.
ctx().
num_val(b, a.get_sort()); }
1932 inline expr
operator>(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) > b; }
1933
1934 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); }
1935 inline expr
operator&(expr
const & a,
int b) {
return a & a.
ctx().
num_val(b, a.get_sort()); }
1936 inline expr
operator&(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) & b; }
1937
1939 inline expr
operator^(expr
const & a,
int b) {
return a ^ a.
ctx().
num_val(b, a.get_sort()); }
1940 inline expr
operator^(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) ^ b; }
1941
1942 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); }
1943 inline expr
operator|(expr
const & a,
int b) {
return a | a.
ctx().
num_val(b, a.get_sort()); }
1944 inline expr
operator|(
int a, expr
const & b) {
return b.
ctx().
num_val(a, b.get_sort()) | b; }
1945
1946 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); }
1947 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); }
1948 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); }
1949 inline expr
min(expr
const& a, expr
const& b) {
1951 Z3_ast r;
1952 if (a.is_arith()) {
1954 }
1955 else if (a.is_bv()) {
1957 }
1958 else {
1959 assert(a.is_fpa());
1961 }
1962 a.check_error();
1963 return expr(a.ctx(), r);
1964 }
1965 inline expr
max(expr
const& a, expr
const& b) {
1967 Z3_ast r;
1968 if (a.is_arith()) {
1970 }
1971 else if (a.is_bv()) {
1973 }
1974 else {
1975 assert(a.is_fpa());
1977 }
1978 a.check_error();
1979 return expr(a.ctx(), r);
1980 }
1981 inline expr
bvredor(expr
const & a) {
1982 assert(a.is_bv());
1984 a.check_error();
1985 return expr(a.ctx(), r);
1986 }
1987 inline expr
bvredand(expr
const & a) {
1988 assert(a.is_bv());
1990 a.check_error();
1991 return expr(a.ctx(), r);
1992 }
1993 inline expr
abs(expr
const & a) {
1994 Z3_ast r;
1995 if (a.is_int()) {
1997 expr ge = a >= zero;
1998 expr na = -a;
2000 }
2001 else if (a.is_real()) {
2002 expr zero = a.ctx().real_val(0);
2003 expr ge = a >= zero;
2004 expr na = -a;
2006 }
2007 else {
2009 }
2010 a.check_error();
2011 return expr(a.ctx(), r);
2012 }
2013 inline expr
sqrt(expr
const & a, expr
const& rm) {
2015 assert(a.is_fpa());
2017 a.check_error();
2018 return expr(a.ctx(), r);
2019 }
2020 inline expr
fp_eq(expr
const & a, expr
const & b) {
2022 assert(a.is_fpa());
2024 a.check_error();
2025 return expr(a.ctx(), r);
2026 }
2027 inline expr
operator~(expr
const & a) { Z3_ast r =
Z3_mk_bvnot(a.ctx(), a);
return expr(a.ctx(), r); }
2028
2029 inline expr
fma(expr
const& a, expr
const& b, expr
const& c, expr
const& rm) {
2031 assert(a.is_fpa() && b.is_fpa() && c.is_fpa());
2033 a.check_error();
2034 return expr(a.ctx(), r);
2035 }
2036
2037 inline expr
fpa_fp(expr
const& sgn, expr
const& exp, expr
const& sig) {
2039 assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());
2041 sgn.check_error();
2042 return expr(sgn.ctx(), r);
2043 }
2044
2045 inline expr
fpa_to_sbv(expr
const& t,
unsigned sz) {
2046 assert(t.is_fpa());
2048 t.check_error();
2049 return expr(t.ctx(), r);
2050 }
2051
2052 inline expr
fpa_to_ubv(expr
const& t,
unsigned sz) {
2053 assert(t.is_fpa());
2055 t.check_error();
2056 return expr(t.ctx(), r);
2057 }
2058
2059 inline expr
sbv_to_fpa(expr
const& t, sort s) {
2060 assert(t.is_bv());
2062 t.check_error();
2063 return expr(t.ctx(), r);
2064 }
2065
2066 inline expr
ubv_to_fpa(expr
const& t, sort s) {
2067 assert(t.is_bv());
2069 t.check_error();
2070 return expr(t.ctx(), r);
2071 }
2072
2073 inline expr
fpa_to_fpa(expr
const& t, sort s) {
2074 assert(t.is_fpa());
2076 t.check_error();
2077 return expr(t.ctx(), r);
2078 }
2079
2081 assert(t.is_fpa());
2083 t.check_error();
2084 return expr(t.ctx(), r);
2085 }
2086
2092 inline expr
ite(expr
const & c, expr
const & t, expr
const & e) {
2094 assert(c.is_bool());
2096 c.check_error();
2097 return expr(c.ctx(), r);
2098 }
2099
2100
2105 inline expr
to_expr(context & c, Z3_ast a) {
2111 return expr(c, a);
2112 }
2113
2114 inline sort
to_sort(context & c, Z3_sort s) {
2116 return sort(c, s);
2117 }
2118
2119 inline func_decl
to_func_decl(context & c, Z3_func_decl f) {
2121 return func_decl(c, f);
2122 }
2123
2127 inline expr
sle(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsle(a.ctx(), a, b)); }
2128 inline expr
sle(expr
const & a,
int b) {
return sle(a, a.ctx().num_val(b, a.get_sort())); }
2129 inline expr
sle(
int a, expr
const & b) {
return sle(b.ctx().num_val(a, b.get_sort()), b); }
2133 inline expr
slt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvslt(a.ctx(), a, b)); }
2134 inline expr
slt(expr
const & a,
int b) {
return slt(a, a.ctx().num_val(b, a.get_sort())); }
2135 inline expr
slt(
int a, expr
const & b) {
return slt(b.ctx().num_val(a, b.get_sort()), b); }
2139 inline expr
sge(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsge(a.ctx(), a, b)); }
2140 inline expr
sge(expr
const & a,
int b) {
return sge(a, a.ctx().num_val(b, a.get_sort())); }
2141 inline expr
sge(
int a, expr
const & b) {
return sge(b.ctx().num_val(a, b.get_sort()), b); }
2145 inline expr
sgt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvsgt(a.ctx(), a, b)); }
2146 inline expr
sgt(expr
const & a,
int b) {
return sgt(a, a.ctx().num_val(b, a.get_sort())); }
2147 inline expr
sgt(
int a, expr
const & b) {
return sgt(b.ctx().num_val(a, b.get_sort()), b); }
2148
2149
2153 inline expr
ule(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvule(a.ctx(), a, b)); }
2154 inline expr
ule(expr
const & a,
int b) {
return ule(a, a.ctx().num_val(b, a.get_sort())); }
2155 inline expr
ule(
int a, expr
const & b) {
return ule(b.ctx().num_val(a, b.get_sort()), b); }
2159 inline expr
ult(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvult(a.ctx(), a, b)); }
2160 inline expr
ult(expr
const & a,
int b) {
return ult(a, a.ctx().num_val(b, a.get_sort())); }
2161 inline expr
ult(
int a, expr
const & b) {
return ult(b.ctx().num_val(a, b.get_sort()), b); }
2165 inline expr
uge(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvuge(a.ctx(), a, b)); }
2166 inline expr
uge(expr
const & a,
int b) {
return uge(a, a.ctx().num_val(b, a.get_sort())); }
2167 inline expr
uge(
int a, expr
const & b) {
return uge(b.ctx().num_val(a, b.get_sort()), b); }
2171 inline expr
ugt(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvugt(a.ctx(), a, b)); }
2172 inline expr
ugt(expr
const & a,
int b) {
return ugt(a, a.ctx().num_val(b, a.get_sort())); }
2173 inline expr
ugt(
int a, expr
const & b) {
return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2178 inline expr
udiv(expr
const & a,
int b) {
return udiv(a, a.ctx().num_val(b, a.get_sort())); }
2179 inline expr
udiv(
int a, expr
const & b) {
return udiv(b.ctx().num_val(a, b.get_sort()), b); }
2180
2185 inline expr
srem(expr
const & a,
int b) {
return srem(a, a.ctx().num_val(b, a.get_sort())); }
2186 inline expr
srem(
int a, expr
const & b) {
return srem(b.ctx().num_val(a, b.get_sort()), b); }
2187
2192 inline expr
smod(expr
const & a,
int b) {
return smod(a, a.ctx().num_val(b, a.get_sort())); }
2193 inline expr
smod(
int a, expr
const & b) {
return smod(b.ctx().num_val(a, b.get_sort()), b); }
2194
2199 inline expr
urem(expr
const & a,
int b) {
return urem(a, a.ctx().num_val(b, a.get_sort())); }
2200 inline expr
urem(
int a, expr
const & b) {
return urem(b.ctx().num_val(a, b.get_sort()), b); }
2201
2205 inline expr
shl(expr
const & a, expr
const & b) {
return to_expr(a.ctx(),
Z3_mk_bvshl(a.ctx(), a, b)); }
2206 inline expr
shl(expr
const & a,
int b) {
return shl(a, a.ctx().num_val(b, a.get_sort())); }
2207 inline expr
shl(
int a, expr
const & b) {
return shl(b.ctx().num_val(a, b.get_sort()), b); }
2208
2213 inline expr
lshr(expr
const & a,
int b) {
return lshr(a, a.ctx().num_val(b, a.get_sort())); }
2214 inline expr
lshr(
int a, expr
const & b) {
return lshr(b.ctx().num_val(a, b.get_sort()), b); }
2215
2220 inline expr
ashr(expr
const & a,
int b) {
return ashr(a, a.ctx().num_val(b, a.get_sort())); }
2221 inline expr
ashr(
int a, expr
const & b) {
return ashr(b.ctx().num_val(a, b.get_sort()), b); }
2222
2227
2231 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); }
2232 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); }
2233
2239 }
2242 }
2245 }
2248 }
2251 }
2254 }
2257 }
2260 }
2261
2262
2267
2268 inline func_decl
linear_order(sort
const& a,
unsigned index) {
2270 }
2271 inline func_decl
partial_order(sort
const& a,
unsigned index) {
2273 }
2276 }
2277 inline func_decl
tree_order(sort
const& a,
unsigned index) {
2279 }
2280
2281 template<> class cast_ast<ast> {
2282 public:
2283 ast operator()(context & c, Z3_ast a) { return ast(c, a); }
2284 };
2285
2286 template<> class cast_ast<expr> {
2287 public:
2288 expr operator()(context & c, Z3_ast a) {
2293 return expr(c, a);
2294 }
2295 };
2296
2297 template<> class cast_ast<sort> {
2298 public:
2299 sort operator()(context & c, Z3_ast a) {
2301 return sort(c, reinterpret_cast<Z3_sort>(a));
2302 }
2303 };
2304
2305 template<> class cast_ast<func_decl> {
2306 public:
2307 func_decl operator()(context & c, Z3_ast a) {
2309 return func_decl(c, reinterpret_cast<Z3_func_decl>(a));
2310 }
2311 };
2312
2313 template<typename T>
2314 template<typename T2>
2315 array<T>::array(ast_vector_tpl<T2> const & v):m_array(new T[v.size()]), m_size(v.size()) {
2316 for (unsigned i = 0; i < m_size; i++) {
2317 m_array[i] = v[i];
2318 }
2319 }
2320
2321
2322
2323 inline expr
forall(expr
const & x, expr
const & b) {
2325 Z3_app vars[] = {(Z3_app) x};
2326 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2327 }
2328 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & b) {
2330 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2331 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2332 }
2333 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2335 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2336 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2337 }
2338 inline expr
forall(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2340 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2341 Z3_ast r =
Z3_mk_forall_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2342 }
2343 inline expr
forall(expr_vector
const & xs, expr
const & b) {
2344 array<Z3_app> vars(xs);
2345 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);
2346 }
2347 inline expr
exists(expr
const & x, expr
const & b) {
2349 Z3_app vars[] = {(Z3_app) x};
2350 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 1, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2351 }
2352 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & b) {
2354 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2355 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 2, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2356 }
2357 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2359 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2360 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 3, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2361 }
2362 inline expr
exists(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2364 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2365 Z3_ast r =
Z3_mk_exists_const(b.ctx(), 0, 4, vars, 0, 0, b); b.check_error();
return expr(b.ctx(), r);
2366 }
2367 inline expr
exists(expr_vector
const & xs, expr
const & b) {
2368 array<Z3_app> vars(xs);
2369 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);
2370 }
2371 inline expr
lambda(expr
const & x, expr
const & b) {
2373 Z3_app vars[] = {(Z3_app) x};
2374 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 1, vars, b); b.check_error();
return expr(b.ctx(), r);
2375 }
2376 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & b) {
2378 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2};
2379 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 2, vars, b); b.check_error();
return expr(b.ctx(), r);
2380 }
2381 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & b) {
2383 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3 };
2384 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 3, vars, b); b.check_error();
return expr(b.ctx(), r);
2385 }
2386 inline expr
lambda(expr
const & x1, expr
const & x2, expr
const & x3, expr
const & x4, expr
const & b) {
2388 Z3_app vars[] = {(Z3_app) x1, (Z3_app) x2, (Z3_app) x3, (Z3_app) x4 };
2389 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), 4, vars, b); b.check_error();
return expr(b.ctx(), r);
2390 }
2391 inline expr
lambda(expr_vector
const & xs, expr
const & b) {
2392 array<Z3_app> vars(xs);
2393 Z3_ast r =
Z3_mk_lambda_const(b.ctx(), vars.size(), vars.ptr(), b); b.check_error();
return expr(b.ctx(), r);
2394 }
2395
2396 inline expr
pble(expr_vector
const& es,
int const* coeffs,
int bound) {
2397 assert(es.size() > 0);
2398 context& ctx = es[0u].ctx();
2399 array<Z3_ast> _es(es);
2400 Z3_ast r =
Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
2401 ctx.check_error();
2402 return expr(ctx, r);
2403 }
2404 inline expr
pbge(expr_vector
const& es,
int const* coeffs,
int bound) {
2405 assert(es.size() > 0);
2406 context& ctx = es[0u].ctx();
2407 array<Z3_ast> _es(es);
2408 Z3_ast r =
Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
2409 ctx.check_error();
2410 return expr(ctx, r);
2411 }
2412 inline expr
pbeq(expr_vector
const& es,
int const* coeffs,
int bound) {
2413 assert(es.size() > 0);
2414 context& ctx = es[0u].ctx();
2415 array<Z3_ast> _es(es);
2416 Z3_ast r =
Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
2417 ctx.check_error();
2418 return expr(ctx, r);
2419 }
2420 inline expr
atmost(expr_vector
const& es,
unsigned bound) {
2421 assert(es.size() > 0);
2422 context& ctx = es[0u].ctx();
2423 array<Z3_ast> _es(es);
2424 Z3_ast r =
Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
2425 ctx.check_error();
2426 return expr(ctx, r);
2427 }
2428 inline expr
atleast(expr_vector
const& es,
unsigned bound) {
2429 assert(es.size() > 0);
2430 context& ctx = es[0u].ctx();
2431 array<Z3_ast> _es(es);
2432 Z3_ast r =
Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
2433 ctx.check_error();
2434 return expr(ctx, r);
2435 }
2436 inline expr
sum(expr_vector
const& args) {
2437 assert(args.size() > 0);
2438 context& ctx = args[0u].ctx();
2439 array<Z3_ast> _args(args);
2440 Z3_ast r =
Z3_mk_add(ctx, _args.size(), _args.ptr());
2441 ctx.check_error();
2442 return expr(ctx, r);
2443 }
2444
2445 inline expr
distinct(expr_vector
const& args) {
2446 assert(args.size() > 0);
2447 context& ctx = args[0u].ctx();
2448 array<Z3_ast> _args(args);
2450 ctx.check_error();
2451 return expr(ctx, r);
2452 }
2453
2454 inline expr
concat(expr
const& a, expr
const& b) {
2456 Z3_ast r;
2458 Z3_ast _args[2] = { a, b };
2460 }
2462 Z3_ast _args[2] = { a, b };
2464 }
2465 else {
2467 }
2468 a.ctx().check_error();
2469 return expr(a.ctx(), r);
2470 }
2471
2472 inline expr
concat(expr_vector
const& args) {
2473 Z3_ast r;
2474 assert(args.size() > 0);
2475 if (args.size() == 1) {
2476 return args[0u];
2477 }
2478 context& ctx = args[0u].ctx();
2479 array<Z3_ast> _args(args);
2482 }
2485 }
2486 else {
2487 r = _args[args.size()-1];
2488 for (unsigned i = args.size()-1; i > 0; ) {
2489 --i;
2491 ctx.check_error();
2492 }
2493 }
2494 ctx.check_error();
2495 return expr(ctx, r);
2496 }
2497
2498 inline expr
mk_or(expr_vector
const& args) {
2499 array<Z3_ast> _args(args);
2500 Z3_ast r =
Z3_mk_or(args.ctx(), _args.size(), _args.ptr());
2501 args.check_error();
2502 return expr(args.ctx(), r);
2503 }
2504 inline expr
mk_and(expr_vector
const& args) {
2505 array<Z3_ast> _args(args);
2506 Z3_ast r =
Z3_mk_and(args.ctx(), _args.size(), _args.ptr());
2507 args.check_error();
2508 return expr(args.ctx(), r);
2509 }
2510 inline expr
mk_xor(expr_vector
const& args) {
2511 if (args.empty())
2513 expr r = args[0u];
2514 for (unsigned i = 1; i < args.size(); ++i)
2515 r = r ^ args[i];
2516 return r;
2517 }
2518
2519
2520 class func_entry : public object {
2521 Z3_func_entry m_entry;
2522 void init(Z3_func_entry e) {
2523 m_entry = e;
2525 }
2526 public:
2527 func_entry(context & c, Z3_func_entry e):object(c) { init(e); }
2528 func_entry(func_entry const & s):object(s) { init(s.m_entry); }
2530 operator Z3_func_entry() const { return m_entry; }
2531 func_entry & operator=(func_entry const & s) {
2534 object::operator=(s);
2535 m_entry = s.m_entry;
2536 return *this;
2537 }
2538 expr value()
const { Z3_ast r =
Z3_func_entry_get_value(ctx(), m_entry); check_error();
return expr(ctx(), r); }
2540 expr arg(
unsigned i)
const { Z3_ast r =
Z3_func_entry_get_arg(ctx(), m_entry, i); check_error();
return expr(ctx(), r); }
2541 };
2542
2543 class func_interp : public object {
2544 Z3_func_interp m_interp;
2545 void init(Z3_func_interp e) {
2546 m_interp = e;
2548 }
2549 public:
2550 func_interp(context & c, Z3_func_interp e):object(c) { init(e); }
2551 func_interp(func_interp const & s):object(s) { init(s.m_interp); }
2553 operator Z3_func_interp() const { return m_interp; }
2554 func_interp & operator=(func_interp const & s) {
2557 object::operator=(s);
2558 m_interp = s.m_interp;
2559 return *this;
2560 }
2561 expr else_value()
const { Z3_ast r =
Z3_func_interp_get_else(ctx(), m_interp); check_error();
return expr(ctx(), r); }
2563 func_entry entry(
unsigned i)
const { Z3_func_entry e =
Z3_func_interp_get_entry(ctx(), m_interp, i); check_error();
return func_entry(ctx(), e); }
2564 void add_entry(expr_vector const& args, expr& value) {
2566 check_error();
2567 }
2568 void set_else(expr& value) {
2570 check_error();
2571 }
2572 };
2573
2574 class model : public object {
2575 Z3_model m_model;
2576 void init(Z3_model m) {
2577 m_model = m;
2579 }
2580 public:
2581 struct translate {};
2582 model(context & c):object(c) { init(
Z3_mk_model(c)); }
2583 model(context & c, Z3_model m):object(c) { init(m); }
2584 model(model const & s):object(s) { init(s.m_model); }
2585 model(model& src, context& dst, translate) : object(dst) { init(
Z3_model_translate(src.ctx(), src, dst)); }
2587 operator Z3_model() const { return m_model; }
2588 model & operator=(model const & s) {
2591 object::operator=(s);
2592 m_model = s.m_model;
2593 return *this;
2594 }
2595
2596 expr eval(expr const & n, bool model_completion=false) const {
2598 Z3_ast r = 0;
2599 bool status =
Z3_model_eval(ctx(), m_model, n, model_completion, &r);
2600 check_error();
2601 if (status == false && ctx().enable_exceptions())
2602 Z3_THROW(exception(
"failed to evaluate expression"));
2603 return expr(ctx(), r);
2604 }
2605
2608 func_decl get_const_decl(
unsigned i)
const { Z3_func_decl r =
Z3_model_get_const_decl(ctx(), m_model, i); check_error();
return func_decl(ctx(), r); }
2609 func_decl get_func_decl(
unsigned i)
const { Z3_func_decl r =
Z3_model_get_func_decl(ctx(), m_model, i); check_error();
return func_decl(ctx(), r); }
2610 unsigned size() const { return num_consts() + num_funcs(); }
2611 func_decl operator[](int i) const {
2612 assert(0 <= i);
2613 return static_cast<unsigned>(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts());
2614 }
2615
2616
2617
2618
2619 expr get_const_interp(func_decl c) const {
2622 check_error();
2623 return expr(ctx(), r);
2624 }
2625 func_interp get_func_interp(func_decl f) const {
2628 check_error();
2629 return func_interp(ctx(), r);
2630 }
2631
2632
2633
2634 bool has_interp(func_decl f) const {
2637 }
2638
2639 func_interp add_func_interp(func_decl& f, expr& else_val) {
2641 check_error();
2642 return func_interp(ctx(), r);
2643 }
2644
2645 void add_const_interp(func_decl& f, expr& value) {
2647 check_error();
2648 }
2649
2650 friend std::ostream &
operator<<(std::ostream & out, model
const & m);
2651
2652 std::string to_string()
const {
return m_model ? std::string(
Z3_model_to_string(ctx(), m_model)) :
"null"; }
2653 };
2654 inline std::ostream &
operator<<(std::ostream & out, model
const & m) {
return out << m.to_string(); }
2655
2656 class stats : public object {
2657 Z3_stats m_stats;
2658 void init(Z3_stats e) {
2659 m_stats = e;
2661 }
2662 public:
2663 stats(context & c):object(c), m_stats(0) {}
2664 stats(context & c, Z3_stats e):object(c) { init(e); }
2665 stats(stats const & s):object(s) { init(s.m_stats); }
2667 operator Z3_stats() const { return m_stats; }
2668 stats & operator=(stats const & s) {
2671 object::operator=(s);
2672 m_stats = s.m_stats;
2673 return *this;
2674 }
2675 unsigned size()
const {
return Z3_stats_size(ctx(), m_stats); }
2677 bool is_uint(
unsigned i)
const {
bool r =
Z3_stats_is_uint(ctx(), m_stats, i); check_error();
return r; }
2678 bool is_double(
unsigned i)
const {
bool r =
Z3_stats_is_double(ctx(), m_stats, i); check_error();
return r; }
2679 unsigned uint_value(
unsigned i)
const {
unsigned r =
Z3_stats_get_uint_value(ctx(), m_stats, i); check_error();
return r; }
2680 double double_value(
unsigned i)
const {
double r =
Z3_stats_get_double_value(ctx(), m_stats, i); check_error();
return r; }
2681 friend std::ostream &
operator<<(std::ostream & out, stats
const & s);
2682 };
2684
2685
2686 inline std::ostream &
operator<<(std::ostream & out, check_result r) {
2687 if (r == unsat) out << "unsat";
2688 else if (r == sat) out << "sat";
2689 else out << "unknown";
2690 return out;
2691 }
2692
2703 class parameter {
2705 func_decl m_decl;
2706 unsigned m_index;
2707 context& ctx() const { return m_decl.ctx(); }
2708 void check_error() const { ctx().check_error(); }
2709 public:
2710 parameter(func_decl const& d, unsigned idx) : m_decl(d), m_index(idx) {
2711 if (ctx().enable_exceptions() && idx >= d.num_parameters())
2712 Z3_THROW(exception(
"parameter index is out of bounds"));
2714 }
2715 parameter(expr const& e, unsigned idx) : m_decl(e.decl()), m_index(idx) {
2716 if (ctx().enable_exceptions() && idx >= m_decl.num_parameters())
2717 Z3_THROW(exception(
"parameter index is out of bounds"));
2719 }
2721 expr get_expr()
const { Z3_ast a =
Z3_get_decl_ast_parameter(ctx(), m_decl, m_index); check_error();
return expr(ctx(), a); }
2722 sort get_sort()
const { Z3_sort s =
Z3_get_decl_sort_parameter(ctx(), m_decl, m_index); check_error();
return sort(ctx(), s); }
2724 symbol get_symbol()
const { Z3_symbol s =
Z3_get_decl_symbol_parameter(ctx(), m_decl, m_index); check_error();
return symbol(ctx(), s); }
2728 };
2729
2730
2731 class solver : public object {
2732 Z3_solver m_solver;
2733 void init(Z3_solver s) {
2734 m_solver = s;
2735 if (s)
2737 }
2738 public:
2739 struct simple {};
2740 struct translate {};
2741 solver(context & c):object(c) { init(
Z3_mk_solver(c)); check_error(); }
2743 solver(context & c, Z3_solver s):object(c) { init(s); }
2744 solver(context & c,
char const * logic):object(c) { init(
Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }
2745 solver(context & c, solver
const& src, translate): object(c) { Z3_solver s =
Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }
2746 solver(solver const & s):object(s) { init(s.m_solver); }
2747 solver(solver const& s, simplifier const& simp);
2749 operator Z3_solver() const { return m_solver; }
2750 solver & operator=(solver const & s) {
2753 object::operator=(s);
2754 m_solver = s.m_solver;
2755 return *this;
2756 }
2758 void set(char const * k, bool v) { params p(ctx()); p.set(k, v); set(p); }
2759 void set(char const * k, unsigned v) { params p(ctx()); p.set(k, v); set(p); }
2760 void set(char const * k, double v) { params p(ctx()); p.set(k, v); set(p); }
2761 void set(char const * k, symbol const & v) { params p(ctx()); p.set(k, v); set(p); }
2762 void set(char const * k, char const* v) { params p(ctx()); p.set(k, v); set(p); }
2774 void pop(
unsigned n = 1) {
Z3_solver_pop(ctx(), m_solver, n); check_error(); }
2776 void add(expr
const & e) { assert(e.is_bool());
Z3_solver_assert(ctx(), m_solver, e); check_error(); }
2777 void add(expr const & e, expr const & p) {
2778 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2780 check_error();
2781 }
2782 void add(expr const & e, char const * p) {
2783 add(e, ctx().bool_const(p));
2784 }
2785 void add(expr_vector const& v) {
2787 for (unsigned i = 0; i < v.size(); ++i)
2788 add(v[i]);
2789 }
2790 void from_file(
char const* file) {
Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
2791 void from_string(
char const* s) {
Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
2792
2794 check_result check(
unsigned n, expr *
const assumptions) {
2795 array<Z3_ast> _assumptions(n);
2796 for (unsigned i = 0; i < n; i++) {
2798 _assumptions[i] = assumptions[i];
2799 }
2801 check_error();
2803 }
2805 unsigned n = assumptions.size();
2806 array<Z3_ast> _assumptions(n);
2807 for (unsigned i = 0; i < n; i++) {
2809 _assumptions[i] = assumptions[i];
2810 }
2812 check_error();
2814 }
2815 model get_model()
const { Z3_model m =
Z3_solver_get_model(ctx(), m_solver); check_error();
return model(ctx(), m); }
2816 check_result consequences(expr_vector& assumptions, expr_vector& vars, expr_vector& conseq) {
2818 check_error();
2820 }
2822 stats statistics()
const { Z3_stats r =
Z3_solver_get_statistics(ctx(), m_solver); check_error();
return stats(ctx(), r); }
2828 expr_vector trail(array<unsigned>& levels)
const {
2830 check_error();
2832 unsigned sz = result.size();
2833 levels.resize(sz);
2835 check_error();
2836 return result;
2837 }
2838 expr proof()
const { Z3_ast r =
Z3_solver_get_proof(ctx(), m_solver); check_error();
return expr(ctx(), r); }
2839 friend std::ostream &
operator<<(std::ostream & out, solver
const & s);
2840
2841 std::string to_smt2(char const* status = "unknown") {
2842 array<Z3_ast> es(assertions());
2843 Z3_ast const* fmls = es.ptr();
2844 Z3_ast fml = 0;
2845 unsigned sz = es.size();
2846 if (sz > 0) {
2847 --sz;
2848 fml = fmls[sz];
2849 }
2850 else {
2851 fml = ctx().bool_val(true);
2852 }
2854 ctx(),
2855 "", "", status, "",
2856 sz,
2857 fmls,
2858 fml));
2859 }
2860
2861 std::string dimacs(
bool include_names =
true)
const {
return std::string(
Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
2862
2864
2865
2866 expr_vector cube(expr_vector& vars,
unsigned cutoff) {
2868 check_error();
2870 }
2871
2872 class cube_iterator {
2873 solver& m_solver;
2874 unsigned& m_cutoff;
2877 bool m_end;
2878 bool m_empty;
2879
2880 void inc() {
2881 assert(!m_end && !m_empty);
2882 m_cube = m_solver.cube(m_vars, m_cutoff);
2883 m_cutoff = 0xFFFFFFFF;
2884 if (m_cube.size() == 1 && m_cube[0u].is_false()) {
2886 m_end = true;
2887 }
2888 else if (m_cube.empty()) {
2889 m_empty = true;
2890 }
2891 }
2892 public:
2893 cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
2894 m_solver(s),
2895 m_cutoff(cutoff),
2896 m_vars(vars),
2897 m_cube(s.ctx()),
2898 m_end(end),
2899 m_empty(false) {
2900 if (!m_end) {
2901 inc();
2902 }
2903 }
2904
2905 cube_iterator& operator++() {
2906 assert(!m_end);
2907 if (m_empty) {
2908 m_end = true;
2909 }
2910 else {
2911 inc();
2912 }
2913 return *this;
2914 }
2915 cube_iterator operator++(int) { assert(false); return *this; }
2918
2919 bool operator==(cube_iterator
const& other)
noexcept {
2920 return other.m_end == m_end;
2921 };
2922 bool operator!=(cube_iterator
const& other)
noexcept {
2923 return other.m_end != m_end;
2924 };
2925
2926 };
2927
2928 class cube_generator {
2929 solver& m_solver;
2930 unsigned m_cutoff;
2933 public:
2934 cube_generator(solver& s):
2935 m_solver(s),
2936 m_cutoff(0xFFFFFFFF),
2937 m_default_vars(s.ctx()),
2938 m_vars(m_default_vars)
2939 {}
2940
2941 cube_generator(solver& s, expr_vector& vars):
2942 m_solver(s),
2943 m_cutoff(0xFFFFFFFF),
2944 m_default_vars(s.ctx()),
2945 m_vars(vars)
2946 {}
2947
2948 cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
2949 cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
2950 void set_cutoff(unsigned c) noexcept { m_cutoff = c; }
2951 };
2952
2953 cube_generator cubes() { return cube_generator(*this); }
2954 cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
2955
2956 };
2958
2959 class goal : public object {
2960 Z3_goal m_goal;
2961 void init(Z3_goal s) {
2962 m_goal = s;
2964 }
2965 public:
2966 goal(context & c,
bool models=
true,
bool unsat_cores=
false,
bool proofs=
false):object(c) { init(
Z3_mk_goal(c, models, unsat_cores, proofs)); }
2967 goal(context & c, Z3_goal s):object(c) { init(s); }
2968 goal(goal const & s):object(s) { init(s.m_goal); }
2970 operator Z3_goal() const { return m_goal; }
2971 goal & operator=(goal const & s) {
2974 object::operator=(s);
2975 m_goal = s.m_goal;
2976 return *this;
2977 }
2979 void add(expr_vector
const& v) {
check_context(*
this, v);
for (
unsigned i = 0; i < v.size(); ++i) add(v[i]); }
2980 unsigned size()
const {
return Z3_goal_size(ctx(), m_goal); }
2981 expr operator[](
int i)
const { assert(0 <= i); Z3_ast r =
Z3_goal_formula(ctx(), m_goal, i); check_error();
return expr(ctx(), r); }
2984 unsigned depth()
const {
return Z3_goal_depth(ctx(), m_goal); }
2989 model convert_model(model const & m) const {
2992 check_error();
2993 return model(ctx(), new_m);
2994 }
2995 model get_model() const {
2997 check_error();
2998 return model(ctx(), new_m);
2999 }
3000 expr as_expr() const {
3001 unsigned n = size();
3002 if (n == 0)
3003 return ctx().bool_val(true);
3004 else if (n == 1)
3005 return operator[](0u);
3006 else {
3007 array<Z3_ast> args(n);
3008 for (unsigned i = 0; i < n; i++)
3009 args[i] = operator[](i);
3010 return expr(ctx(),
Z3_mk_and(ctx(), n, args.ptr()));
3011 }
3012 }
3013 std::string dimacs(
bool include_names =
true)
const {
return std::string(
Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }
3014 friend std::ostream &
operator<<(std::ostream & out, goal
const & g);
3015 };
3017
3018 class apply_result : public object {
3019 Z3_apply_result m_apply_result;
3020 void init(Z3_apply_result s) {
3021 m_apply_result = s;
3023 }
3024 public:
3025 apply_result(context & c, Z3_apply_result s):object(c) { init(s); }
3026 apply_result(apply_result const & s):object(s) { init(s.m_apply_result); }
3028 operator Z3_apply_result() const { return m_apply_result; }
3029 apply_result & operator=(apply_result const & s) {
3032 object::operator=(s);
3033 m_apply_result = s.m_apply_result;
3034 return *this;
3035 }
3037 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); }
3038 friend std::ostream &
operator<<(std::ostream & out, apply_result
const & r);
3039 };
3041
3042 class tactic : public object {
3043 Z3_tactic m_tactic;
3044 void init(Z3_tactic s) {
3045 m_tactic = s;
3047 }
3048 public:
3049 tactic(context & c,
char const * name):object(c) { Z3_tactic r =
Z3_mk_tactic(c, name); check_error(); init(r); }
3050 tactic(context & c, Z3_tactic s):object(c) { init(s); }
3051 tactic(tactic const & s):object(s) { init(s.m_tactic); }
3053 operator Z3_tactic() const { return m_tactic; }
3054 tactic & operator=(tactic const & s) {
3057 object::operator=(s);
3058 m_tactic = s.m_tactic;
3059 return *this;
3060 }
3061 solver mk_solver()
const { Z3_solver r =
Z3_mk_solver_from_tactic(ctx(), m_tactic); check_error();
return solver(ctx(), r); }
3062 apply_result apply(goal const & g) const {
3065 check_error();
3066 return apply_result(ctx(), r);
3067 }
3068 apply_result operator()(goal const & g) const {
3069 return apply(g);
3070 }
3071 std::string help()
const {
char const * r =
Z3_tactic_get_help(ctx(), m_tactic); check_error();
return r; }
3072 friend tactic
operator&(tactic
const & t1, tactic
const & t2);
3073 friend tactic
operator|(tactic
const & t1, tactic
const & t2);
3074 friend tactic
repeat(tactic
const & t,
unsigned max);
3075 friend tactic
with(tactic
const & t, params
const & p);
3076 friend tactic
try_for(tactic
const & t,
unsigned ms);
3077 friend tactic
par_or(
unsigned n, tactic
const* tactics);
3078 friend tactic
par_and_then(tactic
const& t1, tactic
const& t2);
3080 };
3081
3082 inline tactic
operator&(tactic
const & t1, tactic
const & t2) {
3085 t1.check_error();
3086 return tactic(t1.ctx(), r);
3087 }
3088
3089 inline tactic
operator|(tactic
const & t1, tactic
const & t2) {
3092 t1.check_error();
3093 return tactic(t1.ctx(), r);
3094 }
3095
3096 inline tactic
repeat(tactic
const & t,
unsigned max=UINT_MAX) {
3098 t.check_error();
3099 return tactic(t.ctx(), r);
3100 }
3101
3102 inline tactic
with(tactic
const & t, params
const & p) {
3104 t.check_error();
3105 return tactic(t.ctx(), r);
3106 }
3107 inline tactic
try_for(tactic
const & t,
unsigned ms) {
3109 t.check_error();
3110 return tactic(t.ctx(), r);
3111 }
3112 inline tactic
par_or(
unsigned n, tactic
const* tactics) {
3113 if (n == 0) {
3114 Z3_THROW(exception(
"a non-zero number of tactics need to be passed to par_or"));
3115 }
3116 array<Z3_tactic> buffer(n);
3117 for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
3118 return tactic(tactics[0u].ctx(),
Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
3119 }
3120
3121 inline tactic
par_and_then(tactic
const & t1, tactic
const & t2) {
3124 t1.check_error();
3125 return tactic(t1.ctx(), r);
3126 }
3127
3128 class simplifier : public object {
3129 Z3_simplifier m_simplifier;
3130 void init(Z3_simplifier s) {
3131 m_simplifier = s;
3133 }
3134 public:
3135 simplifier(context & c,
char const * name):object(c) { Z3_simplifier r =
Z3_mk_simplifier(c, name); check_error(); init(r); }
3136 simplifier(context & c, Z3_simplifier s):object(c) { init(s); }
3137 simplifier(simplifier const & s):object(s) { init(s.m_simplifier); }
3139 operator Z3_simplifier() const { return m_simplifier; }
3140 simplifier & operator=(simplifier const & s) {
3143 object::operator=(s);
3144 m_simplifier = s.m_simplifier;
3145 return *this;
3146 }
3147 std::string help()
const {
char const * r =
Z3_simplifier_get_help(ctx(), m_simplifier); check_error();
return r; }
3148 friend simplifier
operator&(simplifier
const & t1, simplifier
const & t2);
3149 friend simplifier
with(simplifier
const & t, params
const & p);
3151 };
3152
3153 inline solver::solver(solver
const& s, simplifier
const& simp):object(s) { init(
Z3_solver_add_simplifier(s.ctx(), s, simp)); }
3154
3155
3156 inline simplifier
operator&(simplifier
const & t1, simplifier
const & t2) {
3159 t1.check_error();
3160 return simplifier(t1.ctx(), r);
3161 }
3162
3163 inline simplifier
with(simplifier
const & t, params
const & p) {
3165 t.check_error();
3166 return simplifier(t.ctx(), r);
3167 }
3168
3169 class probe : public object {
3170 Z3_probe m_probe;
3171 void init(Z3_probe s) {
3172 m_probe = s;
3174 }
3175 public:
3176 probe(context & c,
char const * name):object(c) { Z3_probe r =
Z3_mk_probe(c, name); check_error(); init(r); }
3177 probe(context & c,
double val):object(c) { Z3_probe r =
Z3_probe_const(c, val); check_error(); init(r); }
3178 probe(context & c, Z3_probe s):object(c) { init(s); }
3179 probe(probe const & s):object(s) { init(s.m_probe); }
3181 operator Z3_probe() const { return m_probe; }
3182 probe & operator=(probe const & s) {
3185 object::operator=(s);
3186 m_probe = s.m_probe;
3187 return *this;
3188 }
3189 double apply(goal
const & g)
const {
double r =
Z3_probe_apply(ctx(), m_probe, g); check_error();
return r; }
3190 double operator()(goal const & g) const { return apply(g); }
3191 friend probe
operator<=(probe
const & p1, probe
const & p2);
3192 friend probe
operator<=(probe
const & p1,
double p2);
3193 friend probe
operator<=(
double p1, probe
const & p2);
3194 friend probe
operator>=(probe
const & p1, probe
const & p2);
3195 friend probe
operator>=(probe
const & p1,
double p2);
3196 friend probe
operator>=(
double p1, probe
const & p2);
3197 friend probe
operator<(probe
const & p1, probe
const & p2);
3198 friend probe
operator<(probe
const & p1,
double p2);
3199 friend probe
operator<(
double p1, probe
const & p2);
3200 friend probe
operator>(probe
const & p1, probe
const & p2);
3201 friend probe
operator>(probe
const & p1,
double p2);
3202 friend probe
operator>(
double p1, probe
const & p2);
3203 friend probe
operator==(probe
const & p1, probe
const & p2);
3204 friend probe
operator==(probe
const & p1,
double p2);
3205 friend probe
operator==(
double p1, probe
const & p2);
3206 friend probe
operator&&(probe
const & p1, probe
const & p2);
3207 friend probe
operator||(probe
const & p1, probe
const & p2);
3208 friend probe
operator!(probe
const & p);
3209 };
3210
3211 inline probe
operator<=(probe
const & p1, probe
const & p2) {
3213 }
3214 inline probe
operator<=(probe
const & p1,
double p2) {
return p1 <= probe(p1.ctx(), p2); }
3215 inline probe
operator<=(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) <= p2; }
3216 inline probe
operator>=(probe
const & p1, probe
const & p2) {
3218 }
3219 inline probe
operator>=(probe
const & p1,
double p2) {
return p1 >= probe(p1.ctx(), p2); }
3220 inline probe
operator>=(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) >= p2; }
3221 inline probe
operator<(probe
const & p1, probe
const & p2) {
3223 }
3224 inline probe
operator<(probe
const & p1,
double p2) {
return p1 < probe(p1.ctx(), p2); }
3225 inline probe
operator<(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) < p2; }
3226 inline probe
operator>(probe
const & p1, probe
const & p2) {
3228 }
3229 inline probe
operator>(probe
const & p1,
double p2) {
return p1 > probe(p1.ctx(), p2); }
3230 inline probe
operator>(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) > p2; }
3231 inline probe
operator==(probe
const & p1, probe
const & p2) {
3233 }
3234 inline probe
operator==(probe
const & p1,
double p2) {
return p1 == probe(p1.ctx(), p2); }
3235 inline probe
operator==(
double p1, probe
const & p2) {
return probe(p2.ctx(), p1) == p2; }
3236 inline probe
operator&&(probe
const & p1, probe
const & p2) {
3238 }
3239 inline probe
operator||(probe
const & p1, probe
const & p2) {
3241 }
3242 inline probe
operator!(probe
const & p) {
3243 Z3_probe r =
Z3_probe_not(p.ctx(), p); p.check_error();
return probe(p.ctx(), r);
3244 }
3245
3246 class optimize : public object {
3247 Z3_optimize m_opt;
3248
3249 public:
3250 class handle final {
3251 unsigned m_h;
3252 public:
3253 handle(unsigned h): m_h(h) {}
3254 unsigned h() const { return m_h; }
3255 };
3257 optimize(optimize const & o):object(o), m_opt(o.m_opt) {
3259 }
3260 optimize(context& c, optimize& src):object(c) {
3265 for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it);
3266 }
3267 optimize& operator=(optimize const& o) {
3270 m_opt = o.m_opt;
3271 object::operator=(o);
3272 return *this;
3273 }
3275 operator Z3_optimize() const { return m_opt; }
3276 void add(expr const& e) {
3277 assert(e.is_bool());
3279 }
3280 void add(expr_vector const& es) {
3281 for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it);
3282 }
3283 void add(expr const& e, expr const& t) {
3284 assert(e.is_bool());
3286 }
3287 void add(expr const& e, char const* p) {
3288 assert(e.is_bool());
3289 add(e, ctx().bool_const(p));
3290 }
3291 handle add_soft(expr const& e, unsigned weight) {
3292 assert(e.is_bool());
3293 auto str = std::to_string(weight);
3295 }
3296 handle add_soft(expr const& e, char const* weight) {
3297 assert(e.is_bool());
3299 }
3300 handle add(expr const& e, unsigned weight) {
3301 return add_soft(e, weight);
3302 }
3303 handle maximize(expr const& e) {
3305 }
3306 handle minimize(expr const& e) {
3308 }
3309 void push() {
3311 }
3312 void pop() {
3314 }
3317 unsigned n = asms.size();
3318 array<Z3_ast> _asms(n);
3319 for (unsigned i = 0; i < n; i++) {
3321 _asms[i] = asms[i];
3322 }
3324 check_error();
3326 }
3327 model get_model()
const { Z3_model m =
Z3_optimize_get_model(ctx(), m_opt); check_error();
return model(ctx(), m); }
3330 expr lower(handle const& h) {
3332 check_error();
3333 return expr(ctx(), r);
3334 }
3335 expr upper(handle const& h) {
3337 check_error();
3338 return expr(ctx(), r);
3339 }
3343 friend std::ostream &
operator<<(std::ostream & out, optimize
const & s);
3344 void from_file(
char const* filename) {
Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); }
3345 void from_string(
char const* constraints) {
Z3_optimize_from_string(ctx(), m_opt, constraints); check_error(); }
3346 std::string help()
const {
char const * r =
Z3_optimize_get_help(ctx(), m_opt); check_error();
return r; }
3347 };
3349
3350 class fixedpoint : public object {
3351 Z3_fixedpoint m_fp;
3352 public:
3356 fixedpoint & operator=(fixedpoint const & o) {
3359 m_fp = o.m_fp;
3360 object::operator=(o);
3361 return *this;
3362 }
3363 operator Z3_fixedpoint() const { return m_fp; }
3366 check_error();
3368 }
3371 check_error();
3373 }
3374 void add_rule(expr& rule, symbol
const& name) {
Z3_fixedpoint_add_rule(ctx(), m_fp, rule, name); check_error(); }
3375 void add_fact(func_decl& f,
unsigned * args) {
Z3_fixedpoint_add_fact(ctx(), m_fp, f, f.arity(), args); check_error(); }
3378 array<Z3_func_decl> rs(relations);
3380 check_error();
3382 }
3387 expr get_cover_delta(int level, func_decl& p) {
3389 check_error();
3390 return expr(ctx(), r);
3391 }
3392 void add_cover(
int level, func_decl& p, expr& property) {
Z3_fixedpoint_add_cover(ctx(), m_fp, level, p, property); check_error(); }
3401 std::string to_string(expr_vector const& queries) {
3402 array<Z3_ast> qs(queries);
3404 }
3405 };
3407
3408 inline tactic
fail_if(probe
const & p) {
3410 p.check_error();
3411 return tactic(p.ctx(), r);
3412 }
3413 inline tactic
when(probe
const & p, tactic
const & t) {
3416 t.check_error();
3417 return tactic(t.ctx(), r);
3418 }
3419 inline tactic
cond(probe
const & p, tactic
const & t1, tactic
const & t2) {
3422 t1.check_error();
3423 return tactic(t1.ctx(), r);
3424 }
3425
3426 inline symbol context::str_symbol(
char const * s) { Z3_symbol r =
Z3_mk_string_symbol(m_ctx, s); check_error();
return symbol(*
this, r); }
3427 inline symbol context::int_symbol(
int n) { Z3_symbol r =
Z3_mk_int_symbol(m_ctx, n); check_error();
return symbol(*
this, r); }
3428
3429 inline sort context::bool_sort() { Z3_sort s =
Z3_mk_bool_sort(m_ctx); check_error();
return sort(*
this, s); }
3430 inline sort context::int_sort() { Z3_sort s =
Z3_mk_int_sort(m_ctx); check_error();
return sort(*
this, s); }
3431 inline sort context::real_sort() { Z3_sort s =
Z3_mk_real_sort(m_ctx); check_error();
return sort(*
this, s); }
3432 inline sort context::bv_sort(
unsigned sz) { Z3_sort s =
Z3_mk_bv_sort(m_ctx, sz); check_error();
return sort(*
this, s); }
3433 inline sort context::string_sort() { Z3_sort s =
Z3_mk_string_sort(m_ctx); check_error();
return sort(*
this, s); }
3434 inline sort context::char_sort() { Z3_sort s =
Z3_mk_char_sort(m_ctx); check_error();
return sort(*
this, s); }
3435 inline sort context::seq_sort(sort& s) { Z3_sort r =
Z3_mk_seq_sort(m_ctx, s); check_error();
return sort(*
this, r); }
3436 inline sort context::re_sort(sort& s) { Z3_sort r =
Z3_mk_re_sort(m_ctx, s); check_error();
return sort(*
this, r); }
3437 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); }
3438
3439 template<>
3440 inline sort context::fpa_sort<16>() { return fpa_sort(5, 11); }
3441
3442 template<>
3443 inline sort context::fpa_sort<32>() { return fpa_sort(8, 24); }
3444
3445 template<>
3446 inline sort context::fpa_sort<64>() { return fpa_sort(11, 53); }
3447
3448 template<>
3449 inline sort context::fpa_sort<128>() { return fpa_sort(15, 113); }
3450
3451 inline sort context::fpa_rounding_mode_sort() { Z3_sort r =
Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error();
return sort(*
this, r); }
3452
3453 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); }
3454 inline sort context::array_sort(sort_vector const& d, sort r) {
3455 array<Z3_sort> dom(d);
3456 Z3_sort s =
Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error();
return sort(*
this, s);
3457 }
3458 inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
3459 array<Z3_symbol> _enum_names(n);
3460 for (
unsigned i = 0; i < n; i++) { _enum_names[i] =
Z3_mk_string_symbol(*
this, enum_names[i]); }
3461 array<Z3_func_decl> _cs(n);
3462 array<Z3_func_decl> _ts(n);
3465 check_error();
3466 for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
3467 return s;
3468 }
3469 inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
3470 array<Z3_symbol> _names(n);
3471 array<Z3_sort> _sorts(n);
3472 for (
unsigned i = 0; i < n; i++) { _names[i] =
Z3_mk_string_symbol(*
this, names[i]); _sorts[i] = sorts[i]; }
3473 array<Z3_func_decl> _projs(n);
3475 Z3_func_decl tuple;
3476 sort _ignore_s =
to_sort(*
this,
Z3_mk_tuple_sort(*
this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
3477 check_error();
3478 for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
3479 return func_decl(*this, tuple);
3480 }
3481
3482 class constructor_list {
3483 context& ctx;
3484 Z3_constructor_list clist;
3485 public:
3486 constructor_list(constructors const& cs);
3488 operator Z3_constructor_list() const { return clist; }
3489 };
3490
3491 class constructors {
3492 friend class constructor_list;
3493 context& ctx;
3494 std::vector<Z3_constructor> cons;
3495 std::vector<unsigned> num_fields;
3496 public:
3497 constructors(context& ctx): ctx(ctx) {}
3498
3499 ~constructors() {
3500 for (auto con : cons)
3502 }
3503
3504 void add(symbol const& name, symbol const& rec, unsigned n, symbol const* names, sort const* fields) {
3505 array<unsigned> sort_refs(n);
3506 array<Z3_sort> sorts(n);
3507 array<Z3_symbol> _names(n);
3508 for (unsigned i = 0; i < n; ++i) sorts[i] = fields[i], _names[i] = names[i];
3509 cons.push_back(
Z3_mk_constructor(ctx, name, rec, n, _names.ptr(), sorts.ptr(), sort_refs.ptr()));
3510 num_fields.push_back(n);
3511 }
3512
3513 Z3_constructor operator[](unsigned i) const { return cons[i]; }
3514
3515 unsigned size() const { return (unsigned)cons.size(); }
3516
3517 void query(unsigned i, func_decl& constructor, func_decl& test, func_decl_vector& accs) {
3518 Z3_func_decl _constructor;
3519 Z3_func_decl _test;
3520 array<Z3_func_decl> accessors(num_fields[i]);
3521 accs.resize(0);
3523 cons[i],
3524 num_fields[i],
3525 &_constructor,
3526 &_test,
3527 accessors.ptr());
3528 constructor = func_decl(ctx, _constructor);
3529
3530 test = func_decl(ctx, _test);
3531 for (unsigned j = 0; j < num_fields[i]; ++j)
3532 accs.push_back(func_decl(ctx, accessors[j]));
3533 }
3534 };
3535
3536 inline constructor_list::constructor_list(constructors const& cs): ctx(cs.ctx) {
3537 array<Z3_constructor> cons(cs.size());
3538 for (unsigned i = 0; i < cs.size(); ++i)
3539 cons[i] = cs[i];
3541 }
3542
3543 inline sort context::datatype(symbol const& name, constructors const& cs) {
3544 array<Z3_constructor> _cs(cs.size());
3545 for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
3547 check_error();
3548 return sort(*this, s);
3549 }
3550
3552 unsigned n, symbol const* names,
3553 constructor_list *const* cons) {
3555 array<Z3_symbol> _names(n);
3556 array<Z3_sort> _sorts(n);
3557 array<Z3_constructor_list> _cons(n);
3558 for (unsigned i = 0; i < n; ++i)
3559 _names[i] = names[i], _cons[i] = *cons[i];
3561 for (unsigned i = 0; i < n; ++i)
3562 result.push_back(sort(*this, _sorts[i]));
3563 return result;
3564 }
3565
3566
3567 inline sort context::datatype_sort(symbol const& name) {
3569 check_error();
3570 return sort(*this, s);
3571 }
3572
3573
3574 inline sort context::uninterpreted_sort(char const* name) {
3577 }
3578 inline sort context::uninterpreted_sort(symbol const& name) {
3580 }
3581
3582 inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3583 array<Z3_sort> args(arity);
3584 for (unsigned i = 0; i < arity; i++) {
3586 args[i] = domain[i];
3587 }
3588 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
3589 check_error();
3590 return func_decl(*this, f);
3591 }
3592
3593 inline func_decl context::function(char const * name, unsigned arity, sort const * domain, sort const & range) {
3595 }
3596
3597 inline func_decl context::function(symbol const& name, sort_vector const& domain, sort const& range) {
3598 array<Z3_sort> args(domain.size());
3599 for (unsigned i = 0; i < domain.size(); i++) {
3601 args[i] = domain[i];
3602 }
3603 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
3604 check_error();
3605 return func_decl(*this, f);
3606 }
3607
3608 inline func_decl context::function(char const * name, sort_vector const& domain, sort const& range) {
3610 }
3611
3612
3613 inline func_decl context::function(char const * name, sort const & domain, sort const & range) {
3615 Z3_sort args[1] = { domain };
3616 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
3617 check_error();
3618 return func_decl(*this, f);
3619 }
3620
3621 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & range) {
3623 Z3_sort args[2] = { d1, d2 };
3624 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
3625 check_error();
3626 return func_decl(*this, f);
3627 }
3628
3629 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & range) {
3631 Z3_sort args[3] = { d1, d2, d3 };
3632 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
3633 check_error();
3634 return func_decl(*this, f);
3635 }
3636
3637 inline func_decl context::function(char const * name, sort const & d1, sort const & d2, sort const & d3, sort const & d4, sort const & range) {
3639 Z3_sort args[4] = { d1, d2, d3, d4 };
3640 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
3641 check_error();
3642 return func_decl(*this, f);
3643 }
3644
3645 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) {
3647 Z3_sort args[5] = { d1, d2, d3, d4, d5 };
3648 Z3_func_decl f =
Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
3649 check_error();
3650 return func_decl(*this, f);
3651 }
3652
3653 inline func_decl context::recfun(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
3654 array<Z3_sort> args(arity);
3655 for (unsigned i = 0; i < arity; i++) {
3657 args[i] = domain[i];
3658 }
3660 check_error();
3661 return func_decl(*this, f);
3662
3663 }
3664
3665 inline func_decl context::recfun(symbol const & name, sort_vector const& domain, sort const & range) {
3667 array<Z3_sort> domain1(domain);
3669 check_error();
3670 return func_decl(*this, f);
3671 }
3672
3673 inline func_decl context::recfun(char const * name, sort_vector const& domain, sort const & range) {
3674 return recfun(str_symbol(name), domain, range);
3675
3676 }
3677
3678 inline func_decl context::recfun(char const * name, unsigned arity, sort const * domain, sort const & range) {
3679 return recfun(str_symbol(name), arity, domain, range);
3680 }
3681
3682 inline func_decl context::recfun(char const * name, sort const& d1, sort const & range) {
3683 return recfun(str_symbol(name), 1, &d1, range);
3684 }
3685
3686 inline func_decl context::recfun(char const * name, sort const& d1, sort const& d2, sort const & range) {
3687 sort dom[2] = { d1, d2 };
3688 return recfun(str_symbol(name), 2, dom, range);
3689 }
3690
3691 inline void context::recdef(func_decl f, expr_vector const& args, expr const& body) {
3693 array<Z3_ast> vars(args);
3695 }
3696
3697 inline func_decl context::user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range) {
3699 array<Z3_sort> domain1(domain);
3701 check_error();
3702 return func_decl(*this, f);
3703 }
3704
3705 inline expr context::constant(symbol const & name, sort const & s) {
3707 check_error();
3708 return expr(*this, r);
3709 }
3710 inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
3711 inline expr context::variable(unsigned idx, sort const& s) {
3713 check_error();
3714 return expr(*this, r);
3715 }
3716 inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
3717 inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
3718 inline expr context::real_const(char const * name) { return constant(name, real_sort()); }
3719 inline expr context::string_const(char const * name) { return constant(name, string_sort()); }
3720 inline expr context::bv_const(char const * name, unsigned sz) { return constant(name, bv_sort(sz)); }
3721 inline expr context::fpa_const(char const * name, unsigned ebits, unsigned sbits) { return constant(name, fpa_sort(ebits, sbits)); }
3722
3723 template<size_t precision>
3724 inline expr context::fpa_const(char const * name) { return constant(name, fpa_sort<precision>()); }
3725
3726 inline void context::set_rounding_mode(rounding_mode rm) { m_rounding_mode = rm; }
3727
3728 inline expr context::fpa_rounding_mode() {
3729 switch (m_rounding_mode) {
3735 default: return expr(*this);
3736 }
3737 }
3738
3739 inline expr context::bool_val(
bool b) {
return b ? expr(*
this,
Z3_mk_true(m_ctx)) : expr(*this,
Z3_mk_false(m_ctx)); }
3740
3741 inline expr context::int_val(
int n) { Z3_ast r =
Z3_mk_int(m_ctx, n, int_sort()); check_error();
return expr(*
this, r); }
3742 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); }
3743 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); }
3744 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); }
3745 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); }
3746
3747 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); }
3748 inline expr context::real_val(
int n) { Z3_ast r =
Z3_mk_int(m_ctx, n, real_sort()); check_error();
return expr(*
this, r); }
3749 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); }
3750 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); }
3751 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); }
3752 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); }
3753
3754 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); }
3755 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); }
3756 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); }
3757 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); }
3758 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); }
3759 inline expr context::bv_val(unsigned n, bool const* bits) {
3760 array<bool> _bits(n);
3761 for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
3762 Z3_ast r =
Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error();
return expr(*
this, r);
3763 }
3764
3765 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); }
3766 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); }
3767 inline expr context::fpa_nan(sort
const & s) { Z3_ast r =
Z3_mk_fpa_nan(m_ctx, s); check_error();
return expr(*
this, r); }
3768 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); }
3769
3770 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); }
3771 inline expr context::string_val(
char const* s) { Z3_ast r =
Z3_mk_string(m_ctx, s); check_error();
return expr(*
this, r); }
3772 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); }
3773 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); }
3774
3775 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); }
3776
3777 inline expr func_decl::operator()(unsigned n, expr const * args) const {
3778 array<Z3_ast> _args(n);
3779 for (unsigned i = 0; i < n; i++) {
3781 _args[i] = args[i];
3782 }
3783 Z3_ast r =
Z3_mk_app(ctx(), *
this, n, _args.ptr());
3784 check_error();
3785 return expr(ctx(), r);
3786
3787 }
3788 inline expr func_decl::operator()(expr_vector const& args) const {
3789 array<Z3_ast> _args(args.size());
3790 for (unsigned i = 0; i < args.size(); i++) {
3792 _args[i] = args[i];
3793 }
3794 Z3_ast r =
Z3_mk_app(ctx(), *
this, args.size(), _args.ptr());
3795 check_error();
3796 return expr(ctx(), r);
3797 }
3798 inline expr func_decl::operator()() const {
3799 Z3_ast r =
Z3_mk_app(ctx(), *
this, 0, 0);
3800 ctx().check_error();
3801 return expr(ctx(), r);
3802 }
3803 inline expr func_decl::operator()(expr const & a) const {
3805 Z3_ast args[1] = { a };
3806 Z3_ast r =
Z3_mk_app(ctx(), *
this, 1, args);
3807 ctx().check_error();
3808 return expr(ctx(), r);
3809 }
3810 inline expr func_decl::operator()(int a) const {
3811 Z3_ast args[1] = { ctx().num_val(a, domain(0)) };
3812 Z3_ast r =
Z3_mk_app(ctx(), *
this, 1, args);
3813 ctx().check_error();
3814 return expr(ctx(), r);
3815 }
3816 inline expr func_decl::operator()(expr const & a1, expr const & a2) const {
3818 Z3_ast args[2] = { a1, a2 };
3819 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
3820 ctx().check_error();
3821 return expr(ctx(), r);
3822 }
3823 inline expr func_decl::operator()(expr const & a1, int a2) const {
3825 Z3_ast args[2] = { a1, ctx().num_val(a2, domain(1)) };
3826 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
3827 ctx().check_error();
3828 return expr(ctx(), r);
3829 }
3830 inline expr func_decl::operator()(int a1, expr const & a2) const {
3832 Z3_ast args[2] = { ctx().num_val(a1, domain(0)), a2 };
3833 Z3_ast r =
Z3_mk_app(ctx(), *
this, 2, args);
3834 ctx().check_error();
3835 return expr(ctx(), r);
3836 }
3837 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3) const {
3839 Z3_ast args[3] = { a1, a2, a3 };
3840 Z3_ast r =
Z3_mk_app(ctx(), *
this, 3, args);
3841 ctx().check_error();
3842 return expr(ctx(), r);
3843 }
3844 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const {
3846 Z3_ast args[4] = { a1, a2, a3, a4 };
3847 Z3_ast r =
Z3_mk_app(ctx(), *
this, 4, args);
3848 ctx().check_error();
3849 return expr(ctx(), r);
3850 }
3851 inline expr func_decl::operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const {
3853 Z3_ast args[5] = { a1, a2, a3, a4, a5 };
3854 Z3_ast r =
Z3_mk_app(ctx(), *
this, 5, args);
3855 ctx().check_error();
3856 return expr(ctx(), r);
3857 }
3858
3859 inline expr
to_real(expr
const & a) { Z3_ast r =
Z3_mk_int2real(a.ctx(), a); a.check_error();
return expr(a.ctx(), r); }
3860
3861 inline func_decl
function(symbol
const & name,
unsigned arity, sort
const * domain, sort
const &
range) {
3863 }
3864 inline func_decl
function(
char const * name,
unsigned arity, sort
const * domain, sort
const &
range) {
3866 }
3867 inline func_decl
function(
char const * name, sort
const & domain, sort
const &
range) {
3869 }
3870 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const &
range) {
3872 }
3873 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const & d3, sort
const &
range) {
3875 }
3876 inline func_decl
function(
char const * name, sort
const & d1, sort
const & d2, sort
const & d3, sort
const & d4, sort
const &
range) {
3878 }
3879 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) {
3881 }
3882 inline func_decl
function(
char const* name,
sort_vector const& domain, sort
const&
range) {
3884 }
3885 inline func_decl
function(std::string
const& name,
sort_vector const& domain, sort
const&
range) {
3887 }
3888
3889 inline func_decl
recfun(symbol
const & name,
unsigned arity, sort
const * domain, sort
const & range) {
3891 }
3892 inline func_decl
recfun(
char const * name,
unsigned arity, sort
const * domain, sort
const & range) {
3894 }
3895 inline func_decl
recfun(
char const * name, sort
const& d1, sort
const & range) {
3897 }
3898 inline func_decl
recfun(
char const * name, sort
const& d1, sort
const& d2, sort
const & range) {
3900 }
3901
3902 inline expr
select(expr
const & a, expr
const & i) {
3905 a.check_error();
3906 return expr(a.ctx(), r);
3907 }
3908 inline expr
select(expr
const & a,
int i) {
3909 return select(a, a.ctx().num_val(i, a.get_sort().array_domain()));
3910 }
3911 inline expr
select(expr
const & a, expr_vector
const & i) {
3913 array<Z3_ast> idxs(i);
3915 a.check_error();
3916 return expr(a.ctx(), r);
3917 }
3918
3919 inline expr
store(expr
const & a, expr
const & i, expr
const & v) {
3922 a.check_error();
3923 return expr(a.ctx(), r);
3924 }
3925
3926 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); }
3927 inline expr
store(expr
const & a, expr i,
int v) {
return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
3928 inline expr
store(expr
const & a,
int i,
int v) {
3929 return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
3930 }
3931 inline expr
store(expr
const & a, expr_vector
const & i, expr
const & v) {
3933 array<Z3_ast> idxs(i);
3934 Z3_ast r =
Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
3935 a.check_error();
3936 return expr(a.ctx(), r);
3937 }
3938
3939 inline expr
as_array(func_decl & f) {
3941 f.check_error();
3942 return expr(f.ctx(), r);
3943 }
3944
3945#define MK_EXPR1(_fn, _arg) \
3946 Z3_ast r = _fn(_arg.ctx(), _arg); \
3947 _arg.check_error(); \
3948 return expr(_arg.ctx(), r);
3949
3950#define MK_EXPR2(_fn, _arg1, _arg2) \
3951 check_context(_arg1, _arg2); \
3952 Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
3953 _arg1.check_error(); \
3954 return expr(_arg1.ctx(), r);
3955
3956 inline expr
const_array(sort
const & d, expr
const & v) {
3958 }
3959
3962 }
3963
3964 inline expr
full_set(sort
const& s) {
3966 }
3967
3968 inline expr
set_add(expr
const& s, expr
const& e) {
3970 }
3971
3972 inline expr
set_del(expr
const& s, expr
const& e) {
3974 }
3975
3976 inline expr
set_union(expr
const& a, expr
const& b) {
3978 Z3_ast es[2] = { a, b };
3980 a.check_error();
3981 return expr(a.ctx(), r);
3982 }
3983
3986 Z3_ast es[2] = { a, b };
3988 a.check_error();
3989 return expr(a.ctx(), r);
3990 }
3991
3994 }
3995
3998 }
3999
4000 inline expr
set_member(expr
const& s, expr
const& e) {
4002 }
4003
4004 inline expr
set_subset(expr
const& a, expr
const& b) {
4006 }
4007
4008
4009
4010
4011
4012 inline expr
empty(sort
const& s) {
4014 s.check_error();
4015 return expr(s.ctx(), r);
4016 }
4017 inline expr
suffixof(expr
const& a, expr
const& b) {
4020 a.check_error();
4021 return expr(a.ctx(), r);
4022 }
4023 inline expr
prefixof(expr
const& a, expr
const& b) {
4026 a.check_error();
4027 return expr(a.ctx(), r);
4028 }
4029 inline expr
indexof(expr
const& s, expr
const& substr, expr
const& offset) {
4032 s.check_error();
4033 return expr(s.ctx(), r);
4034 }
4035 inline expr
last_indexof(expr
const& s, expr
const& substr) {
4038 s.check_error();
4039 return expr(s.ctx(), r);
4040 }
4041 inline expr
to_re(expr
const& s) {
4043 }
4044 inline expr
in_re(expr
const& s, expr
const& re) {
4046 }
4047 inline expr
plus(expr
const& re) {
4049 }
4050 inline expr
option(expr
const& re) {
4052 }
4053 inline expr
star(expr
const& re) {
4055 }
4056 inline expr
re_empty(sort
const& s) {
4058 s.check_error();
4059 return expr(s.ctx(), r);
4060 }
4061 inline expr
re_full(sort
const& s) {
4063 s.check_error();
4064 return expr(s.ctx(), r);
4065 }
4067 assert(args.size() > 0);
4068 context& ctx = args[0u].ctx();
4069 array<Z3_ast> _args(args);
4071 ctx.check_error();
4072 return expr(ctx, r);
4073 }
4074 inline expr
re_diff(expr
const& a, expr
const& b) {
4076 context& ctx = a.ctx();
4078 ctx.check_error();
4079 return expr(ctx, r);
4080 }
4083 }
4084 inline expr
range(expr
const& lo, expr
const& hi) {
4087 lo.check_error();
4088 return expr(lo.ctx(), r);
4089 }
4090
4091
4092
4093
4094
4095 inline expr_vector context::parse_string(
char const* s) {
4097 check_error();
4099
4100 }
4101 inline expr_vector context::parse_file(
char const* s) {
4103 check_error();
4105 }
4106
4107 inline expr_vector context::parse_string(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls) {
4108 array<Z3_symbol> sort_names(sorts.size());
4109 array<Z3_symbol> decl_names(decls.size());
4110 array<Z3_sort> sorts1(sorts);
4111 array<Z3_func_decl> decls1(decls);
4112 for (unsigned i = 0; i < sorts.size(); ++i) {
4113 sort_names[i] = sorts[i].name();
4114 }
4115 for (unsigned i = 0; i < decls.size(); ++i) {
4116 decl_names[i] = decls[i].name();
4117 }
4118
4119 Z3_ast_vector r =
Z3_parse_smtlib2_string(*
this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4120 check_error();
4122 }
4123
4124 inline expr_vector context::parse_file(
char const* s, sort_vector
const& sorts, func_decl_vector
const& decls) {
4125 array<Z3_symbol> sort_names(sorts.size());
4126 array<Z3_symbol> decl_names(decls.size());
4127 array<Z3_sort> sorts1(sorts);
4128 array<Z3_func_decl> decls1(decls);
4129 for (unsigned i = 0; i < sorts.size(); ++i) {
4130 sort_names[i] = sorts[i].name();
4131 }
4132 for (unsigned i = 0; i < decls.size(); ++i) {
4133 decl_names[i] = decls[i].name();
4134 }
4135 Z3_ast_vector r =
Z3_parse_smtlib2_file(*
this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
4136 check_error();
4138 }
4139
4141 assert(is_datatype());
4144 for (unsigned i = 0; i < n; ++i)
4146 return cs;
4147 }
4148
4150 assert(is_datatype());
4153 for (unsigned i = 0; i < n; ++i)
4155 return rs;
4156 }
4157
4160 assert(s.is_datatype());
4162 unsigned idx = 0;
4163 for (; idx < n; ++idx) {
4165 if (id() == f.id())
4166 break;
4167 }
4168 assert(idx < n);
4169 n = arity();
4171 for (unsigned i = 0; i < n; ++i)
4173 return as;
4174 }
4175
4176
4177 inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
4178 assert(src.size() == dst.size());
4179 array<Z3_ast> _src(src.size());
4180 array<Z3_ast> _dst(dst.size());
4181 for (unsigned i = 0; i < src.size(); ++i) {
4182 _src[i] = src[i];
4183 _dst[i] = dst[i];
4184 }
4185 Z3_ast r =
Z3_substitute(ctx(), m_ast, src.size(), _src.ptr(), _dst.ptr());
4186 check_error();
4187 return expr(ctx(), r);
4188 }
4189
4190 inline expr expr::substitute(expr_vector const& dst) {
4191 array<Z3_ast> _dst(dst.size());
4192 for (unsigned i = 0; i < dst.size(); ++i) {
4193 _dst[i] = dst[i];
4194 }
4196 check_error();
4197 return expr(ctx(), r);
4198 }
4199
4200 inline expr expr::substitute(func_decl_vector const& funs, expr_vector const& dst) {
4201 array<Z3_ast> _dst(dst.size());
4202 array<Z3_func_decl> _funs(funs.size());
4203 if (dst.size() != funs.size()) {
4204 Z3_THROW(exception(
"length of argument lists don't align"));
4205 return expr(ctx(), nullptr);
4206 }
4207 for (unsigned i = 0; i < dst.size(); ++i) {
4208 _dst[i] = dst[i];
4209 _funs[i] = funs[i];
4210 }
4212 check_error();
4213 return expr(ctx(), r);
4214 }
4215
4216 typedef std::function<void(expr
const& proof, std::vector<unsigned>
const& deps, expr_vector
const& clause)>
on_clause_eh_t;
4217
4218 class on_clause {
4219 context& c;
4221
4222 static void _on_clause_eh(
void* _ctx, Z3_ast _proof,
unsigned n,
unsigned const* dep, Z3_ast_vector _literals) {
4223 on_clause* ctx = static_cast<on_clause*>(_ctx);
4225 expr proof(ctx->c, _proof);
4226 std::vector<unsigned> deps;
4227 for (unsigned i = 0; i < n; ++i)
4228 deps.push_back(dep[i]);
4229 ctx->m_on_clause(proof, deps, lits);
4230 }
4231 public:
4232 on_clause(solver& s, on_clause_eh_t& on_clause_eh): c(s.ctx()) {
4235 c.check_error();
4236 }
4237 };
4238
4239 class user_propagator_base {
4240
4241 typedef std::function<void(expr const&, expr const&)> fixed_eh_t;
4242 typedef std::function<void(void)> final_eh_t;
4243 typedef std::function<void(expr const&, expr const&)> eq_eh_t;
4244 typedef std::function<void(expr const&)> created_eh_t;
4245 typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
4246
4247 final_eh_t m_final_eh;
4248 eq_eh_t m_eq_eh;
4249 fixed_eh_t m_fixed_eh;
4250 created_eh_t m_created_eh;
4251 decide_eh_t m_decide_eh;
4252 solver* s;
4253 context* c;
4254 std::vector<z3::context*> subcontexts;
4255
4256 Z3_solver_callback cb { nullptr };
4257
4258 struct scoped_cb {
4259 user_propagator_base& p;
4260 scoped_cb(void* _p, Z3_solver_callback cb):p(*static_cast<user_propagator_base*>(_p)) {
4261 p.cb = cb;
4262 }
4263 ~scoped_cb() {
4264 p.cb = nullptr;
4265 }
4266 };
4267
4268 static void push_eh(void* _p, Z3_solver_callback cb) {
4269 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4270 scoped_cb _cb(p, cb);
4271 static_cast<user_propagator_base*>(p)->push();
4272 }
4273
4274 static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
4275 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4276 scoped_cb _cb(p, cb);
4277 static_cast<user_propagator_base*>(_p)->pop(num_scopes);
4278 }
4279
4280 static void* fresh_eh(void* _p, Z3_context ctx) {
4281 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4282 context* c = new context(ctx);
4283 p->subcontexts.push_back(c);
4284 return p->fresh(*c);
4285 }
4286
4287 static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {
4288 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4289 scoped_cb _cb(p, cb);
4290 expr value(p->ctx(), _value);
4291 expr var(p->ctx(), _var);
4292 p->m_fixed_eh(var, value);
4293 }
4294
4295 static void eq_eh(void* _p, Z3_solver_callback cb, Z3_ast _x, Z3_ast _y) {
4296 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4297 scoped_cb _cb(p, cb);
4298 expr x(p->ctx(), _x), y(p->ctx(), _y);
4299 p->m_eq_eh(x, y);
4300 }
4301
4302 static void final_eh(void* p, Z3_solver_callback cb) {
4303 scoped_cb _cb(p, cb);
4304 static_cast<user_propagator_base*>(p)->m_final_eh();
4305 }
4306
4307 static void created_eh(void* _p, Z3_solver_callback cb, Z3_ast _e) {
4308 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4309 scoped_cb _cb(p, cb);
4310 expr e(p->ctx(), _e);
4311 p->m_created_eh(e);
4312 }
4313
4314 static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit, bool is_pos) {
4315 user_propagator_base* p = static_cast<user_propagator_base*>(_p);
4316 scoped_cb _cb(p, cb);
4317 expr val(p->ctx(), _val);
4318 p->m_decide_eh(val, bit, is_pos);
4319 }
4320
4321 public:
4322 user_propagator_base(context& c) : s(nullptr), c(&c) {}
4323
4324 user_propagator_base(solver* s): s(s), c(nullptr) {
4326 }
4327
4328 virtual void push() = 0;
4329 virtual void pop(unsigned num_scopes) = 0;
4330
4331 virtual ~user_propagator_base() {
4332 for (auto& subcontext : subcontexts) {
4333 subcontext->detach();
4334 delete subcontext;
4335 }
4336 }
4337
4338 context& ctx() {
4339 return c ? *c : s->ctx();
4340 }
4341
4350 virtual user_propagator_base* fresh(context& ctx) = 0;
4351
4358 void register_fixed(fixed_eh_t& f) {
4359 m_fixed_eh = f;
4360 if (s) {
4362 }
4363 }
4364
4365 void register_fixed() {
4366 m_fixed_eh = [this](expr const &id, expr const &e) {
4367 fixed(id, e);
4368 };
4369 if (s) {
4371 }
4372 }
4373
4374 void register_eq(eq_eh_t& f) {
4375 m_eq_eh = f;
4376 if (s) {
4378 }
4379 }
4380
4381 void register_eq() {
4382 m_eq_eh = [this](expr const& x, expr const& y) {
4384 };
4385 if (s) {
4387 }
4388 }
4389
4398 void register_final(final_eh_t& f) {
4399 m_final_eh = f;
4400 if (s) {
4402 }
4403 }
4404
4405 void register_final() {
4406 m_final_eh = [this]() {
4407 final();
4408 };
4409 if (s) {
4411 }
4412 }
4413
4414 void register_created(created_eh_t& c) {
4415 m_created_eh = c;
4416 if (s) {
4418 }
4419 }
4420
4421 void register_created() {
4422 m_created_eh = [this](expr const& e) {
4423 created(e);
4424 };
4425 if (s) {
4427 }
4428 }
4429
4430 void register_decide(decide_eh_t& c) {
4431 m_decide_eh = c;
4432 if (s) {
4434 }
4435 }
4436
4437 void register_decide() {
4438 m_decide_eh = [this](expr val, unsigned bit, bool is_pos) {
4439 decide(val, bit, is_pos);
4440 };
4441 if (s) {
4443 }
4444 }
4445
4446 virtual void fixed(expr const& , expr const& ) { }
4447
4448 virtual void eq(expr
const& , expr
const& ) { }
4449
4450 virtual void final() { }
4451
4452 virtual void created(expr const& ) {}
4453
4454 virtual void decide(expr const& , unsigned , bool ) {}
4455
4456 bool next_split(expr
const& e,
unsigned idx,
Z3_lbool phase) {
4457 assert(cb);
4459 }
4460
4475 void add(expr const& e) {
4476 if (cb)
4478 else if (s)
4480 else
4481 assert(false);
4482 }
4483
4484 void conflict(expr_vector const& fixed) {
4485 assert(cb);
4486 expr conseq = ctx().bool_val(false);
4487 array<Z3_ast> _fixed(fixed);
4489 }
4490
4491 void conflict(expr_vector const& fixed, expr_vector const& lhs, expr_vector const& rhs) {
4492 assert(cb);
4493 assert(lhs.size() == rhs.size());
4494 expr conseq = ctx().bool_val(false);
4495 array<Z3_ast> _fixed(fixed);
4496 array<Z3_ast> _lhs(lhs);
4497 array<Z3_ast> _rhs(rhs);
4499 }
4500
4501 bool propagate(expr_vector const& fixed, expr const& conseq) {
4502 assert(cb);
4503 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4504 array<Z3_ast> _fixed(fixed);
4506 }
4507
4508 bool propagate(expr_vector const& fixed,
4509 expr_vector const& lhs, expr_vector const& rhs,
4510 expr const& conseq) {
4511 assert(cb);
4512 assert((Z3_context)conseq.ctx() == (Z3_context)ctx());
4513 assert(lhs.size() == rhs.size());
4514 array<Z3_ast> _fixed(fixed);
4515 array<Z3_ast> _lhs(lhs);
4516 array<Z3_ast> _rhs(rhs);
4517
4519 }
4520 };
4521
4522}
4523
4526#undef Z3_THROW
4527
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.
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.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
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.
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 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_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.
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.
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.
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_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.
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].
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_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.
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.
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. This is a callback a client may invoke during the fixe...
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.
const char * Z3_string
Z3 string type. It is just an alias for const char *.
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_opt const sorts[], unsigned sort_refs[])
Create a constructor.
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_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_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...
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_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
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.
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_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_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_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name)
create a forward reference to a recursive datatype being declared. The forward reference can be used ...
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_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...
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.
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.
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_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_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.
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_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_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_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_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_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_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_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
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_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.
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
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_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_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_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_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.
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...
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_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_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.
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....
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.
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 ...
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_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_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_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_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_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_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_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.
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 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 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 operator>(expr const &a, expr const &b)
sort to_sort(context &c, Z3_sort 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 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
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)
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 ult(expr const &a, expr const &b)
unsigned less than operator for bitvectors.
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 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 full_set(sort const &s)
expr smod(expr const &a, expr const &b)
signed modulus operator for bitvectors
expr implies(expr const &a, expr const &b)
expr empty_set(sort const &s)
expr in_re(expr const &s, expr const &re)
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)
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)
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 mk_and(expr_vector const &args)
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
expr operator||(expr const &a, expr const &b)
expr set_del(expr const &s, expr const &e)
expr ubv_to_fpa(expr const &t, sort s)
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 uge(expr const &a, expr const &b)
unsigned greater than or equal to operator for bitvectors.
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)
tactic fail_if(probe const &p)
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)