This adds the last two remaining API methods required for implementing the text output of get-model on the API side.
A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.
This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
CVC5_API_TRY_CATCH_END;
}
+std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ NodeManagerScope scope(getNodeManager());
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ << "Cannot get domain elements unless model generation is enabled "
+ "(try --produce-models)";
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Cannot get domain elements unless after a SAT or unknown response.";
+ CVC5_API_SOLVER_CHECK_SORT(s);
+ CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
+ << "Expecting an uninterpreted sort as argument to "
+ "getModelDomainElements.";
+ //////// all checks before this line
+ std::vector<Term> res;
+ std::vector<Node> elements =
+ d_smtEngine->getModelDomainElements(s.getTypeNode());
+ for (const Node& n : elements)
+ {
+ res.push_back(Term(this, n));
+ }
+ return res;
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
+bool Solver::isModelCoreSymbol(const Term& v) const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ NodeManagerScope scope(getNodeManager());
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
+ << "Cannot check if model core symbol unless model generation is enabled "
+ "(try --produce-models)";
+ CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
+ << "Cannot check if model core symbol unless after a SAT or unknown "
+ "response.";
+ CVC5_API_SOLVER_CHECK_TERM(v);
+ CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
+ << "Expecting a free constant as argument to isModelCoreSymbol.";
+ //////// all checks before this line
+ return d_smtEngine->isModelCoreSymbol(v.getNode());
+ ////////
+ CVC5_API_TRY_CATCH_END;
+}
+
Term Solver::getQuantifierElimination(const Term& q) const
{
NodeManagerScope scope(getNodeManager());
std::string getProof() const;
/**
- * Get the value of the given term.
+ * Get the value of the given term in the current model.
* SMT-LIB:
* \verbatim
* ( get-value ( <term> ) )
* @return the value of the given term
*/
Term getValue(const Term& term) const;
+
/**
- * Get the values of the given terms.
+ * Get the values of the given terms in the current model.
* SMT-LIB:
* \verbatim
* ( get-value ( <term>+ ) )
*/
std::vector<Term> getValue(const std::vector<Term>& terms) const;
+ /**
+ * Get the domain elements of uninterpreted sort s in the current model. The
+ * current model interprets s as the finite sort whose domain elements are
+ * given in the return value of this method.
+ *
+ * @param s The uninterpreted sort in question
+ * @return the domain elements of s in the current model
+ */
+ std::vector<Term> getModelDomainElements(const Sort& s) const;
+
+ /**
+ * This returns false if the model value of free constant v was not essential
+ * for showing the satisfiability of the last call to checkSat using the
+ * current model. This method will only return false (for any v) if
+ * the model-cores option has been set.
+ *
+ * @param v The term in question
+ * @return true if v is a model core symbol
+ */
+ bool isModelCoreSymbol(const Term& v) const;
+
/**
* Do quantifier elimination.
* SMT-LIB:
vector[Term] getUnsatCore() except +
Term getValue(Term term) except +
vector[Term] getValue(const vector[Term]& terms) except +
+ vector[Term] getModelDomainElements(Sort sort) except +
+ bint isModelCoreSymbol(Term v) except +
void declareSeparationHeap(Sort locSort, Sort dataSort) except +
Term getSeparationHeap() except +
Term getSeparationNilTerm() except +
term.cterm = self.csolver.getValue(t.cterm)
return term
+ def getModelDomainElements(self, Sort s):
+ result = []
+ cresult = self.csolver.getModelDomainElements(s.csort)
+ for e in cresult:
+ term = Term(self)
+ term.cterm = e
+ result.append(term)
+ return result
+
+ def isModelCoreSymbol(self, Term v):
+ return self.csolver.isModelCoreSymbol(v.cterm)
+
def getSeparationHeap(self):
cdef Term term = Term(self)
term.cterm = self.csolver.getSeparationHeap()
void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const
{
- const theory::TheoryModel* tm = m.getTheoryModel();
- // print the model comments
- std::stringstream c;
- tm->getComments(c);
- std::string ln;
- while (std::getline(c, ln))
- {
- out << "; " << ln << std::endl;
- }
-
// print the model
out << "MODEL BEGIN" << std::endl;
this->Printer::toStream(out, m);
void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const
{
const theory::TheoryModel* tm = m.getTheoryModel();
- //print the model comments
- std::stringstream c;
- tm->getComments(c);
- std::string ln;
- while( std::getline( c, ln ) ){
- out << "; " << ln << std::endl;
- }
//print the model
out << "(" << endl;
// don't need to print approximations since they are built into choice
theory::TheoryModel* m,
options::ModelCoresMode mode)
{
+ if (m->isUsingModelCore())
+ {
+ // already computed
+ return true;
+ }
if (Trace.isOn("model-core"))
{
Trace("model-core") << "Compute model core, assertions:" << std::endl;
return n;
}
+void Preprocessor::expandDefinitions(std::vector<Node>& ns)
+{
+ std::unordered_map<Node, Node> cache;
+ for (size_t i = 0, nasserts = ns.size(); i < nasserts; i++)
+ {
+ ns[i] = expandDefinitions(ns[i], cache);
+ }
+}
+
Node Preprocessor::simplify(const Node& node)
{
Trace("smt") << "SMT simplify(" << node << ")" << endl;
Node expandDefinitions(const Node& n);
/** Same as above, with a cache of previous results. */
Node expandDefinitions(const Node& n, std::unordered_map<Node, Node>& cache);
+ /** Same as above, for a list of assertions, updating in place */
+ void expandDefinitions(std::vector<Node>& ns);
/**
* Set proof node manager. Enables proofs in this preprocessor.
*/
return resultNode;
}
-std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs)
+std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
{
std::vector<Node> result;
for (const Node& e : exprs)
return result;
}
+std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const
+{
+ Assert(tn.isSort());
+ Model* m = getAvailableModel("getModelDomainElements");
+ return m->getTheoryModel()->getDomainElements(tn);
+}
+
+bool SmtEngine::isModelCoreSymbol(Node n)
+{
+ SmtScope smts(this);
+ Assert(n.isVar());
+ const Options& opts = d_env->getOptions();
+ if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE)
+ {
+ // if the model core mode is none, we are always a model core symbol
+ return true;
+ }
+ Model* m = getAvailableModel("isModelCoreSymbol");
+ TheoryModel* tm = m->getTheoryModel();
+ // compute the model core if not done so already
+ if (!tm->isUsingModelCore())
+ {
+ // If we enabled model cores, we compute a model core for m based on our
+ // (expanded) assertions using the model core builder utility. Notice that
+ // we get the assertions using the getAssertionsInternal, which does not
+ // impact whether we are in "sat" mode
+ std::vector<Node> asserts = getAssertionsInternal();
+ d_pp->expandDefinitions(asserts);
+ ModelCoreBuilder::setModelCore(asserts, tm, opts.smt.modelCoresMode);
+ }
+ return tm->isModelCoreSymbol(n);
+}
+
// TODO(#1108): Simplify the error reporting of this method.
Model* SmtEngine::getModel() {
Trace("smt") << "SMT getModel()" << endl;
{
// 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> eassertsProc = getExpandedAssertions();
- ModelCoreBuilder::setModelCore(eassertsProc,
- m->getTheoryModel(),
- d_env->getOptions().smt.modelCoresMode);
+ std::vector<Node> asserts = getAssertionsInternal();
+ d_pp->expandDefinitions(asserts);
+ ModelCoreBuilder::setModelCore(
+ asserts, m->getTheoryModel(), d_env->getOptions().smt.modelCoresMode);
}
// set the information on the SMT-level model
Assert(m != nullptr);
return std::make_pair(heap, nil);
}
+std::vector<Node> SmtEngine::getAssertionsInternal()
+{
+ Assert(d_state->isFullyInited());
+ context::CDList<Node>* al = d_asserts->getAssertionList();
+ Assert(al != nullptr);
+ std::vector<Node> res;
+ for (const Node& n : *al)
+ {
+ res.emplace_back(n);
+ }
+ return res;
+}
+
std::vector<Node> SmtEngine::getExpandedAssertions()
{
std::vector<Node> easserts = getAssertions();
// must expand definitions
- std::vector<Node> eassertsProc;
- std::unordered_map<Node, Node> cache;
- for (const Node& e : easserts)
- {
- Node eae = d_pp->expandDefinitions(e, cache);
- eassertsProc.push_back(eae);
- }
- return eassertsProc;
+ d_pp->expandDefinitions(easserts);
+ return easserts;
}
Env& SmtEngine::getEnv() { return *d_env.get(); }
"Cannot query the current assertion list when not in produce-assertions mode.";
throw ModalException(msg);
}
- context::CDList<Node>* al = d_asserts->getAssertionList();
- Assert(al != nullptr);
- std::vector<Node> res;
- for (const Node& n : *al)
- {
- res.emplace_back(n);
- }
- // copy the result out
- return res;
+ return getAssertionsInternal();
}
void SmtEngine::push()
/**
* Same as getValue but for a vector of expressions
*/
- std::vector<Node> getValues(const std::vector<Node>& exprs);
+ std::vector<Node> getValues(const std::vector<Node>& exprs) const;
+
+ /**
+ * @return the domain elements for uninterpreted sort tn.
+ */
+ std::vector<Node> getModelDomainElements(TypeNode tn) const;
+
+ /**
+ * @return true if v is a model core symbol
+ */
+ bool isModelCoreSymbol(Node v);
/** print instantiations
*
* element is the nil expression.
*/
std::pair<Node, Node> getSepHeapAndNilExpr();
-
+ /**
+ * Get assertions internal, which is only called after initialization. This
+ * should be used internally to get the assertions instead of getAssertions
+ * or getExpandedAssertions, which may trigger initialization and SMT state
+ * changes.
+ */
+ std::vector<Node> getAssertionsInternal();
/* Members -------------------------------------------------------------- */
/** Solver instance that owns this SmtEngine instance. */
Trace("sep-model") << " " << l << " -> ";
if( d_pto_model[l].isNull() ){
Trace("sep-model") << "_";
- //m->d_comment_str << "_";
TypeEnumerator te_range( data_type );
if (d_state.isFiniteType(data_type))
{
void TheoryModel::reset(){
d_modelCache.clear();
- d_comment_str.clear();
d_sep_heap = Node::null();
d_sep_nil_eq = Node::null();
d_approximations.clear();
d_model_core.clear();
}
-void TheoryModel::getComments(std::ostream& out) const {
- Trace("model-builder") << "get comments..." << std::endl;
- out << d_comment_str.str();
-}
-
void TheoryModel::setHeapModel( Node h, Node neq ) {
d_sep_heap = h;
d_sep_nil_eq = neq;
Node predDisj = NodeManager::currentNM()->mkNode(OR, n.eqNode(witness), pred);
recordApproximation(n, predDisj);
}
+bool TheoryModel::isUsingModelCore() const { return d_using_model_core; }
void TheoryModel::setUsingModelCore()
{
d_using_model_core = true;
* has called buildModel(...) on this model.
*/
Node getValue(TNode n) const;
- /** get comments */
- void getComments(std::ostream& out) const;
//---------------------------- separation logic
/** set the heap and value sep.nil is equal to */
RepSet* getRepSetPtr() { return &d_rep_set; }
//---------------------------- model cores
+ /** True if a model core has been computed for this model. */
+ bool isUsingModelCore() const;
/** set using model core */
void setUsingModelCore();
/** record model core symbol */
/** true/false nodes */
Node d_true;
Node d_false;
- /** comment stream to include in printing */
- std::stringstream d_comment_str;
/** are we using model cores? */
bool d_using_model_core;
/** symbols that are in the model core */
ASSERT_THROW(slv.getValue(x), CVC5ApiException);
}
+TEST_F(TestApiBlackSolver, getModelDomainElements)
+{
+ d_solver.setOption("produce-models", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Sort intSort = d_solver.getIntegerSort();
+ 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(DISTINCT, x, y, z);
+ d_solver.assertFormula(f);
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort));
+ ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() >= 3);
+ ASSERT_THROW(d_solver.getModelDomainElements(intSort), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, getModelDomainElements2)
+{
+ d_solver.setOption("produce-models", "true");
+ d_solver.setOption("finite-model-find", "true");
+ Sort uSort = d_solver.mkUninterpretedSort("u");
+ Term x = d_solver.mkVar(uSort, "x");
+ Term y = d_solver.mkVar(uSort, "y");
+ Term eq = d_solver.mkTerm(EQUAL, x, y);
+ Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y);
+ Term f = d_solver.mkTerm(FORALL, bvl, eq);
+ d_solver.assertFormula(f);
+ d_solver.checkSat();
+ ASSERT_NO_THROW(d_solver.getModelDomainElements(uSort));
+ // a model for the above must interpret u as size 1
+ ASSERT_TRUE(d_solver.getModelDomainElements(uSort).size() == 1);
+}
+
+TEST_F(TestApiBlackSolver, isModelCoreSymbol)
+{
+ d_solver.setOption("produce-models", "true");
+ d_solver.setOption("model-cores", "simple");
+ 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 zero = d_solver.mkInteger(0);
+ Term f = d_solver.mkTerm(NOT, d_solver.mkTerm(EQUAL, x, y));
+ d_solver.assertFormula(f);
+ d_solver.checkSat();
+ ASSERT_TRUE(d_solver.isModelCoreSymbol(x));
+ ASSERT_TRUE(d_solver.isModelCoreSymbol(y));
+ ASSERT_FALSE(d_solver.isModelCoreSymbol(z));
+ ASSERT_THROW(d_solver.isModelCoreSymbol(zero), CVC5ApiException);
+}
+
TEST_F(TestApiBlackSolver, getQuantifierElimination)
{
Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
projects / cvc5.git / commitdiff