48 squolem.options.set_freeOnExit(
true);
51 squolem.options.set_debugFilename(
"debug.qdimacs");
52 squolem.options.set_saveDebugFile(
true);
87 std::vector<Literal> buffer(
new_bv.size());
116 const quantifiert::typet type,
120 squolem.requantifyVariable(l.
var_no(), type==quantifiert::UNIVERSAL);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual void set_no_variables(size_t no)
virtual size_t no_variables() const override
mstreamt & status() const
virtual void set_no_variables(size_t no)
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual tvt l_get(literalt a) const
virtual void lcnf(const bvt &bv)
virtual size_t no_clauses() const
virtual void add_quantifier(const quantifiert &quantifier)
virtual void add_quantifier(const quantifiert &quantifier)
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
std::vector< literalt > bvt
#define UNREACHABLE
This should be used to mark dead code.