45 return P_UNSATISFIABLE;
48 squolem.options.set_freeOnExit(
true);
51 squolem.options.set_debugFilename(
"debug.qdimacs");
52 squolem.options.set_saveDebugFile(
true);
65 return P_UNSATISFIABLE;
87 std::vector<Literal> buffer(new_bv.size());
91 buffer[i]=new_bv[i].dimacs();
94 while(i<new_bv.size());
104 quantifier.
type==quantifiert::UNIVERSAL);
116 const quantifiert::typet type,
120 squolem.requantifyVariable(l.
var_no(), type==quantifiert::UNIVERSAL);
virtual void lcnf(const bvt &bv)
virtual void set_no_variables(size_t no)
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
virtual const std::string solver_text()
static mstreamt & eom(mstreamt &m)
virtual size_t no_clauses() const
virtual void add_quantifier(const quantifiert &quantifier)
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
virtual void add_quantifier(const quantifiert &quantifier)
mstreamt & result() const
mstreamt & status() const
virtual void set_no_variables(size_t no)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual size_t no_variables() const override
std::vector< literalt > bvt