36 squolem->options.set_keepModelFunctions(
true);
37 squolem->options.set_keepResolutionProof(
false);
38 squolem->options.set_freeOnExit(
true);
40 squolem->options.set_debugFilename(
"debug.qdimacs");
41 squolem->options.set_saveDebugFile(
true);
42 squolem->options.set_compressModel(
true);
79 return "Squolem (Certifying)";
103 return P_UNSATISFIABLE;
142 std::vector<Literal> buffer(new_bv.size());
146 buffer[i]=new_bv[i].dimacs();
149 while(i<new_bv.size());
151 if(!
squolem->addClause(buffer))
157 squolem->quantifyVariableInner(
159 quantifier.
type==quantifiert::UNIVERSAL);
166 squolem->setLastVariable(no+1);
171 const quantifiert::typet type,
175 squolem->requantifyVariable(l.
var_no(), type==quantifiert::UNIVERSAL);
180 squolem->options.set_debugFilename(str.c_str());
196 throw "variable map error";
198 const exprt &sym=it->second.first;
199 unsigned index=it->second.second;
213 std::cout <<
"CACHE HIT for " << l.
dimacs() <<
'\n';
223 WitnessStack *wsp=
squolem->getModelFunction(Literal(l.
dimacs()));
226 if(wsp==NULL || wsp->empty())
231 else if(wsp->pSize<=wsp->nSize)
247 Clause *p=wsp->negWits;
258 for(
unsigned i=0; i<p->size; i++)
260 const Literal &lit=p->literals[i];
269 else if(clause.
operands().size()==1)
276 std::cout <<
"CLAUSE: " << clause <<
'\n';
279 operands.push_back(clause);
289 Clause *p=wsp->posWits;
300 for(
unsigned i=0; i<p->size; i++)
302 const Literal &lit=p->literals[i];
320 std::cout <<
"CUBE: " << cube <<
'\n';
323 operands.push_back(cube);
The type of an expression.
virtual const std::string solver_text()
variable_mapt variable_map
virtual void add_quantifier(const quantifiert &quantifier)
virtual modeltypet m_get(literalt a) const
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
void simplify_extractbits(exprt &expr) const
void move_to_operands(exprt &expr)
virtual ~qbf_squolem_coret()
static mstreamt & eom(mstreamt &m)
virtual void add_quantifier(const quantifiert &quantifier)
const exprt f_get_dnf(WitnessStack *wsp)
The boolean constant true.
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
API to expression classes.
virtual size_t no_clauses() const
virtual void set_no_variables(size_t no)
The boolean constant false.
Squolem Backend (with Proofs)
std::vector< exprt > operandst
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
Unbounded, signed integers.
virtual void write_qdimacs_cnf(std::ostream &out)
mstreamt & result() const
mstreamt & status() const
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
Base class for all expressions.
virtual void set_no_variables(size_t no)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual const exprt f_get(literalt l)
void set_debug_filename(const std::string &str)
function_cachet function_cache
virtual void lcnf(const bvt &bv)
virtual size_t no_variables() const override
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
const exprt f_get_cnf(WitnessStack *wsp)
std::vector< literalt > bvt
virtual bool is_in_core(literalt l) const