cprover
|
#include <smt2_prop.h>
Public Member Functions | |
smt2_propt (const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out) | |
virtual | ~smt2_propt () |
virtual literalt | land (literalt a, literalt b) |
virtual literalt | lor (literalt a, literalt b) |
virtual literalt | land (const bvt &bv) |
virtual literalt | lor (const bvt &bv) |
virtual literalt | lxor (const bvt &bv) |
virtual literalt | lxor (literalt a, literalt b) |
virtual literalt | lnand (literalt a, literalt b) |
virtual literalt | lnor (literalt a, literalt b) |
virtual literalt | lequal (literalt a, literalt b) |
virtual literalt | limplies (literalt a, literalt b) |
virtual literalt | lselect (literalt a, literalt b, literalt c) |
virtual literalt | new_variable () |
virtual size_t | no_variables () const |
virtual void | set_no_variables (size_t no) |
virtual void | lcnf (const bvt &bv) |
virtual const std::string | solver_text () |
virtual tvt | l_get (literalt literal) const |
virtual void | set_assignment (literalt a, bool value) |
virtual propt::resultt | prop_solve () |
virtual void | clear () |
virtual void | reset_assignment () |
void | finalize () |
![]() | |
propt () | |
virtual | ~propt () |
virtual void | set_equal (literalt a, literalt b) |
asserts a==b in the propositional formula More... | |
virtual void | l_set_to (literalt a, bool value) |
void | l_set_to_true (literalt a) |
void | l_set_to_false (literalt a) |
void | lcnf (literalt l0, literalt l1) |
void | lcnf (literalt l0, literalt l1, literalt l2) |
void | lcnf (literalt l0, literalt l1, literalt l2, literalt l3) |
virtual bool | has_set_to () const |
virtual bool | cnf_handled_well () const |
virtual void | set_assumptions (const bvt &_assumptions) |
virtual bool | has_set_assumptions () const |
virtual void | set_variable_name (literalt a, const std::string &name) |
bvt | new_variables (std::size_t width) |
generates a bitvector of given width with new variables More... | |
virtual void | copy_assignment_from (const propt &prop) |
virtual bool | is_in_conflict (literalt l) const |
virtual bool | has_is_in_conflict () const |
virtual void | set_frozen (literalt a) |
![]() | |
virtual | ~prop_assignmentt () |
Protected Types | |
typedef std::set< std::string > | smt2_identifierst |
Protected Member Functions | |
std::string | smt2_literal (literalt l) |
literalt | def_smt2_literal () |
literalt | define_new_variable () |
Protected Attributes | |
size_t | _no_variables |
std::ostream & | out |
std::vector< tvt > | assignment |
smt2_identifierst | smt2_identifiers |
bool | core_enabled |
![]() | |
bvt | lcnf_bv |
Friends | |
class | smt2_convt |
class | smt2_dect |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Definition at line 20 of file smt2_prop.h.
|
protected |
Definition at line 84 of file smt2_prop.h.
smt2_propt::smt2_propt | ( | const std::string & | _benchmark, |
const std::string & | _source, | ||
const std::string & | _logic, | ||
bool | _core_enabled, | ||
std::ostream & | _out | ||
) |
Definition at line 13 of file smt2_prop.cpp.
References _no_variables, core_enabled, and out.
|
virtual |
Definition at line 37 of file smt2_prop.cpp.
|
inlinevirtual |
Definition at line 57 of file smt2_prop.h.
References assignment.
|
protected |
|
protected |
Definition at line 254 of file smt2_prop.cpp.
References _no_variables, out, literalt::set(), and smt2_literal().
void smt2_propt::finalize | ( | ) |
Definition at line 41 of file smt2_prop.cpp.
References core_enabled, out, and smt2_identifiers.
Implements propt.
Definition at line 307 of file smt2_prop.cpp.
References assignment, literalt::is_false(), literalt::is_true(), r, literalt::sign(), tvt::TV_UNKNOWN, and literalt::var_no().
Referenced by solver_text().
Implements propt.
Definition at line 117 of file smt2_prop.cpp.
References const_literal(), define_new_variable(), out, and smt2_literal().
Referenced by lnand().
Implements propt.
Definition at line 61 of file smt2_prop.cpp.
References define_new_variable(), forall_literals, out, and smt2_literal().
|
virtual |
Implements propt.
Definition at line 267 of file smt2_prop.cpp.
References out, and smt2_literal().
Referenced by set_no_variables().
Implements propt.
Definition at line 143 of file smt2_prop.cpp.
References const_literal(), define_new_variable(), out, and smt2_literal().
Referenced by limplies(), and lnor().
Implements propt.
Definition at line 78 of file smt2_prop.cpp.
References define_new_variable(), forall_literals, out, and smt2_literal().
Implements propt.
Definition at line 213 of file smt2_prop.cpp.
References const_literal(), define_new_variable(), out, and smt2_literal().
Implements propt.
Definition at line 95 of file smt2_prop.cpp.
References const_literal(), define_new_variable(), forall_literals, out, and smt2_literal().
Referenced by lequal().
Implements propt.
Definition at line 169 of file smt2_prop.cpp.
References const_literal(), new_variable(), out, and smt2_literal().
|
virtual |
Implements propt.
Definition at line 243 of file smt2_prop.cpp.
References _no_variables, out, literalt::set(), and smt2_literal().
Referenced by lxor().
|
inlinevirtual |
Implements propt.
Definition at line 44 of file smt2_prop.h.
References _no_variables.
Referenced by reset_assignment().
|
virtual |
|
inlinevirtual |
Definition at line 62 of file smt2_prop.h.
References assignment, no_variables(), and tvt::TV_UNKNOWN.
|
virtual |
Reimplemented from propt.
Definition at line 321 of file smt2_prop.cpp.
References assignment, literalt::is_false(), literalt::is_true(), and literalt::var_no().
Referenced by solver_text().
|
inlinevirtual |
Definition at line 45 of file smt2_prop.h.
References lcnf().
|
protected |
Definition at line 290 of file smt2_prop.cpp.
References const_literal(), literalt::sign(), smt2_identifiers, and literalt::var_no().
Referenced by define_new_variable(), land(), lcnf(), lor(), lselect(), lxor(), and new_variable().
|
inlinevirtual |
Implements propt.
Definition at line 49 of file smt2_prop.h.
References l_get(), prop_solve(), and set_assignment().
|
friend |
Definition at line 68 of file smt2_prop.h.
|
friend |
Definition at line 69 of file smt2_prop.h.
|
protected |
Definition at line 74 of file smt2_prop.h.
Referenced by define_new_variable(), new_variable(), no_variables(), and smt2_propt().
|
protected |
Definition at line 80 of file smt2_prop.h.
Referenced by clear(), l_get(), reset_assignment(), and set_assignment().
|
protected |
Definition at line 87 of file smt2_prop.h.
Referenced by finalize(), and smt2_propt().
|
protected |
Definition at line 75 of file smt2_prop.h.
Referenced by define_new_variable(), finalize(), land(), lcnf(), lor(), lselect(), lxor(), new_variable(), and smt2_propt().
|
protected |
Definition at line 85 of file smt2_prop.h.
Referenced by finalize(), and smt2_literal().