A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/classz3_1_1solver.html below:

Z3: solver Class Reference

  solver (context &c)     solver (context &c, simple)     solver (context &c, Z3_solver s)     solver (context &c, char const *logic)     solver (context &c, solver const &src, translate)     solver (solver const &s)     solver (solver const &s, simplifier const &simp)     ~solver () override     operator Z3_solver () const   solver &  operator= (solver const &s)   void  set (params const &p)   void  set (char const *k, bool v)   void  set (char const *k, unsigned v)   void  set (char const *k, double v)   void  set (char const *k, symbol const &v)   void  set (char const *k, char const *v)   void  push ()   Create a backtracking point. More...
  void  pop (unsigned n=1)   void  reset ()   void  add (expr const &e)   void  add (expr const &e, expr const &p)   void  add (expr const &e, char const *p)   void  add (expr_vector const &v)   void  from_file (char const *file)   void  from_string (char const *s)   check_result  check ()   check_result  check (unsigned n, expr *const assumptions)   check_result  check (expr_vector const &assumptions)   model  get_model () const   check_result  consequences (expr_vector &assumptions, expr_vector &vars, expr_vector &conseq)   std::string  reason_unknown () const   stats  statistics () const   expr_vector  unsat_core () const   expr_vector  assertions () const   expr_vector  non_units () const   expr_vector  units () const   expr_vector  trail () const   expr_vector  trail (array< unsigned > &levels) const   void  set_initial_value (expr const &var, expr const &value)   void  set_initial_value (expr const &var, int i)   void  set_initial_value (expr const &var, bool b)   expr  proof () const   std::string  to_smt2 (char const *status="unknown")   std::string  dimacs (bool include_names=true) const   param_descrs  get_param_descrs ()   expr_vector  cube (expr_vector &vars, unsigned cutoff)   cube_generator  cubes ()   cube_generator  cubes (expr_vector &vars)     object (context &c)   virtual  ~object ()=default   context &  ctx () const   Z3_error_code  check_error () const  

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

◆ solver() [1/7]

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

Z3_error_code check_error() const

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 ...

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [2/7]

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

Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)

Create a new incremental solver.

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [3/7]

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

2773

:

object

(c) { init(s); }

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [4/7]

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

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...

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [5/7]

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

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.

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [6/7]

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

2776

:

object

(s) { init(s.m_solver); }

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ solver() [7/7]

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

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.

Referenced by Solver::__del__(), UserPropagateBase::add(), UserPropagateBase::add_created(), UserPropagateBase::add_decide(), UserPropagateBase::add_diseq(), UserPropagateBase::add_eq(), UserPropagateBase::add_final(), UserPropagateBase::add_fixed(), Solver::assert_and_track(), Solver::assert_exprs(), Solver::assertions(), Solver::check(), Solver::consequences(), UserPropagateBase::ctx(), Solver::dimacs(), Solver::from_file(), Solver::from_string(), Solver::help(), Solver::import_model_converter(), Solver::interrupt(), Solver::model(), Solver::next(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::root(), Solver::set(), Solver::set_initial_value(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

◆ ~solver()

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

void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)

Decrement the reference counter of the given solver.

◆ add() [1/4] void add ( expr const &  e ) inline ◆ add() [2/4] void add ( expr const &  e, char const *  p  ) inline ◆ add() [3/4] void add ( expr const &  e, expr const &  p  ) inline

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

2808

assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());

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.

Referenced by Solver::__iadd__(), Fixedpoint::__iadd__(), and Optimize::__iadd__().

◆ add() [4/4] ◆ assertions()

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

Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)

Return the set of asserted formulas on the solver.

System.IntPtr Z3_ast_vector

ast_vector_tpl< expr > expr_vector

Referenced by solver::to_smt2(), and Solver::to_smt2().

◆ check() [1/3]

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

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_lbool

Lifted Boolean type: false, undefined, true.

check_result to_check_result(Z3_lbool l)

◆ check() [2/3]

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

2835  unsigned

n = assumptions.size();

2836

array<Z3_ast> _assumptions(n);

2837  for

(

unsigned

i = 0; i < n; i++) {

2839

_assumptions[i] = assumptions[i];

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.

◆ check() [3/3]

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

2825

array<Z3_ast> _assumptions(n);

2826  for

(

unsigned

i = 0; i < n; i++) {

2828

_assumptions[i] = assumptions[i];

◆ consequences()

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

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.

◆ cube()

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

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...

◆ cubes() [1/2]

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

2994

{

return

cube_generator(*

this

); }

◆ cubes() [2/2]

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

2995

{

return

cube_generator(*

this

, vars); }

◆ dimacs() std::string dimacs ( bool  include_names = true ) const inline

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

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.

◆ from_file() void from_file ( char const *  file ) inline

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

void check_parser_error() const

void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)

load solver assertions from a file.

◆ from_string() void from_string ( char const *  s ) inline

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

void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string str)

load solver assertions from a string.

◆ get_model() model get_model ( ) const inline

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

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.

◆ get_param_descrs()

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

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.

◆ non_units()

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

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.

◆ operator Z3_solver() operator Z3_solver ( ) const inline

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

2779

{

return

m_solver; }

◆ operator=()

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

2783

object::operator=(s);

2784

m_solver = s.m_solver;

void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)

Increment the reference counter of the given solver.

◆ pop() void pop ( unsigned  n = 1 ) inline

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

void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)

Backtrack n backtracking points.

Referenced by Solver::__exit__().

◆ proof()

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

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.

◆ push()

Create a backtracking point.

The solver contains a stack of assertions.

See also
Z3_solver_get_num_scopes
Z3_solver_pop

def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER)))

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

void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)

Create a backtracking point.

Referenced by Solver::__enter__().

◆ reason_unknown() std::string reason_unknown ( ) const inline

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

const char * Z3_string

Z3 string type. It is just an alias for const char *.

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...

◆ reset()

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

void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)

Remove all assertions from the solver.

◆ set() [1/6] void set ( char const *  k, bool  v  ) inline ◆ set() [2/6] void set ( char const *  k, char const *  v  ) inline ◆ set() [3/6] void set ( char const *  k, double  v  ) inline ◆ set() [4/6] void set ( char const *  k, symbol const &  v  ) inline ◆ set() [5/6] void set ( char const *  k, unsigned  v  ) inline ◆ set() [6/6]

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

void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)

Set the given solver using the given parameters.

◆ set_initial_value() [1/3] void set_initial_value ( expr const &  var, bool  b  ) inline

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

void set_initial_value(expr const &var, expr const &value)

◆ set_initial_value() [2/3] void set_initial_value ( expr const &  var, expr const &  value  ) inline

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

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...

Referenced by solver::set_initial_value().

◆ set_initial_value() [3/3] void set_initial_value ( expr const &  var, int  i  ) inline ◆ statistics() stats statistics ( ) const inline

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

Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)

Return statistics for the given solver.

◆ to_smt2() std::string to_smt2 ( char const *  status = "unknown" ) inline

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

2884  Z3_ast const

* fmls = es.ptr();

2886  unsigned

sz = es.size();

2896  ""

,

""

, status,

""

,

expr_vector assertions() const

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.

◆ trail() [1/2]

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

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...

Referenced by Solver::trail_levels().

◆ trail() [2/2]

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

2862  unsigned

sz = result.size();

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...

Referenced by Solver::trail_levels().

◆ units()

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

Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)

Return the set of units modulo model conversion.

◆ unsat_core()

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

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...

◆ operator<< std::ostream& operator<< ( std::ostream &  out, solver const &  s  ) friend

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

Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)

Convert a solver into a string.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4