10 #ifndef CPROVER_SOLVERS_PROP_AIG_PROP_H 11 #define CPROVER_SOLVERS_PROP_AIG_PROP_H 34 void lcnf(
const bvt &clause)
override { assert(
false); }
55 {
return "conversion into and-inverter graph"; }
104 "conversion into and-inverter graph followed by "+
105 solver.solver_text();
114 solver.set_message_handler(m);
122 std::vector<unsigned> &p_usage_count, std::vector<unsigned> &n_usage_count);
123 void compute_phase(std::vector<bool> &n_pos, std::vector<bool> &n_neg);
129 std::vector<unsigned> &p_usage_count,
130 std::vector<unsigned> &n_usage_count);
133 #endif // CPROVER_SOLVERS_PROP_AIG_PROP_H bool has_set_to() const override
literalt land(literalt a, literalt b) override
literalt lnor(literalt a, literalt b) override
tvt l_get(literalt a) const override
resultt prop_solve() override
void l_set_to(literalt a, bool value) override
aig_prop_solvert(propt &_solver)
aig_prop_constraintt(aig_plus_constraintst &_dest)
literalt lxor(literalt a, literalt b) override
const std::string solver_text() override
void set_equal(literalt a, literalt b) override
asserts a==b in the propositional formula
void set_message_handler(message_handlert &m) override
void l_set_to(literalt a, bool value) override
void l_set_to_true(literalt a)
aig_prop_baset(aigt &_dest)
nodest::size_type number_of_nodes() const
literalt lnand(literalt a, literalt b) override
bool cnf_handled_well() const override
size_t no_variables() const override
void lcnf(const bvt &clause) override
literalt lselect(literalt a, literalt b, literalt c) override
virtual void set_message_handler(message_handlert &_message_handler)
aig_plus_constraintst & dest
void lcnf(const bvt &clause) override
literalt lequal(literalt a, literalt b) override
bool has_set_to() const override
literalt new_variable() override
const std::string solver_text() override
literalt limplies(literalt a, literalt b) override
literalt lor(literalt a, literalt b) override
aig_plus_constraintst aig
std::vector< literalt > bvt