diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/model_core_builder.cpp | 21 | ||||
-rw-r--r-- | src/smt/model_core_builder.h | 27 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
3 files changed, 40 insertions, 16 deletions
diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 1cbc18c1a..a077bb2fa 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -21,7 +21,8 @@ using namespace CVC4::kind; namespace CVC4 { bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions, - Model* m) + Model* m, + ModelCoresMode mode) { if (Trace.isOn("model-core")) { @@ -74,8 +75,22 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Expr>& assertions, Trace("model-core") << "Minimizing substitution..." << std::endl; std::vector<Node> coreVars; - bool minimized = - theory::SubstitutionMinimize::find(formula, truen, vars, subs, coreVars); + std::vector<Node> impliedVars; + bool minimized = false; + if (mode == MODEL_CORES_NON_IMPLIED) + { + minimized = theory::SubstitutionMinimize::findWithImplied( + formula, vars, subs, coreVars, impliedVars); + } + else if (mode == MODEL_CORES_SIMPLE) + { + minimized = theory::SubstitutionMinimize::find( + formula, truen, vars, subs, coreVars); + } + else + { + Unreachable("Unknown model cores mode"); + } Assert(minimized, "cannot compute model core, since model does not satisfy input!"); if (minimized) diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index 29348a4f4..a60a3767c 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -20,6 +20,7 @@ #include <vector> #include "expr/expr.h" +#include "options/smt_options.h" #include "smt/model.h" namespace CVC4 { @@ -32,22 +33,30 @@ class ModelCoreBuilder public: /** set model core * - * This function updates the model m so that it is a minimal "core" of - * substitutions that satisfy the formulas in assertions, interpreted - * conjunctively. This is specified via calls to - * Model::setUsingModelCore, Model::recordModelCoreSymbol, - * for details see smt/model.h. + * This function updates model m so that it has information regarding its + * "model core". A model core for m is a substitution of the form + * { s1 -> m(s1), ..., sn -> m(sn) } * - * It returns true if m is a model for assertions. In this case, we set: + * The criteria for what consistutes a model core given by mode. For + * example, if mode is MODEL_CORES_SIMPLE, then a model core corresponds to a + * subset of assignments from the model that suffice to show that the set of + * assertions, interpreted conjunctively, evaluates to true under the + * substitution corresponding to the model core. + * + * The model core is recorded on the model object m via calls to + * m->setUsingModelCore, m->recordModelCoreSymbol, for details see + * smt/model.h. In particular, we call: * m->usingModelCore(); * m->recordModelCoreSymbol(s1); ... m->recordModelCoreSymbol(sn); - * such that each formula in assertions under the substitution - * { s1 -> m(s1), ..., sn -> m(sn) } rewrites to true. + * such that { s1 -> m(s1), ..., sn -> m(sn) } is the model core computed + * by this class. * * If m is not a model for assertions, this method returns false and m is * left unchanged. */ - static bool setModelCore(const std::vector<Expr>& assertions, Model* m); + static bool setModelCore(const std::vector<Expr>& assertions, + Model* m, + ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ } // namespace CVC4 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a2dd8276b..63c970920 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1235,7 +1235,7 @@ void SmtEngine::setDefaults() { } if ((options::checkModels() || options::checkSynthSol() - || options::produceModelCores()) + || options::modelCoresMode() != MODEL_CORES_NONE) && !options::produceAssertions()) { Notice() << "SmtEngine: turning on produce-assertions to support " @@ -1432,7 +1432,7 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() && (options::produceAssignments() || options::sygusRewSynthCheck() - || options::produceModelCores() || is_sygus)) + || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); @@ -4263,12 +4263,12 @@ Model* SmtEngine::getModel() { } TheoryModel* m = d_theoryEngine->getModel(); - if (options::produceModelCores()) + if (options::modelCoresMode() != MODEL_CORES_NONE) { // If we enabled model cores, we compute a model core for m based on our // assertions using the model core builder utility std::vector<Expr> easserts = getAssertions(); - ModelCoreBuilder::setModelCore(easserts, m); + ModelCoreBuilder::setModelCore(easserts, m, options::modelCoresMode()); } m->d_inputName = d_filename; return m; |