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<Node, Var>* vars, map<Var, Node>* 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);
}
}
}
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<Node, CVC4::prop::minisat::Var> vars;
+ std::map<CVC4::prop::minisat::Var, Node> 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;
}
}
namespace CVC4 {
namespace smt {
-
static void printAST(std::ostream& out, const Node& n, int indent = 0) {
for(int i = 0; i < indent; ++i) {
out << " ";
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)) {
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);
}
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;
}
}
projects / cvc5.git / commitdiff