updated preprocessing and rewriting input equalities into inequalities for LRA

2 files changed, 0 insertions, 42 deletions

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index ddfd2ab59..1c779bd79 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,47 +26,6 @@ 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()) {
 
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index a97773dce..4e62401ff 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,7 +31,6 @@ class TheoryBuiltin : public Theory {
 public:
   TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
     Theory(THEORY_BUILTIN, c, out, valuation) {}
-  Node simplify(TNode in, Substitutions& outSubstitutions);
   Node getValue(TNode n);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */