23 inline DdNode *DD::getNode()
const 90 return "QBF/BDD/CORE";
108 unsigned var=it->var_no;
110 if(it->type==quantifiert::typet::EXISTENTIAL)
113 std::cout <<
"BDD E: " << var <<
", " <<
114 matrix->nodeCount() <<
" nodes\n";
117 BDD *model=
new BDD();
119 *model=
matrix->AndAbstract(
126 else if(it->type==quantifiert::typet::UNIVERSAL)
129 std::cout <<
"BDD A: " << var <<
", " <<
130 matrix->nodeCount() <<
" nodes\n";
136 throw "unquantified variable";
168 BDD &var=*(
new BDD());
243 status() <<
"Compressing Certificate" <<
eom;
247 if(it->type==quantifiert::typet::EXISTENTIAL)
260 model2=model2.AndAbstract(~var, var);
262 model2=model2.AndAbstract(var, var);
273 throw "no model for unquantified variable";
276 if(q.
type==quantifiert::typet::UNIVERSAL)
282 throw "variable map error";
284 const exprt &sym=it->second.first;
285 unsigned index=it->second.second;
297 assert(q.
type==quantifiert::typet::EXISTENTIAL);
303 std::cout <<
"CACHE HIT for " << l.
dimacs() <<
'\n';
318 std::cout <<
"Model " << l.
var_no() <<
'\n';
319 model.PrintMinterm();
337 std::cout <<
"CUBE: ";
339 std::cout << cube[i];
362 result.move_to_operands(prime);
369 if(
result.operands().empty())
371 else if(
result.operands().size()==1)
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()
Deprecated expression utility functions.
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 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.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
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.
Unbounded, signed integers.
literalt const_literal(bool value)
mstreamt & result() const
mstreamt & status() const
Base class for all expressions.
void compress_certificate(void)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
std::vector< literalt > bvt