summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cpp/cvc5.cpp45
-rw-r--r--src/api/cpp/cvc5.h26
-rw-r--r--src/api/python/cvc5.pxd2
-rw-r--r--src/api/python/cvc5.pxi12
-rw-r--r--src/printer/cvc/cvc_printer.cpp10
-rw-r--r--src/printer/smt2/smt2_printer.cpp7
-rw-r--r--src/smt/model_core_builder.cpp5
-rw-r--r--src/smt/preprocessor.cpp9
-rw-r--r--src/smt/preprocessor.h2
-rw-r--r--src/smt/smt_engine.cpp76
-rw-r--r--src/smt/smt_engine.h20
-rw-r--r--src/theory/sep/theory_sep.cpp1
-rw-r--r--src/theory/theory_model.cpp7
-rw-r--r--src/theory/theory_model.h6
-rw-r--r--test/unit/api/solver_black.cpp51
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");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback