23 std::vector<bool> quantified;
27 for(quantifierst::const_iterator
36 assert(!quantified[quantifier.
var_no]);
37 quantified[quantifier.
var_no]=
true;
39 switch(quantifier.
type)
53 out <<
" " << quantifier.
var_no <<
" 0\n";
61 out <<
"e " << i <<
" 0\n";
90 for(quantifierst::const_iterator
96 for(clausest::const_iterator
107 for(quantifierst::const_iterator it=
quantifiers.begin();
117 for(quantifierst::const_iterator it=
quantifiers.begin();
120 if(it->var_no==l.
var_no())
128 for(quantifierst::const_iterator it=
quantifiers.begin();
131 if(it->var_no==l.
var_no())
void write_prefix(std::ostream &out) const
bool is_quantified(const literalt l) const
void write_clauses(std::ostream &out)
virtual void add_quantifier(const quantifiert &quantifier)
bool operator==(const qdimacs_cnft &other) const
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual void lcnf(const bvt &bv)
bool find_quantifier(const literalt l, quantifiert &q) const
mstreamt & result() const
virtual void set_no_variables(size_t no)
void write_problem_line(std::ostream &out)
void copy_to(qdimacs_cnft &cnf) const
virtual size_t no_variables() const override
virtual void write_qdimacs_cnf(std::ostream &out)