From 39b707ad22813c184da61c3e2337359ca8061797 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 30 Jan 2010 02:22:25 +0000 Subject: [PATCH] cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases --- src/expr/node_builder.h | 72 +++++-- src/parser/antlr_parser.cpp | 2 +- src/prop/prop_engine.cpp | 52 +++-- src/prop/prop_engine.h | 8 +- src/smt/cnf_converter.cpp | 407 ++++++++++++++++++++++++++---------- src/smt/cnf_converter.h | 46 ++-- src/smt/smt_engine.h | 2 +- src/util/options.h | 2 +- 8 files changed, 428 insertions(+), 163 deletions(-) diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 7c6405ace..77ff05ab5 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -125,10 +125,21 @@ public: return d_ev->ev_end(); } + Kind getKind() const { + return d_ev->getKind(); + } + unsigned getNumChildren() const { return d_ev->getNumChildren(); } + Node operator[](int i) const { + Assert(i >= 0 && i < d_ev->getNumChildren()); + return Node(d_ev->d_children[i]); + } + + void clear(Kind k = UNDEFINED_KIND); + // Compound expression constructors /* NodeBuilder& eqExpr(const Node& right); @@ -372,6 +383,7 @@ namespace CVC4 { template inline NodeBuilder::NodeBuilder() : d_size(nchild_thresh), + d_hash(0), d_nm(NodeManager::currentNM()), d_used(false), d_ev(&d_inlineEv), @@ -381,6 +393,7 @@ inline NodeBuilder::NodeBuilder() : template inline NodeBuilder::NodeBuilder(Kind k) : d_size(nchild_thresh), + d_hash(0), d_nm(NodeManager::currentNM()), d_used(false), d_ev(&d_inlineEv), @@ -394,6 +407,7 @@ inline NodeBuilder::NodeBuilder(Kind k) : template inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : d_size(nchild_thresh), + d_hash(0), d_nm(nb.d_nm), d_used(nb.d_used), d_ev(&d_inlineEv), @@ -402,16 +416,19 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& if(evIsAllocated(nb)) { realloc(nb.d_size, false); - std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin()); + std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_ev->ev_begin()); } else { - std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin()); + std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_inlineEv.ev_begin()); } + d_ev->d_kind = nb.d_ev->d_kind; + d_ev->d_nchildren = nb.d_ev->d_nchildren; } template template inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : d_size(nchild_thresh), + d_hash(0), d_nm(NodeManager::currentNM()), d_used(nb.d_used), d_ev(&d_inlineEv), @@ -420,15 +437,18 @@ inline NodeBuilder::NodeBuilder(const NodeBuilder& nb) : if(nb.d_ev->d_nchildren > nchild_thresh) { realloc(nb.d_size, false); - std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_ev->begin()); + std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_ev->ev_begin()); } else { - std::copy(nb.d_ev->begin(), nb.d_ev->end(), d_inlineEv.begin()); + std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_inlineEv.ev_begin()); } + d_ev->d_kind = nb.d_ev->d_kind; + d_ev->d_nchildren = nb.d_ev->d_nchildren; } template inline NodeBuilder::NodeBuilder(NodeManager* nm) : d_size(nchild_thresh), + d_hash(0), d_nm(nm), d_used(false), d_ev(&d_inlineEv), @@ -438,6 +458,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm) : template inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : d_size(nchild_thresh), + d_hash(0), d_nm(nm), d_used(false), d_ev(&d_inlineEv), @@ -450,19 +471,42 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : template inline NodeBuilder::~NodeBuilder() { - Assert(d_used, "NodeBuilder unused at destruction"); + if(!d_used) { + Warning("NodeBuilder unused at destruction\n"); - return; - /* - for(iterator i = d_ev->ev_begin(); - i != d_ev->ev_end(); - ++i) { - (*i)->dec(); + for(iterator i = d_ev->ev_begin(); + i != d_ev->ev_end(); + ++i) { + (*i)->dec(); + } + if(evIsAllocated()) { + free(d_ev); + } } - if(evIsAllocated()) { - free(d_ev); +} + +template +void NodeBuilder::clear(Kind k) { + if(!d_used) { + Warning("NodeBuilder unused at clear\n"); + + for(iterator i = d_ev->ev_begin(); + i != d_ev->ev_end(); + ++i) { + (*i)->dec(); + } + if(evIsAllocated()) { + free(d_ev); + } } - */ + + d_size = nchild_thresh; + d_hash = 0; + d_nm = NodeManager::currentNM(); + d_used = false; + d_ev = &d_inlineEv; + d_inlineEv.d_kind = k; + d_inlineEv.d_nchildren = 0; } template diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index dd052ca2e..b7361eb0f 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -47,7 +47,7 @@ unsigned AntlrParser::getPrecedence(Kind kind) { case AND: return 5; default: - Unhandled ("Undefined precedence - necessary for proper parsing of CVC files!"); + Unhandled("Undefined precedence - necessary for proper parsing of CVC files!"); } return 0; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 16b807904..bc46e39d5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -30,21 +30,21 @@ using namespace std; namespace CVC4 { PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) : - d_de(de), d_te(te), d_sat() { + d_de(de), d_te(te) { } -void PropEngine::addVars(Node e) { +void PropEngine::addVars(SimpSolver* minisat, map* vars, map* varsReverse, Node e) { Debug("prop") << "adding vars to " << e << endl; for(Node::iterator i = e.begin(); i != e.end(); ++i) { Debug("prop") << "expr " << *i << endl; if((*i).getKind() == VARIABLE) { - if(d_vars.find(*i) == d_vars.end()) { - Var v = d_sat.newVar(); + if(vars->find(*i) == vars->end()) { + Var v = minisat->newVar(); Debug("prop") << "adding var " << *i << " <--> " << v << endl; - d_vars.insert(make_pair(*i, v)); - d_varsReverse.insert(make_pair(v, *i)); - } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl; - } else addVars(*i); + (*vars).insert(make_pair(*i, v)); + (*varsReverse).insert(make_pair(v, *i)); + } else Debug("prop") << "using var " << *i << " <--> " << (*vars)[*i] << endl; + } else addVars(minisat, vars, varsReverse, *i); } } @@ -110,35 +110,41 @@ static void doClause(SimpSolver* minisat, map* vars, map* } void PropEngine::solve(Node e) { + // FIXME: when context mgr comes online, keep the solver around + // between solve() calls if we can + CVC4::prop::minisat::SimpSolver sat; + std::map vars; + std::map varsReverse; + Debug("prop") << "SOLVING " << e << endl; - addVars(e); + addVars(&sat, &vars, &varsReverse, e); if(e.getKind() == AND) { Debug("prop") << "AND" << endl; for(Node::iterator i = e.begin(); i != e.end(); ++i) - doClause(&d_sat, &d_vars, &d_varsReverse, *i); - } else doClause(&d_sat, &d_vars, &d_varsReverse, e); + doClause(&sat, &vars, &varsReverse, *i); + } else doClause(&sat, &vars, &varsReverse, e); - d_sat.verbosity = 1; - bool result = d_sat.solve(); + sat.verbosity = 1; + bool result = sat.solve(); Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl; if(result) { Notice() << "model:" << endl; - for(int i = 0; i < d_sat.model.size(); ++i) - Notice() << " " << toInt(d_sat.model[i]); + for(int i = 0; i < sat.model.size(); ++i) + Notice() << " " << toInt(sat.model[i]); Notice() << endl; - for(int i = 0; i < d_sat.model.size(); ++i) - Notice() << " " << d_varsReverse[i] << " is " - << (d_sat.model[i] == l_False ? "FALSE" : - (d_sat.model[i] == l_Undef ? "UNDEF" : + for(int i = 0; i < sat.model.size(); ++i) + Notice() << " " << varsReverse[i] << " is " + << (sat.model[i] == l_False ? "FALSE" : + (sat.model[i] == l_Undef ? "UNDEF" : "TRUE")) << endl; } else { Notice() << "conflict:" << endl; - for(int i = 0; i < d_sat.conflict.size(); ++i) - Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]); + for(int i = 0; i < sat.conflict.size(); ++i) + Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << var(sat.conflict[i]); Notice() << " [["; - for(int i = 0; i < d_sat.conflict.size(); ++i) - Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])]; + for(int i = 0; i < sat.conflict.size(); ++i) + Notice() << " " << (sign(sat.conflict[i]) ? "-" : "") << varsReverse[var(sat.conflict[i])]; Notice() << " ]] " << endl; } } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6cb818d10..6e1f8cb61 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -35,11 +35,11 @@ namespace CVC4 { class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; - CVC4::prop::minisat::SimpSolver d_sat; - std::map d_vars; - std::map d_varsReverse; + //CVC4::prop::minisat::SimpSolver d_sat; + //std::map d_vars; + //std::map d_varsReverse; - void addVars(Node); + void addVars(CVC4::prop::minisat::SimpSolver*, std::map*, std::map*, Node); public: /** diff --git a/src/smt/cnf_converter.cpp b/src/smt/cnf_converter.cpp index c94d62524..7c53e9b04 100644 --- a/src/smt/cnf_converter.cpp +++ b/src/smt/cnf_converter.cpp @@ -22,7 +22,6 @@ namespace CVC4 { namespace smt { - static void printAST(std::ostream& out, const Node& n, int indent = 0) { for(int i = 0; i < indent; ++i) { out << " "; @@ -46,8 +45,33 @@ static void printAST(std::ostream& out, const Node& n, int indent = 0) { out << ")" << std::endl; } - Node CnfConverter::convert(const Node& e) { + if(d_conversion == CNF_DIRECT_EXPONENTIAL) { + return doConvert(e, NULL); + } + + NodeBuilder<> b(AND); + Node f = doConvert(e, &b); + + Debug("cnf") << "side conditions are:\n"; + NodeBuilder<> c = b; + printAST(Debug("cnf"), c); + + if(f.getKind() == AND) { + for(Node::iterator i = f.begin(); i != f.end(); ++i) { + Debug("cnf") << "adding condition:\n"; + printAST(Debug("cnf"), *i); + b << *i; + } + } else { + Debug("cnf") << "adding condition:\n"; + printAST(Debug("cnf"), f); + b << f; + } + return b; +} + +Node CnfConverter::doConvert(const Node& e, NodeBuilder<>* sideConditions) { Node n; if(conversionMapped(e)) { @@ -55,12 +79,22 @@ Node CnfConverter::convert(const Node& e) { n = getConversionMap(e); } else { switch(d_conversion) { + case CNF_DIRECT_EXPONENTIAL: - n = directConvert(e); + Debug("cnf") << "direct conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl; + n = directConvert(e, sideConditions); break; - case CNF_VAR_INTRODUCTION: - n = varIntroductionConvert(e); + + case CNF_VAR_INTRODUCTION: { + Debug("cnf") << "var-intro conversion for " << e << " with id " << e.getId() << " is being computed!" << std::endl; + std::vector v; + n = varIntroductionConvert(e, sideConditions); + Debug("cnf") << "got" << std::endl; + printAST(Debug("cnf"), n); + break; + } + default: Unhandled(d_conversion); } @@ -80,153 +114,316 @@ Node CnfConverter::convert(const Node& e) { return n; } -Node CnfConverter::compressNOT(const Node& e) { +Node CnfConverter::compressNOT(const Node& e, NodeBuilder<>* sideConditions) { Assert(e.getKind() == NOT); + Node f = doConvert(e[0], sideConditions); + + Debug("stari") << "compress-not " << e.getId() << "\n"; + // short-circuit trivial NOTs - if(e[0].getKind() == TRUE) { + if(f.getKind() == TRUE) { return d_nm->mkNode(FALSE); - } else if(e[0].getKind() == FALSE) { + } else if(f.getKind() == FALSE) { return d_nm->mkNode(TRUE); - } else if(e[0].getKind() == NOT) { - return convert(e[0][0]); - } else { - Node f = convert(e[0]); - // push NOTs inside of ANDs and ORs - if(f.getKind() == AND) { - NodeBuilder<> n(OR); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } + } else if(f.getKind() == NOT) { + return doConvert(f[0], sideConditions); + } else if(f.getKind() == AND) { + Debug("stari") << "not-converting a NOT AND\nstarted with\n"; + printAST(Debug("stari"), e[0]); + Debug("stari") << "now have\n"; + printAST(Debug("stari"), f); + NodeBuilder<> n(OR); + for(Node::iterator i = f.begin(); i != f.end(); ++i) { + if((*i).getKind() == NOT) { + n << (*i)[0]; + } else { + n << d_nm->mkNode(NOT, *i); } - return n; } - if(f.getKind() == OR) { - NodeBuilder<> n(AND); - for(Node::iterator i = f.begin(); i != f.end(); ++i) { - if((*i).getKind() == NOT) { - n << (*i)[0]; - } else { - n << d_nm->mkNode(NOT, *i); - } + return n; + } else if(f.getKind() == OR) { + NodeBuilder<> n(AND); + for(Node::iterator i = f.begin(); i != f.end(); ++i) { + if((*i).getKind() == NOT) { + n << (*i)[0]; + } else { + n << d_nm->mkNode(NOT, *i); } - return n; } - return e; + return n; + } else { + return d_nm->mkNode(NOT, f); } } -Node CnfConverter::directConvert(const Node& e) { - if(e.getKind() == NOT) { - return compressNOT(e); - } else if(e.getKind() == AND) { - return flatten(e); - } else if(e.getKind() == OR) { - Node n = flatten(e); +Node CnfConverter::directConvert(const Node& e, NodeBuilder<>* sideConditions) { + switch(e.getKind()) { + + case NOT: + return compressNOT(e, sideConditions); + + case AND: + return flatten(e, sideConditions); + + case OR: { + Node n = flatten(e, sideConditions); NodeBuilder<> m(OR); - directOrHelper(n.begin(), n.end(), m); + Debug("dor") << "calling directOrHelper on\n"; + printAST(Debug("dor"), n); + directOrHelper(n.begin(), n.end(), m, sideConditions); return m; } - return e; + case IMPLIES: { + Assert( e.getNumChildren() == 2 ); + // just turn x IMPLIES y into (NOT x) OR y + Node x = doConvert(e[0], sideConditions); + Node y = doConvert(e[1], sideConditions); + return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions); + } + + case IFF: + if(e.getNumChildren() == 2) { + // common case: + // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) + Node x = doConvert(e[0], sideConditions); + Node y = doConvert(e[1], sideConditions); + Node r = d_nm->mkNode(OR, + doConvert(d_nm->mkNode(AND, x, y), sideConditions), + doConvert(d_nm->mkNode(AND, + doConvert(d_nm->mkNode(NOT, x), sideConditions), + doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); + Debug("cnf") << "working on an IFF\n"; + printAST(Debug("cnf"), e); + Debug("cnf") << "which is\n"; + printAST(Debug("cnf"), r); + return doConvert(r, sideConditions); + } else { + // more than 2 children: + // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ... + Node::iterator i = e.begin(); + Node x = doConvert(*i++, sideConditions); + NodeBuilder<> r(AND); + while(i != e.end()) { + Node y = doConvert(*i++, sideConditions); + // now we just have two: + // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) + r << d_nm->mkNode(OR, + doConvert(d_nm->mkNode(AND, x, y), sideConditions), + doConvert(d_nm->mkNode(AND, + doConvert(d_nm->mkNode(NOT, x), sideConditions), + doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); + x = y; + } + return doConvert(r, sideConditions); + } + + case XOR: + Assert( e.getNumChildren() == 2 ); + // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y) + return doConvert(d_nm->mkNode(OR, + d_nm->mkNode(AND, + e[0], + d_nm->mkNode(NOT, e[1])), + d_nm->mkNode(AND, + d_nm->mkNode(NOT, e[0]), + e[1])), sideConditions); + + default: + // variable or theory atom + return e; + } } -void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result) { +/** + * OR: all ORs and NOTs + * -- do nothing + * + * find an AND. + * prefix: a \/ b \/ c + * and term: d /\ e + * rest: f \/ g \/ h + * + * construct: prefix \/ child + * + * then, process rest. + * + * if rest has no additional ANDs + * then I get prefix \/ child \/ rest + * and I do same with other children + * + * if rest has additional ANDs + * then I get (prefix \/ child \/ rest'1) /\ (prefix \/ child \/ rest'2) /\ ... + * and I do same with other children + */ +void CnfConverter::directOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>* sideConditions) { + static int nextID = 0; + int ID = ++nextID; + Debug("dor") << "beginning of directOrHelper " << ID << "\n"; + while(p != end) { - if((*p).getKind() == AND) { - Debug("cnf") << "orHelper: p " << *p << std::endl; - Debug("cnf") << " end " << std::endl; - Debug("cnf") << " result " << result << std::endl; + // for each child of the expression: + + Debug("dor") << "CHILD == directOrHelper " << ID << "\n"; + printAST(Debug("dor"), *p); + + // convert the child first + Node n = doConvert(*p, sideConditions); + + Debug("dor") << "CNV CHILD == directOrHelper " << ID << "\n"; + printAST(Debug("dor"), *p); + + // if the child is an AND + if(n.getKind() == AND) { + Debug("dor") << "directOrHelper found AND " << ID << "\n"; - NodeBuilder<> resultPrefix = result; - result = NodeBuilder<>(AND); + NodeBuilder<> prefix = result; + result.clear(AND); - for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) { - NodeBuilder<> r = resultPrefix; + for(Node::iterator i = n.begin(); i != n.end(); ++i) { + // for each child of the AND + NodeBuilder<> r = prefix; - // is this a double-convert since we did OR flattening before? - r << convert(*i); + Debug("dor") << "directOrHelper AND " << ID << ", converting\n"; + printAST(Debug("dor"), *i); + + r << doConvert(*i, sideConditions); + NodeBuilder<> rx = r; + Debug("dor") << "prefix \\/ child is " << ID << "\n"; + printAST(Debug("dor"), rx); Node::iterator p2 = p; - directOrHelper(++p2, end, r); + directOrHelper(++p2, end, r, sideConditions); + + Debug("dor") << "directOrHelper recursion done " << ID << "\n"; + Node rr = r; + Debug("dor") << "directOrHelper subterm of AND " << ID << "\n"; + printAST(Debug("dor"), rr); - result << r; + result << rr; } + + Debug("dor") << "end of directOrHelper AND " << ID << "\n"; + NodeBuilder<> resultnb = result; + printAST(Debug("dor"), resultnb); + + return; } else { - Debug("cnf") << "orHelper: passing through a conversion of " << *p << std::endl; - // is this a double-convert since we did OR flattening before? - result << convert(*p); + // if it's not an AND, pass it through, it's fine + result << n; } Debug("cnf") << " ** result now " << result << std::endl; ++p; } -} - -Node CnfConverter::varIntroductionConvert(const Node& e) { - if(e.getKind() == NOT) { - return compressNOT(e); - } else if(e.getKind() == AND) { - return flatten(e); - } else if(e.getKind() == OR) { - Node n = flatten(e); - Debug("cnf") << "about to handle an OR:" << std::endl; - printAST(Debug("cnf"), n); + Debug("dor") << "end of directOrHelper NO AND " << ID << "\n"; + NodeBuilder<> resultnb = result; + printAST(Debug("dor"), resultnb); +} - NodeBuilder<> m(AND); - NodeBuilder<> extras(OR); - varIntroductionOrHelper(n.begin(), n.end(), m, extras); +Node CnfConverter::varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions) { + switch(e.getKind()) { - if(m.getNumChildren() > 0) { - return m << extras; - } else { - return extras; - } + case NOT: { + Node f = compressNOT(e, sideConditions); + Debug("stari") << "compressNOT:\n"; + printAST(Debug("stari"), e); + printAST(Debug("stari"), f); + return f; } - return e; -} - -void CnfConverter::varIntroductionOrHelper(Node::iterator p, Node::iterator end, NodeBuilder<>& result, NodeBuilder<>& extras) { - while(p != end) { - if((*p).getKind() == AND) { - Debug("cnf") << "orHelper: p " << *p << std::endl; - printAST(Debug("cnf"), *p); - Debug("cnf") << " end " << std::endl; - Debug("cnf") << " result " << result << std::endl; - Debug("cnf") << " extras " << extras << std::endl; + case AND: { + Node n = flatten(e, sideConditions); + Node var = d_nm->mkVar(); + Node notVar = d_nm->mkNode(NOT, var); + for(Node::iterator i = n.begin(); i != n.end(); ++i) { + // *i has already been converted by flatten<>() + if((*i).getKind() == OR) { + NodeBuilder<> b(OR); + b << notVar; + for(Node::iterator j = (*i).begin(); j != (*i).end(); ++j) { + b << *j; + } + *sideConditions << b; + } else { + Debug("stari") << "*i should have been flattened:\n"; + printAST(Debug("stari"), *i); + Node x = convert(*i); + printAST(Debug("stari"), x); + //Assert(x == *i); + *sideConditions << d_nm->mkNode(OR, notVar, *i); + } + } - Node var = d_nm->mkVar(); - extras << var; + return var; + } - Debug("cnf") << " introduced var " << var << "(" << var.getId() << ")" << std::endl; + case OR: + return flatten(e, sideConditions); - Node notVar = d_nm->mkNode(NOT, var); + case IMPLIES: { + Assert( e.getNumChildren() == 2 ); + // just turn x IMPLIES y into (NOT x) OR y + Node x = doConvert(e[0], sideConditions); + Node y = doConvert(e[1], sideConditions); + return doConvert(d_nm->mkNode(OR, doConvert(d_nm->mkNode(NOT, x), sideConditions), y), sideConditions); + } - for(Node::iterator i = (*p).begin(); i != (*p).end(); ++i) { - // is this a double-convert since we did OR flattening before? - result << d_nm->mkNode(OR, notVar, convert(*i)); - } + case IFF: + if(e.getNumChildren() == 2) { + // common case: + // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) + Node x = doConvert(e[0], sideConditions); + Node y = doConvert(e[1], sideConditions); + Node r = d_nm->mkNode(OR, + doConvert(d_nm->mkNode(AND, x, y), sideConditions), + doConvert(d_nm->mkNode(AND, + doConvert(d_nm->mkNode(NOT, x), sideConditions), + doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); + Debug("cnf") << "working on an IFF\n"; + printAST(Debug("cnf"), e); + Debug("cnf") << "which is\n"; + printAST(Debug("cnf"), r); + return doConvert(r, sideConditions); } else { - // is this a double-convert since we did OR flattening before? - Debug("cnf") << "orHelper: p " << *p << std::endl; - Debug("cnf") << " end " << std::endl; - Debug("cnf") << " result " << result << std::endl; - Debug("cnf") << " extras " << extras << std::endl; - Debug("cnf") << " passing through" << std::endl; - extras << convert(*p); + // more than 2 children: + // treat x IFF y IFF z as (x IFF y) AND (y IFF z) ... + Node::iterator i = e.begin(); + Node x = doConvert(*i++, sideConditions); + NodeBuilder<> r(AND); + while(i != e.end()) { + Node y = doConvert(*i++, sideConditions); + // now we just have two: + // just turn x IFF y into (x AND y) OR ((NOT x) AND (NOT y)) + r << d_nm->mkNode(OR, + doConvert(d_nm->mkNode(AND, x, y), sideConditions), + doConvert(d_nm->mkNode(AND, + doConvert(d_nm->mkNode(NOT, x), sideConditions), + doConvert(d_nm->mkNode(NOT, y), sideConditions)), sideConditions)); + x = y; + } + return doConvert(r, sideConditions); } - Debug("cnf") << " ** result now " << result << std::endl; - Debug("cnf") << " ** extras now " << extras << std::endl; - ++p; + case XOR: + Assert( e.getNumChildren() == 2 ); + // just turn x XOR y into (x AND (NOT y)) OR ((NOT x) AND y) + return doConvert(d_nm->mkNode(OR, + d_nm->mkNode(AND, + e[0], + d_nm->mkNode(NOT, e[1])), + d_nm->mkNode(AND, + d_nm->mkNode(NOT, e[0]), + e[1])), sideConditions); + + default: + // variable or theory atom + return e; } } diff --git a/src/smt/cnf_converter.h b/src/smt/cnf_converter.h index d045f4d64..7b7be0480 100644 --- a/src/smt/cnf_converter.h +++ b/src/smt/cnf_converter.h @@ -64,9 +64,9 @@ private: /** * Compress a NOT: do NNF transformation plus a bit. Does DNE, * NOT FALSE ==> TRUE, NOT TRUE ==> FALSE, and pushes NOT inside - * of ANDs and ORs. Calls convert() on subnodes. + * of ANDs and ORs. Calls doConvert() on subnodes. */ - Node compressNOT(const Node& e); + Node compressNOT(const Node& e, NodeBuilder<>* sideConditions); /** * Flatten a Node of kind K. K here is going to be AND or OR. @@ -75,21 +75,22 @@ private: * (AND (AND x y) (AND (AND z)) w) ==> (AND x y z w). */ template - Node flatten(const Node& e); + Node flatten(const Node& e, NodeBuilder<>* sideConditions); /** * Do a direct CNF conversion (with possible exponential blow-up in * the number of clauses). No new variables are introduced. The * output is equivalent to the input. */ - Node directConvert(const Node& e); + Node directConvert(const Node& e, NodeBuilder<>* sideConditions); /** * Helper method for "direct" CNF preprocessing. CNF-converts an OR. */ void directOrHelper(Node::iterator p, Node::iterator end, - NodeBuilder<>& result); + NodeBuilder<>& result, + NodeBuilder<>* sideConditions); /** * Do a satisfiability-preserving CNF conversion with variable @@ -97,16 +98,14 @@ private: * number of clauses, but new variables are introduced and the * output is equisatisfiable (but not equivalent) to the input. */ - Node varIntroductionConvert(const Node& e); + Node varIntroductionConvert(const Node& e, NodeBuilder<>* sideConditions); /** - * Helper method for "variable introduction" CNF preprocessing. - * CNF-converts an OR. + * Convert an expression into CNF. If a conversion already exists + * for the Node, it is returned. If a conversion doesn't exist, it + * is computed and returned (caching the result). */ - void varIntroductionOrHelper(Node::iterator p, - Node::iterator end, - NodeBuilder<>& result, - NodeBuilder<>& extras); + Node doConvert(const Node& e, NodeBuilder<>* sideconditions); public: @@ -127,17 +126,36 @@ public: };/* class CnfConverter */ template -Node CnfConverter::flatten(const Node& e) { +struct flatten_traits; + +template <> +struct flatten_traits { + static const CVC4::Kind ignore = TRUE; // TRUE AND x == x + static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE +}; + +template <> +struct flatten_traits { + static const CVC4::Kind ignore = FALSE; // FALSE OR x == x + static const CVC4::Kind shortout = TRUE; // TRUE OR x == TRUE +}; + +template +Node CnfConverter::flatten(const Node& e, NodeBuilder<>* sideConditions) { Assert(e.getKind() == K); NodeBuilder<> n(K); for(Node::iterator i = e.begin(); i != e.end(); ++i) { - Node f = convert(*i); + Node f = doConvert(*i, sideConditions); if(f.getKind() == K) { for(Node::iterator j = f.begin(); j != f.end(); ++j) { n << *j; } + } else if(f.getKind() == flatten_traits::ignore) { + /* do nothing */ + } else if(f.getKind() == flatten_traits::shortout) { + return f; } else { n << f; } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 65375ab65..b073a68c9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -96,7 +96,7 @@ public: Expr simplify(const Expr& e); /** - * Get a (counter)model (only if preceded by a SAT or INVALID query. + * Get a (counter)model (only if preceded by a SAT or INVALID query). */ Model getModel(); diff --git a/src/util/options.h b/src/util/options.h index 57b20c47f..2e696d0db 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -52,7 +52,7 @@ struct Options { err(0), verbosity(0), lang(parser::Parser::LANG_AUTO), - d_cnfConversion(CVC4::CNF_DIRECT_EXPONENTIAL) + d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION) {} };/* struct Options */ -- 2.30.2