Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

1 files changed, 41 insertions, 0 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1c779bd79..ddfd2ab59 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,6 +26,47 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
+Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) {
+  if(in.getKind() == kind::EQUAL) {
+    Node lhs = d_valuation.simplify(in[0], outSubstitutions);
+    Node rhs = d_valuation.simplify(in[1], outSubstitutions);
+    Node n = lhs.eqNode(rhs);
+    if( n[0].getMetaKind() == kind::metakind::VARIABLE &&
+        n[1].getMetaKind() == kind::metakind::CONSTANT ) {
+      Debug("simplify:builtin") << "found new substitution! "
+                                << n[0] << " => " << n[1] << endl;
+      outSubstitutions.push_back(make_pair(n[0], n[1]));
+      // with our substitutions we've subsumed the equality
+      return NodeManager::currentNM()->mkConst(true);
+    } else if( n[1].getMetaKind() == kind::metakind::VARIABLE &&
+               n[0].getMetaKind() == kind::metakind::CONSTANT ) {
+      Debug("simplify:builtin") << "found new substitution! "
+                                << n[1] << " => " << n[0] << endl;
+      outSubstitutions.push_back(make_pair(n[1], n[0]));
+      // with our substitutions we've subsumed the equality
+      return NodeManager::currentNM()->mkConst(true);
+    }
+  } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) {
+    TNode::iterator found = in[0].end();
+    for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
+      if((*i).getMetaKind() == kind::metakind::CONSTANT) {
+        found = i;
+        break;
+      }
+    }
+    if(found != in[0].end()) {
+      for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
+        if(i != found) {
+          outSubstitutions.push_back(make_pair(*i, *found));
+        }
+      }
+      // with our substitutions we've subsumed the (NOT (DISTINCT...))
+      return NodeManager::currentNM()->mkConst(true);
+    }
+  }
+  return in;
+}
+
 Node TheoryBuiltin::getValue(TNode n) {
   switch(n.getKind()) {