10 #ifndef CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H 11 #define CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H 49 virtual void lcnf(
const bvt &bv);
56 unsigned v=literal.
var_no();
60 return literal.
sign()?!r:
r;
91 #endif // CPROVER_SOLVERS_DPLIB_DPLIB_PROP_H virtual void lnand(literalt a, literalt b, literalt o)
virtual const std::string solver_text()
virtual tvt l_get(literalt literal) const
virtual propt::resultt prop_solve()
std::string dplib_literal(literalt l)
virtual void set_no_variables(size_t no)
virtual size_t no_variables() const
virtual void lcnf(const bvt &bv)
virtual literalt new_variable()
std::vector< tvt > assignment
virtual void land(literalt a, literalt b, literalt o)
virtual void limplies(literalt a, literalt b, literalt o)
dplib_propt(std::ostream &_out)
literalt def_dplib_literal()
virtual void lnor(literalt a, literalt b, literalt o)
virtual void lequal(literalt a, literalt b, literalt o)
virtual literalt lselect(literalt a, literalt b, literalt c)
virtual void lor(literalt a, literalt b, literalt o)
std::vector< literalt > bvt
virtual void lxor(literalt a, literalt b, literalt o)