From c7507cebfa909d6662b7a8635a9dc9e3f2bf801a Mon Sep 17 00:00:00 2001 From: yoni206 Date: Sat, 26 Mar 2022 20:10:06 +0300 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 15 ++++++------- src/options/smt_options.toml | 21 ++++++++++++------- src/smt/interpolation_solver.cpp | 4 ++-- src/smt/set_defaults.cpp | 3 +-- src/smt/solver_engine.cpp | 3 +-- .../quantifiers/sygus/sygus_interpol.cpp | 11 +++++----- .../regress1/sygus/interpol1-push-pop.smt2 | 2 +- .../regress/cli/regress1/sygus/interpol1.smt2 | 2 +- .../cli/regress1/sygus/interpol3-next.smt2 | 2 +- .../regress/cli/regress1/sygus/interpol3.smt2 | 2 +- .../cli/regress1/sygus/interpol_arr1.smt2 | 2 +- .../cli/regress1/sygus/interpol_arr2.smt2 | 2 +- .../cli/regress1/sygus/interpol_cosa_1.smt2 | 4 +--- .../cli/regress1/sygus/interpol_dt.smt2 | 2 +- .../regress1/sygus/interpol_from_pono_1.smt2 | 2 +- .../regress1/sygus/interpol_from_pono_2.smt2 | 2 +- .../regress1/sygus/interpol_from_pono_3.smt2 | 2 +- test/regress/cli/regress3/interpol2.smt2 | 2 +- test/unit/api/cpp/solver_black.cpp | 4 ++-- test/unit/api/java/SolverTest.java | 4 ++-- test/unit/api/python/test_solver.py | 4 ++-- 21 files changed, 46 insertions(+), 49 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b73920182..5b36f4d38 100644 --- 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 97f4b408d..4b84b4404 100644 --- 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 2f45c611e..549d4f28b 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -41,10 +41,10 @@ bool InterpolationSolver::getInterpolant(const std::vector& 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 888800e4f..4b7e70b4a 100644 --- 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 65acec2ee..5a27454b7 100644 --- 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 a217b375e..cfd49f97b 100644 --- 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>& 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> 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 4e68b2517..120683519 100644 --- 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 5962d1353..4597a2592 100644 --- 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 b92a4254e..3108e08f8 100644 --- 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 8681acf3a..293ff545f 100644 --- 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 dde124bed..a15078bdb 100644 --- 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 fdd1a162d..9bc7846ad 100644 --- 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 0bee17ad9..78a441384 100644 --- 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 f64ce4a0e..50ab5749a 100644 --- 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 4970e2fd5..71c9e4a80 100644 --- 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 ca8f14da6..89c067a73 100644 --- 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 5de1d4ebd..37be96f10 100644 --- 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 bfd034547..7050fbd63 100644 --- 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 717865c71..1921cd645 100644 --- 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 77cd3b09f..e4b981dfa 100644 --- 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 ca3862819..baf52b897 100644 --- 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() -- 2.30.2