updated preprocessing and rewriting input equalities into inequalities for LRA

1 files changed, 16 insertions, 121 deletions

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 836022bc2..01185281a 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -97,134 +97,29 @@ Node TheoryBool::getValue(TNode n) {
   }
 }
 
-static void
-findAtoms(TNode in, vector<TNode>& atoms,
-          hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) {
-  Kind k CVC4_UNUSED = in.getKind();
-  Assert(kindToTheoryId(k) == THEORY_BOOL);
-
-  stack< pair<TNode, TNode::iterator> > trail;
-  hash_set<TNode, TNodeHashFunction> seen;
-  trail.push(make_pair(in, in.begin()));
-
-  while(!trail.empty()) {
-    pair<TNode, TNode::iterator>& pr = trail.top();
-    Debug("simplify") << "looking at: " << pr.first << endl;
-    if(pr.second == pr.first.end()) {
-      trail.pop();
-    } else {
-      if(pr.second == pr.first.begin()) {
-        Debug("simplify") << "first visit: " << pr.first << endl;
-        // first time we've visited this node?
-        if(seen.find(pr.first) == seen.end()) {
-          Debug("simplify") << "+ haven't seen it yet." << endl;
-          seen.insert(pr.first);
-        } else {
-          Debug("simplify") << "+ saw it before." << endl;
-          trail.pop();
-          continue;
-        }
-      }
-      TNode n = *pr.second++;
-      if(seen.find(n) == seen.end()) {
-        Debug("simplify") << "back edge " << n << " to " << pr.first << endl;
-        backEdges[n].push_back(pr.first);
-        Kind nk = n.getKind();
-        if(kindToTheoryId(nk) == THEORY_BOOL) {
-          trail.push(make_pair(n, n.begin()));
-        } else {
-          Debug("simplify") << "atom: " << n << endl;
-          atoms.push_back(n);
-        }
-      }
-    }
-  }
-}
+Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) {
 
-Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) {
-  const unsigned prev = outSubstitutions.size();
-
-  if(kindToTheoryId(in.getKind()) != THEORY_BOOL) {
-    Assert(in.getMetaKind() == kind::metakind::VARIABLE &&
-           in.getType().isBoolean());
-    return in;
+  if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
+    // If we get a false literal, we're in conflict
+    return SOLVE_STATUS_CONFLICT;
   }
 
-  // form back edges and atoms
-  vector<TNode> atoms;
-  hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges;
-  Debug("simplify") << "finding atoms..." << endl << push;
-  findAtoms(in, atoms, backEdges);
-  Debug("simplify") << pop << "done finding atoms..." << endl;
-
-  hash_map<TNode, Node, TNodeHashFunction> simplified;
-
-  vector<Node> newFacts;
-  CircuitPropagator circuit(atoms, backEdges);
-  Debug("simplify") << "propagate..." << endl;
-  if(circuit.propagate(in, true, newFacts)) {
-    Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl;
-    return NodeManager::currentNM()->mkConst(false);
-  }
-  Debug("simplify") << "done w/ propagate..." << endl;
-
-  for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) {
-    TNode a = *i;
-    if(a.getKind() == kind::NOT) {
-      if(a[0].getMetaKind() == kind::metakind::VARIABLE ) {
-        Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl;
-        outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false)));
-      } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) {
-        Debug("simplify") << "simplifying: " << a << endl;
-        simplified[a] = d_valuation.simplify(a, outSubstitutions);
-        Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
-      }
+  // Add the substitution from the variable to it's value
+  if (in.getKind() == kind::NOT) {
+    if (in[0].getKind() == kind::VARIABLE) {
+      outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
     } else {
-      if(a.getMetaKind() == kind::metakind::VARIABLE) {
-        Debug("simplify") << "found bool unit " << a << "..." << endl;
-        outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true)));
-      } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) {
-        Debug("simplify") << "simplifying: " << a << endl;
-        simplified[a] = d_valuation.simplify(a, outSubstitutions);
-        Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
-      }
+      return SOLVE_STATUS_UNSOLVED;
     }
-  }
-
-  Debug("simplify") << "substituting in root..." << endl;
-  Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end());
-  Debug("simplify") << "got: " << n << endl;
-  if(Debug.isOn("simplify")) {
-    Debug("simplify") << "new substitutions:" << endl;
-    copy(outSubstitutions.begin() + prev, outSubstitutions.end(),
-         ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n"));
-    Debug("simplify") << "done." << endl;
-  }
-  if(outSubstitutions.size() > prev) {
-    NodeBuilder<> b(kind::AND);
-    b << n;
-    for(Substitutions::iterator i = outSubstitutions.begin() + prev,
-          i_end = outSubstitutions.end();
-        i != i_end;
-        ++i) {
-      if((*i).first.getType().isBoolean()) {
-        if((*i).second.getMetaKind() == kind::metakind::CONSTANT) {
-          if((*i).second.getConst<bool>()) {
-            b << (*i).first;
-          } else {
-            b << BooleanSimplification::negate((*i).first);
-          }
-        } else {
-          b << (*i).first.iffNode((*i).second);
-        }
-      } else {
-        b << (*i).first.eqNode((*i).second);
-      }
+  } else {
+    if (in.getKind() == kind::VARIABLE) {
+      outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
+    } else {
+      return SOLVE_STATUS_UNSOLVED;
     }
-    n = b;
   }
-  Debug("simplify") << "final boolean simplification returned: " << n << endl;
-  return n;
+
+  return SOLVE_STATUS_SOLVED;
 }