Refactoring and fixes of set defaults for quantifiers (#7120)

This PR further refactors set defaults for incompatibility issues related to quantifiers.

It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.

Also does minor rearrangements to the order in which default options are set.

6 files changed, 75 insertions, 44 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 65762a50b..034ca30e2 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -193,13 +193,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   if (opts.smt.solveIntAsBV > 0)
   {
-    // not compatible with incremental
-    if (opts.base.incrementalSolving)
-    {
-      throw OptionException(
-          "solving integers as bitvectors is currently not supported "
-          "when solving incrementally.");
-    }
     // Int to BV currently always eliminates arithmetic completely (or otherwise
     // fails). Thus, it is safe to eliminate arithmetic. Also, bit-vectors
     // are required.
@@ -253,17 +246,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   if (opts.smt.ackermann)
   {
-    if (opts.base.incrementalSolving)
-    {
-      throw OptionException(
-          "Incremental Ackermannization is currently not supported.");
-    }
-
-    if (logic.isQuantified())
-    {
-      throw LogicException("Cannot use Ackermannization on quantified formula");
-    }
-
     if (logic.isTheoryEnabled(THEORY_UF))
     {
       logic = logic.getUnlockedCopy();
@@ -394,25 +376,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
     opts.smt.produceAssertions = true;
   }
 
-  if (opts.bv.bvAssertInput && opts.smt.produceProofs)
-  {
-    Notice() << "Disabling bv-assert-input since it is incompatible with proofs."
-             << std::endl;
-    opts.bv.bvAssertInput = false;
-  }
-
-  // If proofs are required and the user did not specify a specific BV solver,
-  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
-  if (opts.smt.produceProofs
-      && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
-      && !opts.bv.bvSolverWasSetByUser
-      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
-  {
-    Notice() << "Forcing internal bit-vector solver due to proof production."
-             << std::endl;
-    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
-  }
-
   if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
     /**
@@ -513,6 +476,18 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
   // widen the logic
   widenLogic(logic, opts);
+
+  // check if we have any options that are not supported with quantified logics
+  if (logic.isQuantified())
+  {
+    std::stringstream reasonNoQuant;
+    if (incompatibleWithQuantifiers(opts, reasonNoQuant))
+    {
+      std::stringstream ss;
+      ss << reasonNoQuant.str() << " not supported in quantified logics.";
+      throw OptionException(ss.str());
+    }
+  }
 }
 
 void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
@@ -895,7 +870,7 @@ bool SetDefaults::usesSygus(const Options& opts) const
   return false;
 }
 
-bool SetDefaults::incompatibleWithProofs(const Options& opts,
+bool SetDefaults::incompatibleWithProofs(Options& opts,
                                          std::ostream& reason) const
 {
   if (opts.quantifiers.globalNegate)
@@ -912,6 +887,24 @@ bool SetDefaults::incompatibleWithProofs(const Options& opts,
     reason << "sygus";
     return true;
   }
+  // options that are automatically set to support proofs
+  if (opts.bv.bvAssertInput)
+  {
+    Notice()
+        << "Disabling bv-assert-input since it is incompatible with proofs."
+        << std::endl;
+    opts.bv.bvAssertInput = false;
+  }
+  // If proofs are required and the user did not specify a specific BV solver,
+  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
+  if (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
+      && !opts.bv.bvSolverWasSetByUser
+      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+  {
+    Notice() << "Forcing internal bit-vector solver due to proof production."
+             << std::endl;
+    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+  }
   return false;
 }
 
@@ -946,6 +939,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
                                               std::ostream& reason,
                                               std::ostream& suggest) const
 {
+  if (opts.smt.ackermann)
+  {
+    reason << "ackermann";
+    return true;
+  }
   if (opts.smt.unconstrainedSimp)
   {
     if (opts.smt.unconstrainedSimpWasSetByUser)
@@ -977,6 +975,11 @@ bool SetDefaults::incompatibleWithIncremental(const LogicInfo& logic,
              << std::endl;
     opts.quantifiers.sygusInference = false;
   }
+  if (opts.smt.solveIntAsBV > 0)
+  {
+    reason << "solveIntAsBV";
+    return true;
+  }
   return false;
 }
 
@@ -1134,6 +1137,26 @@ bool SetDefaults::safeUnsatCores(const Options& opts) const
   return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
 }
 
+bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
+                                              std::ostream& reason) const
+{
+  if (opts.smt.ackermann)
+  {
+    reason << "ackermann";
+    return true;
+  }
+  if (opts.arith.nlRlvMode != options::NlRlvMode::NONE)
+  {
+    // Theory relevance is incompatible with CEGQI and SyQI, since there is no
+    // appropriate policy for the relevance of counterexample lemmas (when their
+    // guard is entailed to be false, the entire lemma is relevant, not just the
+    // guard). Hence, we throw an option exception if quantifiers are enabled.
+    reason << "--nl-ext-rlv";
+    return true;
+  }
+  return false;
+}
+
 void SetDefaults::widenLogic(LogicInfo& logic, Options& opts) const
 {
   bool needsUf = false;
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 8b83931b5..293f1398d 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -71,8 +71,11 @@ class SetDefaults
    * Return true if proofs must be disabled. This is the case for any technique
    * that answers "unsat" without showing a proof of unsatisfiabilty. The output
    * stream reason is similar to above.
+   *
+   * Notice this method may modify the options to ensure that we are compatible
+   * with proofs.
    */
-  bool incompatibleWithProofs(const Options& opts, std::ostream& reason) const;
+  bool incompatibleWithProofs(Options& opts, std::ostream& reason) const;
   /**
    * Check whether we should disable models. The output stream reason is similar
    * to above.
@@ -89,6 +92,12 @@ class SetDefaults
    * techniques that may interfere with producing correct unsat cores.
    */
   bool safeUnsatCores(const Options& opts) const;
+  /**
+   * Check if incompatible with quantified formulas. Notice this method may
+   * modify the options to ensure that we are compatible with quantified logics.
+   * The output stream reason is similar to above.
+   */
+  bool incompatibleWithQuantifiers(Options& opts, std::ostream& reason) const;
   //------------------------- options setting, prior finalization of logic
   /**
    * Set defaults pre, which sets all options prior to finalizing the logic.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8804563b4..8909bfc06 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2345,7 +2345,6 @@ set(regress_1_tests
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
   regress1/sygus/issue3644.smt2
-  regress1/sygus/issue3648.smt2
   regress1/sygus/issue3649.sy
   regress1/sygus/issue3802-default-consts.sy
   regress1/sygus/issue3839-cond-rewrite.smt2
@@ -2740,6 +2739,8 @@ set(regression_disabled_tests
   regress1/sygus/interpol_from_pono_3.smt2
   regress1/sygus/interpol_dt.smt2
   regress1/sygus/inv_gen_fig8.sy
+  # timeout since nl-rlv is required; however it cannot be used with quantifiers
+  regress1/sygus/issue3648.smt2
   # new reconstruct algorithm is slow at reconstructing random constants (see wishue #82)
   regress0/sygus/c100.sy
   # For the six regressions below, solution terms require rewrites not in
diff --git a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2 b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
index 3aeb38c6e..95deeb141 100644
--- a/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
+++ b/test/regress/regress0/quantifiers/cegqi-needs-justify.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --nl-rlv=always --no-sygus-inst
-; EXPECT: unsat
 (set-logic NRA)
 (set-info :status unsat)
 (declare-fun c () Real)
diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2
index 6c66d2e4c..f863842de 100644
--- a/test/regress/regress1/nl/issue3647.smt2
+++ b/test/regress/regress1/nl/issue3647.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always
 ; EXPECT: sat
-(set-logic ALL)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (assert (distinct (sin 1.0) 0.0))
 (check-sat)
diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2
index 2fc1a6115..e7b7547c4 100644
--- a/test/regress/regress1/sygus/issue3648.smt2
+++ b/test/regress/regress1/sygus/issue3648.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always
+; COMMAND-LINE: --sygus-inference --no-check-models
 (set-logic ALL)
 (declare-fun a () Real)
 (assert (> a 0.000001))