solver Class Reference

#include <z3++.h>

Inheritance diagram for solver:

Data Structures
struct	simple
struct	translate
class	cube_iterator
class	cube_generator

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 (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.
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	congruence_root (expr const &t) const
expr	congruence_next (expr const &t) const
expr	congruence_explain (expr const &a, expr const &b) 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)
void	solve_for (expr_vector const &vars, expr_vector &terms, expr_vector &guards)
void	import_model_converter (solver const &src)
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)
virtual	~object ()=default
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 3078 of file z3++.h.

Constructor & Destructor Documentation

solver() [1/7]

solver ( context & c )

inline

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

:object(c) { init(Z3_mk_solver(c)); check_error(); }

Referenced by solver::cube_generator::cube_generator(), solver::cube_generator::cube_generator(), solver::cube_iterator::cube_iterator(), import_model_converter(), tactic::mk_solver(), operator<<, operator=(), solver(), solver(), and solver().

solver() [2/7]

solver ( context & c, simple  )

inline

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

:object(c) { init(Z3_mk_simple_solver(c)); check_error(); }

solver() [3/7]

solver ( context & c, Z3_solver s )

inline

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

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

solver() [4/7]

solver ( context & c, char const * logic )

inline

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

:object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); check_error(); }

solver() [5/7]

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

inline

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

: object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); }

solver() [6/7]

solver ( solver const & s )

inline

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

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

solver() [7/7]

solver ( solver const & s, simplifier const & simp )

inline

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

:object(s) { init(Z3_solver_add_simplifier(s.ctx(), s, simp)); }

~solver()

~solver ( )

inlineoverride

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

{ Z3_solver_dec_ref(ctx(), m_solver); }

Member Function Documentation

add() [1/4]

void add ( expr const & e )

inline

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

{ assert(e.is_bool()); Z3_solver_assert(ctx(), m_solver, e); check_error(); }

Referenced by add(), and add().

add() [2/4]

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

inline

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

                                                 {
            add(e, ctx().bool_const(p));
        }        

add() [3/4]

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

inline

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

                                                 {
            assert(e.is_bool()); assert(p.is_bool()); assert(p.is_const());
            Z3_solver_assert_and_track(ctx(), m_solver, e, p);
            check_error();
        }

add() [4/4]

void add ( expr_vector const & v )

inline

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

                                       { 
            check_context(*this, v); 
            for (unsigned i = 0; i < v.size(); ++i) 
                add(v[i]); 
        }

assertions()

expr_vector assertions ( ) const

inline

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

{ Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

Referenced by to_smt2().

check() [1/3]

check_result check ( )

inline

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

{ Z3_lbool r = Z3_solver_check(ctx(), m_solver); check_error(); return to_check_result(r); }

check() [2/3]

check_result check ( expr_vector const & assumptions )

inline

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

                                                           {
            unsigned n = assumptions.size();
            array<Z3_ast> _assumptions(n);
            for (unsigned i = 0; i < n; ++i) {
                check_context(*this, assumptions[i]);
                _assumptions[i] = assumptions[i];
            }
            Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
            check_error();
            return to_check_result(r);
        }

check() [3/3]

check_result check ( unsigned n, expr *const assumptions )

inline

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

                                                                 {
            array<Z3_ast> _assumptions(n);
            for (unsigned i = 0; i < n; ++i) {
                check_context(*this, assumptions[i]);
                _assumptions[i] = assumptions[i];
            }
            Z3_lbool r = Z3_solver_check_assumptions(ctx(), m_solver, n, _assumptions.ptr());
            check_error();
            return to_check_result(r);
        }

congruence_explain()

expr congruence_explain ( expr const & a, expr const & b ) const

inline

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

                                                                    {
            check_context(*this, a);
            check_context(*this, b);
            Z3_ast r = Z3_solver_congruence_explain(ctx(), m_solver, a, b);
            check_error();
            return expr(ctx(), r);
        }

congruence_next()

expr congruence_next ( expr const & t ) const

inline

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

                                                  {
            check_context(*this, t);
            Z3_ast r = Z3_solver_congruence_next(ctx(), m_solver, t);
            check_error();
            return expr(ctx(), r);
        }

congruence_root()

expr congruence_root ( expr const & t ) const

inline

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

                                                  {
            check_context(*this, t);
            Z3_ast r = Z3_solver_congruence_root(ctx(), m_solver, t);
            check_error();
            return expr(ctx(), r);
        }

consequences()

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

inline

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

                                                                                                    {
            Z3_lbool r = Z3_solver_get_consequences(ctx(), m_solver, assumptions, vars, conseq);
            check_error();
            return to_check_result(r);
        }

cube()

expr_vector cube ( expr_vector & vars, unsigned cutoff )

inline

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

                                                             {
            Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff);
            check_error();
            return expr_vector(ctx(), r);
        }

cubes() [1/2]

cube_generator cubes ( )

inline

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

{ return cube_generator(*this); }

cubes() [2/2]

cube_generator cubes ( expr_vector & vars )

inline

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

{ return cube_generator(*this, vars); }

dimacs()

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

inline

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

{ return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver, include_names)); }

from_file()

void from_file ( char const * file )

inline

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

{ Z3_solver_from_file(ctx(), m_solver, file); ctx().check_parser_error(); }

from_string()

void from_string ( char const * s )

inline

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

{ Z3_solver_from_string(ctx(), m_solver, s); ctx().check_parser_error(); }

get_model()

model get_model ( ) const

inline

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

{ Z3_model m = Z3_solver_get_model(ctx(), m_solver); check_error(); return model(ctx(), m); }

get_param_descrs()

param_descrs get_param_descrs ( )

inline

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

{ return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }

import_model_converter()

void import_model_converter ( solver const & src )

inline

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

                                                       {
            check_context(*this, src);
            Z3_solver_import_model_converter(ctx(), src.m_solver, m_solver);
            check_error();
        }

non_units()

expr_vector non_units ( ) const

inline

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

{ Z3_ast_vector r = Z3_solver_get_non_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

operator Z3_solver()

operator Z3_solver ( ) const

inline

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

{ return m_solver; }

operator=()

solver & operator= ( solver const & s )

inline

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

                                           {
            Z3_solver_inc_ref(s.ctx(), s.m_solver);
            Z3_solver_dec_ref(ctx(), m_solver);
            object::operator=(s);
            m_solver = s.m_solver;
            return *this;
        }

pop()

void pop ( unsigned n = 1 )

inline

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

{ Z3_solver_pop(ctx(), m_solver, n); check_error(); }

proof()

expr proof ( ) const

inline

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

{ Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }

push()

void push ( )

inline

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 3120 of file z3++.h.

{ Z3_solver_push(ctx(), m_solver); check_error(); }

reason_unknown()

std::string reason_unknown ( ) const

inline

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

{ Z3_string r = Z3_solver_get_reason_unknown(ctx(), m_solver); check_error(); return r; }

reset()

void reset ( )

inline

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

{ Z3_solver_reset(ctx(), m_solver); check_error(); }

set() [1/6]

void set ( char const * k, bool v )

inline

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

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

Referenced by set().

set() [2/6]

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

inline

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

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

Referenced by set().

set() [3/6]

void set ( char const * k, double v )

inline

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

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

Referenced by set().

set() [4/6]

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

inline

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

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

Referenced by set().

set() [5/6]

void set ( char const * k, unsigned v )

inline

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

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

Referenced by set().

set() [6/6]

void set ( params const & p )

inline

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

{ Z3_solver_set_params(ctx(), m_solver, p); check_error(); }

set_initial_value() [1/3]

void set_initial_value ( expr const & var, bool b )

inline

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

                                                        {
            set_initial_value(var, ctx().bool_val(b));            
        }

set_initial_value() [2/3]

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

inline

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

                                                                   {
            Z3_solver_set_initial_value(ctx(), m_solver, var, value);
            check_error();
        }

Referenced by set_initial_value(), and set_initial_value().

set_initial_value() [3/3]

void set_initial_value ( expr const & var, int i )

inline

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

                                                       {
            set_initial_value(var, ctx().num_val(i, var.get_sort()));
        }

solve_for()

void solve_for ( expr_vector const & vars, expr_vector & terms, expr_vector & guards )

inline

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

                                                                                         {
            // Create a copy of vars since the C API modifies the variables vector
            expr_vector variables(ctx());
            for (unsigned i = 0; i < vars.size(); ++i) {
                check_context(*this, vars[i]);
                variables.push_back(vars[i]);
            }
            // Clear output vectors before calling C API
            terms = expr_vector(ctx());
            guards = expr_vector(ctx());
            Z3_solver_solve_for(ctx(), m_solver, variables, terms, guards);
            check_error();
        }

statistics()

stats statistics ( ) const

inline

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

{ Z3_stats r = Z3_solver_get_statistics(ctx(), m_solver); check_error(); return stats(ctx(), r); }

to_smt2()

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

inline

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

                                                        {
            array<Z3_ast> es(assertions());
            Z3_ast const* fmls = es.ptr();
            Z3_ast fml = 0;
            unsigned sz = es.size();
            if (sz > 0) {
                --sz;
                fml = fmls[sz];
            }
            else {
                fml = ctx().bool_val(true);
            }
            return std::string(Z3_benchmark_to_smtlib_string(
                                   ctx(),
                                   "", "", status, "",
                                   sz,
                                   fmls,
                                   fml));
        }

trail() [1/2]

expr_vector trail ( ) const

inline

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

{ Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

trail() [2/2]

expr_vector trail ( array< unsigned > & levels ) const

inline

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

                                                         { 
            Z3_ast_vector r = Z3_solver_get_trail(ctx(), m_solver); 
            check_error(); 
            expr_vector result(ctx(), r);
            unsigned sz = result.size();
            levels.resize(sz);
            Z3_solver_get_levels(ctx(), m_solver, r, sz, levels.ptr());
            check_error(); 
            return result; 
        }

units()

expr_vector units ( ) const

inline

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

{ Z3_ast_vector r = Z3_solver_get_units(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

unsat_core()

expr_vector unsat_core ( ) const

inline

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

{ Z3_ast_vector r = Z3_solver_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }

Friends And Related Symbol Documentation

operator<<

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

friend

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

{ out << Z3_solver_to_string(s.ctx(), s); return out; }

Referenced by operator<<.