summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rw-r--r--src/theory/model_manager.cpp59
-rw-r--r--src/theory/model_manager.h16
-rw-r--r--src/theory/theory_model.cpp13
-rw-r--r--src/theory/theory_model.h13
-rw-r--r--src/theory/valuation.cpp9
-rw-r--r--src/theory/valuation.h5
7 files changed, 117 insertions, 0 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index f85b79c53..c7e2c7c1b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -108,6 +108,8 @@ void TheoryDatatypes::finishInit()
// do congruence on evaluation functions
d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
}
+ // testers are not relevant for model building
+ d_valuation.setIrrelevantKind(APPLY_TESTER);
}
TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 1451b6ab0..89daa922c 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -162,5 +162,64 @@ bool ModelManager::collectModelBooleanVariables()
return true;
}
+void ModelManager::collectAssertedTerms(TheoryId tid,
+ std::set<Node>& termSet,
+ bool includeShared) const
+{
+ Theory* t = d_te.theoryOf(tid);
+ // Collect all terms appearing in assertions
+ context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(),
+ assert_it_end = t->facts_end();
+ for (; assert_it != assert_it_end; ++assert_it)
+ {
+ collectTerms(tid, *assert_it, termSet);
+ }
+
+ if (includeShared)
+ {
+ // Add terms that are shared terms
+ context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(),
+ shared_it_end =
+ t->shared_terms_end();
+ for (; shared_it != shared_it_end; ++shared_it)
+ {
+ collectTerms(tid, *shared_it, termSet);
+ }
+ }
+}
+
+void ModelManager::collectTerms(TheoryId tid,
+ TNode n,
+ std::set<Node>& termSet) const
+{
+ const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds();
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (termSet.find(cur) != termSet.end())
+ {
+ // already visited
+ continue;
+ }
+ Kind k = cur.getKind();
+ // only add to term set if a relevant kind
+ if (irrKinds.find(k) == irrKinds.end())
+ {
+ Assert(Theory::theoryOf(cur) == tid);
+ termSet.insert(cur);
+ }
+ // traverse owned terms, don't go under quantifiers
+ if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid)
+ && !cur.isClosure())
+ {
+ visit.insert(visit.end(), cur.begin(), cur.end());
+ }
+ } while (!visit.empty());
+}
+
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 12b99dc18..9fc2e1156 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -91,6 +91,22 @@ class ModelManager
* @return true if we are in conflict.
*/
bool collectModelBooleanVariables();
+ /**
+ * Collect asserted terms for theory with the given identifier, add to
+ * termSet.
+ *
+ * @param tid The theory whose assertions we are collecting
+ * @param termSet The set to add terms to
+ * @param includeShared Whether to include the shared terms of the theory
+ */
+ void collectAssertedTerms(TheoryId tid,
+ std::set<Node>& termSet,
+ bool includeShared = true) const;
+ /**
+ * Helper function for collectAssertedTerms, adds all subterms
+ * belonging to theory tid to termSet.
+ */
+ void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
/** Reference to the theory engine */
TheoryEngine& d_te;
/** Logic info of theory engine (cached) */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 31b44aa70..869e9100e 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -72,6 +72,12 @@ void TheoryModel::finishInit()
{
setSemiEvaluatedKind(kind::APPLY_UF);
}
+ // Equal and not terms are not relevant terms. In other words, asserted
+ // equalities and negations of predicates (as terms) do not need to be sent
+ // to the model. Regardless, theories should send information to the model
+ // that ensures that all assertions are satisfied.
+ setIrrelevantKind(EQUAL);
+ setIrrelevantKind(NOT);
}
void TheoryModel::reset(){
@@ -627,6 +633,13 @@ void TheoryModel::setSemiEvaluatedKind(Kind k)
d_semi_evaluated_kinds.insert(k);
}
+void TheoryModel::setIrrelevantKind(Kind k) { d_irrKinds.insert(k); }
+
+const std::set<Kind>& TheoryModel::getIrrelevantKinds() const
+{
+ return d_irrKinds;
+}
+
bool TheoryModel::isLegalElimination(TNode x, TNode val)
{
return !expr::hasSubtermKinds(d_unevaluated_kinds, val);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index b725cfa09..c31f208a0 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -262,6 +262,17 @@ public:
*/
void setUnevaluatedKind(Kind k);
void setSemiEvaluatedKind(Kind k);
+ /**
+ * Set irrelevant kind. These kinds do not impact model generation, that is,
+ * registered terms in theories of this kind do not need to be sent to
+ * the model. An example is APPLY_TESTER.
+ */
+ void setIrrelevantKind(Kind k);
+ /**
+ * Get the set of irrelevant kinds that have been registered by the above
+ * method.
+ */
+ const std::set<Kind>& getIrrelevantKinds() const;
/** is legal elimination
*
* Returns true if x -> val is a legal elimination of variable x.
@@ -358,6 +369,8 @@ public:
std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
/** a set of kinds that are semi-evaluated */
std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
+ /** The set of irrelevant kinds */
+ std::set<Kind> d_irrKinds;
/**
* Map of representatives of equality engine to used representatives in
* representative set
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 9375a4868..bec528215 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -145,6 +145,15 @@ void Valuation::setSemiEvaluatedKind(Kind k)
}
}
+void Valuation::setIrrelevantKind(Kind k)
+{
+ TheoryModel* m = getModel();
+ if (m != nullptr)
+ {
+ m->setIrrelevantKind(k);
+ }
+}
+
Node Valuation::ensureLiteral(TNode n) {
Assert(d_engine != nullptr);
return d_engine->ensureLiteral(n);
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 35d990715..dc12d030d 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -122,6 +122,11 @@ public:
* See TheoryModel::setSemiEvaluatedKind for details.
*/
void setSemiEvaluatedKind(Kind k);
+ /**
+ * Set that k is an irrelevant kind in the TheoryModel, if it exists.
+ * See TheoryModel::setIrrelevantKind for details.
+ */
+ void setIrrelevantKind(Kind k);
//-------------------------------------- end static configuration of the model
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback