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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 65762a50bd1c84080529d0ac4feb4305cc969796..034ca30e221f20e69e9839166468c2e990e9d00d 100644 (file)
--- 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 8b83931b5389df00cb84f2dd2ac45b48bff1d5b1..293f1398dee0ded1f77d9238321d71d36d998601 100644 (file)
--- 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 8804563b4f78674f2268d7fba5298f6797c6d011..8909bfc0668528804c15b6279a96aa33ce9464f0 100644 (file)
--- 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 3aeb38c6e108e39fb938e19db1e16e046c72c2ad..95deeb1415908f33a75d1bb44056363c63cf27e6 100644 (file)
--- 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 6c66d2e4c9d4343dfcfbb39f1a1db3e8d227d13a..f863842def025462c35d2fd755f21963324f4054 100644 (file)
--- 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 2fc1a6115f0ce23f9b84620ed24f375b49cf49c6..e7b7547c47411e28196c8163e886c0a2b09e8780 100644 (file)
--- 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))