solver Class Reference

Inheritance diagram for solver:

Data Structures
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	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)
check_result	check ()
check_result	check (unsigned n, expr *const assumptions)
check_result	check (expr_vector 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	proof () const
std::string	to_smt2 (char const *status="unknown")
param_descrs	get_param_descrs ()
Public Member Functions inherited from object
	object (context &c)
	object (object const &s)
context &	ctx () const
void	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 1686 of file z3++.h.

Constructor & Destructor Documentation

solver() [1/6]

solver ( context &  c )

inline

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

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

solver() [2/6]

solver ( context &  c, simple    )

inline

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

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

solver() [3/6]

solver ( context &  c, Z3_solver  s  )

inline

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

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

solver() [4/6]

solver ( context &  c, char const *  logic  )

inline

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

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

solver() [5/6]

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

inline

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

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

solver() [6/6]

solver ( solver const &  s )

inline

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

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

~solver()

~solver ( )

inline

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

{ Z3_solver_dec_ref(ctx(), m_solver); }

Member Function Documentation

add() [1/3]

void add ( expr const &  e )

inline

Definition at line 1714 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/3]

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

inline

Definition at line 1715 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() [3/3]

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

inline

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

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

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

assertions()

expr_vector assertions ( ) const

inline

Definition at line 1754 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 1723 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 ( unsigned  n, expr *const  assumptions  )

inline

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

check() [3/3]

check_result check ( expr_vector  assumptions )

inline

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

consequences()

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

inline

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

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

get_model()

model get_model ( ) const

inline

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

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

operator Z3_solver()

operator Z3_solver ( ) const

inline

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

{ return m_solver; }

operator=()

solver& operator= ( solver const &  s )

inline

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

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

proof()

expr proof ( ) const

inline

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

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

reason_unknown()

std::string reason_unknown ( ) const

inline

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

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

set()

void set ( params const &  p )

inline

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

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

statistics()

stats statistics ( ) const

inline

Definition at line 1752 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 1758 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));
        }

unsat_core()

expr_vector unsat_core ( ) const

inline

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

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