Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.

1 files changed, 20 insertions, 2 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 94afdb1d0..d1734674d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -23,6 +23,7 @@
 #include "expr/attribute.h"
 #include "expr/command.h"
 #include "theory/valuation.h"
+#include "theory/substitutions.h"
 #include "theory/output_channel.h"
 #include "theory/logic_info.h"
 #include "theory/options.h"
@@ -48,7 +49,6 @@ class TheoryEngine;
 namespace theory {
 
 class QuantifiersEngine;
-class SubstitutionMap;
 class TheoryModel;
 
 namespace rrinst {
@@ -576,7 +576,25 @@ public:
    * Given a literal, add the solved substitutions to the map, if any.
    * The method should return true if the literal can be safely removed.
    */
-  virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+    if (in.getKind() == kind::EQUAL) {
+      if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[0].isConst() && in[1].isConst()) {
+        if (in[0] != in[1]) {
+          return PP_ASSERT_STATUS_CONFLICT;
+        }
+      }
+    }
+
+    return PP_ASSERT_STATUS_UNSOLVED;
+  }
 
   /**
    * Given an atom of the theory coming from the input formula, this