Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

1 files changed, 6 insertions, 0 deletions

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);