From f02847cdee29a810dbf8e25af1502458fcbdd562 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 1 Apr 2022 09:26:14 -0700 Subject: [PATCH] [API] Add mode argument for `Solver::blockModel()` (#8521) This commit changes Solver::blockModel() to take a mode as an argument instead of relying on an option. --- src/api/cpp/cvc5.cpp | 4 +-- src/api/cpp/cvc5.h | 4 ++- src/api/java/CMakeLists.txt | 2 +- src/api/java/genenums.py.in | 3 ++- src/api/java/io/github/cvc5/Solver.java | 9 ++++--- src/api/java/jni/solver.cpp | 10 ++++--- src/api/python/cvc5.pxd | 3 ++- src/api/python/cvc5.pxi | 7 +++-- src/options/smt_options.toml | 18 ------------- src/parser/smt2/Smt2.g | 10 ++++--- src/parser/smt2/smt2.cpp | 14 ++++++++++ src/parser/smt2/smt2.h | 2 ++ src/printer/printer.cpp | 3 ++- src/printer/printer.h | 3 ++- src/printer/smt2/smt2_printer.cpp | 12 +++++++-- src/printer/smt2/smt2_printer.h | 3 ++- src/smt/command.cpp | 10 ++++--- src/smt/command.h | 6 ++++- src/smt/model_blocker.cpp | 6 ++--- src/smt/model_blocker.h | 4 +-- src/smt/solver_engine.cpp | 14 +++------- src/smt/solver_engine.h | 2 +- .../cli/regress1/model-blocker-simple.smt2 | 6 ++--- .../cli/regress1/model-blocker-values.smt2 | 6 ++--- test/unit/api/cpp/solver_black.cpp | 26 +++++-------------- test/unit/api/java/SolverTest.java | 26 ++++--------------- test/unit/api/python/test_solver.py | 26 ++++--------------- 27 files changed, 108 insertions(+), 131 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b7e44a850..f5d8f6ad4 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7282,7 +7282,7 @@ Term Solver::getAbductNext() const CVC5_API_TRY_CATCH_END; } -void Solver::blockModel() const +void Solver::blockModel(modes::BlockModelsMode mode) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) @@ -7291,7 +7291,7 @@ void Solver::blockModel() const CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only block model after SAT or UNKNOWN response."; //////// all checks before this line - d_slv->blockModel(); + d_slv->blockModel(mode); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index b8bab4bcc..147700fe5 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4506,8 +4506,10 @@ class CVC5_EXPORT Solver * \endverbatim * * @warning This method is experimental and may change in future versions. + * + * @param mode The mode to use for blocking */ - void blockModel() const; + void blockModel(modes::BlockModelsMode mode) const; /** * Block the current model values of (at least) the values in terms. Can be diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 1c2507f38..2c73f48c2 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -40,7 +40,7 @@ add_custom_command( add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) set(JAVA_TYPES_FILES - "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/BlockModelsMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/modes/BlockModelsMode.java" "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/RoundingMode.java" "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/UnknownExplanation.java" ) diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index a83076486..0140a6fb2 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -36,6 +36,7 @@ DEFAULT_PREFIX = 'Kind' ENUM_JAVA_TOP = \ r"""package io.github.{namespace}; +import io.github.cvc5.CVC5ApiException; import java.util.HashMap; import java.util.Map; @@ -162,7 +163,7 @@ def gen_java(parser: EnumParser, path): for namespace in parser.namespaces: for enum in namespace.enums: subnamespace = namespace.name.replace('::', '.') - filedir = os.path.join(path, subnamespace) + filedir = os.path.join(path, subnamespace.replace('.', '/')) if not os.path.exists(filedir): os.mkdir(filedir) filename = os.path.join(filedir, enum.name + ".java") diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index ea4bc5f11..23ad027e4 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -15,6 +15,7 @@ package io.github.cvc5; +import io.github.cvc5.modes.BlockModelsMode; import java.io.IOException; import java.util.*; @@ -2420,13 +2421,15 @@ public class Solver implements IPointer, AutoCloseable * to a mode other than "none". * * @api.note This method is experimental and may change in future versions. + * + * @param mode The mode to use for blocking */ - public void blockModel() + public void blockModel(BlockModelsMode mode) { - blockModel(pointer); + blockModel(pointer, mode.getValue()); } - private native void blockModel(long pointer); + private native void blockModel(long pointer, int modeValue); /** * Block the current model values of (at least) the values in terms. Can be diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 41ada6ade..4bf41d335 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -2289,15 +2289,17 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_getAbductNext( /* * Class: io_github_cvc5_Solver * Method: blockModel - * Signature: (J)V + * Signature: (JI)V */ JNIEXPORT void JNICALL Java_io_github_cvc5_Solver_blockModel(JNIEnv* env, - jobject, - jlong pointer) + jobject, + jlong pointer, + jint modeValue) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Solver* solver = reinterpret_cast(pointer); - solver->blockModel(); + modes::BlockModelsMode mode = static_cast(modeValue); + solver->blockModel(mode); CVC5_JAVA_API_TRY_CATCH_END(env); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 13e5041ca..bfde85399 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -9,7 +9,7 @@ from libcpp.vector cimport vector from libcpp.map cimport map from libcpp.pair cimport pair from cvc5kinds cimport Kind -from cvc5types cimport RoundingMode, UnknownExplanation +from cvc5types cimport BlockModelsMode, RoundingMode, UnknownExplanation cdef extern from "" namespace "std": @@ -352,6 +352,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Term getAbduct(const Term& conj, Grammar& grammar) except + Term getAbductNext() except + void blockModel() except + + void blockModel(BlockModelsMode mode) except + void blockModelValues(const vector[Term]& terms) except + string getInstantiations() except + Statistics getStatistics() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 1b227e504..bfc139b1a 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -37,6 +37,7 @@ from cvc5 cimport wstring as c_wstring from cvc5 cimport tuple as c_tuple from cvc5 cimport get0, get1, get2 from cvc5kinds cimport Kind as c_Kind +from cvc5types cimport BlockModelsMode as c_BlockModelsMode from cvc5types cimport RoundingMode as c_RoundingMode from cvc5types cimport UnknownExplanation as c_UnknownExplanation @@ -2843,7 +2844,7 @@ cdef class Solver: result.cterm = self.csolver.getAbductNext() return result - def blockModel(self): + def blockModel(self, mode): """ Block the current model. Can be called only if immediately preceded by a SAT or INVALID query. @@ -2862,8 +2863,10 @@ cdef class Solver: .. warning:: This method is experimental and may change in future versions. + + :param mode: The mode to use for blocking """ - self.csolver.blockModel() + self.csolver.blockModel( mode.value) def blockModelValues(self, terms): """ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 9aebabde6..645d06296 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -92,24 +92,6 @@ name = "SMT Layer" name = "non-implied" help = "Only include a subset of variables whose values, in addition to the values of variables whose values are implied, are sufficient to show the input formula is satisfied by the given model." -[[option]] - name = "blockModelsMode" - category = "expert" - long = "block-models=MODE" - type = "BlockModelsMode" - default = "NONE" - help = "mode for producing several models" - help_mode = "Blocking models modes." -[[option.mode.NONE]] - name = "none" - help = "Do not block models." -[[option.mode.LITERALS]] - name = "literals" - help = "Block models based on the SAT skeleton." -[[option.mode.VALUES]] - name = "values" - help = "Block models based on the concrete model values for the free variables." - [[option]] name = "produceLearnedLiterals" category = "regular" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c0458c4f5..188f6ad06 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1045,9 +1045,13 @@ extendedCommand[std::unique_ptr* cmd] PARSER_STATE->defineVar(name, pool); cmd->reset(new DeclarePoolCommand(name, pool, t, terms)); } - | BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd->reset(new BlockModelCommand()); } - + | BLOCK_MODEL_TOK KEYWORD { PARSER_STATE->checkThatLogicIsSet(); } + { + modes::BlockModelsMode mode = + PARSER_STATE->getBlockModelsMode( + AntlrInput::tokenText($KEYWORD).c_str() + 1); + cmd->reset(new BlockModelCommand(mode)); + } | BLOCK_MODEL_VALUES_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,e] RPAREN_TOK { cmd->reset(new BlockModelValuesCommand(terms)); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b27d477c9..bf610ae86 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -299,6 +299,20 @@ bool Smt2::isOperatorEnabled(const std::string& name) const { return d_operatorKindMap.find(name) != d_operatorKindMap.end(); } +modes::BlockModelsMode Smt2::getBlockModelsMode(const std::string& mode) +{ + if (mode == "literals") + { + return modes::BlockModelsMode::LITERALS; + } + else if (mode == "values") + { + return modes::BlockModelsMode::VALUES; + } + parseError(std::string("Unknown block models mode `") + mode + "'"); + return modes::BlockModelsMode::LITERALS; +} + bool Smt2::isTheoryEnabled(internal::theory::TheoryId theory) const { return d_logic.isTheoryEnabled(theory); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index f844c9802..bdf329538 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -100,6 +100,8 @@ class Smt2 : public Parser bool isOperatorEnabled(const std::string& name) const; + modes::BlockModelsMode getBlockModelsMode(const std::string& mode); + bool isTheoryEnabled(internal::theory::TheoryId theory) const; /** diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index accba62ea..642a24eab 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -376,7 +376,8 @@ void Printer::toStreamCmdGetModel(std::ostream& out) const printUnknownCommand(out, "ge-model"); } -void Printer::toStreamCmdBlockModel(std::ostream& out) const +void Printer::toStreamCmdBlockModel(std::ostream& out, + modes::BlockModelsMode mode) const { printUnknownCommand(out, "block-model"); } diff --git a/src/printer/printer.h b/src/printer/printer.h index d873b3acc..9b655077c 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -185,7 +185,8 @@ class Printer virtual void toStreamCmdGetModel(std::ostream& out) const; /** Print block-model command */ - virtual void toStreamCmdBlockModel(std::ostream& out) const; + virtual void toStreamCmdBlockModel(std::ostream& out, + modes::BlockModelsMode mode) const; /** Print block-model-values command */ virtual void toStreamCmdBlockModelValues( diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0187c2768..2aab3d980 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1691,9 +1691,17 @@ void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const out << "(get-model)" << std::endl; } -void Smt2Printer::toStreamCmdBlockModel(std::ostream& out) const +void Smt2Printer::toStreamCmdBlockModel(std::ostream& out, + modes::BlockModelsMode mode) const { - out << "(block-model)" << std::endl; + out << "(block-model :"; + switch (mode) + { + case modes::BlockModelsMode::LITERALS: out << "literals"; break; + case modes::BlockModelsMode::VALUES: out << "values"; break; + default: Unreachable() << "Invalid block models mode " << mode; + } + out << ")" << std::endl; } void Smt2Printer::toStreamCmdBlockModelValues( diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 91a17266e..afa1539ad 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -159,7 +159,8 @@ class Smt2Printer : public cvc5::internal::Printer void toStreamCmdGetModel(std::ostream& out) const override; /** Print block-model command */ - void toStreamCmdBlockModel(std::ostream& out) const override; + void toStreamCmdBlockModel(std::ostream& out, + modes::BlockModelsMode mode) const override; /** Print block-model-values command */ void toStreamCmdBlockModelValues( diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d2f80e853..e98209405 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1698,12 +1698,14 @@ void GetModelCommand::toStream(std::ostream& out, /* class BlockModelCommand */ /* -------------------------------------------------------------------------- */ -BlockModelCommand::BlockModelCommand() {} +BlockModelCommand::BlockModelCommand(modes::BlockModelsMode mode) : d_mode(mode) +{ +} void BlockModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) { try { - solver->blockModel(); + solver->blockModel(d_mode); d_commandStatus = CommandSuccess::instance(); } catch (cvc5::CVC5ApiRecoverableException& e) @@ -1718,7 +1720,7 @@ void BlockModelCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) Command* BlockModelCommand::clone() const { - BlockModelCommand* c = new BlockModelCommand(); + BlockModelCommand* c = new BlockModelCommand(d_mode); return c; } @@ -1729,7 +1731,7 @@ void BlockModelCommand::toStream(std::ostream& out, size_t dag, Language language) const { - Printer::getPrinter(language)->toStreamCmdBlockModel(out); + Printer::getPrinter(language)->toStreamCmdBlockModel(out, d_mode); } /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index e4bab01a9..a502568d6 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -969,7 +969,7 @@ class CVC5_EXPORT GetModelCommand : public Command class CVC5_EXPORT BlockModelCommand : public Command { public: - BlockModelCommand(); + BlockModelCommand(modes::BlockModelsMode mode); void invoke(cvc5::Solver* solver, SymbolManager* sm) override; Command* clone() const override; @@ -979,6 +979,10 @@ class CVC5_EXPORT BlockModelCommand : public Command size_t dag = 1, internal::Language language = internal::Language::LANG_AUTO) const override; + + private: + /** The mode to use for blocking. */ + modes::BlockModelsMode d_mode; }; /* class BlockModelCommand */ /** The command to block model values. */ diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 4cd3f20a2..518dcd7a6 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -29,7 +29,7 @@ ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {} Node ModelBlocker::getModelBlocker(const std::vector& assertions, theory::TheoryModel* m, - options::BlockModelsMode mode, + modes::BlockModelsMode mode, const std::vector& exprToBlock) { NodeManager* nm = NodeManager::currentNM(); @@ -38,7 +38,7 @@ Node ModelBlocker::getModelBlocker(const std::vector& assertions, std::vector nodesToBlock = exprToBlock; Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl; Node blocker; - if (mode == options::BlockModelsMode::LITERALS) + if (mode == modes::BlockModelsMode::LITERALS) { Assert(nodesToBlock.empty()); // optimization: filter out top-level unit assertions, as they cannot @@ -229,7 +229,7 @@ Node ModelBlocker::getModelBlocker(const std::vector& assertions, } else { - Assert(mode == options::BlockModelsMode::VALUES); + Assert(mode == modes::BlockModelsMode::VALUES); std::vector blockers; // if specific terms were not specified, block all variables of // the model diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index b6b1f8d0f..6d10e6c27 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -20,8 +20,8 @@ #include +#include "api/cpp/cvc5_types.h" #include "expr/node.h" -#include "options/smt_options.h" #include "smt/env_obj.h" namespace cvc5::internal { @@ -68,7 +68,7 @@ class ModelBlocker : protected EnvObj Node getModelBlocker( const std::vector& assertions, theory::TheoryModel* m, - options::BlockModelsMode mode, + modes::BlockModelsMode mode, const std::vector& exprToBlock = std::vector()); }; /* class TheoryModelCoreBuilder */ diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 3babf40ae..a074ab758 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1089,7 +1089,7 @@ std::string SolverEngine::getModel(const std::vector& declaredSorts, return ssm.str(); } -void SolverEngine::blockModel() +void SolverEngine::blockModel(modes::BlockModelsMode mode) { Trace("smt") << "SMT blockModel()" << endl; SolverEngineScope smts(this); @@ -1098,18 +1098,10 @@ void SolverEngine::blockModel() TheoryModel* m = getAvailableModel("block model"); - if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) - { - std::stringstream ss; - ss << "Cannot block model when block-models is set to none."; - throw RecoverableModalException(ss.str().c_str()); - } - // get expanded assertions std::vector eassertsProc = getExpandedAssertions(); ModelBlocker mb(*d_env.get()); - Node eblocker = mb.getModelBlocker( - eassertsProc, m, d_env->getOptions().smt.blockModelsMode); + Node eblocker = mb.getModelBlocker(eassertsProc, m, mode); Trace("smt") << "Block formula: " << eblocker << std::endl; assertFormulaInternal(eblocker); } @@ -1133,7 +1125,7 @@ void SolverEngine::blockModelValues(const std::vector& exprs) // we always do block model values mode here ModelBlocker mb(*d_env.get()); Node eblocker = mb.getModelBlocker( - eassertsProc, m, options::BlockModelsMode::VALUES, exprs); + eassertsProc, m, modes::BlockModelsMode::VALUES, exprs); assertFormulaInternal(eblocker); } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index bfcc45dce..ea45784e7 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -227,7 +227,7 @@ class CVC5_EXPORT SolverEngine * This adds an assertion to the assertion stack that blocks the current * model based on the current options configured by cvc5. */ - void blockModel(); + void blockModel(modes::BlockModelsMode mode); /** * Block the current model values of (at least) the values in exprs. diff --git a/test/regress/cli/regress1/model-blocker-simple.smt2 b/test/regress/cli/regress1/model-blocker-simple.smt2 index 526b51007..d29f83f2a 100644 --- a/test/regress/cli/regress1/model-blocker-simple.smt2 +++ b/test/regress/cli/regress1/model-blocker-simple.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --produce-models --block-models=literals +; COMMAND-LINE: --incremental --produce-models ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat @@ -10,9 +10,9 @@ (check-sat) (block-model-values (x)) (check-sat) -(block-model) +(block-model :literals) (check-sat) (block-model-values ((+ x 1))) (check-sat) -(block-model) +(block-model :literals) (check-sat) diff --git a/test/regress/cli/regress1/model-blocker-values.smt2 b/test/regress/cli/regress1/model-blocker-values.smt2 index 25cb0810c..94b7a7717 100644 --- a/test/regress/cli/regress1/model-blocker-values.smt2 +++ b/test/regress/cli/regress1/model-blocker-values.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --produce-models --block-models=values +; COMMAND-LINE: --incremental --produce-models ; EXPECT: sat ; EXPECT: sat ; if we only block models restricted to (a,b), then there are only 2 models @@ -14,7 +14,7 @@ (assert (distinct a b)) (assert (and (>= a 0) (>= b 0) (< a 2) (< b 2))) (check-sat) -(block-model) +(block-model :values) (check-sat) -(block-model) +(block-model :values) (check-sat) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 69bdf60c1..204d270a0 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2226,45 +2226,34 @@ TEST_F(TestApiBlackSolver, pop3) TEST_F(TestApiBlackSolver, blockModel1) { - d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); + ASSERT_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS), + CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel2) -{ - d_solver.setOption("block-models", "literals"); - Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); - d_solver.assertFormula(x.eqTerm(x)); - d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); -} - -TEST_F(TestApiBlackSolver, blockModel3) { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); - ASSERT_THROW(d_solver.blockModel(), CVC5ApiException); + ASSERT_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS), + CVC5ApiException); } -TEST_F(TestApiBlackSolver, blockModel4) +TEST_F(TestApiBlackSolver, blockModel3) { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_NO_THROW(d_solver.blockModel()); + ASSERT_NO_THROW(d_solver.blockModel(modes::BlockModelsMode::LITERALS)); } TEST_F(TestApiBlackSolver, blockModelValues1) { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); @@ -2285,7 +2274,6 @@ TEST_F(TestApiBlackSolver, blockModelValues2) TEST_F(TestApiBlackSolver, blockModelValues3) { - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); @@ -2295,7 +2283,6 @@ TEST_F(TestApiBlackSolver, blockModelValues3) TEST_F(TestApiBlackSolver, blockModelValues4) { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException); @@ -2304,7 +2291,6 @@ TEST_F(TestApiBlackSolver, blockModelValues4) TEST_F(TestApiBlackSolver, blockModelValues5) { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 41ebf499a..33ebd2ddb 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -20,6 +20,7 @@ import static io.github.cvc5.RoundingMode.*; import static org.junit.jupiter.api.Assertions.*; import io.github.cvc5.*; +import io.github.cvc5.modes.BlockModelsMode; import java.math.BigInteger; import java.util.*; import java.util.concurrent.atomic.AtomicReference; @@ -2268,49 +2269,35 @@ class SolverTest @Test void blockModel1() { - d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); + assertThrows(CVC5ApiException.class, () -> d_solver.blockModel(BlockModelsMode.LITERALS)); } @Test void blockModel2() throws CVC5ApiException - { - d_solver.setOption("block-models", "literals"); - Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); - d_solver.assertFormula(x.eqTerm(x)); - d_solver.checkSat(); - assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); - } - - @Test - void blockModel3() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); - assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); + assertThrows(CVC5ApiException.class, () -> d_solver.blockModel(BlockModelsMode.LITERALS)); } @Test - void blockModel4() throws CVC5ApiException + void blockModel3() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - assertDoesNotThrow(() -> d_solver.blockModel()); + assertDoesNotThrow(() -> d_solver.blockModel(BlockModelsMode.LITERALS)); } @Test void blockModelValues1() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); @@ -2336,7 +2323,6 @@ class SolverTest @Test void blockModelValues3() throws CVC5ApiException { - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); @@ -2347,7 +2333,6 @@ class SolverTest void blockModelValues4() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x})); @@ -2357,7 +2342,6 @@ class SolverTest void blockModelValues5() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); - d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 7478f244a..74dc04620 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -15,7 +15,7 @@ import pytest import cvc5 import sys -from cvc5 import Kind, RoundingMode +from cvc5 import Kind, BlockModelsMode, RoundingMode @pytest.fixture @@ -1577,41 +1577,28 @@ def test_pop3(solver): solver.pop(1) def test_block_model1(solver): - solver.setOption("produce-models", "true") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() with pytest.raises(RuntimeError): - solver.blockModel() + solver.blockModel(BlockModelsMode.Literals) def test_block_model2(solver): - solver.setOption("block-models", "literals") - x = solver.mkConst(solver.getBooleanSort(), "x") - solver.assertFormula(x.eqTerm(x)) - solver.checkSat() - with pytest.raises(RuntimeError): - solver.blockModel() - -def test_block_model3(solver): solver.setOption("produce-models", "true") - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) with pytest.raises(RuntimeError): - solver.blockModel() + solver.blockModel(BlockModelsMode.Literals) - -def test_block_model4(solver): +def test_block_model3(solver): solver.setOption("produce-models", "true") - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x"); solver.assertFormula(x.eqTerm(x)) solver.checkSat() - solver.blockModel() + solver.blockModel(BlockModelsMode.Literals) def test_block_model_values1(solver): solver.setOption("produce-models", "true") - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x"); solver.assertFormula(x.eqTerm(x)) solver.checkSat() @@ -1630,7 +1617,6 @@ def test_block_model_values2(solver): solver.blockModelValues([x]) def test_block_model_values3(solver): - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() @@ -1639,7 +1625,6 @@ def test_block_model_values3(solver): def test_block_model_values4(solver): solver.setOption("produce-models", "true") - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) with pytest.raises(RuntimeError): @@ -1647,7 +1632,6 @@ def test_block_model_values4(solver): def test_block_model_values5(solver): solver.setOption("produce-models", "true") - solver.setOption("block-models", "literals") x = solver.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() -- 2.30.2