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)
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;
}
* \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
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"
)
ENUM_JAVA_TOP = \
r"""package io.github.{namespace};
+import io.github.cvc5.CVC5ApiException;
import java.util.HashMap;
import java.util.Map;
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")
package io.github.cvc5;
+import io.github.cvc5.modes.BlockModelsMode;
import java.io.IOException;
import java.util.*;
* 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
/*
* 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<Solver*>(pointer);
- solver->blockModel();
+ modes::BlockModelsMode mode = static_cast<modes::BlockModelsMode>(modeValue);
+ solver->blockModel(mode);
CVC5_JAVA_API_TRY_CATCH_END(env);
}
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 "<iostream>" namespace "std":
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 +
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
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.
.. 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(<c_BlockModelsMode> mode.value)
def blockModelValues(self, terms):
"""
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"
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)); }
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);
bool isOperatorEnabled(const std::string& name) const;
+ modes::BlockModelsMode getBlockModelsMode(const std::string& mode);
+
bool isTheoryEnabled(internal::theory::TheoryId theory) 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");
}
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(
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(
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(
/* 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)
Command* BlockModelCommand::clone() const
{
- BlockModelCommand* c = new BlockModelCommand();
+ BlockModelCommand* c = new BlockModelCommand(d_mode);
return c;
}
size_t dag,
Language language) const
{
- Printer::getPrinter(language)->toStreamCmdBlockModel(out);
+ Printer::getPrinter(language)->toStreamCmdBlockModel(out, d_mode);
}
/* -------------------------------------------------------------------------- */
class CVC5_EXPORT BlockModelCommand : public Command
{
public:
- BlockModelCommand();
+ BlockModelCommand(modes::BlockModelsMode mode);
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
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. */
Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
theory::TheoryModel* m,
- options::BlockModelsMode mode,
+ modes::BlockModelsMode mode,
const std::vector<Node>& exprToBlock)
{
NodeManager* nm = NodeManager::currentNM();
std::vector<Node> 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
}
else
{
- Assert(mode == options::BlockModelsMode::VALUES);
+ Assert(mode == modes::BlockModelsMode::VALUES);
std::vector<Node> blockers;
// if specific terms were not specified, block all variables of
// the model
#include <vector>
+#include "api/cpp/cvc5_types.h"
#include "expr/node.h"
-#include "options/smt_options.h"
#include "smt/env_obj.h"
namespace cvc5::internal {
Node getModelBlocker(
const std::vector<Node>& assertions,
theory::TheoryModel* m,
- options::BlockModelsMode mode,
+ modes::BlockModelsMode mode,
const std::vector<Node>& exprToBlock = std::vector<Node>());
}; /* class TheoryModelCoreBuilder */
return ssm.str();
}
-void SolverEngine::blockModel()
+void SolverEngine::blockModel(modes::BlockModelsMode mode)
{
Trace("smt") << "SMT blockModel()" << endl;
SolverEngineScope smts(this);
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<Node> 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);
}
// 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);
}
* 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.
-; COMMAND-LINE: --incremental --produce-models --block-models=literals
+; COMMAND-LINE: --incremental --produce-models
; EXPECT: sat
; EXPECT: sat
; EXPECT: sat
(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)
-; 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
(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)
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();
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();
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);
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();
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;
@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();
@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();
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}));
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();
import cvc5
import sys
-from cvc5 import Kind, RoundingMode
+from cvc5 import Kind, BlockModelsMode, RoundingMode
@pytest.fixture
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()
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()
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):
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()
projects / cvc5.git / commitdiff