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

15 files changed, 161 insertions, 12 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 4d39ec60f..3532116bc 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -451,6 +451,15 @@ public:
   }
 
   /**
+   * Returns true if this node represents a constant
+   * @return true if const
+   */
+  inline bool isVar() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::VARIABLE;
+  }
+
+  /**
    * Returns the unique id of this node
    * @return the ud
    */
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index ade887b23..b9db8dace 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -49,6 +49,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNRA"] = QF_UFNRA;
   logicMap["QF_ABV"] = QF_ABV;
   logicMap["QF_AUFBV"] = QF_AUFBV;
+  logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
+  logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
@@ -219,6 +221,20 @@ void Smt::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case QF_AUFBVLIA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case QF_AUFBVLRA:
+    addUf();
+    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case QF_AUFLIA:
     addTheory(THEORY_INT_ARRAYS_EX);
     addUf();
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index 1606d7bab..34ec624bc 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -42,6 +42,8 @@ public:
     LRA,
     QF_ABV,
     QF_AUFBV,
+    QF_AUFBVLIA,
+    QF_AUFBVLRA,
     QF_AUFLIA,
     QF_AUFLIRA,
     QF_AX,
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index dc1b47bde..3fa00baae 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,20 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
     break;
 
+  case Smt::QF_AUFBVLIA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_INTS);
+    break;
+
+  case Smt::QF_AUFBVLRA:
+    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_ARRAYS);
+    addTheory(THEORY_BITVECTORS);
+    addTheory(THEORY_REALS);
+    break;
+
   case Smt::QF_AUFLIA:
     addTheory(THEORY_ARRAYS);
     addOperator(kind::APPLY_UF);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 68485ca8a..14b3e3b42 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -159,6 +159,9 @@ class SmtEnginePrivate {
   // Simplify ITE structure
   void simpITE();
 
+  // Simplify based on unconstrained values
+  void unconstrainedSimp();
+
   /**
    * Any variable in a assertion that is declared as a subtype type
    * (predicate subtype or integer subrange type) must be constrained
@@ -255,6 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
   d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
   d_simpITETime("smt::SmtEngine::simpITETime"),
+  d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
   d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
   d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
   d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
@@ -268,6 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::registerStat(&d_staticLearningTime);
   StatisticsRegistry::registerStat(&d_simpITETime);
+  StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
   StatisticsRegistry::registerStat(&d_iteRemovalTime);
   StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
   StatisticsRegistry::registerStat(&d_cnfConversionTime);
@@ -373,6 +378,7 @@ SmtEngine::~SmtEngine() throw() {
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
     StatisticsRegistry::unregisterStat(&d_simpITETime);
+    StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
     StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
     StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
@@ -449,6 +455,13 @@ void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
     NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
   }
+  // Turn on unconstrained simplification for all but QF_SAT as long as we are not in incremental solving mode
+  if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
+    bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+    bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
+    Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
+    NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
+  }
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! Options::current()->arithRewriteEqSetByUser) {
     bool arithRewriteEq = logic.isPure(theory::THEORY_ARITH) && !logic.isQuantified();
@@ -886,16 +899,24 @@ void SmtEnginePrivate::nonClausalSimplify() {
     d_nonClausalLearnedLiterals.resize(j);
   }
 
+  hash_set<TNode, TNodeHashFunction> s;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])));
+    Node assertion = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
+    s.insert(assertion);
+    d_assertionsToCheck.push_back(assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "non-clausal preprocessed: "
-                      << d_assertionsToCheck.back() << endl;
+                      << assertion << endl;
   }
   d_assertionsToPreprocess.clear();
 
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
-    d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])));
+    Node learned = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]));
+    if (s.find(learned) != s.end()) {
+      continue;
+    }
+    s.insert(learned);
+    d_assertionsToCheck.push_back(learned);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "non-clausal learned : "
                       << d_assertionsToCheck.back() << endl;
@@ -916,6 +937,16 @@ void SmtEnginePrivate::simpITE()
   }
 }
 
+
+void SmtEnginePrivate::unconstrainedSimp()
+{
+  TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_unconstrainedSimpTime);
+
+  Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
+  d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertionsToCheck);
+}
+
+
 void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
   throw(AssertionException) {
 
@@ -993,7 +1024,10 @@ void SmtEnginePrivate::simplifyAssertions()
       // Perform non-clausal simplification
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << "performing non-clausal simplification" << endl;
+      // Abuse the user context to make sure circuit propagator gets backtracked
+      d_smt.d_userContext->push();
       nonClausalSimplify();
+      d_smt.d_userContext->pop();
     } else {
       Assert(d_assertionsToCheck.empty());
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
@@ -1004,9 +1038,16 @@ void SmtEnginePrivate::simplifyAssertions()
       simpITE();
     }
 
+    if(Options::current()->unconstrainedSimp) {
+      unconstrainedSimp();
+    }
+
     if(Options::current()->repeatSimp) {
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
+      // Abuse the user context to make sure circuit propagator gets backtracked
+      d_smt.d_userContext->push();
       nonClausalSimplify();
+      d_smt.d_userContext->pop();
     }
 
     if(Options::current()->doStaticLearning) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 10a37b712..f07815e2e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -231,6 +231,8 @@ class CVC4_PUBLIC SmtEngine {
   TimerStat d_staticLearningTime;
   /** time spent in simplifying ITEs */
   TimerStat d_simpITETime;
+  /** time spent in simplifying ITEs */
+  TimerStat d_unconstrainedSimpTime;
   /** time spent removing ITEs */
   TimerStat d_iteRemovalTime;
   /** time spent in theory preprocessing */
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 */
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 01b9648ff..e9ef7d959 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -85,6 +85,8 @@ Options::Options() :
   doStaticLearning(true),
   doITESimp(false),
   doITESimpSetByUser(false),
+  unconstrainedSimp(false),
+  unconstrainedSimpSetByUser(false),
   repeatSimp(false),
   repeatSimpSetByUser(false),
   interactive(false),
@@ -189,6 +191,8 @@ Additional CVC4 options:\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
    --ite-simp             turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
    --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
+   --unconstrained-simp   turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
+   --no-unconstrained-simp turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)\n\
    --repeat-simp          make multiple passes with nonclausal simplifier\n\
    --no-repeat-simp       do not make multiple passes with nonclausal simplifier\n\
    --replay=file          replay decisions from file\n\
@@ -430,6 +434,8 @@ enum OptionValue {
   NO_STATIC_LEARNING,
   ITE_SIMP,
   NO_ITE_SIMP,
+  UNCONSTRAINED_SIMP,
+  NO_UNCONSTRAINED_SIMP,
   REPEAT_SIMP,
   NO_REPEAT_SIMP,
   INTERACTIVE,
@@ -530,6 +536,8 @@ static struct option cmdlineOptions[] = {
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "ite-simp", no_argument, NULL, ITE_SIMP },
   { "no-ite-simp", no_argument, NULL, NO_ITE_SIMP },
+  { "unconstrained-simp", no_argument, NULL, UNCONSTRAINED_SIMP },
+  { "no-unconstrained-simp", no_argument, NULL, NO_UNCONSTRAINED_SIMP },
   { "repeat-simp", no_argument, NULL, REPEAT_SIMP },
   { "no-repeat-simp", no_argument, NULL, NO_REPEAT_SIMP },
   { "interactive", no_argument      , NULL, INTERACTIVE },
@@ -855,6 +863,16 @@ throw(OptionException) {
       doITESimpSetByUser = true;
       break;
 
+    case UNCONSTRAINED_SIMP:
+      unconstrainedSimp = true;
+      unconstrainedSimpSetByUser = true;
+      break;
+
+    case NO_UNCONSTRAINED_SIMP:
+      unconstrainedSimp = false;
+      unconstrainedSimpSetByUser = true;
+      break;
+
     case REPEAT_SIMP:
       repeatSimp = true;
       repeatSimpSetByUser = true;
diff --git a/src/util/options.h b/src/util/options.h
index e6135dacb..f48b45b49 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -154,6 +154,14 @@ struct CVC4_PUBLIC Options {
    */
   bool doITESimpSetByUser;
 
+  /** Whether to do the unconstrained simplification pass */
+  bool unconstrainedSimp;
+
+  /**
+   * Whether the user explicitly requested unconstrained simplification
+   */
+  bool unconstrainedSimpSetByUser;
+
   /** Whether to do multiple rounds of nonclausal simplification */
   bool repeatSimp;