10 #ifndef CPROVER_SOLVERS_PROP_PROP_H 11 #define CPROVER_SOLVERS_PROP_PROP_H 75 virtual void lcnf(
const bvt &bv)=0;
116 #endif // CPROVER_SOLVERS_PROP_PROP_H
void lcnf(literalt l0, literalt l1, literalt l2)
virtual void set_frozen(literalt a)
virtual bool has_is_in_conflict() const
void lcnf(literalt l0, literalt l1)
virtual const std::string solver_text()=0
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt lor(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1, literalt l2, literalt l3)
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
virtual bool has_set_assumptions() const
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
virtual void l_set_to(literalt a, bool value)
virtual void set_variable_name(literalt a, const std::string &name)
virtual literalt lxor(literalt a, literalt b)=0
virtual size_t no_variables() const =0
virtual void set_assignment(literalt a, bool value)
void l_set_to_false(literalt a)
virtual bool cnf_handled_well() const
virtual void set_assumptions(const bvt &_assumptions)
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
literalt const_literal(bool value)
virtual bool has_set_to() const
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bool is_in_conflict(literalt l) const
virtual void copy_assignment_from(const propt &prop)
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt