solver Class Reference

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)
	object (object const &s)
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 2362 of file z3++.h.

Constructor & Destructor Documentation

solver() [1/6]

solver ( context &  c )

inline

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

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

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

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

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

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

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

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

: object(c) { init(Z3_solver_translate(src.ctx(), src, c)); }

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

: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 2377 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 2395 of file z3++.h.

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

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

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

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

add() [3/4]

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

inline

Definition at line 2396 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();
        }

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

add() [4/4]

void add ( expr_vector const &  v )

inline

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

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

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

assertions()

expr_vector assertions ( ) const

inline

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

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

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

check() [1/3]

check_result check ( )

inline

Definition at line 2412 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 2423 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 2413 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);
        }

consequences()

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

inline

Definition at line 2435 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 2485 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 2572 of file z3++.h.

{ return cube_generator(*this); }

cubes() [2/2]

cube_generator cubes ( expr_vector &  vars )

inline

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

{ return cube_generator(*this, vars); }

dimacs()

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

inline

Definition at line 2480 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 2409 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 2410 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 2434 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 2482 of file z3++.h.

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

non_units()

expr_vector non_units ( ) const

inline

Definition at line 2444 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 2378 of file z3++.h.

{ return m_solver; }

operator=()

solver& operator= ( solver const &  s )

inline

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

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

pop()

void pop ( unsigned  n = 1 )

inline

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

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

proof()

expr proof ( ) const

inline

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

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

push()

void push ( )

inline

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

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

reason_unknown()

std::string reason_unknown ( ) const

inline

Definition at line 2440 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 2394 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 2387 of file z3++.h.

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

Referenced by solver::set().

set() [2/6]

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

inline

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

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

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

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

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

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

statistics()

stats statistics ( ) const

inline

Definition at line 2441 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 2460 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 2446 of file z3++.h.

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

Referenced by Solver::trail_levels().

trail() [2/2]

expr_vector trail ( array< unsigned > &  levels ) const

inline

Definition at line 2447 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; 
        }

Referenced by Solver::trail_levels().

units()

expr_vector units ( ) const

inline

Definition at line 2445 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 2442 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 Function Documentation

operator<<

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

friend

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

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