38 d_commonRules(tm->getRules()),
43 d_statistics(statistics),
45 d_nullExpr(tm->getEM()->getNullExpr()),
52 if (flags[
"minimizeClauses"].getBool()) {
53 CLFlags flags = ValidityChecker::createFlags();
54 flags.
setFlag(
"minimizeClauses",
false);
55 d_vc = ValidityChecker::create(flags);
81 bool foundInCache =
false;
101 vector<Theorem> thms;
102 vector<unsigned> changed;
106 for(i = e.
begin(), iend = e.
end(); i!=iend; ++i, ++index) {
111 for(i = e.
begin(), iend = e.
end(); i!=iend; ++i, ++index) {
115 changed.push_back(index);
118 if(changed.size() > 0) {
126 if (!foundInCache)
d_iteMap[e] = thm;
157 return Lit((*iMap).second);
162 bool translateOnly =
false;
166 translateOnly =
true;
184 for (i = e.
begin(), iend = e.
end(); i != iend; ++i) {
188 vector<Expr> new_chls;
189 vector<Theorem> thms;
190 for (idx = 0; idx < lits.size(); ++idx) {
195 Expr after = (isAnd ?
Expr(
AND,new_chls) : Expr(
OR,new_chls)) ;
199 for (idx = 0; idx < lits.size(); ++idx) {
206 std::string reasonStr = (isAnd ?
"and_mid" :
"or_mid");
213 for (idx = 0; idx < lits.size(); ++idx) {
217 std::string reasonStr = (isAnd ?
"and_final" :
"or_final") ;
220 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
227 vector<Theorem> thms;
258 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
268 vector<Theorem> thms;
304 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
316 vector<Theorem> thms;
352 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
368 after.push_back(aftere0);
369 after.push_back(aftere1);
370 after.push_back(aftere2);
384 vector<Theorem> thms ;
385 thms.push_back(e0thm);
386 thms.push_back(e1thm);
387 thms.push_back(e2thm);
432 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
438 "Corrupted Varinfo");
444 DebugAssert(!
d_flags[
"cnf-formula"].getBool(),
"Found impossible case when cnf-formula is enabled");
463 "Expected existing literal");
475 if (!translateOnly) {
501 for (i = e.
begin(), iend = e.
end(); i != iend; ++i) {
504 if (!translateOnly)
d_varInfo[v].fanins.push_back(l);
543 if (!translateOnly)
d_varInfo[v].fanins.push_back(l);
553 newLits.push_back(lb);
556 unsigned new_lb = (ub-lb+1)/2 + lb;
560 for (index = new_lb; index <= ub; ++index) {
566 cons(new_lb, ub, e2, newLits);
570 unsigned new_ub = new_lb-1;
572 for (index = lb; index <= new_ub; ++index) {
578 cons(lb, new_ub, e2, newLits);
582 cons(new_lb, ub, e2, newLits);
585 for (index = 0; index < newLits.size(); ++index) {
588 cons(lb, new_ub, e2, newLits);
596 vector<Theorem> clauses;
600 vector<Theorem>::iterator i = clauses.begin(), iend = clauses.end();
601 for (; i < iend; ++i) {
604 Expr e = (*i).getExpr();
625 if (
d_flags[
"cnf-formula"].getBool()) {
630 "expr:" + e.
toString() +
" is not an OR Expr or Ture or False" );
633 for (
int i = 0; i < e.
arity(); i++){
677 vector<Theorem> clauses;
679 DebugAssert(clauses.size() == 1,
"expected single clause");
std::deque< bool > d_translateQueueFlags
Whether thm to translate is "translate only".
Abstract proof rules for CNF conversion.
iterator begin() const
Begin iterator.
bool isAtomic() const
Test if e is atomic.
Data structure of expressions in CVC3.
Generic API for a validity checker.
virtual Theorem CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0
std::vector< Varinfo > d_varInfo
vector that maps a variable index to information for that variable
virtual void learnedClauses(const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0
Learned clause rule: .
void setFlag(const std::string &name, const CLFlag &f)
Lit translateExpr(const CVC3::Theorem &thmIn, CNF_Formula &cnf)
Recursively translate e into cnf.
void setClauseTheorem(CVC3::Theorem thm)
bool isTranslated() const
std::deque< CVC3::Theorem > d_translateQueueThms
Queue of theorems to translate.
virtual void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)=0
Register an atom.
Lit translateExprRec(const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn)
Recursively translate e into cnf.
bool isAbsAtomicFormula() const
An abstract atomic formua is an atomic formula or a quantified formula.
virtual Theorem reflexivityRule(const Expr &a)=0
#define DebugAssert(cond, str)
void registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)
Register a new atomic formula.
Lit getCNFLit(const CVC3::Expr &e)
Look up the CNF literal for an Expr.
CVC3::ExprHashMap< CVC3::Theorem > d_iteMap
Cached translation of term-ite-containing expressions.
CVC3::Theorem replaceITErec(const CVC3::Expr &e, Var v, bool translateOnly)
Recursively traverse an expression with an embedded term ITE.
virtual void push()=0
Checkpoint the current context and increase the scope level.
void cons(unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits)
virtual Theorem CNFAddUnit(const Theorem &thm)=0
Expr impExpr(const Expr &right) const
virtual void pop()=0
Restore the current context to its state at the last checkpoint.
virtual Theorem ifLiftRule(const Expr &e, int itePos)=0
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
Information kept for each CNF variable.
virtual Theorem CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0
CNFCallback * d_cnfCallback
Instance of CNF_CallBack: must be registered.
virtual Theorem substitutivityRule(const Expr &e, const Theorem &thm)=0
Optimized case for expr with one child.
CVC3::Theorem concreteThm(const CVC3::Expr &e)
Return the theorem if e is not as concreteExpr(e).
std::string toString() const
Print the expression to a string.
CVC3::ExprHashMap< Var > d_cnfVars
Map from Exprs to Vars representing those Exprs.
Expr iffExpr(const Expr &right) const
virtual void assertFormula(const Expr &e)=0
Assert a new formula in the current context.
std::deque< Var > d_translateQueueVars
Queue of fanouts corresponding to thms to translate.
virtual Theorem CNFConvert(const Expr &e, const Theorem &thm)=0
const Expr & getRHS() const
CVC3::CNF_Rules * createProofRules(CVC3::TheoremManager *tm, const CVC3::CLFlags &)
virtual QueryResult query(const Expr &e)=0
Check validity of e in the current context.
CVC3::ValidityChecker * d_vc
For clause minimization.
Manager for conversion to and traversal of CNF formulas.
bool isUserRegisteredAtom() const
void setTranslated(int scope=-1) const
Set the translated flag for this Expr.
CVC3::CommonProofRules * d_commonRules
Common proof rules.
virtual Expr falseExpr()=0
Return FALSE Expr.
bool isRegisteredAtom() const
CVC3::Expr concreteLit(Lit l, bool checkTranslated=true)
Convert a CNF literal to an Expr literal.
iterator find(const Expr &e)
Expr xorExpr(const Expr &right) const
const CVC3::CLFlags & d_flags
Reference to command-line flags.
virtual Theorem iffMP(const Theorem &e1, const Theorem &e1_iff_e2)=0
CVC3::Expr concreteExpr(const CVC3::Expr &e, const Lit &literal)
Return the expr corresponding to the literal unless the expr is TRUE of FALSE.
int d_bottomScope
Whether expr has already been translated.
void convertLemma(const CVC3::Theorem &thm, CNF_Formula &cnf)
Convert thm A |- B (A is a set of literals) into one or more clauses.
Type getType() const
Get the type. Recursively compute if necessary.
CVC3::CNF_Rules * d_rules
Rules for manipulating CNF.
virtual Theorem symmetryRule(const Theorem &a1_eq_a2)=0
(same for IFF)
virtual Theorem varIntroSkolem(const Expr &e)=0
Retrun a theorem "|- e = v" for a new Skolem constant v.
Lit addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf)
Given thm of form A |- B, convert B to CNF and add it to cnf.
Lit addLemma(CVC3::Theorem thm, CNF_Formula &cnf)
Convert thm to CNF and add it to the current formula.
iterator end() const
End iterator.