diff options
-rw-r--r-- | src/api/cpp/cvc5.cpp | 45 | ||||
-rw-r--r-- | src/api/cpp/cvc5.h | 26 | ||||
-rw-r--r-- | src/api/python/cvc5.pxd | 2 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 12 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 10 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 7 | ||||
-rw-r--r-- | src/smt/model_core_builder.cpp | 5 | ||||
-rw-r--r-- | src/smt/preprocessor.cpp | 9 | ||||
-rw-r--r-- | src/smt/preprocessor.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 76 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 20 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 1 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_model.h | 6 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 51 |
15 files changed, 225 insertions, 54 deletions
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<Term> Solver::getValue(const std::vector<Term>& terms) const 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()); 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 ( <term> ) ) @@ -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 ( <term>+ ) ) @@ -3803,6 +3804,27 @@ class CVC5_EXPORT Solver 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: * \verbatim 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<Node>& 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<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; 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<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. */ 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<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) @@ -1176,6 +1176,39 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& 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; @@ -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<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); @@ -1294,18 +1327,25 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) 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(); } @@ -1787,15 +1827,7 @@ std::vector<Node> SmtEngine::getAssertions() "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() 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<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 * @@ -1022,7 +1032,13 @@ class CVC5_EXPORT SmtEngine * 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. */ 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"); |