10 #ifndef CPROVER_SOLVERS_PROP_PROP_H 11 #define CPROVER_SOLVERS_PROP_PROP_H 77 virtual void lcnf(
const bvt &bv)=0;
116 warning() <<
"CPU limit ignored (not implemented)" <<
eom;
124 #endif // CPROVER_SOLVERS_PROP_PROP_H
void lcnf(literalt l0, literalt l1, literalt l2)
virtual void set_time_limit_seconds(uint32_t)
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
virtual void set_assumptions(const bvt &)
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)
mstreamt & warning() const
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 literalt lxor(literalt a, literalt b)=0
virtual size_t no_variables() const =0
virtual void set_variable_name(literalt, const irep_idt &)
void l_set_to_false(literalt a)
virtual void set_frozen(literalt)
virtual bool cnf_handled_well() const
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual literalt lnand(literalt a, literalt b)=0
virtual void set_assignment(literalt a, bool value)=0
virtual literalt lequal(literalt a, literalt b)=0
literalt const_literal(bool value)
virtual bool has_set_to() const
virtual bool is_in_conflict(literalt l) const =0
Returns true if an assumption is in the final conflict.
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt