|
| 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) |
|
| object (context &c) |
|
| object (object const &s) |
|
context & | ctx () const |
|
Z3_error_code | check_error () const |
|
Definition at line 2362 of file z3++.h.
◆ solver() [1/6]
◆ solver() [2/6]
◆ solver() [3/6]
◆ solver() [4/6]
◆ solver() [5/6]
◆ solver() [6/6]
◆ ~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 2396 of file z3++.h.
2397 assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
◆ add() [4/4]
Definition at line 2404 of file z3++.h.
2406 for (
unsigned i = 0; i < v.size(); ++i)
◆ assertions()
◆ check() [1/3]
◆ check() [2/3]
Definition at line 2423 of file z3++.h.
2424 unsigned n = assumptions.size();
2425 array<Z3_ast> _assumptions(n);
2426 for (
unsigned i = 0; i < n; i++) {
2428 _assumptions[i] = assumptions[i];
◆ check() [3/3]
Definition at line 2413 of file z3++.h.
2414 array<Z3_ast> _assumptions(n);
2415 for (
unsigned i = 0; i < n; i++) {
2417 _assumptions[i] = assumptions[i];
◆ consequences()
◆ cube()
◆ cubes() [1/2]
Definition at line 2572 of file z3++.h.
2572 {
return cube_generator(*
this); }
◆ cubes() [2/2]
Definition at line 2573 of file z3++.h.
2573 {
return cube_generator(*
this, vars); }
◆ dimacs()
std::string dimacs |
( |
bool |
include_names = true | ) |
const |
|
inline |
◆ from_file()
void from_file |
( |
char const * |
file | ) |
|
|
inline |
◆ from_string()
void from_string |
( |
char const * |
s | ) |
|
|
inline |
◆ get_model()
model get_model |
( |
| ) |
const |
|
inline |
◆ get_param_descrs()
◆ non_units()
◆ operator Z3_solver()
operator Z3_solver |
( |
| ) |
const |
|
inline |
Definition at line 2378 of file z3++.h.
2378 {
return m_solver; }
◆ operator=()
Definition at line 2379 of file z3++.h.
2383 m_solver = s.m_solver;
◆ pop()
void pop |
( |
unsigned |
n = 1 | ) |
|
|
inline |
◆ proof()
◆ push()
◆ reason_unknown()
std::string reason_unknown |
( |
| ) |
const |
|
inline |
◆ reset()
◆ 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]
◆ statistics()
stats statistics |
( |
| ) |
const |
|
inline |
◆ to_smt2()
std::string to_smt2 |
( |
char const * |
status = "unknown" | ) |
|
|
inline |
Definition at line 2460 of file z3++.h.
2462 Z3_ast
const* fmls = es.ptr();
2464 unsigned sz = es.size();
◆ trail() [1/2]
◆ trail() [2/2]
Definition at line 2447 of file z3++.h.
2451 unsigned sz = result.size();
◆ units()
◆ unsat_core()
◆ operator<<
std::ostream& operator<< |
( |
std::ostream & |
out, |
|
|
solver const & |
s |
|
) |
| |
|
friend |
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.
expr_vector assertions() const
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_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s)
Check whether the assertions in a given solver are consistent or not.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
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_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...
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
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_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...
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
Z3_lbool
Lifted Boolean type: false, undefined, true.
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_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_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_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...
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
Z3_ast_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 check_parser_error() const
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
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.
ast_vector_tpl< expr > expr_vector
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
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_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_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...
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
friend void check_context(object const &a, object const &b)
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 set(params const &p)
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_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
check_result to_check_result(Z3_lbool l)
Z3_error_code check_error() const
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_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.
const typedef char * Z3_string
Z3 string type. It is just an alias for const char *.
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_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.