This changes our implementation of GetModelCommand so that we use the API to print the model.
It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.
It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.
This eliminates the last call to getSmtEngine() from the command layer.
CVC5_API_TRY_CATCH_END;
}
+std::string Solver::getModel(const std::vector<Sort>& sorts,
+ const std::vector<Term>& vars) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ NodeManagerScope scope(getNodeManager());
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ << "Cannot get model unless model generation is enabled "
+ "(try --produce-models)";
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Cannot get model unless after a SAT or unknown response.";
+ CVC5_API_SOLVER_CHECK_SORTS(sorts);
+ for (const Sort& s : sorts)
+ {
+ CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
+ << "Expecting an uninterpreted sort as argument to "
+ "getModel.";
+ }
+ CVC5_API_SOLVER_CHECK_TERMS(vars);
+ for (const Term& v : vars)
+ {
+ CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
+ << "Expecting a free constant as argument to getModel.";
+ }
+ //////// all checks before this line
+ return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts),
+ Term::termVectorToNodes(vars));
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
Term Solver::getQuantifierElimination(const Term& q) const
{
NodeManagerScope scope(getNodeManager());
CVC5_API_TRY_CATCH_END;
}
-/*
- * !!! This is only temporarily available until the parser is fully migrated to
- * the new API. !!!
- */
-SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
-
Statistics Solver::getStatistics() const
{
return Statistics(d_smtEngine->getStatisticsRegistry());
*/
bool isModelCoreSymbol(const Term& v) const;
+ /**
+ * Get the model
+ * SMT-LIB:
+ * \verbatim
+ * ( get-model )
+ * \endverbatim
+ * Requires to enable option 'produce-models'.
+ * @param sorts The list of uninterpreted sorts that should be printed in the
+ * model.
+ * @param vars The list of free constants that should be printed in the
+ * model. A subset of these may be printed based on isModelCoreSymbol.
+ * @return a string representing the model.
+ */
+ std::string getModel(const std::vector<Sort>& sorts,
+ const std::vector<Term>& vars) const;
+
/**
* Do quantifier elimination.
* SMT-LIB:
*/
std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
- // !!! This is only temporarily available until the parser is fully migrated
- // to the new API. !!!
- SmtEngine* getSmtEngine(void) const;
-
/**
* Returns a snapshot of the current state of the statistic values of this
* solver. The returned object is completely decoupled from the solver and
class Command;
-namespace smt {
-class SmtEngine;
-}
-
namespace main {
class CommandExecutor
api::Result getResult() const { return d_result; }
void reset();
- SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
-
/** Store the current options as the original options */
void storeOptionsAsOriginal();
}
void AstPrinter::toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const
+ TypeNode tn,
+ const std::vector<Node>& elements) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
}
void AstPrinter::toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const
+ const Node& n,
+ const Node& value) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
* tn declared via declare-sort or declare-datatype.
*/
void toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const override;
+ TypeNode tn,
+ const std::vector<Node>& elements) const override;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
void toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const override;
+ const Node& n,
+ const Node& value) const override;
/**
* To stream with let binding. This prints n, possibly in the scope
* of letification generated by this method based on lbind.
}/* CvcPrinter::toStream(CommandStatus*) */
void CvcPrinter::toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const
+ TypeNode tn,
+ const std::vector<Node>& elements) const
{
if (!tn.isSort())
{
<< tn << std::endl;
return;
}
- const theory::TheoryModel* tm = m.getTheoryModel();
- const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn);
- if (type_reps != nullptr)
+ out << "% cardinality of " << tn << " is " << elements.size() << std::endl;
+ toStreamCmdDeclareType(out, tn);
+ for (const Node& type_rep : elements)
{
- out << "% cardinality of " << tn << " is " << type_reps->size()
- << std::endl;
- toStreamCmdDeclareType(out, tn);
- for (Node type_rep : *type_reps)
+ if (type_rep.isVar())
{
- if (type_rep.isVar())
- {
- out << type_rep << " : " << tn << ";" << std::endl;
- }
- else
- {
- out << "% rep: " << type_rep << std::endl;
- }
+ out << type_rep << " : " << tn << ";" << std::endl;
+ }
+ else
+ {
+ out << "% rep: " << type_rep << std::endl;
}
- }
- else
- {
- toStreamCmdDeclareType(out, tn);
}
}
void CvcPrinter::toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const
+ const Node& n,
+ const Node& value) const
{
- const theory::TheoryModel* tm = m.getTheoryModel();
TypeNode tn = n.getType();
out << n << " : ";
if (tn.isFunction() || tn.isPredicate())
{
out << tn;
}
- // We get the value from the theory model directly, which notice
- // does not have to go through the standard SmtEngine::getValue interface.
- Node val = tm->getValue(n);
- out << " = " << val << ";" << std::endl;
+ out << " = " << value << ";" << std::endl;
}
void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const
LetBinding* lbind) const;
/**
* To stream model sort. This prints the appropriate output for type
- * tn declared via declare-sort or declare-datatype.
+ * tn declared via declare-sort.
*/
void toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const override;
+ TypeNode tn,
+ const std::vector<Node>& elements) const override;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
void toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const override;
+ const Node& n,
+ const Node& value) const override;
/**
* To stream with let binding. This prints n, possibly in the scope
* of letification generated by this method based on lbind.
const std::vector<TypeNode>& dsorts = m.getDeclaredSorts();
for (const TypeNode& tn : dsorts)
{
- toStreamModelSort(out, m, tn);
+ toStreamModelSort(out, tn, m.getDomainElements(tn));
}
-
// print the declared terms
const std::vector<Node>& dterms = m.getDeclaredTerms();
for (const Node& n : dterms)
{
- // take into account model core, independently of the format
- if (!m.isModelCoreSymbol(n))
- {
- continue;
- }
- toStreamModelTerm(out, m, n);
+ toStreamModelTerm(out, n, m.getValue(n));
}
-
-}/* Printer::toStream(Model) */
+}
void Printer::toStreamUsing(Language lang,
std::ostream& out,
/**
* To stream model sort. This prints the appropriate output for type
- * tn declared via declare-sort or declare-datatype.
+ * tn declared via declare-sort.
*/
virtual void toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const = 0;
+ TypeNode tn,
+ const std::vector<Node>& elements) const = 0;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
virtual void toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const = 0;
+ const Node& n,
+ const Node& value) const = 0;
/** write model response to command using another language printer */
void toStreamUsing(Language lang,
void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
{
- const theory::TheoryModel* tm = m.getTheoryModel();
//print the model
out << "(" << endl;
// don't need to print approximations since they are built into choice
out << ")" << endl;
//print the heap model, if it exists
Node h, neq;
- if (tm->getHeapModel(h, neq))
+ if (m.getHeapModel(h, neq))
{
// description of the heap+what nil is equal to fully describes model
out << "(heap" << endl;
}
void Smt2Printer::toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const
+ TypeNode tn,
+ const std::vector<Node>& elements) const
{
if (!tn.isSort())
{
<< tn << std::endl;
return;
}
- const theory::TheoryModel* tm = m.getTheoryModel();
- std::vector<Node> elements = tm->getDomainElements(tn);
// print the cardinality
out << "; cardinality of " << tn << " is " << elements.size() << endl;
if (options::modelUninterpPrint()
}
void Smt2Printer::toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const
+ const Node& n,
+ const Node& value) const
{
- const theory::TheoryModel* tm = m.getTheoryModel();
- // We get the value from the theory model directly, which notice
- // does not have to go through the standard SmtEngine::getValue interface.
- Node val = tm->getValue(n);
- if (val.getKind() == kind::LAMBDA)
+ if (value.getKind() == kind::LAMBDA)
{
TypeNode rangeType = n.getType().getRangeType();
- out << "(define-fun " << n << " " << val[0] << " " << rangeType << " ";
+ out << "(define-fun " << n << " " << value[0] << " " << rangeType << " ";
// call toStream and force its type to be proper
- toStreamCastToType(out, val[1], -1, rangeType);
+ toStreamCastToType(out, value[1], -1, rangeType);
out << ")" << endl;
}
else
{
out << "(define-fun " << n << " () " << n.getType() << " ";
// call toStream and force its type to be proper
- toStreamCastToType(out, val, -1, n.getType());
+ toStreamCastToType(out, value, -1, n.getType());
out << ")" << endl;
}
}
* tn declared via declare-sort or declare-datatype.
*/
void toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const override;
+ TypeNode tn,
+ const std::vector<Node>& elements) const override;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
void toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const override;
+ const Node& n,
+ const Node& value) const override;
/**
* To stream with let binding. This prints n, possibly in the scope
}
void TptpPrinter::toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const
+ TypeNode tn,
+ const std::vector<Node>& elements) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
}
void TptpPrinter::toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const
+ const Node& n,
+ const Node& value) const
{
// shouldn't be called; only the non-Command* version above should be
Unreachable();
* tn declared via declare-sort or declare-datatype.
*/
void toStreamModelSort(std::ostream& out,
- const smt::Model& m,
- TypeNode tn) const override;
+ TypeNode tn,
+ const std::vector<Node>& elements) const override;
/**
* To stream model term. This prints the appropriate output for term
* n declared via declare-fun.
*/
void toStreamModelTerm(std::ostream& out,
- const smt::Model& m,
- Node n) const override;
+ const Node& n,
+ const Node& value) const override;
}; /* class TptpPrinter */
#include "base/modal_exception.h"
#include "options/smt_options.h"
#include "smt/env.h"
-#include "smt/model.h"
#include "smt/node_command.h"
#include "smt/preprocessor.h"
#include "smt/smt_solver.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
#include "theory/theory_engine.h"
+#include "theory/theory_model.h"
using namespace cvc5::theory;
CheckModels::CheckModels(Env& e) : d_env(e) {}
CheckModels::~CheckModels() {}
-void CheckModels::checkModel(Model* m,
+void CheckModels::checkModel(TheoryModel* m,
context::CDList<Node>* al,
bool hardFailure)
{
class Env;
-namespace smt {
+namespace theory {
+class TheoryModel;
+}
-class Model;
+namespace smt {
/**
* This utility is responsible for checking the current model.
* This throws an exception if we fail to verify that m is a proper model
* given assertion list al based on the model checking policy.
*/
- void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure);
+ void checkModel(theory::TheoryModel* m,
+ context::CDList<Node>* al,
+ bool hardFailure);
private:
/** Reference to the environment */
#include "proof/unsat_core.h"
#include "smt/dump.h"
#include "smt/model.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
#include "util/unsafe_interrupt_exception.h"
#include "util/utility.h"
/* class GetModelCommand */
/* -------------------------------------------------------------------------- */
-GetModelCommand::GetModelCommand() : d_result(nullptr) {}
+GetModelCommand::GetModelCommand() {}
void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- d_result = solver->getSmtEngine()->getModel();
- // set the model declarations, which determines what is printed in the model
- d_result->clearModelDeclarations();
std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts();
- for (const api::Sort& s : declareSorts)
- {
- d_result->addDeclarationSort(sortToTypeNode(s));
- }
std::vector<api::Term> declareTerms = sm->getModelDeclareTerms();
- for (const api::Term& t : declareTerms)
- {
- d_result->addDeclarationTerm(termToNode(t));
- }
+ d_result = solver->getModel(declareSorts, declareTerms);
d_commandStatus = CommandSuccess::instance();
}
- catch (RecoverableModalException& e)
+ catch (api::CVC5ApiRecoverableException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
}
}
-/* Model is private to the library -- for now
-Model* GetModelCommand::getResult() const {
- return d_result;
-}
-*/
-
void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
{
if (!ok())
}
else
{
- out << *d_result;
+ out << d_result;
}
}
Command* GetModelCommand::clone() const
{
- GetModelCommand* c = new GetModelCommand();
+ GetModelCommand* c = new GetModelCommand;
c->d_result = d_result;
return c;
}
Language language = Language::LANG_AUTO) const override;
protected:
- smt::Model* d_result;
+ /** Result of printing the model */
+ std::string d_result;
}; /* class GetModelCommand */
/** The command to block models. */
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
-#include "smt/dump_manager.h"
-#include "smt/node_command.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/theory_model.h"
namespace cvc5 {
namespace smt {
-Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
+Model::Model(bool isKnownSat, const std::string& inputName)
+ : d_inputName(inputName), d_isKnownSat(isKnownSat)
{
- Assert(d_tmodel != nullptr);
}
std::ostream& operator<<(std::ostream& out, const Model& m) {
return out;
}
-theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
+const std::vector<Node>& Model::getDomainElements(TypeNode tn) const
+{
+ std::map<TypeNode, std::vector<Node>>::const_iterator it =
+ d_domainElements.find(tn);
+ Assert(it != d_domainElements.end());
+ return it->second;
+}
-const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }
+Node Model::getValue(TNode n) const
+{
+ std::map<Node, Node>::const_iterator it = d_declareTermValues.find(n);
+ Assert(it != d_declareTermValues.end());
+ return it->second;
+}
-bool Model::isModelCoreSymbol(TNode sym) const
+bool Model::getHeapModel(Node& h, Node& nilEq) const
{
- return d_tmodel->isModelCoreSymbol(sym);
+ if (d_sepHeap.isNull() || d_sepNilEq.isNull())
+ {
+ return false;
+ }
+ h = d_sepHeap;
+ nilEq = d_sepNilEq;
+ return true;
}
-Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
-bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
+void Model::addDeclarationSort(TypeNode tn, const std::vector<Node>& elements)
+{
+ d_declareSorts.push_back(tn);
+ d_domainElements[tn] = elements;
+}
-void Model::clearModelDeclarations()
+void Model::addDeclarationTerm(Node n, Node value)
{
- d_declareTerms.clear();
- d_declareSorts.clear();
+ d_declareTerms.push_back(n);
+ d_declareTermValues[n] = value;
}
-void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
+void Model::setHeapModel(Node h, Node nilEq)
+{
+ d_sepHeap = h;
+ d_sepNilEq = nilEq;
+}
-void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); }
const std::vector<TypeNode>& Model::getDeclaredSorts() const
{
return d_declareSorts;
}
+
const std::vector<Node>& Model::getDeclaredTerms() const
{
return d_declareTerms;
#include "cvc5_private.h"
-#ifndef CVC5__MODEL_H
-#define CVC5__MODEL_H
+#ifndef CVC5__SMT__MODEL_H
+#define CVC5__SMT__MODEL_H
#include <iosfwd>
#include <vector>
#include "expr/node.h"
namespace cvc5 {
-
-class SmtEngine;
-
-namespace theory {
-class TheoryModel;
-}
-
namespace smt {
class Model;
std::ostream& operator<<(std::ostream&, const Model&);
/**
- * This is the SMT-level model object, that is responsible for maintaining
- * the necessary information for how to print the model, as well as
- * holding a pointer to the underlying implementation of the theory model.
- *
- * The model declarations maintained by this class are context-independent
- * and should be updated when this model is printed.
+ * A utility for representing a model for pretty printing.
*/
class Model {
- friend std::ostream& operator<<(std::ostream&, const Model&);
- friend class ::cvc5::SmtEngine;
-
public:
- /** construct */
- Model(theory::TheoryModel* tm);
- /** virtual destructor */
- ~Model() {}
+ /** Constructor
+ * @param isKnownSat True if this model is associated with a "sat" response,
+ * or false if it is associated with an "unknown" response.
+ */
+ Model(bool isKnownSat, const std::string& inputName);
/** get the input name (file name, etc.) this model is associated to */
std::string getInputName() const { return d_inputName; }
/**
* only a candidate solution.
*/
bool isKnownSat() const { return d_isKnownSat; }
- /** Get the underlying theory model */
- theory::TheoryModel* getTheoryModel();
- /** Get the underlying theory model (const version) */
- const theory::TheoryModel* getTheoryModel() const;
- //----------------------- helper methods in the underlying theory model
- /** Is the node n a model core symbol? */
- bool isModelCoreSymbol(TNode sym) const;
+ /** Get domain elements */
+ const std::vector<Node>& getDomainElements(TypeNode tn) const;
/** Get value */
Node getValue(TNode n) const;
- /** Does this model have approximations? */
- bool hasApproximations() const;
- //----------------------- end helper methods
+ /** Get separation logic heap and nil, return true if they have been set */
+ bool getHeapModel(Node& h, Node& nilEq) const;
//----------------------- model declarations
- /** Clear the current model declarations. */
- void clearModelDeclarations();
/**
* Set that tn is a sort that should be printed in the model, when applicable,
* based on the output language.
+ *
+ * @param tn The uninterpreted sort
+ * @param elements The domain elements of tn in the model
*/
- void addDeclarationSort(TypeNode tn);
+ void addDeclarationSort(TypeNode tn, const std::vector<Node>& elements);
/**
* Set that n is a variable that should be printed in the model, when
* applicable, based on the output language.
+ *
+ * @param n The variable
+ * @param value The value of the variable in the model
+ */
+ void addDeclarationTerm(Node n, Node value);
+ /**
+ * Set the separation logic model information where h is the heap and nilEq
+ * is the value of sep.nil.
+ *
+ * @param h The value of heap in the heap model
+ * @param nilEq The value of sep.nil in the heap model
*/
- void addDeclarationTerm(Node n);
+ void setHeapModel(Node h, Node nilEq);
/** get declared sorts */
const std::vector<TypeNode>& getDeclaredSorts() const;
/** get declared terms */
* from the solver.
*/
bool d_isKnownSat;
- /**
- * Pointer to the underlying theory model, which maintains all data regarding
- * the values of sorts and terms.
- */
- theory::TheoryModel* d_tmodel;
/**
* The list of types to print, generally corresponding to declare-sort
* commands.
*/
std::vector<TypeNode> d_declareSorts;
+ /** The interpretation of the above sorts, as a list of domain elements. */
+ std::map<TypeNode, std::vector<Node>> d_domainElements;
/**
* The list of terms to print, is typically one-to-one with declare-fun
* commands.
*/
std::vector<Node> d_declareTerms;
+ /** Mapping terms to values */
+ std::map<Node, Node> d_declareTermValues;
+ /** Separation logic heap and nil */
+ Node d_sepHeap;
+ Node d_sepNilEq;
};
} // namespace smt
} // namespace cvc5
-#endif /* CVC5__MODEL_H */
+#endif /* CVC5__SMT__MODEL_H */
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),
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()));
}
d_absValues.reset(nullptr);
d_asserts.reset(nullptr);
- d_model.reset(nullptr);
d_abductSolver.reset(nullptr);
d_interpolSolver.reset(nullptr);
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)
{
throw RecoverableModalException(ss.str().c_str());
}
- return d_model.get();
+ return m;
}
QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) 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;
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)
// 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())
{
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()
getPrinter().toStreamCmdBlockModel(d_env->getDumpOut());
}
- Model* m = getAvailableModel("block model");
+ TheoryModel* m = getAvailableModel("block model");
if (d_env->getOptions().smt.blockModelsMode
== options::BlockModelsMode::NONE)
// 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);
}
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);
}
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 =
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
class NodeManager;
class TheoryEngine;
class UnsatCore;
-class LogicRequest;
class StatisticsRegistry;
class Printer;
class ResourceManager;
namespace smt {
/** Utilities */
-class Model;
class SmtEngineState;
class AbstractValues;
class Assertions;
/* -------------------------------------------------------------------------- */
namespace theory {
- class Rewriter;
- class QuantifiersEngine;
- } // namespace theory
+class TheoryModel;
+class Rewriter;
+class QuantifiersEngine;
+} // namespace theory
/* -------------------------------------------------------------------------- */
friend class ::cvc5::api::Solver;
friend class ::cvc5::smt::SmtEngineState;
friend class ::cvc5::smt::SmtScope;
- friend class ::cvc5::LogicRequest;
/* ....................................................................... */
public:
/** Is this an internal subsolver? */
bool isInternalSubsolver() const;
- /**
- * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
- * query). Only permitted if produce-models is on.
- *
- * TODO (issues#287): eliminate this method.
- */
- smt::Model* getModel();
-
/**
* Block the current model. Can be called only if immediately preceded by
* a SAT or INVALID query. Only permitted if produce-models is on, and the
*/
bool isModelCoreSymbol(Node v);
+ /**
+ * Get a model (only if immediately preceded by an SAT or unknown query).
+ * Only permitted if the model option is on.
+ *
+ * @param declaredSorts The sorts to print in the model
+ * @param declaredFuns The free constants to print in the model. A subset
+ * of these may be printed based on isModelCoreSymbol.
+ * @return the string corresponding to the model. If the output language is
+ * smt2, then this corresponds to a response to the get-model command.
+ */
+ std::string getModel(const std::vector<TypeNode>& declaredSorts,
+ const std::vector<Node>& declaredFuns);
+
/** print instantiations
*
* Print all instantiations for all quantified formulas on out,
* @param c used for giving an error message to indicate the context
* this method was called.
*/
- smt::Model* getAvailableModel(const char* c) const;
+ theory::TheoryModel* getAvailableModel(const char* c) const;
/**
* Get available quantifiers engine, which throws a modal exception if it
* does not exist. This can happen if a quantifiers-specific call (e.g.
/** The SMT solver */
std::unique_ptr<smt::SmtSolver> d_smtSolver;
- /**
- * The SMT-level model object, which contains information about how to
- * print the model, as well as a pointer to the underlying TheoryModel
- * implementation maintained by the SmtSolver.
- */
- std::unique_ptr<smt::Model> d_model;
-
/**
* The utility used for checking models
*/
% EXPECT: entailed
-% EXPECT: Cannot get model unless immediately preceded by SAT/NOT_ENTAILED or UNKNOWN response.
+% EXPECT: Cannot get model unless after a SAT or unknown response.
OPTION "logic" "ALL";
OPTION "produce-models" true;
x : INT;
ASSERT_THROW(d_solver.isModelCoreSymbol(zero), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, getModel)
+{
+ d_solver.setOption("produce-models", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkConst(uSort, "x");
+ Term y = d_solver.mkConst(uSort, "y");
+ Term z = d_solver.mkConst(uSort, "z");
+ Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y));
+ d_solver.assertFormula(f);
+ d_solver.checkSat();
+ std::vector<Sort> sorts;
+ sorts.push_back(uSort);
+ std::vector<Term> terms;
+ terms.push_back(x);
+ terms.push_back(y);
+ ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
+ Term null;
+ terms.push_back(null);
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, getModel2)
+{
+ d_solver.setOption("produce-models", "true");
+ std::vector<Sort> sorts;
+ std::vector<Term> terms;
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, getModel3)
+{
+ d_solver.setOption("produce-models", "true");
+ std::vector<Sort> sorts;
+ std::vector<Term> terms;
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getModel(sorts, terms));
+ Sort integer = d_solver.getIntegerSort();
+ sorts.push_back(integer);
+ ASSERT_THROW(d_solver.getModel(sorts, terms), CVC5ApiException);
+}
+
TEST_F(TestApiBlackSolver, getQuantifierElimination)
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
projects / cvc5.git / commitdiff