Go to the documentation of this file.
23 inline DdNode *DD::getNode()
const
89 return "QBF/BDD/CORE";
107 unsigned var=it->var_no;
109 if(it->type==quantifiert::typet::EXISTENTIAL)
112 std::cout <<
"BDD E: " << var <<
", " <<
113 matrix->nodeCount() <<
" nodes\n";
116 BDD *model=
new BDD();
118 *model=
matrix->AndAbstract(
128 it->type == quantifiert::typet::UNIVERSAL,
129 "only handles quantified variables");
131 std::cout <<
"BDD A: " << var <<
", " <<
132 matrix->nodeCount() <<
" nodes\n";
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);
276 if(q.
type==quantifiert::typet::UNIVERSAL)
278 INVARIANT(l.
var_no() != 0,
"input literal wasn't properly initialized");
282 it !=
variable_map.end(),
"variable not found in the variable map");
284 const exprt &sym=it->second.first;
285 unsigned index=it->second.second;
298 q.
type == quantifiert::typet::EXISTENTIAL,
299 "only quantified literals are supported");
305 std::cout <<
"CACHE HIT for " << l.
dimacs() <<
'\n';
318 "there must be a model BDD for the literal");
322 std::cout <<
"Model " << l.
var_no() <<
'\n';
323 model.PrintMinterm();
341 std::cout <<
"CUBE: ";
343 std::cout << cube[i];
366 result.move_to_operands(prime);
373 if(
result.operands().empty())
375 else if(
result.operands().size()==1)
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
std::vector< literalt > bvt
bool is_quantified(const literalt l) const
mstreamt & status() const
Unbounded, signed integers (mathematical integers, not bitvectors)
Base class for all expressions.
bool find_quantifier(const literalt l, quantifiert &q) const
virtual modeltypet m_get(literalt a) const
virtual const exprt f_get(literalt l)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
This should be used to mark dead code.
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
mstreamt & result() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
virtual const std::string solver_text()
bdd_variable_mapt bdd_variable_map
literalt const_literal(bool value)
The Boolean constant false.
virtual void lcnf(const bvt &bv)
virtual tvt l_get(literalt a) const
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Deprecated expression utility functions.
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
qbf_bdd_certificatet(void)
virtual tvt l_get(literalt a) const
void simplify_extractbits(exprt &expr) const
virtual resultt prop_solve()
virtual literalt lor(literalt a, literalt b)
variable_mapt variable_map
virtual size_t no_variables() const override
virtual bool is_in_core(literalt l) const
The Boolean constant true.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
virtual void add_quantifier(const quantifiert &quantifier)
virtual ~qbf_bdd_certificatet(void)
function_cachet function_cache
void compress_certificate(void)