24 inline DdNode *DD::getNode()
const 91 return "QBF/BDD/CORE";
99 << std::to_string(
matrix->nodeCount()) <<
" nodes" <<
eom;
109 unsigned var=it->var_no;
111 if(it->type==quantifiert::typet::EXISTENTIAL)
114 std::cout <<
"BDD E: " << var <<
", " <<
115 matrix->nodeCount() <<
" nodes\n";
118 BDD *model=
new BDD();
120 *model=
matrix->AndAbstract(
127 else if(it->type==quantifiert::typet::UNIVERSAL)
130 std::cout <<
"BDD A: " << var <<
", " <<
131 matrix->nodeCount() <<
" nodes\n";
137 throw "unquantified variable";
169 BDD &var=*(
new BDD());
244 status() <<
"Compressing Certificate" <<
eom;
248 if(it->type==quantifiert::typet::EXISTENTIAL)
261 model2=model2.AndAbstract(~var, var);
263 model2=model2.AndAbstract(var, var);
274 throw "no model for unquantified variable";
277 if(q.
type==quantifiert::typet::UNIVERSAL)
283 throw "variable map error";
285 const exprt &sym=it->second.first;
286 unsigned index=it->second.second;
288 exprt extract_expr(ID_extractbit,
typet(ID_bool));
291 typet uint_type(ID_unsignedbv);
292 uint_type.
set(ID_width, 32);
303 assert(q.
type==quantifiert::typet::EXISTENTIAL);
309 std::cout <<
"CACHE HIT for " << l.
dimacs() <<
'\n';
324 std::cout <<
"Model " << l.
var_no() <<
'\n';
325 model.PrintMinterm();
343 std::cout <<
"CUBE: ";
345 std::cout << cube[i];
368 result.move_to_operands(prime);
375 if(
result.operands().empty())
377 else if(
result.operands().size()==1)
The type of an expression.
virtual bool is_in_core(literalt l) const
variable_mapt variable_map
virtual void lcnf(const bvt &bv)
virtual resultt prop_solve()
virtual const std::string solver_text()
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses ...
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
void simplify_extractbits(exprt &expr) const
virtual tvt l_get(literalt a) const
void copy_to_operands(const exprt &expr)
void move_to_operands(exprt &expr)
bool is_quantified(const literalt l) const
qbf_bdd_certificatet(void)
static mstreamt & eom(mstreamt &m)
virtual literalt lor(literalt a, literalt b)
virtual void add_quantifier(const quantifiert &quantifier)
virtual tvt l_get(literalt a) const
virtual modeltypet m_get(literalt a) const
bdd_variable_mapt bdd_variable_map
The boolean constant true.
API to expression classes.
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
function_cachet function_cache
virtual ~qbf_bdd_certificatet(void)
bool find_quantifier(const literalt l, quantifiert &q) const
The boolean constant false.
literalt const_literal(bool value)
Base class for all expressions.
void compress_certificate(void)
virtual const exprt f_get(literalt l)
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual size_t no_variables() const override
std::vector< literalt > bvt
void set(const irep_namet &name, const irep_idt &value)