cprover
aig_prop_baset Class Reference

#include <aig_prop.h>

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

Public Member Functions

 aig_prop_baset (aigt &_dest)
 
bool has_set_to () const override
 
bool cnf_handled_well () const override
 
literalt land (literalt a, literalt b) override
 
literalt lor (literalt a, literalt b) override
 
literalt land (const bvt &bv) override
 
literalt lor (const bvt &bv) override
 
void lcnf (const bvt &clause) override
 
literalt lxor (literalt a, literalt b) override
 
literalt lxor (const bvt &bv) override
 
literalt lnand (literalt a, literalt b) override
 
literalt lnor (literalt a, literalt b) override
 
literalt lequal (literalt a, literalt b) override
 
literalt limplies (literalt a, literalt b) override
 
literalt lselect (literalt a, literalt b, literalt c) override
 
void set_equal (literalt a, literalt b) override
 asserts a==b in the propositional formula More...
 
void l_set_to (literalt a, bool value) override
 
literalt new_variable () override
 
size_t no_variables () const override
 
const std::string solver_text () override
 
tvt l_get (literalt a) const override
 
resultt prop_solve () override
 
- Public Member Functions inherited from propt
 propt ()
 
virtual ~propt ()
 
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 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 set_assignment (literalt a, bool value)
 
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 Attributes

aigtdest
 
- Protected Attributes inherited from propt
bvt lcnf_bv
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

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 aig_prop.h.

Constructor & Destructor Documentation

◆ aig_prop_baset()

aig_prop_baset::aig_prop_baset ( aigt _dest)
inlineexplicit

Definition at line 23 of file aig_prop.h.

Member Function Documentation

◆ cnf_handled_well()

bool aig_prop_baset::cnf_handled_well ( ) const
inlineoverridevirtual

Reimplemented from propt.

Definition at line 28 of file aig_prop.h.

◆ has_set_to()

bool aig_prop_baset::has_set_to ( ) const
inlineoverridevirtual

Reimplemented from propt.

Reimplemented in aig_prop_constraintt.

Definition at line 27 of file aig_prop.h.

◆ l_get()

tvt aig_prop_baset::l_get ( literalt  a) const
inlineoverridevirtual

Implements propt.

Reimplemented in aig_prop_solvert.

Definition at line 57 of file aig_prop.h.

References tvt::unknown().

◆ l_set_to()

void aig_prop_baset::l_set_to ( literalt  a,
bool  value 
)
inlineoverridevirtual

Reimplemented from propt.

Reimplemented in aig_prop_constraintt.

Definition at line 44 of file aig_prop.h.

◆ land() [1/2]

literalt aig_prop_baset::land ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 56 of file aig_prop.cpp.

References const_literal(), dest, literalt::is_false(), literalt::is_true(), neg(), and aigt::new_and_node().

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

◆ land() [2/2]

literalt aig_prop_baset::land ( const bvt bv)
overridevirtual

Implements propt.

Definition at line 22 of file aig_prop.cpp.

References const_literal(), forall_literals, and land().

◆ lcnf()

void aig_prop_baset::lcnf ( const bvt clause)
inlineoverridevirtual

Implements propt.

Reimplemented in aig_prop_constraintt.

Definition at line 34 of file aig_prop.h.

◆ lequal()

literalt aig_prop_baset::lequal ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 107 of file aig_prop.cpp.

References lxor().

Referenced by set_equal().

◆ limplies()

literalt aig_prop_baset::limplies ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 112 of file aig_prop.cpp.

References lor(), and neg().

◆ lnand()

literalt aig_prop_baset::lnand ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 97 of file aig_prop.cpp.

References land().

◆ lnor()

literalt aig_prop_baset::lnor ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 102 of file aig_prop.cpp.

References lor().

◆ lor() [1/2]

literalt aig_prop_baset::lor ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 71 of file aig_prop.cpp.

References land(), and neg().

Referenced by aig_prop_constraintt::lcnf(), limplies(), lnor(), lselect(), lxor(), and set_equal().

◆ lor() [2/2]

literalt aig_prop_baset::lor ( const bvt bv)
overridevirtual

Implements propt.

Definition at line 34 of file aig_prop.cpp.

References const_literal(), forall_literals, land(), and neg().

◆ lselect()

literalt aig_prop_baset::lselect ( literalt  a,
literalt  b,
literalt  c 
)
overridevirtual

Implements propt.

Definition at line 117 of file aig_prop.cpp.

References literalt::is_false(), literalt::is_true(), land(), lor(), and neg().

◆ lxor() [1/2]

literalt aig_prop_baset::lxor ( literalt  a,
literalt  b 
)
overridevirtual

Implements propt.

Definition at line 76 of file aig_prop.cpp.

References const_literal(), literalt::is_false(), literalt::is_true(), land(), lor(), and neg().

Referenced by lequal(), and lxor().

◆ lxor() [2/2]

literalt aig_prop_baset::lxor ( const bvt bv)
overridevirtual

Implements propt.

Definition at line 46 of file aig_prop.cpp.

References const_literal(), forall_literals, and lxor().

◆ new_variable()

literalt aig_prop_baset::new_variable ( void  )
inlineoverridevirtual

Implements propt.

Definition at line 46 of file aig_prop.h.

References dest, and aigt::new_node().

◆ no_variables()

size_t aig_prop_baset::no_variables ( ) const
inlineoverridevirtual

Implements propt.

Definition at line 51 of file aig_prop.h.

References dest, and aigt::number_of_nodes().

◆ prop_solve()

resultt aig_prop_baset::prop_solve ( )
inlineoverridevirtual

Implements propt.

Reimplemented in aig_prop_solvert.

Definition at line 60 of file aig_prop.h.

References propt::P_ERROR.

◆ set_equal()

void aig_prop_baset::set_equal ( literalt  a,
literalt  b 
)
overridevirtual

asserts a==b in the propositional formula

Reimplemented from propt.

Definition at line 132 of file aig_prop.cpp.

References propt::l_set_to_true(), lequal(), lor(), neg(), and pos().

◆ solver_text()

const std::string aig_prop_baset::solver_text ( )
inlineoverridevirtual

Implements propt.

Reimplemented in aig_prop_solvert.

Definition at line 54 of file aig_prop.h.

Member Data Documentation

◆ dest

aigt& aig_prop_baset::dest
protected

Definition at line 64 of file aig_prop.h.

Referenced by land(), new_variable(), and no_variables().


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