7 files changed, 48 insertions, 9 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 1341c048a..85d6fbdf8 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -31,7 +31,9 @@ libtheory_la_SOURCES = \
 	term_registration_visitor.h \
 	term_registration_visitor.cpp \
 	ite_simplifier.h \
-	ite_simplifier.cpp
+	ite_simplifier.cpp \
+	unconstrained_simplifier.h \
+	unconstrained_simplifier.cpp
 
 nodist_libtheory_la_SOURCES = \
 	rewriter_tables.h \
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index f5e4f4630..60e48dba2 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -68,10 +68,6 @@ public:
 
 private:
 
-  /** Back edges from nodes to where they are used */
-  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
-  BackEdgesMap d_backEdges;
-
   /** The propagation queue */
   std::vector<TNode> d_propagationQueue;
 
@@ -111,6 +107,15 @@ private:
    */
   DataClearer< std::vector<Node> > d_learnedLiteralClearer;
 
+  /** Back edges from nodes to where they are used */
+  typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap;
+  BackEdgesMap d_backEdges;
+
+  /**
+   * Similar data clearer for back edges.
+   */
+  DataClearer<BackEdgesMap> d_backEdgesClearer;
+
   /** Nodes that have been attached already (computed forward edges for) */
   // All the nodes we've visited so far
   context::CDHashSet<TNode, TNodeHashFunction> d_seen;
@@ -231,12 +236,13 @@ public:
    */
   CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals,
                     bool enableForward = true, bool enableBackward = true) :
-    d_backEdges(),
     d_propagationQueue(),
     d_propagationQueueClearer(context, d_propagationQueue),
     d_conflict(context, false),
     d_learnedLiterals(outLearnedLiterals),
     d_learnedLiteralClearer(context, outLearnedLiterals),
+    d_backEdges(),
+    d_backEdgesClearer(context, d_backEdges),
     d_seen(context),
     d_state(context),
     d_forwardPropagation(enableForward),
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 5be052947..197134b6a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -405,6 +405,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
       updateCoefMap(left[i], size, leftMap, leftConst);
     }
   }
+  else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) {
+    return utils::mkFalse();
+  }
   else {
     updateCoefMap(left, size, leftMap, leftConst);
   }
@@ -415,6 +418,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
       updateCoefMap(right[i], size, rightMap, rightConst);
     }
   }
+  else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) {
+    return utils::mkFalse();
+  }
   else {
     updateCoefMap(right, size, rightMap, rightConst);
   }
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index caf7566b9..b7ad1d174 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -71,6 +71,10 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
       }
       // Mark the substitution and continue
       Node result = builder;
+      find = substitutionCache.find(result);
+      if (find != substitutionCache.end()) {
+        result = find->second;
+      }
       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl;
       substitutionCache[current] = result;
       toVisit.pop_back();
@@ -114,13 +118,16 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
     d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
   }
 
-  // Put the new substitution in
-  d_substitutions[x] = t;
+  // Put the new substitution in, but apply existing substitutions to rhs first
+  d_substitutions[x] = apply(t);
 
   // Also invalidate the cache
   if (invalidateCache) {
     d_cacheInvalidated = true;
   }
+  else {
+    d_substitutionCache[x] = d_substitutions[x];
+  }
 }
 
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 958f50276..711ff9b72 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -107,6 +107,12 @@ public:
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 
   /**
+   * Returns true iff x is in the substitution map
+   */
+  bool hasSubstitution(TNode x)
+    { return d_substitutions.find(x) != d_substitutions.end(); }
+
+  /**
    * Apply the substitutions to the node.
    */
   Node apply(TNode t);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f72275cb2..4ed0bcb60 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -62,7 +62,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_inPreregister(false),
   d_preRegistrationVisitor(this, context),
-  d_sharedTermsVisitor(d_sharedTerms)
+  d_sharedTermsVisitor(d_sharedTerms),
+  d_unconstrainedSimp(context, logicInfo)
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
     d_theoryTable[theoryId] = NULL;
@@ -1011,3 +1012,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
   result = Rewriter::rewrite(result);
   return result;
 }
+
+
+void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
+{
+  d_unconstrainedSimp.processAssertions(assertions);
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 019818a5f..bc9f4c889 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -42,6 +42,7 @@
 #include "util/hash.h"
 #include "util/cache.h"
 #include "theory/ite_simplifier.h"
+#include "theory/unconstrained_simplifier.h"
 
 namespace CVC4 {
 
@@ -734,8 +735,12 @@ private:
   /** For preprocessing pass simplifying ITEs */
   ITESimplifier d_iteSimplifier;
 
+  /** For preprocessing pass simplifying unconstrained expressions */
+  UnconstrainedSimplifier d_unconstrainedSimp;
+
 public:
   Node ppSimpITE(TNode assertion);
+  void ppUnconstrainedSimp(std::vector<Node>& assertions);
 
 };/* class TheoryEngine */