10 #ifndef CPROVER_SOLVERS_PROP_PROP_WRAPPER_H 11 #define CPROVER_SOLVERS_PROP_PROP_WRAPPER_H 22 {
return p.constant(value); }
26 {
return p.
land(a, b); }
29 {
return p.
lor(a, b); }
32 {
return p.
land(bv); }
38 {
return p.
lxor(a, b); }
41 {
return p.
lxor(bv); }
47 {
return p.
lnor(a, b); }
86 #endif // CPROVER_SOLVERS_PROP_PROP_WRAPPER_H virtual literalt new_variable()
virtual resultt prop_solve()
virtual literalt land(literalt a, literalt b)
virtual literalt lxor(literalt a, literalt b)
void lcnf(literalt l0, literalt l1)
virtual const std::string solver_text()=0
virtual literalt lselect(literalt a, literalt b, literalt c)
virtual const std::string solver_text()
virtual literalt lor(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)
virtual std::size_t no_variables() const
virtual literalt limplies(literalt a, literalt b)
virtual literalt limplies(literalt a, literalt b)=0
prop_wrappert(propt &_prop)
virtual literalt lor(const bvt &bv)
virtual literalt land(literalt a, literalt b)=0
virtual literalt constant(bool value)
virtual tvt l_get(literalt a) const
virtual literalt new_variable()=0
virtual void l_set_to(literalt a, bool value)
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 literalt lxor(const bvt &bv)
virtual void lcnf(const bvt &bv)
virtual literalt lnand(literalt a, literalt b)=0
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt lnand(literalt a, literalt b)
virtual literalt lnor(literalt a, literalt b)
virtual tvt l_get(literalt a) const =0
virtual resultt prop_solve()=0
virtual literalt lequal(literalt a, literalt b)
virtual literalt land(const bvt &bv)
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lnor(literalt a, literalt b)=0
std::vector< literalt > bvt