Z3 |

Data Structures | Public Member Functions | Friends
solver Class Reference

`#include <z3++.h>`

Inheritance diagram for solver:

## Data Structures
class | cube_generator
class | cube_iterator
struct | simple
struct | translate

## Public Member Functions
| 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 ()
| 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 ()
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
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)
Public Member Functions inherited from object
| object (context &c)
context & | ctx () const
Z3_error_code | check_error () const

## Friends
std::ostream & | operator<< (std::ostream &out, solver const &s)

## Additional Inherited Members
Protected Attributes inherited from object
context * | m_ctx

## Detailed Description

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

## Constructor & Destructor Documentation

## ◆ solver() [1/6]

solver | ( | context & | c | ) |
| inline

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

2561:object(c) { init(Z3_mk_solver(c)); }
z3::object::object
object(context &c)
Definition: z3++.h:421
Z3_mk_solver
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_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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ solver() [2/6]

solver | ( | context & | c,
|  | simple |
| ) |  |
| inline

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

2562:object(c) { init(Z3_mk_simple_solver(c)); }
Z3_mk_simple_solver
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.

Referenced by Solver::__del__(), UserPropagateBase::add(), 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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ solver() [3/6]

solver | ( | context & | c,
|  | Z3_solver | s
| ) |  |
| inline

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

2563:object(c) { init(s); }

Referenced by Solver::__del__(), UserPropagateBase::add(), 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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ solver() [4/6]

solver | ( | context & | c,
|  | char const * | logic
| ) |  |
| inline

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

2564:object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); }
Z3_mk_solver_for_logic
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_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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ solver() [5/6]

solver | ( | context & | c,
|  | solver const & | src,
|  | translate |
| ) |  |
| inline

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

2565: object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }
Z3_solver_translate
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_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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ solver() [6/6]

solver | ( | solver const & | s | ) |
| inline

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

2566:object(s) { init(s.m_solver); }

Referenced by Solver::__del__(), UserPropagateBase::add(), 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::model(), Solver::non_units(), Solver::num_scopes(), Solver::param_descrs(), Solver::pop(), Solver::proof(), Solver::push(), Solver::reason_unknown(), Solver::reset(), Solver::set(), Solver::sexpr(), Solver::statistics(), Solver::trail(), Solver::trail_levels(), Solver::translate(), Solver::units(), and Solver::unsat_core().

## ◆ ~solver()

~solver | ( |  | ) |
| inline

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

2567{ Z3_solver_dec_ref(ctx(), m_solver); }
z3::object::ctx
context & ctx() const
Definition: z3++.h:422
Z3_solver_dec_ref
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

## Member Function Documentation

## ◆ add() [1/4]

void add | ( | expr const & | e | ) |
| inline

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

2585{ assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }
z3::object::check_error
Z3_error_code check_error() const
Definition: z3++.h:423
Z3_solver_assert
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.

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

## ◆ add() [2/4]

void add | ( | expr const & | e,
|  | char const * | p
| ) |  |
| inline

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

2591 {
2592 add(e, ctx().bool_const(p));
2593 }
z3::solver::add
void add(expr const &e)
Definition: z3++.h:2585

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

## ◆ add() [3/4]

void add | ( | expr const & | e,
|  | expr const & | p
| ) |  |
| inline

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

2586 {
2587 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
2588 Z3_solver_assert_and_track(ctx(), m_solver, e, p);
2589 check_error();
2590 }
Z3_solver_assert_and_track
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]

void add | ( | expr_vector const & | v | ) |
| inline

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

2594 {
2595 check_context(*this, v);
2596 for (unsigned i = 0; i < v.size(); ++i)
2597 add(v[i]);
2598 }
z3::object::check_context
friend void check_context(object const &a, object const &b)
Definition: z3++.h:426

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

## ◆ assertions()

expr_vector assertions | ( |  | ) | const
| inline

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

2633{ Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
z3::expr_vector
ast_vector_tpl< expr > expr_vector
Definition: z3++.h:73
Z3_solver_get_assertions
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

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

## ◆ check() [1/3]

check_result check | ( |  | ) |
| inline

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

2602{ Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }
z3::to_check_result
check_result to_check_result(Z3_lbool l)
Definition: z3++.h:144
Z3_solver_check
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
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ check() [2/3]

check_result check | ( | expr_vector const & | assumptions | ) |
| inline

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

2613 {
2614 unsigned n = assumptions.size();
2615 array<Z3_ast> _assumptions(n);
2616 for (unsigned i = 0; i < n; i++) {
2617 check_context(*this, assumptions[i]);
2618 _assumptions[i] = assumptions[i];
2619 }
2620 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2621 check_error();
2622 return to_check_result(r);
2623 }
Z3_solver_check_assumptions
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]

check_result check | ( | unsigned | n,
|  | expr *const | assumptions
| ) |  |
| inline

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

2603 {
2604 array<Z3_ast> _assumptions(n);
2605 for (unsigned i = 0; i < n; i++) {
2606 check_context(*this, assumptions[i]);
2607 _assumptions[i] = assumptions[i];
2608 }
2609 Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
2610 check_error();
2611 return to_check_result(r);
2612 }

## ◆ consequences()

check_result consequences | ( | expr_vector & | assumptions,
|  | expr_vector & | vars,
|  | expr_vector & | conseq
| ) |  |
| inline

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

2625 {
2626 Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
2627 check_error();
2628 return to_check_result(r);
2629 }
Z3_solver_get_consequences
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()

expr_vector cube | ( | expr_vector & | vars,
|  | unsigned | cutoff
| ) |  |
| inline

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

2675 {
2676 Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
2677 check_error();
2678 return expr_vector(ctx(), r);
2679 }
Z3_solver_cube
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]

cube_generator cubes | ( |  | ) |
| inline

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

2762{ return cube_generator(*this); }

## ◆ cubes() [2/2]

cube_generator cubes | ( | expr_vector & | vars | ) |
| inline

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

2763{ return cube_generator(*this, vars); }

## ◆ dimacs()

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

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

2670{ return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }
Z3_solver_to_dimacs_string
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 2599 of file z3++.h.

2599{ Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }
z3::context::check_parser_error
void check_parser_error() const
Definition: z3++.h:195
Z3_solver_from_file
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 2600 of file z3++.h.

2600{ Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }
Z3_solver_from_string
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.

## ◆ get_model()

model get_model | ( |  | ) | const
| inline

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

2624{ Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }
Z3_solver_get_model
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()

param_descrs get_param_descrs | ( |  | ) |
| inline

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

2672{ return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
Z3_solver_get_param_descrs
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()

expr_vector non_units | ( |  | ) | const
| inline

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

2634{ Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_solver_get_non_units
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 2568 of file z3++.h.

2568{ return m_solver; }

## ◆ operator=()

solver & operator= | ( | solver const & | s | ) |
| inline

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

2569 {
2570 Z3_solver_inc_ref(s.ctx(), s.m_solver);
2571 Z3_solver_dec_ref(ctx(), m_solver);
2572 object::operator=(s);
2573 m_solver = s.m_solver;
2574 return *this;
2575 }
Z3_solver_inc_ref
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 2583 of file z3++.h.

2583{ Z3_solver_pop(ctx(), m_solver, n); check_error(); }
Z3_solver_pop
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

## ◆ proof()

expr proof | ( |  | ) | const
| inline

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

2647{ Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
Z3_solver_get_proof
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()

void push | ( |  | ) |
| inline

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

2582{ Z3_solver_push(ctx(), m_solver); check_error(); }
Z3_solver_push
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.

## ◆ reason_unknown()

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

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

2630{ Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }
Z3_string
const char * Z3_string
Z3 string type. It is just an alias for const char *.
Definition: z3_api.h:84
Z3_solver_get_reason_unknown
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()

void reset | ( |  | ) |
| inline

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

2584{ Z3_solver_reset(ctx(), m_solver); check_error(); }
Z3_solver_reset
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

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

2577{ params p(ctx()); p.set(k, v); set(p); }
z3::solver::set
void set(params const &p)
Definition: z3++.h:2576

Referenced by solver::set().

## ◆ set() [2/6]

void set | ( | char const * | k,
|  | char const * | v
| ) |  |
| inline

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

2581{ params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

## ◆ set() [3/6]

void set | ( | char const * | k,
|  | double | v
| ) |  |
| inline

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

2579{ params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

## ◆ set() [4/6]

void set | ( | char const * | k,
|  | symbol const & | v
| ) |  |
| inline

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

2580{ params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

## ◆ set() [5/6]

void set | ( | char const * | k,
|  | unsigned | v
| ) |  |
| inline

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

2578{ params p(ctx()); p.set(k, v); set(p); }

Referenced by solver::set().

## ◆ set() [6/6]

void set | ( | params const & | p | ) |
| inline

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

2576{ Z3_solver_set_params(ctx(), m_solver, p); check_error(); }
Z3_solver_set_params
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

## ◆ statistics()

stats statistics | ( |  | ) | const
| inline

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

2631{ Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }
Z3_solver_get_statistics
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 2650 of file z3++.h.

2650 {
2651 array<Z3_ast> es(assertions());
2652 Z3_ast const* fmls = es.ptr();
2653 Z3_ast fml = 0;
2654 unsigned sz = es.size();
2655 if (sz > 0) {
2656 --sz;
2657 fml = fmls[sz];
2658 }
2659 else {
2660 fml = ctx().bool_val(true);
2661 }
2662 return std::string(Z3_benchmark_to_smtlib_string(
2663 ctx(),
2664 "", "", status, "",
2665 sz,
2666 fmls,
2667 fml));
2668 }
z3::context::bool_val
expr bool_val(bool b)
Definition: z3++.h:3388
z3::solver::assertions
expr_vector assertions() const
Definition: z3++.h:2633
Z3_benchmark_to_smtlib_string
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]

expr_vector trail | ( |  | ) | const
| inline

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

2636{ Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_solver_get_trail
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]

expr_vector trail | ( | array< unsigned > & | levels | ) | const
| inline

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

2637 {
2638 Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver);
2639 check_error();
2640 expr_vector result(ctx(), r);
2641 unsigned sz = result.size();
2642 levels.resize(sz);
2643 Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
2644 check_error();
2645 return result;
2646 }
Z3_solver_get_levels
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()

expr_vector units | ( |  | ) | const
| inline

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

2635{ Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_solver_get_units
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()

expr_vector unsat_core | ( |  | ) | const
| inline

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

2632{ Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
Z3_solver_get_unsat_core
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...

## Friends And Related Function Documentation

## ◆ operator<<

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

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

2766{ out << Z3_solver_to_string(s.ctx(), s); return out; }
Z3_solver_to_string
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.