cprover
|
#include <aig_prop.h>
Public Member Functions | |
aig_prop_solvert (propt &_solver) | |
const std::string | solver_text () override |
tvt | l_get (literalt a) const override |
resultt | prop_solve () override |
void | set_message_handler (message_handlert &m) override |
![]() | |
aig_prop_constraintt (aig_plus_constraintst &_dest) | |
bool | has_set_to () const override |
void | lcnf (const bvt &clause) override |
void | l_set_to (literalt a, bool value) override |
![]() | |
aig_prop_baset (aigt &_dest) | |
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 |
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... | |
literalt | new_variable () override |
size_t | no_variables () const override |
![]() | |
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 irep_idt &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) |
virtual void | set_time_limit_seconds (uint32_t lim) |
Public Attributes | |
aig_plus_constraintst | aig |
![]() | |
aig_plus_constraintst & | dest |
Protected Member Functions | |
void | convert_aig () |
void | usage_count (std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count) |
Compact encoding for single usage variable. More... | |
void | compute_phase (std::vector< bool > &n_pos, std::vector< bool > &n_neg) |
Compute the phase information needed for Plaisted-Greenbaum encoding. More... | |
void | convert_node (unsigned n, const aigt::nodet &node, bool n_pos, bool n_neg, std::vector< unsigned > &p_usage_count, std::vector< unsigned > &n_usage_count) |
Convert one AIG node, including special handling of a couple of cases. More... | |
Protected Attributes | |
propt & | solver |
![]() | |
aigt & | dest |
![]() | |
bvt | lcnf_bv |
Additional Inherited Members | |
![]() | |
enum | resultt { resultt::P_SATISFIABLE, resultt::P_UNSATISFIABLE, resultt::P_ERROR } |
Definition at line 90 of file aig_prop.h.
|
inlineexplicit |
Definition at line 93 of file aig_prop.h.
|
protected |
Compute the phase information needed for Plaisted-Greenbaum encoding.
Definition at line 164 of file aig_prop.cpp.
References aig_nodet::a, aig, aig_nodet::b, aig_plus_constraintst::constraints, messaget::eom(), aig_nodet::is_and(), literalt::is_constant(), aigt::nodes, literalt::sign(), messaget::statistics(), and literalt::var_no().
Referenced by convert_aig().
|
protected |
Definition at line 551 of file aig_prop.cpp.
References aig, compute_phase(), aig_plus_constraintst::constraints, convert_node(), propt::l_set_to(), propt::new_variable(), propt::no_variables(), aigt::nodes, solver, and usage_count().
Referenced by prop_solve().
|
protected |
Convert one AIG node, including special handling of a couple of cases.
Definition at line 340 of file aig_prop.cpp.
References aig_nodet::a, aig, aig_nodet::b, forall_literals, aig_nodet::is_and(), propt::lcnf(), neg(), aigt::nodes, pos(), literalt::sign(), size_type(), solver, and literalt::var_no().
Referenced by convert_aig().
Reimplemented from aig_prop_baset.
Definition at line 147 of file aig_prop.cpp.
References propt::l_get(), and solver.
|
overridevirtual |
Reimplemented from aig_prop_baset.
Definition at line 152 of file aig_prop.cpp.
References aig, convert_aig(), messaget::eom(), aigt::nodes, propt::prop_solve(), solver, and messaget::status().
|
inlineoverridevirtual |
Reimplemented from messaget.
Definition at line 111 of file aig_prop.h.
References messaget::set_message_handler(), and solver.
|
inlineoverridevirtual |
Reimplemented from aig_prop_baset.
Definition at line 101 of file aig_prop.h.
References solver, and propt::solver_text().
|
protected |
Compact encoding for single usage variable.
Definition at line 229 of file aig_prop.cpp.
References aig_nodet::a, aig, aig_nodet::b, aig_plus_constraintst::constraints, messaget::eom(), aig_nodet::is_and(), aigt::nodes, literalt::sign(), messaget::statistics(), and literalt::var_no().
Referenced by convert_aig().
aig_plus_constraintst aig_prop_solvert::aig |
Definition at line 99 of file aig_prop.h.
Referenced by compute_phase(), convert_aig(), convert_node(), prop_solve(), and usage_count().
|
protected |
Definition at line 118 of file aig_prop.h.
Referenced by convert_aig(), convert_node(), l_get(), prop_solve(), set_message_handler(), and solver_text().