Merge branch 'master' into fixPolyfixPoly

9 files changed, 114 insertions, 91 deletions

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 6a1d89d33..120c68a91 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -36,7 +36,8 @@ PreprocessingPassResult PreprocessingPass::apply(
 
 void PreprocessingPass::dumpAssertions(const char* key,
                                        const AssertionPipeline& assertionList) {
-  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions::") + key)) {
+  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
+  {
     // Push the simplified assertions to the dump output stream
     for (const auto& n : assertionList) {
       Dump("assertions") << AssertCommand(Expr(n.toExpr()));
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 372f8eb04..a4b0248e0 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -357,8 +357,11 @@ void Solver::cancelUntil(int level) {
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
             if (marker[x] == 2) marker[x] = 1;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
-                polarity[x] = sign(trail[c]);
+            if (phase_saving > 1
+                || ((phase_saving == 1) && c > trail_lim.last()))
+            {
+              polarity[x] = sign(trail[c]);
+            }
             insertVarOrder(x); }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
@@ -1080,16 +1083,19 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               cancelUntil(assumptions.size()); 
               throw e; 
             }
-            
-            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
-                !isWithinBudget) {
-                // Reached bound on number of conflicts:
-                Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
-                progress_estimate = progressEstimate();
-                cancelUntil(assumptions.size());
-                return l_Undef;
+
+            if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0
+                 && conflictC >= nof_conflicts)
+                || !isWithinBudget)
+            {
+              // Reached bound on number of conflicts:
+              Debug("bvminisat::search")
+                  << OUTPUT_TAG << " restarting " << std::endl;
+              progress_estimate = progressEstimate();
+              cancelUntil(assumptions.size());
+              return l_Undef;
             }
- 
+
             // Simplify the set of problem clauses:
             if (decisionLevel() == 0 && !simplify()) {
                 Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 2fa8d472d..698d2a776 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -255,17 +255,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     const Clause& ps  =  ps_smallest ? _qs : _ps;
     const Clause& qs  =  ps_smallest ? _ps : _qs;
 
-    for (int i = 0; i < qs.size(); i++){
-        if (var(qs[i]) != v){
-            for (int j = 0; j < ps.size(); j++)
-                if (var(ps[j]) == var(qs[i]))
-                    if (ps[j] == ~qs[i])
-                        return false;
-                    else
-                        goto next;
-            out_clause.push(qs[i]);
+    for (int i = 0; i < qs.size(); i++)
+    {
+      if (var(qs[i]) != v)
+      {
+        for (int j = 0; j < ps.size(); j++)
+        {
+          if (var(ps[j]) == var(qs[i]))
+          {
+            if (ps[j] == ~qs[i])
+              return false;
+            else
+              goto next;
+          }
         }
-        next:;
+        out_clause.push(qs[i]);
+      }
+    next:;
     }
 
     for (int i = 0; i < ps.size(); i++)
@@ -289,17 +295,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 
     size = ps.size()-1;
 
-    for (int i = 0; i < qs.size(); i++){
-        if (var(__qs[i]) != v){
-            for (int j = 0; j < ps.size(); j++)
-                if (var(__ps[j]) == var(__qs[i]))
-                    if (__ps[j] == ~__qs[i])
-                        return false;
-                    else
-                        goto next;
-            size++;
+    for (int i = 0; i < qs.size(); i++)
+    {
+      if (var(__qs[i]) != v)
+      {
+        for (int j = 0; j < ps.size(); j++)
+        {
+          if (var(__ps[j]) == var(__qs[i]))
+          {
+            if (__ps[j] == ~__qs[i])
+              return false;
+            else
+              goto next;
+          }
         }
-        next:;
+        size++;
+      }
+    next:;
     }
 
     return true;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dbe417dbc..c8a2e16c2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1349,15 +1349,16 @@ lbool Solver::search(int nof_conflicts)
               check_type = CHECK_WITH_THEORY;
             }
 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts ||
-                !withinBudget(options::satConflictStep())) {
-                // Reached bound on number of conflicts:
-                progress_estimate = progressEstimate();
-                cancelUntil(0);
-                // [mdeters] notify theory engine of restarts for deferred
-                // theory processing
-                proxy->notifyRestart();
-                return l_Undef;
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts)
+                || !withinBudget(options::satConflictStep()))
+            {
+              // Reached bound on number of conflicts:
+              progress_estimate = progressEstimate();
+              cancelUntil(0);
+              // [mdeters] notify theory engine of restarts for deferred
+              // theory processing
+              proxy->notifyRestart();
+              return l_Undef;
             }
 
             // Simplify the set of problem clauses:
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 96fea2147..a101a0c2d 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -256,17 +256,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou
     const Clause& ps  =  ps_smallest ? _qs : _ps;
     const Clause& qs  =  ps_smallest ? _ps : _qs;
 
-    for (int i = 0; i < qs.size(); i++){
-        if (var(qs[i]) != v){
-            for (int j = 0; j < ps.size(); j++)
-                if (var(ps[j]) == var(qs[i]))
-                    if (ps[j] == ~qs[i])
-                        return false;
-                    else
-                        goto next;
-            out_clause.push(qs[i]);
+    for (int i = 0; i < qs.size(); i++)
+    {
+      if (var(qs[i]) != v)
+      {
+        for (int j = 0; j < ps.size(); j++)
+        {
+          if (var(ps[j]) == var(qs[i]))
+          {
+            if (ps[j] == ~qs[i])
+              return false;
+            else
+              goto next;
+          }
         }
-        next:;
+        out_clause.push(qs[i]);
+      }
+    next:;
     }
 
     for (int i = 0; i < ps.size(); i++)
@@ -290,17 +296,23 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
 
     size = ps.size()-1;
 
-    for (int i = 0; i < qs.size(); i++){
-        if (var(__qs[i]) != v){
-            for (int j = 0; j < ps.size(); j++)
-                if (var(__ps[j]) == var(__qs[i]))
-                    if (__ps[j] == ~__qs[i])
-                        return false;
-                    else
-                        goto next;
-            size++;
+    for (int i = 0; i < qs.size(); i++)
+    {
+      if (var(__qs[i]) != v)
+      {
+        for (int j = 0; j < ps.size(); j++)
+        {
+          if (var(__ps[j]) == var(__qs[i]))
+          {
+            if (__ps[j] == ~__qs[i])
+              return false;
+            else
+              goto next;
+          }
         }
-        next:;
+        size++;
+      }
+    next:;
     }
 
     return true;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 58a1e2912..eae11606f 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -15,8 +15,10 @@
  **/
 
 #include "smt/dump.h"
-#include "lib/strtok_r.h"
+
 #include "base/output.h"
+#include "lib/strtok_r.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 
 namespace CVC4 {
 
@@ -55,25 +57,10 @@ void DumpC::setDumpFromString(const std::string& optarg) {
                               optargPtr + "'.  Please consult --dump help.");
       }
       if(!strcmp(p, "everything")) {
-      } else if(!strcmp(p, "definition-expansion")) {
-      } else if(!strcmp(p, "boolean-terms")) {
-      } else if(!strcmp(p, "constrain-subtypes")) {
-      } else if(!strcmp(p, "substitution")) {
-      } else if(!strcmp(p, "bv-to-bool")) {
-      } else if(!strcmp(p, "bool-to-bv")) {
-      } else if(!strcmp(p, "strings-pp")) {
-      } else if(!strcmp(p, "skolem-quant")) {
-      } else if(!strcmp(p, "simplify")) {
-      } else if(!strcmp(p, "static-learning")) {
-      } else if(!strcmp(p, "ite-removal")) {
-      } else if(!strcmp(p, "repeat-simplify")) {
-      } else if(!strcmp(p, "rewrite-apply-to-const")) {
-      } else if(!strcmp(p, "theory-preprocessing")) {
-      } else if(!strcmp(p, "nonclausal")) {
-      } else if(!strcmp(p, "theorypp")) {
-      } else if(!strcmp(p, "itesimp")) {
-      } else if(!strcmp(p, "unconstrained")) {
-      } else if(!strcmp(p, "repeatsimp")) {
+      }
+      else if (preprocessing::PreprocessingPassRegistry::getInstance().hasPass(
+                   p))
+      {
       } else {
         throw OptionException(std::string("don't know how to dump `") +
                               optargPtr + "'.  Please consult --dump help.");
@@ -116,6 +103,16 @@ void DumpC::setDumpFromString(const std::string& optarg) {
       }
     } else if(!strcmp(optargPtr, "help")) {
       puts(s_dumpHelp.c_str());
+
+      std::stringstream ss;
+      ss << "Available preprocessing passes:\n";
+      for (const std::string& pass :
+           preprocessing::PreprocessingPassRegistry::getInstance()
+               .getAvailablePasses())
+      {
+        ss << "- " << pass << "\n";
+      }
+      puts(ss.str().c_str());
       exit(1);
     } else if(!strcmp(optargPtr, "bv-abstraction")) {
       Dump.on("bv-abstraction");
@@ -140,7 +137,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
 #endif /* CVC4_DUMPING */
 }
 
-
 const std::string DumpC::s_dumpHelp = "\
 Dump modes currently supported by the --dump option:\n\
 \n\
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b133f3a36..11c03de6c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2742,8 +2742,6 @@ static void dumpAssertions(const char* key,
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
 {
-  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
   spendResource(options::preprocessStep());
   Assert(d_smt.d_pendingPops == 0);
   try {
@@ -2972,8 +2970,6 @@ void SmtEnginePrivate::processAssertions() {
   SubstitutionMap& top_level_substs =
       d_preprocessingPassContext->getTopLevelSubstitutions();
 
-  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
   // Dump the assertions
   dumpAssertions("pre-everything", d_assertions);
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f5c3eac08..ff71f6432 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -711,9 +711,8 @@ bool Constraint::wellFormedFarkasProof() const {
   }
   Debug("constraints::wffp") << "final sum: " << lhs << " <= " << rhs << endl;
   // 0 = lhs <= rhs < 0
-  return
-    (lhs.isNull() || Constant::isMember(lhs) && Constant(lhs).isZero() ) &&
-    rhs.sgn() < 0;
+  return (lhs.isNull() || (Constant::isMember(lhs) && Constant(lhs).isZero()))
+         && rhs.sgn() < 0;
 
 #else  /* IS_PROOFS_BUILD */
   return true;
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 3a879640f..b307876ed 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -29,7 +29,7 @@ namespace theory {
 namespace quantifiers {
 
 EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
-    : d_tds(tds)
+    : d_tds(tds), d_first(true), d_curr_ind(0)
 {
 }
 
@@ -323,7 +323,7 @@ bool EnumStreamPermutation::PermutationState::getNextPermutation()
 }
 
 EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
-    : d_tds(tds), d_stream_permutations(tds)
+    : d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
 {
 }