cprover
smt2_propt Class Reference

#include <smt2_prop.h>

Inheritance diagram for smt2_propt:
[legend]
Collaboration diagram for smt2_propt:
[legend]

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 ()
 
- Public Member Functions inherited from propt
 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)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 
- Public Member Functions inherited from prop_assignmentt
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< tvtassignment
 
smt2_identifierst smt2_identifiers
 
bool core_enabled
 
- Protected Attributes inherited from propt
bvt lcnf_bv
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Friends

class smt2_convt
 
class smt2_dect
 

Additional Inherited Members

- Public Types inherited from propt
enum  resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR }
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Definition at line 20 of file smt2_prop.h.

Member Typedef Documentation

§ smt2_identifierst

typedef std::set<std::string> smt2_propt::smt2_identifierst
protected

Definition at line 84 of file smt2_prop.h.

Constructor & Destructor Documentation

§ smt2_propt()

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.

§ ~smt2_propt()

smt2_propt::~smt2_propt ( )
virtual

Definition at line 37 of file smt2_prop.cpp.

Member Function Documentation

§ clear()

virtual void smt2_propt::clear ( void  )
inlinevirtual

Definition at line 57 of file smt2_prop.h.

References assignment.

§ def_smt2_literal()

literalt smt2_propt::def_smt2_literal ( )
protected

§ define_new_variable()

literalt smt2_propt::define_new_variable ( )
protected

Definition at line 254 of file smt2_prop.cpp.

References _no_variables, out, literalt::set(), and smt2_literal().

Referenced by land(), lor(), lselect(), and lxor().

§ finalize()

void smt2_propt::finalize ( )

Definition at line 41 of file smt2_prop.cpp.

References core_enabled, out, and smt2_identifiers.

§ l_get()

tvt smt2_propt::l_get ( literalt  literal) const
virtual

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().

§ land() [1/2]

literalt smt2_propt::land ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 117 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), out, and smt2_literal().

Referenced by lnand().

§ land() [2/2]

literalt smt2_propt::land ( const bvt bv)
virtual

Implements propt.

Definition at line 61 of file smt2_prop.cpp.

References define_new_variable(), forall_literals, out, and smt2_literal().

§ lcnf()

void smt2_propt::lcnf ( const bvt bv)
virtual

Implements propt.

Definition at line 267 of file smt2_prop.cpp.

References out, and smt2_literal().

Referenced by set_no_variables().

§ lequal()

literalt smt2_propt::lequal ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 203 of file smt2_prop.cpp.

References lxor().

§ limplies()

literalt smt2_propt::limplies ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 208 of file smt2_prop.cpp.

References lor().

§ lnand()

literalt smt2_propt::lnand ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 193 of file smt2_prop.cpp.

References land().

§ lnor()

literalt smt2_propt::lnor ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 198 of file smt2_prop.cpp.

References lor().

§ lor() [1/2]

literalt smt2_propt::lor ( literalt  a,
literalt  b 
)
virtual

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().

§ lor() [2/2]

literalt smt2_propt::lor ( const bvt bv)
virtual

Implements propt.

Definition at line 78 of file smt2_prop.cpp.

References define_new_variable(), forall_literals, out, and smt2_literal().

§ lselect()

literalt smt2_propt::lselect ( literalt  a,
literalt  b,
literalt  c 
)
virtual

Implements propt.

Definition at line 213 of file smt2_prop.cpp.

References const_literal(), define_new_variable(), out, and smt2_literal().

§ lxor() [1/2]

literalt smt2_propt::lxor ( const bvt bv)
virtual

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().

§ lxor() [2/2]

literalt smt2_propt::lxor ( literalt  a,
literalt  b 
)
virtual

Implements propt.

Definition at line 169 of file smt2_prop.cpp.

References const_literal(), new_variable(), out, and smt2_literal().

§ new_variable()

literalt smt2_propt::new_variable ( void  )
virtual

Implements propt.

Definition at line 243 of file smt2_prop.cpp.

References _no_variables, out, literalt::set(), and smt2_literal().

Referenced by lxor().

§ no_variables()

virtual size_t smt2_propt::no_variables ( ) const
inlinevirtual

Implements propt.

Definition at line 44 of file smt2_prop.h.

References _no_variables.

Referenced by reset_assignment().

§ prop_solve()

propt::resultt smt2_propt::prop_solve ( )
virtual

Implements propt.

Definition at line 331 of file smt2_prop.cpp.

Referenced by solver_text().

§ reset_assignment()

virtual void smt2_propt::reset_assignment ( )
inlinevirtual

Definition at line 62 of file smt2_prop.h.

References assignment, no_variables(), and tvt::TV_UNKNOWN.

§ set_assignment()

void smt2_propt::set_assignment ( literalt  a,
bool  value 
)
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().

§ set_no_variables()

virtual void smt2_propt::set_no_variables ( size_t  no)
inlinevirtual

Definition at line 45 of file smt2_prop.h.

References lcnf().

§ smt2_literal()

std::string smt2_propt::smt2_literal ( literalt  l)
protected

§ solver_text()

virtual const std::string smt2_propt::solver_text ( )
inlinevirtual

Implements propt.

Definition at line 49 of file smt2_prop.h.

References l_get(), prop_solve(), and set_assignment().

Friends And Related Function Documentation

§ smt2_convt

friend class smt2_convt
friend

Definition at line 68 of file smt2_prop.h.

§ smt2_dect

friend class smt2_dect
friend

Definition at line 69 of file smt2_prop.h.

Member Data Documentation

§ _no_variables

size_t smt2_propt::_no_variables
protected

Definition at line 74 of file smt2_prop.h.

Referenced by define_new_variable(), new_variable(), no_variables(), and smt2_propt().

§ assignment

std::vector<tvt> smt2_propt::assignment
protected

Definition at line 80 of file smt2_prop.h.

Referenced by clear(), l_get(), reset_assignment(), and set_assignment().

§ core_enabled

bool smt2_propt::core_enabled
protected

Definition at line 87 of file smt2_prop.h.

Referenced by finalize(), and smt2_propt().

§ out

std::ostream& smt2_propt::out
protected

§ smt2_identifiers

smt2_identifierst smt2_propt::smt2_identifiers
protected

Definition at line 85 of file smt2_prop.h.

Referenced by finalize(), and smt2_literal().


The documentation for this class was generated from the following files: