summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp109
1 files changed, 56 insertions, 53 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2276956b5..27e7b8530 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -92,7 +92,6 @@ SmtEngine::SmtEngine(NodeManager* nm, const Options* optr)
d_routListener(new ResourceOutListener(*this)),
d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
d_smtSolver(nullptr),
- d_model(nullptr),
d_checkModels(nullptr),
d_pfManager(nullptr),
d_ucManager(nullptr),
@@ -224,7 +223,6 @@ void SmtEngine::finishInit()
TheoryModel* tm = te->getModel();
if (tm != nullptr)
{
- d_model.reset(new Model(tm));
// make the check models utility
d_checkModels.reset(new CheckModels(*d_env.get()));
}
@@ -305,7 +303,6 @@ SmtEngine::~SmtEngine()
d_absValues.reset(nullptr);
d_asserts.reset(nullptr);
- d_model.reset(nullptr);
d_abductSolver.reset(nullptr);
d_interpolSolver.reset(nullptr);
@@ -712,7 +709,7 @@ Result SmtEngine::quickCheck() {
Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
}
-Model* SmtEngine::getAvailableModel(const char* c) const
+TheoryModel* SmtEngine::getAvailableModel(const char* c) const
{
if (!d_env->getOptions().theory.assignFunctionValues)
{
@@ -751,7 +748,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const
throw RecoverableModalException(ss.str().c_str());
}
- return d_model.get();
+ return m;
}
QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const
@@ -1121,7 +1118,7 @@ Node SmtEngine::getValue(const Node& ex) const
}
Trace("smt") << "--- getting value of " << n << endl;
- Model* m = getAvailableModel("get-value");
+ TheoryModel* m = getAvailableModel("get-value");
Assert(m != nullptr);
Node resultNode = m->getValue(n);
Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
@@ -1163,8 +1160,8 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const
{
Assert(tn.isSort());
- Model* m = getAvailableModel("getModelDomainElements");
- return m->getTheoryModel()->getDomainElements(tn);
+ TheoryModel* m = getAvailableModel("getModelDomainElements");
+ return m->getDomainElements(tn);
}
bool SmtEngine::isModelCoreSymbol(Node n)
@@ -1177,8 +1174,7 @@ bool SmtEngine::isModelCoreSymbol(Node n)
// if the model core mode is none, we are always a model core symbol
return true;
}
- Model* m = getAvailableModel("isModelCoreSymbol");
- TheoryModel* tm = m->getTheoryModel();
+ TheoryModel* tm = getAvailableModel("isModelCoreSymbol");
// compute the model core if not done so already
if (!tm->isUsingModelCore())
{
@@ -1193,41 +1189,54 @@ bool SmtEngine::isModelCoreSymbol(Node n)
return tm->isModelCoreSymbol(n);
}
-// TODO(#1108): Simplify the error reporting of this method.
-Model* SmtEngine::getModel() {
- Trace("smt") << "SMT getModel()" << endl;
+std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts,
+ const std::vector<Node>& declaredFuns)
+{
SmtScope smts(this);
-
- finishInit();
-
- if (Dump.isOn("benchmark"))
+ // !!! Note that all methods called here should have a version at the API
+ // level. This is to ensure that the information associated with a model is
+ // completely accessible by the user. This is currently not rigorously
+ // enforced. An alternative design would be to have this method implemented
+ // at the API level, but this makes exceptions in the text interface less
+ // intuitive and makes it impossible to implement raw-benchmark at the
+ // SmtEngine level.
+ if (Dump.isOn("raw-benchmark"))
{
getPrinter().toStreamCmdGetModel(d_env->getDumpOut());
}
-
- Model* m = getAvailableModel("get model");
-
- // Notice that the returned model is (currently) accessed by the
- // GetModelCommand only, and is not returned to the user. The information
- // in that model may become stale after it is returned. This is safe
- // since GetModelCommand always calls this command again when it prints
- // a model.
-
- if (d_env->getOptions().smt.modelCoresMode
- != options::ModelCoresMode::NONE)
+ TheoryModel* tm = getAvailableModel("get model");
+ // use the smt::Model model utility for printing
+ const Options& opts = d_env->getOptions();
+ bool isKnownSat = (d_state->getMode() == SmtMode::SAT);
+ Model m(isKnownSat, opts.driver.filename);
+ // set the model declarations, which determines what is printed in the model
+ for (const TypeNode& tn : declaredSorts)
{
- // If we enabled model cores, we compute a model core for m based on our
- // (expanded) assertions using the model core builder utility
- std::vector<Node> asserts = getAssertionsInternal();
- d_pp->expandDefinitions(asserts);
- ModelCoreBuilder::setModelCore(
- asserts, m->getTheoryModel(), d_env->getOptions().smt.modelCoresMode);
+ m.addDeclarationSort(tn, getModelDomainElements(tn));
}
- // set the information on the SMT-level model
- Assert(m != nullptr);
- m->d_inputName = d_env->getOptions().driver.filename;
- m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
- return m;
+ bool usingModelCores =
+ (opts.smt.modelCoresMode != options::ModelCoresMode::NONE);
+ for (const Node& n : declaredFuns)
+ {
+ if (usingModelCores && !tm->isModelCoreSymbol(n))
+ {
+ // skip if not in model core
+ continue;
+ }
+ Node value = tm->getValue(n);
+ m.addDeclarationTerm(n, value);
+ }
+ // for separation logic
+ TypeNode locT, dataT;
+ if (getSepHeapTypes(locT, dataT))
+ {
+ std::pair<Node, Node> sh = getSepHeapAndNilExpr();
+ m.setHeapModel(sh.first, sh.second);
+ }
+ // print the model
+ std::stringstream ssm;
+ ssm << m;
+ return ssm.str();
}
Result SmtEngine::blockModel()
@@ -1242,7 +1251,7 @@ Result SmtEngine::blockModel()
getPrinter().toStreamCmdBlockModel(d_env->getDumpOut());
}
- Model* m = getAvailableModel("block model");
+ TheoryModel* m = getAvailableModel("block model");
if (d_env->getOptions().smt.blockModelsMode
== options::BlockModelsMode::NONE)
@@ -1254,10 +1263,8 @@ Result SmtEngine::blockModel()
// get expanded assertions
std::vector<Node> eassertsProc = getExpandedAssertions();
- Node eblocker =
- ModelBlocker::getModelBlocker(eassertsProc,
- m->getTheoryModel(),
- d_env->getOptions().smt.blockModelsMode);
+ Node eblocker = ModelBlocker::getModelBlocker(
+ eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
Trace("smt") << "Block formula: " << eblocker << std::endl;
return assertFormula(eblocker);
}
@@ -1274,16 +1281,13 @@ Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs);
}
- Model* m = getAvailableModel("block model values");
+ TheoryModel* m = getAvailableModel("block model values");
// get expanded assertions
std::vector<Node> eassertsProc = getExpandedAssertions();
// we always do block model values mode here
- Node eblocker =
- ModelBlocker::getModelBlocker(eassertsProc,
- m->getTheoryModel(),
- options::BlockModelsMode::VALUES,
- exprs);
+ Node eblocker = ModelBlocker::getModelBlocker(
+ eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
return assertFormula(eblocker);
}
@@ -1299,8 +1303,7 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
NodeManagerScope nms(getNodeManager());
Node heap;
Node nil;
- Model* m = getAvailableModel("get separation logic heap and nil");
- TheoryModel* tm = m->getTheoryModel();
+ TheoryModel* tm = getAvailableModel("get separation logic heap and nil");
if (!tm->getHeapModel(heap, nil))
{
const char* msg =
@@ -1548,7 +1551,7 @@ void SmtEngine::checkModel(bool hardFailure) {
TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
Notice() << "SmtEngine::checkModel(): generating model" << endl;
- Model* m = getAvailableModel("check model");
+ TheoryModel* m = getAvailableModel("check model");
Assert(m != nullptr);
// check the model with the theory engine for debugging
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback