diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-01-30 02:22:25 +0000 |
commit | 39b707ad22813c184da61c3e2337359ca8061797 (patch) | |
tree | f1e4f3476822c4da3f423dc114ca1583bdcf063e /src/smt | |
parent | e081fe6309b02a23b81330c151876f04ad774465 (diff) |
cnf conversion (variable-introducing), cleanups, fixes to minisat calling for multiple-query cases
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/cnf_converter.cpp | 407 | ||||
-rw-r--r-- | src/smt/cnf_converter.h | 46 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
3 files changed, 335 insertions, 120 deletions
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<Node> 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<AND>(e); - } else if(e.getKind() == OR) { - Node n = flatten<OR>(e); +Node CnfConverter::directConvert(const Node& e, NodeBuilder<>* sideConditions) { + switch(e.getKind()) { + + case NOT: + return compressNOT(e, sideConditions); + + case AND: + return flatten<AND>(e, sideConditions); + + case OR: { + Node n = flatten<OR>(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<AND>(e); - } else if(e.getKind() == OR) { - Node n = flatten<OR>(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<AND>(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<OR>(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 <CVC4::Kind K> - 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 <CVC4::Kind K> -Node CnfConverter::flatten(const Node& e) { +struct flatten_traits; + +template <> +struct flatten_traits<AND> { + static const CVC4::Kind ignore = TRUE; // TRUE AND x == x + static const CVC4::Kind shortout = FALSE; // FALSE AND x == FALSE +}; + +template <> +struct flatten_traits<OR> { + static const CVC4::Kind ignore = FALSE; // FALSE OR x == x + static const CVC4::Kind shortout = TRUE; // TRUE OR x == TRUE +}; + +template <CVC4::Kind K> +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<K>::ignore) { + /* do nothing */ + } else if(f.getKind() == flatten_traits<K>::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(); |