From: Andrew Reynolds Date: Fri, 27 Aug 2021 15:36:27 +0000 (-0500) Subject: Add missing methods to Solver API for models (#7052) X-Git-Tag: cvc5-1.0.0~1328 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8d3e68b892225aba597dc65da2ca2074e520889;p=cvc5.git Add missing methods to Solver API for models (#7052) 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. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index f85286acb..1eaae8761 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7131,6 +7131,51 @@ std::vector Solver::getValue(const std::vector& terms) const CVC5_API_TRY_CATCH_END; } +std::vector 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 res; + std::vector 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()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3c0241311..9f805fa65 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3782,7 +3782,7 @@ class CVC5_EXPORT Solver 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 ( ) ) @@ -3791,8 +3791,9 @@ class CVC5_EXPORT Solver * @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 ( + ) ) @@ -3802,6 +3803,27 @@ class CVC5_EXPORT Solver */ std::vector getValue(const std::vector& 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 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: diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 2665706c0..ef9971c20 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -278,6 +278,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": 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 + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 36dcc066e..68998d521 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1296,6 +1296,18 @@ cdef class Solver: 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() diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b42304ecc..1f1296b7f 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1095,16 +1095,6 @@ void CvcPrinter::toStreamModelTerm(std::ostream& out, 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); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index b7f32123d..523b3efa9 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1262,13 +1262,6 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const 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 diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 0395a32fd..9e9eb5f23 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -25,6 +25,11 @@ bool ModelCoreBuilder::setModelCore(const std::vector& assertions, 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; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 3c0a4ac5b..c36ff1bce 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -135,6 +135,15 @@ Node Preprocessor::expandDefinitions(const Node& node, return n; } +void Preprocessor::expandDefinitions(std::vector& ns) +{ + std::unordered_map 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; diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 3a1f9f080..03246ed67 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -90,6 +90,8 @@ class Preprocessor Node expandDefinitions(const Node& n); /** Same as above, with a cache of previous results. */ Node expandDefinitions(const Node& n, std::unordered_map& cache); + /** Same as above, for a list of assertions, updating in place */ + void expandDefinitions(std::vector& ns); /** * Set proof node manager. Enables proofs in this preprocessor. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ea253e4ef..be5c75af0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const return resultNode; } -std::vector SmtEngine::getValues(const std::vector& exprs) +std::vector SmtEngine::getValues(const std::vector& exprs) const { std::vector result; for (const Node& e : exprs) @@ -1176,6 +1176,39 @@ std::vector SmtEngine::getValues(const std::vector& exprs) return result; } +std::vector 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 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; @@ -1201,10 +1234,10 @@ Model* SmtEngine::getModel() { { // 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 eassertsProc = getExpandedAssertions(); - ModelCoreBuilder::setModelCore(eassertsProc, - m->getTheoryModel(), - d_env->getOptions().smt.modelCoresMode); + std::vector 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); @@ -1294,18 +1327,25 @@ std::pair SmtEngine::getSepHeapAndNilExpr(void) return std::make_pair(heap, nil); } +std::vector SmtEngine::getAssertionsInternal() +{ + Assert(d_state->isFullyInited()); + context::CDList* al = d_asserts->getAssertionList(); + Assert(al != nullptr); + std::vector res; + for (const Node& n : *al) + { + res.emplace_back(n); + } + return res; +} + std::vector SmtEngine::getExpandedAssertions() { std::vector easserts = getAssertions(); // must expand definitions - std::vector eassertsProc; - std::unordered_map 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(); } @@ -1787,15 +1827,7 @@ std::vector SmtEngine::getAssertions() "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } - context::CDList* al = d_asserts->getAssertionList(); - Assert(al != nullptr); - std::vector res; - for (const Node& n : *al) - { - res.emplace_back(n); - } - // copy the result out - return res; + return getAssertionsInternal(); } void SmtEngine::push() diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index d9786f6a1..a250e2a7f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -532,7 +532,17 @@ class CVC5_EXPORT SmtEngine /** * Same as getValue but for a vector of expressions */ - std::vector getValues(const std::vector& exprs); + std::vector getValues(const std::vector& exprs) const; + + /** + * @return the domain elements for uninterpreted sort tn. + */ + std::vector getModelDomainElements(TypeNode tn) const; + + /** + * @return true if v is a model core symbol + */ + bool isModelCoreSymbol(Node v); /** print instantiations * @@ -1022,7 +1032,13 @@ class CVC5_EXPORT SmtEngine * element is the nil expression. */ std::pair 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 getAssertionsInternal(); /* Members -------------------------------------------------------------- */ /** Solver instance that owns this SmtEngine instance. */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 92d15653e..ba1680c6b 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -198,7 +198,6 @@ void TheorySep::postProcessModel( TheoryModel* m ){ 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)) { diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 3e902463c..02a837899 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -74,7 +74,6 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) void TheoryModel::reset(){ d_modelCache.clear(); - d_comment_str.clear(); d_sep_heap = Node::null(); d_sep_nil_eq = Node::null(); d_approximations.clear(); @@ -91,11 +90,6 @@ void TheoryModel::reset(){ 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; @@ -610,6 +604,7 @@ void TheoryModel::recordApproximation(TNode n, TNode pred, Node witness) 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; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 4034e43bd..6841a11d8 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -296,8 +296,6 @@ class TheoryModel * 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 */ @@ -318,6 +316,8 @@ class TheoryModel 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 */ @@ -394,8 +394,6 @@ class TheoryModel /** 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 */ diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 99a60aa76..312d57319 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -1473,6 +1473,57 @@ TEST_F(TestApiBlackSolver, getValue3) 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");