10 #ifndef CPROVER_SOLVERS_CVC_CVC_PROP_H 11 #define CPROVER_SOLVERS_CVC_CVC_PROP_H 48 virtual void lcnf(
const bvt &bv);
55 unsigned v=literal.
var_no();
59 return literal.
sign()?!
r:
r;
88 #endif // CPROVER_SOLVERS_CVC_CVC_PROP_H
virtual void limplies(literalt a, literalt b, literalt o)
virtual void lor(literalt a, literalt b, literalt o)
virtual void lnor(literalt a, literalt b, literalt o)
virtual void set_no_variables(size_t no)
virtual void lxor(literalt a, literalt b, literalt o)
std::vector< tvt > assignment
virtual void land(literalt a, literalt b, literalt o)
cvc_propt(std::ostream &_out)
virtual void lcnf(const bvt &bv)
literalt def_cvc_literal()
std::string cvc_literal(literalt l)
virtual void lequal(literalt a, literalt b, literalt o)
virtual const std::string solver_text()
virtual size_t no_variables() const
virtual literalt new_variable()
virtual propt::resultt prop_solve()
virtual void lnand(literalt a, literalt b, literalt o)
virtual tvt l_get(literalt literal) const
virtual literalt lselect(literalt a, literalt b, literalt c)
std::vector< literalt > bvt