Separating produce-interpols from the mode of interpolant generation (#8326)

In current master, --produce-interpols takes a mode, where "none" is the default mode, in which interpolant generation is not enabled.
This PR makes --produce-interpols a Boolean, and adds a interpols-mode option to determine the mode, similarly to unsat cores.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b739201821b1df5dc922f87f1cc413cfcb2e2b38..5b36f4d388d83281bfd7f70ee1afe75705961ef6 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7143,10 +7143,9 @@ Term Solver::getInterpolant(const Term& conj) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
-  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
-                 != options::ProduceInterpols::NONE)
+  CVC5_API_CHECK(d_slv->getOptions().smt.interpols)
       << "Cannot get interpolant unless interpolants are enabled (try "
-         "--produce-interpols=mode)";
+         "--produce-interpols)";
   //////// all checks before this line
   TypeNode nullType;
   Node result = d_slv->getInterpolant(*conj.d_node, nullType);
@@ -7159,10 +7158,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
-  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
-                 != options::ProduceInterpols::NONE)
+  CVC5_API_CHECK(d_slv->getOptions().smt.interpols)
       << "Cannot get interpolant unless interpolants are enabled (try "
-         "--produce-interpols=mode)";
+         "--produce-interpols)";
   //////// all checks before this line
   Node result = d_slv->getInterpolant(*conj.d_node, *grammar.resolve().d_type);
   return Term(this, result);
@@ -7173,10 +7171,9 @@ Term Solver::getInterpolant(const Term& conj, Grammar& grammar) const
 Term Solver::getInterpolantNext() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_slv->getOptions().smt.produceInterpols
-                 != options::ProduceInterpols::NONE)
+  CVC5_API_CHECK(d_slv->getOptions().smt.interpols)
       << "Cannot get interpolant unless interpolants are enabled (try "
-         "--produce-interpols=mode)";
+         "--produce-interpols)";
   CVC5_API_CHECK(d_slv->getOptions().base.incrementalSolving)
       << "Cannot get next interpolant when not solving incrementally (try "
          "--incremental)";

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 97f4b408d3d982b2f357c5ebdcba267d4dfa3095..4b84b4404bf5c1e97fe798af8363e872b0078846 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -425,16 +425,21 @@ name   = "SMT Layer"
   help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
 
 [[option]]
-  name       = "produceInterpols"
+  name       = "interpols"
   category   = "regular"
-  long       = "produce-interpols=MODE"
-  type       = "ProduceInterpols"
-  default    = "NONE"
-  help       = "support the get-interpol command"
+  long       = "produce-interpols"
+  type       = "bool"
+  default    = "false"
+  help       = "turn on interpolation generation."
+
+[[option]]
+  name       = "interpolsMode"
+  category   = "regular"
+  long       = "interpols-mode=MODE"
+  type       = "InterpolsMode"
+  default    = "DEFAULT"
+  help       = "choose interpolants production mode, see --interpols-mode=help"
   help_mode  = "Interpolants grammar mode"
-[[option.mode.NONE]]
-  name = "none"
-  help = "don't compute interpolants"
 [[option.mode.DEFAULT]]
   name = "default"
   help = "use the default grammar for the theory or the user-defined grammar if given"

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 2f45c611e62b3297f8572d6e24d165c0a35ad2f6..549d4f28b705bbe698be51f30391de787edb7f13 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -41,10 +41,10 @@ bool InterpolationSolver::getInterpolant(const std::vector<Node>& axioms,
                                          const TypeNode& grammarType,
                                          Node& interpol)
 {
-  if (options().smt.produceInterpols == options::ProduceInterpols::NONE)
+  if (!options().smt.interpols)
   {
     const char* msg =
-        "Cannot get interpolation when produce-interpol options is off.";
+        "Cannot get interpolation when produce-interpols options is off.";
     throw ModalException(msg);
   }
   Trace("sygus-interpol") << "SolverEngine::getInterpol: conjecture " << conj

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 888800e4f4cc03f4e31b34ec8eee9ebeab9aed47..4b7e70b4a3d4597c4eebdbfb5f4e0b717e9260d3 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -856,8 +856,7 @@ bool SetDefaults::isSygus(const Options& opts) const
   }
   if (!d_isInternalSubsolver)
   {
-    if (opts.smt.produceAbducts
-        || opts.smt.produceInterpols != options::ProduceInterpols::NONE
+    if (opts.smt.produceAbducts || opts.smt.interpols
         || opts.quantifiers.sygusInference
         || opts.quantifiers.sygusRewSynthInput)
     {

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 65acec2eeb635202b3c7eebb661ff660e9c2e779..5a27454b7c7b5eccd198a789a1274fa296d0c226 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -220,8 +220,7 @@ void SolverEngine::finishInit()
   {
     d_abductSolver.reset(new AbductionSolver(*d_env.get()));
   }
-  if (d_env->getOptions().smt.produceInterpols
-      != options::ProduceInterpols::NONE)
+  if (d_env->getOptions().smt.interpols)
   {
     d_interpolSolver.reset(new InterpolationSolver(*d_env));
   }

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index a217b375e95e11514e5038cba241e062bf3775a6..cfd49f97b9cbec8ce73426930e55eb58fe813772 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -99,22 +99,21 @@ void SygusInterpol::getIncludeCons(
     std::map<TypeNode, std::unordered_set<Node>>& result)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Assert(options().smt.produceInterpols != options::ProduceInterpols::NONE);
+  Assert(options().smt.interpols);
   // ASSUMPTIONS
-  if (options().smt.produceInterpols == options::ProduceInterpols::ASSUMPTIONS)
+  if (options().smt.interpolsMode == options::InterpolsMode::ASSUMPTIONS)
   {
     Node tmpAssumptions =
         (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
     expr::getOperatorsMap(tmpAssumptions, result);
   }
   // CONJECTURE
-  else if (options().smt.produceInterpols
-           == options::ProduceInterpols::CONJECTURE)
+  else if (options().smt.interpolsMode == options::InterpolsMode::CONJECTURE)
   {
     expr::getOperatorsMap(conj, result);
   }
   // SHARED
-  else if (options().smt.produceInterpols == options::ProduceInterpols::SHARED)
+  else if (options().smt.interpolsMode == options::InterpolsMode::SHARED)
   {
     // Get operators from axioms
     std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms;
@@ -154,7 +153,7 @@ void SygusInterpol::getIncludeCons(
     }
   }
   // ALL
-  else if (options().smt.produceInterpols == options::ProduceInterpols::ALL)
+  else if (options().smt.interpolsMode == options::InterpolsMode::ALL)
   {
     Node tmpAssumptions =
         (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));

diff --git a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2 b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2
index 4e68b25176ee2704574b8950608356f2e7504694..120683519c2a84f7bc85198e38cb83d8e092c052 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2
+++ b/test/regress/cli/regress1/sygus/interpol1-push-pop.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols -i
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols -i
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic NIA)

diff --git a/test/regress/cli/regress1/sygus/interpol1.smt2 b/test/regress/cli/regress1/sygus/interpol1.smt2
index 5962d1353bf9b8b853cf45f4ffb4d1fbbc48f00c..4597a25921a7a8e4957f9cab379852285a76d745 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol1.smt2
+++ b/test/regress/cli/regress1/sygus/interpol1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic NIA)

diff --git a/test/regress/cli/regress1/sygus/interpol3-next.smt2 b/test/regress/cli/regress1/sygus/interpol3-next.smt2
index b92a4254e0db6e51f77ef6509250c1cc0e4579af..3108e08f8017ca12010786e6a85549956d8ce0d8 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol3-next.smt2
+++ b/test/regress/cli/regress1/sygus/interpol3-next.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --check-interpols -i
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols -i
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic LIA)

diff --git a/test/regress/cli/regress1/sygus/interpol3.smt2 b/test/regress/cli/regress1/sygus/interpol3.smt2
index 8681acf3a0aaec1ba896795de679fda5d181d7ae..293ff545f153559fb95539a7e64033ce149695dd 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol3.smt2
+++ b/test/regress/cli/regress1/sygus/interpol3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic LIA)

diff --git a/test/regress/cli/regress1/sygus/interpol_arr1.smt2 b/test/regress/cli/regress1/sygus/interpol_arr1.smt2
index dde124bed2776195382629de43e44d2d15686c1e..a15078bdbf5dc8c9886e542c77bf668ce79d9fd4 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_arr1.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_arr1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/sygus/interpol_arr2.smt2 b/test/regress/cli/regress1/sygus/interpol_arr2.smt2
index fdd1a162d3ba05b2e6072a4e40f0e86ffd3868f2..9bc7846ad4bd0af07a89d9f1954ebdd227825193 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_arr2.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_arr2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2
index 0bee17ad99a26ba36581e704b9c805044bef2bf6..78a441384b7e37a8cced9011bf71bc3ea8ca2870 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_cosa_1.smt2
@@ -1,9 +1,7 @@
-; COMMAND-LINE: --produce-interpols=conjecture --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=conjecture --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)
-(set-option :produce-interpols conjecture)
-(set-option :sygus-enum fast)
 (declare-fun cfg@1 () (_ BitVec 1))
 (declare-fun witness_0@1 () Bool)
 (declare-fun op@1 () (_ BitVec 4))

diff --git a/test/regress/cli/regress1/sygus/interpol_dt.smt2 b/test/regress/cli/regress1/sygus/interpol_dt.smt2
index f64ce4a0e5c781368537e135663773e84331ac27..50ab5749a91ea76e61043b3955a8b7136052a254 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_dt.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_dt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default
+; COMMAND-LINE: --produce-interpols --interpols-mode=default
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2
index 4970e2fd5ae60e9ed401839afdc2c37a2f332db9..71c9e4a800d16838a222742066388c9249ed2c1a 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_from_pono_1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2
index ca8f14da6791f756c28c948fb4fc59ffe63f5f9a..89c067a73143b3c6347c3957dde3241065e529e6 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_from_pono_2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2
index 5de1d4ebd44d7d3629d1f9ddfe446057cad38495..37be96f10bc7d34e6caf9949247538c5f014c519 100644 (file)
--- a/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2
+++ b/test/regress/cli/regress1/sygus/interpol_from_pono_3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default
+; COMMAND-LINE: --produce-interpols --interpols-mode=default
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 (set-logic ALL)

diff --git a/test/regress/cli/regress3/interpol2.smt2 b/test/regress/cli/regress3/interpol2.smt2
index bfd0345476024c0dab543a9c0d194c86b653f24b..7050fbd63470430cf5d1c80787e97f83637c15e6 100644 (file)
--- a/test/regress/cli/regress3/interpol2.smt2
+++ b/test/regress/cli/regress3/interpol2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --produce-interpols=default --sygus-enum=fast --check-interpols
+; COMMAND-LINE: --produce-interpols --interpols-mode=default --sygus-enum=fast --check-interpols
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 717865c71f877e8d8fe84c943841778611c2156f..1921cd645f91a04d7528ccbffb9fc7604623374c 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1402,7 +1402,7 @@ TEST_F(TestApiBlackSolver, getAbductNext)
 TEST_F(TestApiBlackSolver, getInterpolant)
 {
   d_solver.setLogic("QF_LIA");
-  d_solver.setOption("produce-interpols", "default");
+  d_solver.setOption("produce-interpols", "true");
   d_solver.setOption("incremental", "false");
 
   Sort intSort = d_solver.getIntegerSort();
@@ -1430,7 +1430,7 @@ TEST_F(TestApiBlackSolver, getInterpolant)
 TEST_F(TestApiBlackSolver, getInterpolantNext)
 {
   d_solver.setLogic("QF_LIA");
-  d_solver.setOption("produce-interpols", "default");
+  d_solver.setOption("produce-interpols", "true");
   d_solver.setOption("incremental", "true");
 
   Sort intSort = d_solver.getIntegerSort();

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 77cd3b09fe8b3a553b2020a5dd4acb5049807daf..e4b981dfa6411a495749a0cd607d5c056e7ad6b2 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1394,7 +1394,7 @@ class SolverTest
   @Test void getInterpolant() throws CVC5ApiException
   {
     d_solver.setLogic("QF_LIA");
-    d_solver.setOption("produce-interpols", "default");
+    d_solver.setOption("produce-interpols", "true");
     d_solver.setOption("incremental", "false");
 
     Sort intSort = d_solver.getIntegerSort();
@@ -1419,7 +1419,7 @@ class SolverTest
   @Test void getInterpolantNext() throws CVC5ApiException
   {
     d_solver.setLogic("QF_LIA");
-    d_solver.setOption("produce-interpols", "default");
+    d_solver.setOption("produce-interpols", "true");
     d_solver.setOption("incremental", "true");
 
     Sort intSort = d_solver.getIntegerSort();

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index ca38628194d7395e042fc5e013e28364401f5769..baf52b897097cbc9bcb0787080b1dc6bc1771cbe 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -2147,7 +2147,7 @@ def test_get_abduct_next(solver):
 
 def test_get_interpolant(solver):
     solver.setLogic("QF_LIA")
-    solver.setOption("produce-interpols", "default")
+    solver.setOption("produce-interpols", "true")
     solver.setOption("incremental", "false")
 
     intSort = solver.getIntegerSort()
@@ -2168,7 +2168,7 @@ def test_get_interpolant(solver):
 
 def test_get_interpolant_next(solver):
     solver.setLogic("QF_LIA")
-    solver.setOption("produce-interpols", "default")
+    solver.setOption("produce-interpols", "true")
     solver.setOption("incremental", "true")
 
     intSort = solver.getIntegerSort()