Merge branch 'master' into optimizeRunscriptSLIAoptimizeRunscriptSLIA

9 files changed, 93 insertions, 9 deletions

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index 67c1f414d..cdf8e4d9a 100644
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -67,6 +67,20 @@ check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
 check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R)
 check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
 
+# Check whether the verison of CaDiCaL used supports incremental solving
+if(USE_CADICAL)
+  check_cxx_source_compiles(
+    "
+    #include <${CaDiCaL_HOME}/src/cadical.hpp>
+    int main() { return sizeof(&CaDiCaL::Solver::assume); }
+    "
+    CVC4_INCREMENTAL_CADICAL
+  )
+  if(CVC4_INCREMENTAL_CADICAL)
+    add_definitions(-DCVC4_INCREMENTAL_CADICAL)
+  endif()
+endif()
+
 # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
 check_c_source_compiles(
   "
diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-application
index 58db84d36..a7d4d985c 100755
--- a/contrib/run-script-smtcomp2019-application
+++ b/contrib/run-script-smtcomp2019-application
@@ -44,7 +44,7 @@ QF_AUFLIA)
   runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental
   ;;
 QF_BV)
-  runcvc4 --tear-down-incremental=4 --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2
+  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_LIA)
   runcvc4 --tear-down-incremental=1 --unconstrained-simp
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 2a59ace11..5e98f8f5a 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1175,14 +1175,16 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
   }
   else if (optarg == "cadical")
   {
+#ifndef CVC4_INCREMENTAL_CADICAL
     if (options::incrementalSolving()
         && options::incrementalSolving.wasSetByUser())
     {
-      throw OptionException(
-          std::string("CaDiCaL does not support incremental mode. \n\
-                         Try --bv-sat-solver=cryptominisat or "
-                      "--bv-sat-solver=minisat"));
+      throw OptionException(std::string(
+          "CaDiCaL version used does not support incremental mode. \n\
+                       Update CaDiCal or Try --bv-sat-solver=cryptominisat or "
+          "--bv-sat-solver=minisat"));
     }
+#endif
 
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
         && options::bitblastMode.wasSetByUser())
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 5a0968ec8..b4851f945 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -117,6 +117,23 @@ SatValue CadicalSolver::solve(long unsigned int&)
   Unimplemented("Setting limits for CaDiCaL not supported yet");
 };
 
+SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+#ifdef CVC4_INCREMENTAL_CADICAL
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  for (const SatLiteral& lit : assumptions)
+  {
+    d_solver->assume(toCadicalLit(lit));
+  }
+  SatValue res = toSatValue(d_solver->solve());
+  d_okay = (res == SAT_VALUE_TRUE);
+  ++d_statistics.d_numSatCalls;
+  return res;
+#else
+  Unimplemented("CaDiCaL version used does not support incremental solving");
+#endif
+}
+
 void CadicalSolver::interrupt() { d_solver->terminate(); }
 
 SatValue CadicalSolver::value(SatLiteral l)
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index e43a2d278..6ab0c2850 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -48,8 +48,8 @@ class CadicalSolver : public SatSolver
   SatVariable falseVar() override;
 
   SatValue solve() override;
-
   SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
 
   void interrupt() override;
 
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 0f7629c5f..6b160ea67 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -171,9 +171,20 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
   Node resultNode =
       LinearRewriteStrategy<RewriteRule<EvalITEBv>,
                             RewriteRule<BvIteConstCond>,
-                            RewriteRule<BvIteEqualChildren>,
-                            RewriteRule<BvIteConstChildren>,
-                            RewriteRule<BvIteEqualCond>>::apply(node);
+                            RewriteRule<BvIteEqualChildren>>::apply(node);
+  // If the node has been rewritten, we return here because we need to make
+  // sure that `BvIteEqualChildren` has been applied until we reach a fixpoint
+  // before applying `BvIteConstChildren`. Otherwise, `BvIteConstChildren`
+  // potentially performs an unsound rewrite. Returning hands back the control
+  // to the `Rewriter` which will then call this method again, ensuring that
+  // the rewrites are applied in the correct order.
+  if (resultNode != node)
+  {
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
+
+  resultNode = LinearRewriteStrategy<RewriteRule<BvIteConstChildren>,
+                                     RewriteRule<BvIteEqualCond>>::apply(node);
   if (resultNode != node)
   {
     return RewriteResponse(REWRITE_AGAIN, resultNode);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c3f2bc866..c920f21a9 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -451,6 +451,7 @@ set(regress_0_tests
   regress0/fmf/tail_rec.smt2
   regress0/fp/abs-unsound.smt2
   regress0/fp/abs-unsound2.smt2
+  regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
   regress0/fp/wrong-model.smt2
diff --git a/test/regress/regress0/fp/down-cast-RNA.smt2 b/test/regress/regress0/fp/down-cast-RNA.smt2
new file mode 100644
index 000000000..d14c63be5
--- /dev/null
+++ b/test/regress/regress0/fp/down-cast-RNA.smt2
@@ -0,0 +1,24 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --fp-exp
+; EXPECT: unsat
+
+(set-logic QF_FP)
+(set-info :source |Written by Andres Noetzli for issue #2183|)
+(set-info :smt-lib-version 2.5)
+(set-info :category crafted)
+(set-info :status unsat)
+
+(declare-fun r () (_ FloatingPoint 5 9))
+(declare-fun rr () (_ FloatingPoint 5 9) ((_ to_fp 5 9) RNA (fp #b1 #b00000 #b1111111110)))
+
+; Let's work out this one out manually
+; #b1111111110 is an significand of
+;  11111111110, rounding positions (g for guard, s for sticky)
+;  123456789gs
+; so g = 1, s = 0 which is the tie break case
+; RNA says tie break goes away from zero, so this is a round up
+; incrementing the significand carries up so the true result should be
+; (fp #b1 #b00001 #x00000000)
+
+(assert (= (fp #b1 #b00000 #xff) rr))
+(check-sat)
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index 1f4cc0c2c..bf0ca73b3 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -85,6 +85,21 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
     TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr));
   }
 
+  void testRewriteBvIte()
+  {
+    TypeNode boolType = d_nm->booleanType();
+    TypeNode bvType = d_nm->mkBitVectorType(1);
+
+    Node zero = d_nm->mkConst(BitVector(1, 0u));
+    Node c1 = d_nm->mkVar("c1", bvType);
+    Node c2 = d_nm->mkVar("c2", bvType);
+
+    Node ite = d_nm->mkNode(BITVECTOR_ITE, c2, zero, zero);
+    Node n = d_nm->mkNode(BITVECTOR_ITE, c1, ite, ite);
+    Node nr = Rewriter::rewrite(n);
+    TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr));
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;