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);
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;
201 exprt extract_expr(ID_extractbit,
typet(ID_bool));
203 typet uint_type(ID_unsignedbv);
204 uint_type.
set(ID_width, 32);
217 std::cout <<
"CACHE HIT for " << l.
dimacs() <<
'\n';
227 WitnessStack *wsp=
squolem->getModelFunction(Literal(l.
dimacs()));
230 if(wsp==NULL || wsp->empty())
235 else if(wsp->pSize<=wsp->nSize)
251 Clause *p=wsp->negWits;
262 for(
unsigned i=0; i<p->size; i++)
264 const Literal &lit=p->literals[i];
273 else if(clause.
operands().size()==1)
280 std::cout <<
"CLAUSE: " << clause <<
'\n';
283 operands.push_back(clause);
293 Clause *p=wsp->posWits;
304 for(
unsigned i=0; i<p->size; i++)
306 const Literal &lit=p->literals[i];
324 std::cout <<
"CUBE: " << cube <<
'\n';
327 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 copy_to_operands(const exprt &expr)
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)
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)
virtual void write_qdimacs_cnf(std::ostream &out)
virtual resultt prop_solve()
virtual tvt l_get(literalt a) const
Base class for all expressions.
virtual void set_no_variables(size_t no)
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
const exprt f_get_cnf(WitnessStack *wsp)
std::vector< literalt > bvt
virtual bool is_in_core(literalt l) const
void set(const irep_namet &name, const irep_idt &value)