goal Class Reference

Inheritance diagram for goal:

Public Member Functions
	goal (context &c, bool models=true, bool unsat_cores=false, bool proofs=false)
	goal (context &c, Z3_goal s)
	goal (goal const &s)
	~goal () override
	operator Z3_goal () const
goal &	operator= (goal const &s)
void	add (expr const &f)
void	add (expr_vector const &v)
unsigned	size () const
expr	operator[] (int i) const
Z3_goal_prec	precision () const
bool	inconsistent () const
unsigned	depth () const
void	reset ()
unsigned	num_exprs () const
bool	is_decided_sat () const
bool	is_decided_unsat () const
model	convert_model (model const &m) const
model	get_model () const
expr	as_expr () const
std::string	dimacs (bool include_names=true) const
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, goal const &g)

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

goal() [1/3]

goal ( context &  c, bool  models = true, bool  unsat_cores = false, bool  proofs = false  )

inline

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

:object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); }

Referenced by Goal::__del__(), Goal::assert_exprs(), Goal::convert_model(), Goal::depth(), Goal::dimacs(), Goal::get(), Goal::inconsistent(), Goal::prec(), Goal::sexpr(), Goal::size(), and Goal::translate().

goal() [2/3]

goal ( context &  c, Z3_goal  s  )

inline

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

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

Referenced by Goal::__del__(), Goal::assert_exprs(), Goal::convert_model(), Goal::depth(), Goal::dimacs(), Goal::get(), Goal::inconsistent(), Goal::prec(), Goal::sexpr(), Goal::size(), and Goal::translate().

goal() [3/3]

goal ( goal const &  s )

inline

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

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

Referenced by Goal::__del__(), Goal::assert_exprs(), Goal::convert_model(), Goal::depth(), Goal::dimacs(), Goal::get(), Goal::inconsistent(), Goal::prec(), Goal::sexpr(), Goal::size(), and Goal::translate().

~goal()

~goal ( )

inlineoverride

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

{ Z3_goal_dec_ref(ctx(), m_goal); }

Member Function Documentation

add() [1/2]

void add ( expr const &  f )

inline

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

{ check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }

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

add() [2/2]

void add ( expr_vector const &  v )

inline

Definition at line 3020 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__(), Optimize::__iadd__(), and goal::add().

as_expr()

expr as_expr ( ) const

inline

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

                             {
            unsigned n = size();
            if (n == 0)
                return ctx().bool_val(true);
            else if (n == 1)
                return operator[](0u);
            else {
                array<Z3_ast> args(n);
                for (unsigned i = 0; i < n; i++)
                    args[i] = operator[](i);
                return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
            }
        }

convert_model()

model convert_model ( model const &  m ) const

inline

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

                                                   {
            check_context(*this, m);
            Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);
            check_error();
            return model(ctx(), new_m);
        }

depth()

unsigned depth ( ) const

inline

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

{ return Z3_goal_depth(ctx(), m_goal); }

dimacs()

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

inline

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

{ return std::string(Z3_goal_to_dimacs_string(ctx(), m_goal, include_names)); }

get_model()

model get_model ( ) const

inline

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

                                {
            Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, 0);
            check_error();
            return model(ctx(), new_m);
        }

inconsistent()

bool inconsistent ( ) const

inline

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

{ return Z3_goal_inconsistent(ctx(), m_goal); }

is_decided_sat()

bool is_decided_sat ( ) const

inline

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

{ return Z3_goal_is_decided_sat(ctx(), m_goal); }

is_decided_unsat()

bool is_decided_unsat ( ) const

inline

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

{ return Z3_goal_is_decided_unsat(ctx(), m_goal); }

num_exprs()

unsigned num_exprs ( ) const

inline

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

{ return Z3_goal_num_exprs(ctx(), m_goal); }

operator Z3_goal()

operator Z3_goal ( ) const

inline

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

{ return m_goal; }

operator=()

goal& operator= ( goal const &  s )

inline

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

                                         {
            Z3_goal_inc_ref(s.ctx(), s.m_goal);
            Z3_goal_dec_ref(ctx(), m_goal);
            object::operator=(s);
            m_goal = s.m_goal;
            return *this;
        }

operator[]()

expr operator[] ( int  i ) const

inline

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

{ assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }

Referenced by goal::as_expr().

precision()

Z3_goal_prec precision ( ) const

inline

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

{ return Z3_goal_precision(ctx(), m_goal); }

reset()

void reset ( )

inline

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

{ Z3_goal_reset(ctx(), m_goal); }

size()

unsigned size ( ) const

inline

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

{ return Z3_goal_size(ctx(), m_goal); }

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), goal::as_expr(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  out, goal const &  g  )

friend

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

{ out << Z3_goal_to_string(g.ctx(), g); return out; }