Z3
 
Loading...
Searching...
No Matches
Data Structures | Namespaces | Macros | Typedefs | Enumerations | Functions
z3++.h File Reference

Go to the source code of this file.

Data Structures

class  exception
 Exception used to sign API usage errors. More...
 
class  config
 Z3 global configuration object. More...
 
class  context
 A Context manages all other Z3 objects, global configuration options, etc. More...
 
class  array< T >
 
class  object
 
class  symbol
 
class  param_descrs
 
class  params
 
class  ast
 
class  ast_vector_tpl< T >
 
class  ast_vector_tpl< T >::iterator
 
class  ast_map
 A map from ASTs to ASTs. More...
 
class  sort
 A Z3 sort (aka type). Every expression (i.e., formula or term) in Z3 has a sort. More...
 
class  func_decl
 Function declaration (aka function definition). It is the signature of interpreted and uninterpreted functions in Z3. The basic building block in Z3 is the function application. More...
 
class  parser_context
 
class  expr
 A Z3 expression is used to represent formulas and terms. For Z3, a formula is any expression of sort Boolean. Every expression has a sort. More...
 
class  expr::iterator
 
class  cast_ast< ast >
 
class  cast_ast< expr >
 
class  cast_ast< sort >
 
class  cast_ast< func_decl >
 
class  func_entry
 
class  func_interp
 
class  model
 
struct  model::translate
 
class  stats
 
class  parameter
 class for auxiliary parameters associated with func_decl The class is initialized with a func_decl or application expression and an index The accessor get_expr, get_sort, ... is available depending on the value of kind(). The caller is responsible to check that the kind of the parameter aligns with the call (get_expr etc). More...
 
class  solver
 
struct  solver::simple
 
struct  solver::translate
 
class  solver::cube_iterator
 
class  solver::cube_generator
 
class  goal
 
class  apply_result
 
class  tactic
 
class  simplifier
 
class  probe
 
class  optimize
 
struct  optimize::translate
 
class  optimize::handle
 
class  fixedpoint
 
class  constructor_list
 
class  constructors
 
class  on_clause
 
class  user_propagator_base
 
class  rcf_num
 Wrapper for Z3 Real Closed Field (RCF) numerals. More...
 

Namespaces

namespace  z3
 Z3 C++ namespace.
 

Macros

#define Z3_THROW(x)   {}
 
#define _Z3_MK_BIN_(a, b, binop)
 
#define _Z3_MK_UN_(a, mkun)
 
#define MK_EXPR1(_fn, _arg)
 
#define MK_EXPR2(_fn, _arg1, _arg2)
 

Typedefs

typedef ast_vector_tpl< ast > ast_vector
 
typedef ast_vector_tpl< expr > expr_vector
 
typedef ast_vector_tpl< sort > sort_vector
 
typedef ast_vector_tpl< func_decl > func_decl_vector
 
typedef std::function< void(expr const &proof, std::vector< unsigned > const &deps, expr_vector const &clause)> on_clause_eh_t
 

Enumerations

enum  check_result { unsat , sat , unknown }
 
enum  rounding_mode {
  RNA , RNE , RTP , RTN ,
  RTZ
}
 

Functions

void set_param (char const *param, char const *value)
 
void set_param (char const *param, bool value)
 
void set_param (char const *param, int value)
 
void reset_params ()
 
void get_version (unsigned &major, unsigned &minor, unsigned &build_number, unsigned &revision_number)
 Return Z3 version number information.
 
std::string get_full_version ()
 Return a string that fully describes the version of Z3 in use.
 
void enable_trace (char const *tag)
 Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
 
void disable_trace (char const *tag)
 Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
 
std::ostream & operator<< (std::ostream &out, exception const &e)
 
check_result to_check_result (Z3_lbool l)
 
void check_context (object const &a, object const &b)
 
std::ostream & operator<< (std::ostream &out, symbol const &s)
 
std::ostream & operator<< (std::ostream &out, param_descrs const &d)
 
std::ostream & operator<< (std::ostream &out, params const &p)
 
std::ostream & operator<< (std::ostream &out, ast const &n)
 
bool eq (ast const &a, ast const &b)
 
expr select (expr const &a, expr const &i)
 forward declarations
 
expr select (expr const &a, expr_vector const &i)
 
expr implies (expr const &a, expr const &b)
 
expr implies (expr const &a, bool b)
 
expr implies (bool a, expr const &b)
 
expr pw (expr const &a, expr const &b)
 
expr pw (expr const &a, int b)
 
expr pw (int a, expr const &b)
 
expr mod (expr const &a, expr const &b)
 
expr mod (expr const &a, int b)
 
expr mod (int a, expr const &b)
 
expr operator% (expr const &a, expr const &b)
 
expr operator% (expr const &a, int b)
 
expr operator% (int a, expr const &b)
 
expr rem (expr const &a, expr const &b)
 
expr rem (expr const &a, int b)
 
expr rem (int a, expr const &b)
 
expr complex (expr const &re, expr const &im)
 Construct a Complex expression from Int or Real components.
 
expr real_part (expr const &z)
 
expr imag_part (expr const &z)
 
expr operator! (expr const &a)
 
expr is_int (expr const &e)
 
expr operator&& (expr const &a, expr const &b)
 
expr operator&& (expr const &a, bool b)
 
expr operator&& (bool a, expr const &b)
 
expr operator|| (expr const &a, expr const &b)
 
expr operator|| (expr const &a, bool b)
 
expr operator|| (bool a, expr const &b)
 
expr operator== (expr const &a, expr const &b)
 
expr operator== (expr const &a, int b)
 
expr operator== (int a, expr const &b)
 
expr operator== (expr const &a, double b)
 
expr operator== (double a, expr const &b)
 
expr operator!= (expr const &a, expr const &b)
 
expr operator!= (expr const &a, int b)
 
expr operator!= (int a, expr const &b)
 
expr operator!= (expr const &a, double b)
 
expr operator!= (double a, expr const &b)
 
expr operator+ (expr const &a, expr const &b)
 
expr operator+ (expr const &a, int b)
 
expr operator+ (int a, expr const &b)
 
expr operator* (expr const &a, expr const &b)
 
expr operator* (expr const &a, int b)
 
expr operator* (int a, expr const &b)
 
expr operator>= (expr const &a, expr const &b)
 
expr operator/ (expr const &a, expr const &b)
 
expr operator/ (expr const &a, int b)
 
expr operator/ (int a, expr const &b)
 
expr operator- (expr const &a)
 
expr operator- (expr const &a, expr const &b)
 
expr operator- (expr const &a, int b)
 
expr operator- (int a, expr const &b)
 
expr operator<= (expr const &a, expr const &b)
 
expr operator<= (expr const &a, int b)
 
expr operator<= (int a, expr const &b)
 
expr operator>= (expr const &a, int b)
 
expr operator>= (int a, expr const &b)
 
expr operator< (expr const &a, expr const &b)
 
expr operator< (expr const &a, int b)
 
expr operator< (int a, expr const &b)
 
expr operator> (expr const &a, expr const &b)
 
expr operator> (expr const &a, int b)
 
expr operator> (int a, expr const &b)
 
expr operator& (expr const &a, expr const &b)
 
expr operator& (expr const &a, int b)
 
expr operator& (int a, expr const &b)
 
expr operator^ (expr const &a, expr const &b)
 
expr operator^ (expr const &a, int b)
 
expr operator^ (int a, expr const &b)
 
expr operator| (expr const &a, expr const &b)
 
expr operator| (expr const &a, int b)
 
expr operator| (int a, expr const &b)
 
expr nand (expr const &a, expr const &b)
 
expr nor (expr const &a, expr const &b)
 
expr xnor (expr const &a, expr const &b)
 
expr min (expr const &a, expr const &b)
 
expr max (expr const &a, expr const &b)
 
expr bvredor (expr const &a)
 
expr bvredand (expr const &a)
 
expr abs (expr const &a)
 
expr sqrt (expr const &a, expr const &rm)
 
expr fp_eq (expr const &a, expr const &b)
 
expr operator~ (expr const &a)
 
expr fma (expr const &a, expr const &b, expr const &c, expr const &rm)
 
expr fpa_fp (expr const &sgn, expr const &exp, expr const &sig)
 
expr fpa_to_sbv (expr const &t, unsigned sz)
 
expr fpa_to_ubv (expr const &t, unsigned sz)
 
expr sbv_to_fpa (expr const &t, sort s)
 
expr ubv_to_fpa (expr const &t, sort s)
 
expr fpa_to_fpa (expr const &t, sort s)
 
expr round_fpa_to_closest_integer (expr const &t)
 
expr ite (expr const &c, expr const &t, expr const &e)
 Create the if-then-else expression ite(c, t, e)
 
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 whole C API with the C++ layer defined in this file.
 
sort to_sort (context &c, Z3_sort s)
 
func_decl to_func_decl (context &c, Z3_func_decl f)
 
expr sle (expr const &a, expr const &b)
 signed less than or equal to operator for bitvectors.
 
expr sle (expr const &a, int b)
 
expr sle (int a, expr const &b)
 
expr slt (expr const &a, expr const &b)
 signed less than operator for bitvectors.
 
expr slt (expr const &a, int b)
 
expr slt (int a, expr const &b)
 
expr sge (expr const &a, expr const &b)
 signed greater than or equal to operator for bitvectors.
 
expr sge (expr const &a, int b)
 
expr sge (int a, expr const &b)
 
expr sgt (expr const &a, expr const &b)
 signed greater than operator for bitvectors.
 
expr sgt (expr const &a, int b)
 
expr sgt (int a, expr const &b)
 
expr ule (expr const &a, expr const &b)
 unsigned less than or equal to operator for bitvectors.
 
expr ule (expr const &a, int b)
 
expr ule (int a, expr const &b)
 
expr ult (expr const &a, expr const &b)
 unsigned less than operator for bitvectors.
 
expr ult (expr const &a, int b)
 
expr ult (int a, expr const &b)
 
expr uge (expr const &a, expr const &b)
 unsigned greater than or equal to operator for bitvectors.
 
expr uge (expr const &a, int b)
 
expr uge (int a, expr const &b)
 
expr ugt (expr const &a, expr const &b)
 unsigned greater than operator for bitvectors.
 
expr ugt (expr const &a, int b)
 
expr ugt (int a, expr const &b)
 
expr sdiv (expr const &a, expr const &b)
 signed division operator for bitvectors.
 
expr sdiv (expr const &a, int b)
 
expr sdiv (int a, expr const &b)
 
expr udiv (expr const &a, expr const &b)
 unsigned division operator for bitvectors.
 
expr udiv (expr const &a, int b)
 
expr udiv (int a, expr const &b)
 
expr srem (expr const &a, expr const &b)
 signed remainder operator for bitvectors
 
expr srem (expr const &a, int b)
 
expr srem (int a, expr const &b)
 
expr smod (expr const &a, expr const &b)
 signed modulus operator for bitvectors
 
expr smod (expr const &a, int b)
 
expr smod (int a, expr const &b)
 
expr urem (expr const &a, expr const &b)
 unsigned reminder operator for bitvectors
 
expr urem (expr const &a, int b)
 
expr urem (int a, expr const &b)
 
expr shl (expr const &a, expr const &b)
 shift left operator for bitvectors
 
expr shl (expr const &a, int b)
 
expr shl (int a, expr const &b)
 
expr lshr (expr const &a, expr const &b)
 logic shift right operator for bitvectors
 
expr lshr (expr const &a, int b)
 
expr lshr (int a, expr const &b)
 
expr ashr (expr const &a, expr const &b)
 arithmetic shift right operator for bitvectors
 
expr ashr (expr const &a, int b)
 
expr ashr (int a, expr const &b)
 
expr zext (expr const &a, unsigned i)
 Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
 
expr bv2int (expr const &a, bool is_signed)
 bit-vector and integer conversions.
 
expr int2bv (unsigned n, expr const &a)
 
expr bvadd_no_overflow (expr const &a, expr const &b, bool is_signed)
 bit-vector overflow/underflow checks
 
expr bvadd_no_underflow (expr const &a, expr const &b)
 
expr bvsub_no_overflow (expr const &a, expr const &b)
 
expr bvsub_no_underflow (expr const &a, expr const &b, bool is_signed)
 
expr bvsdiv_no_overflow (expr const &a, expr const &b)
 
expr bvneg_no_overflow (expr const &a)
 
expr bvmul_no_overflow (expr const &a, expr const &b, bool is_signed)
 
expr bvmul_no_underflow (expr const &a, expr const &b)
 
expr sext (expr const &a, unsigned i)
 Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
 
func_decl linear_order (sort const &a, unsigned index)
 
func_decl partial_order (sort const &a, unsigned index)
 
func_decl piecewise_linear_order (sort const &a, unsigned index)
 
func_decl tree_order (sort const &a, unsigned index)
 
expr_vector polynomial_subresultants (expr const &p, expr const &q, expr const &x)
 Return the nonzero subresultants of p and q with respect to the "variable" x.
 
expr forall (expr const &x, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr forall (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr forall (expr_vector const &xs, expr const &b)
 
expr exists (expr const &x, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr exists (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr exists (expr_vector const &xs, expr const &b)
 
expr lambda (expr const &x, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &b)
 
expr lambda (expr const &x1, expr const &x2, expr const &x3, expr const &x4, expr const &b)
 
expr lambda (expr_vector const &xs, expr const &b)
 
expr pble (expr_vector const &es, int const *coeffs, int bound)
 
expr pbge (expr_vector const &es, int const *coeffs, int bound)
 
expr pbeq (expr_vector const &es, int const *coeffs, int bound)
 
expr atmost (expr_vector const &es, unsigned bound)
 
expr atleast (expr_vector const &es, unsigned bound)
 
expr sum (expr_vector const &args)
 
expr distinct (expr_vector const &args)
 
expr concat (expr const &a, expr const &b)
 
expr concat (expr_vector const &args)
 
expr map (expr const &f, expr const &list)
 
expr mapi (expr const &f, expr const &i, expr const &list)
 
expr foldl (expr const &f, expr const &a, expr const &list)
 
expr foldli (expr const &f, expr const &i, expr const &a, expr const &list)
 
expr mk_or (expr_vector const &args)
 
expr mk_and (expr_vector const &args)
 
expr mk_xor (expr_vector const &args)
 
expr qe_lite (expr_vector const &vars, expr const &body)
 
std::vector< Z3_app > to_apps (expr_vector const &bounds)
 
expr qe_model_project (model const &m, expr_vector const &bounds, expr const &body)
 
expr qe_model_project_skolem (model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
 Project variables and write the introduced Skolem terms to map.
 
expr qe_model_project_with_witness (model const &m, expr_vector const &bounds, expr const &body, ast_map &map)
 Project variables and write the introduced witnesses to map.
 
std::ostream & operator<< (std::ostream &out, model const &m)
 
std::ostream & operator<< (std::ostream &out, stats const &s)
 
std::ostream & operator<< (std::ostream &out, check_result r)
 
std::ostream & operator<< (std::ostream &out, solver const &s)
 
std::ostream & operator<< (std::ostream &out, goal const &g)
 
std::ostream & operator<< (std::ostream &out, apply_result const &r)
 
tactic operator& (tactic const &t1, tactic const &t2)
 
tactic operator| (tactic const &t1, tactic const &t2)
 
tactic repeat (tactic const &t, unsigned max=UINT_MAX)
 
tactic with (tactic const &t, params const &p)
 
tactic try_for (tactic const &t, unsigned ms)
 
tactic par_or (unsigned n, tactic const *tactics)
 
tactic par_and_then (tactic const &t1, tactic const &t2)
 
simplifier operator& (simplifier const &t1, simplifier const &t2)
 
simplifier with (simplifier const &t, params const &p)
 
probe operator<= (probe const &p1, probe const &p2)
 
probe operator<= (probe const &p1, double p2)
 
probe operator<= (double p1, probe const &p2)
 
probe operator>= (probe const &p1, probe const &p2)
 
probe operator>= (probe const &p1, double p2)
 
probe operator>= (double p1, probe const &p2)
 
probe operator< (probe const &p1, probe const &p2)
 
probe operator< (probe const &p1, double p2)
 
probe operator< (double p1, probe const &p2)
 
probe operator> (probe const &p1, probe const &p2)
 
probe operator> (probe const &p1, double p2)
 
probe operator> (double p1, probe const &p2)
 
probe operator== (probe const &p1, probe const &p2)
 
probe operator== (probe const &p1, double p2)
 
probe operator== (double p1, probe const &p2)
 
probe operator&& (probe const &p1, probe const &p2)
 
probe operator|| (probe const &p1, probe const &p2)
 
probe operator! (probe const &p)
 
std::ostream & operator<< (std::ostream &out, optimize const &s)
 
std::ostream & operator<< (std::ostream &out, fixedpoint const &f)
 
tactic fail_if (probe const &p)
 
tactic when (probe const &p, tactic const &t)
 
tactic cond (probe const &p, tactic const &t1, tactic const &t2)
 
expr to_real (expr const &a)
 
func_decl function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl function (char const *name, sort const &domain, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
 
func_decl function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
 
func_decl function (char const *name, sort_vector const &domain, sort const &range)
 
func_decl function (std::string const &name, sort_vector const &domain, sort const &range)
 
func_decl recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &range)
 
func_decl recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
 
expr select (expr const &a, int i)
 
expr store (expr const &a, expr const &i, expr const &v)
 
expr store (expr const &a, int i, expr const &v)
 
expr store (expr const &a, expr i, int v)
 
expr store (expr const &a, int i, int v)
 
expr store (expr const &a, expr_vector const &i, expr const &v)
 
expr as_array (func_decl &f)
 
expr array_default (expr const &a)
 
expr array_ext (expr const &a, expr const &b)
 
expr const_array (sort const &d, expr const &v)
 
expr empty_set (sort const &s)
 
expr full_set (sort const &s)
 
expr set_add (expr const &s, expr const &e)
 
expr set_del (expr const &s, expr const &e)
 
expr set_union (expr const &a, expr const &b)
 
expr set_intersect (expr const &a, expr const &b)
 
expr set_difference (expr const &a, expr const &b)
 
expr set_complement (expr const &a)
 
expr set_member (expr const &s, expr const &e)
 
expr set_subset (expr const &a, expr const &b)
 
expr finite_set_empty (sort const &s)
 
expr finite_set_singleton (expr const &e)
 
expr finite_set_union (expr const &a, expr const &b)
 
expr finite_set_intersect (expr const &a, expr const &b)
 
expr finite_set_difference (expr const &a, expr const &b)
 
expr finite_set_member (expr const &e, expr const &s)
 
expr finite_set_size (expr const &s)
 
expr finite_set_subset (expr const &a, expr const &b)
 
expr finite_set_map (expr const &f, expr const &s)
 
expr finite_set_filter (expr const &f, expr const &s)
 
expr finite_set_range (expr const &low, expr const &high)
 
expr empty (sort const &s)
 
expr suffixof (expr const &a, expr const &b)
 
expr prefixof (expr const &a, expr const &b)
 
expr indexof (expr const &s, expr const &substr, expr const &offset)
 
expr last_indexof (expr const &s, expr const &substr)
 
expr to_re (expr const &s)
 
expr in_re (expr const &s, expr const &re)
 
expr plus (expr const &re)
 
expr option (expr const &re)
 
expr star (expr const &re)
 
expr re_empty (sort const &s)
 
expr re_full (sort const &s)
 
expr re_intersect (expr_vector const &args)
 
expr re_diff (expr const &a, expr const &b)
 
expr re_complement (expr const &a)
 
expr range (expr const &lo, expr const &hi)
 
rcf_num rcf_pi (context &c)
 Create an RCF numeral representing pi.
 
rcf_num rcf_e (context &c)
 Create an RCF numeral representing e (Euler's constant).
 
rcf_num rcf_infinitesimal (context &c)
 Create an RCF numeral representing an infinitesimal.
 
std::vector< rcf_num > rcf_roots (context &c, std::vector< rcf_num > const &coeffs)
 Find roots of a polynomial with given coefficients.
 

Macro Definition Documentation

◆ _Z3_MK_BIN_

#define _Z3_MK_BIN_ (   a,
  b,
  binop 
)
Value:
check_context(a, b); \
Z3_ast r = binop(a.ctx(), a, b); \
a.check_error(); \
return expr(a.ctx(), r); \

Definition at line 1846 of file z3++.h.

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

◆ _Z3_MK_UN_

#define _Z3_MK_UN_ (   a,
  mkun 
)
Value:
Z3_ast r = mkun(a.ctx(), a); \
a.check_error(); \
return expr(a.ctx(), r); \

Definition at line 1893 of file z3++.h.

◆ MK_EXPR1

#define MK_EXPR1 (   _fn,
  _arg 
)
Value:
Z3_ast r = _fn(_arg.ctx(), _arg); \
_arg.check_error(); \
return expr(_arg.ctx(), r);

Definition at line 4444 of file z3++.h.

◆ MK_EXPR2

#define MK_EXPR2 (   _fn,
  _arg1,
  _arg2 
)
Value:
check_context(_arg1, _arg2); \
Z3_ast r = _fn(_arg1.ctx(), _arg1, _arg2); \
_arg1.check_error(); \
return expr(_arg1.ctx(), r);

Definition at line 4449 of file z3++.h.

◆ Z3_THROW

#define Z3_THROW (   x)    {}

Definition at line 134 of file z3++.h.