This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.
d_ee->assertEquality(eq, true, reason);
}
-void ArithCongruenceManager::addSharedTerm(Node x){
- d_ee->addTriggerTerm(x, THEORY_ARITH);
-}
-
bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
std::vector<Node> andComponents(TNode an)
void equalsConstant(ConstraintCP eq);
void equalsConstant(ConstraintCP lb, ConstraintCP ub);
-
- void addSharedTerm(Node x);
-
private:
class Statistics {
public:
d_internal->propagate(e);
}
-bool TheoryArith::collectModelInfo(TheoryModel* m)
+bool TheoryArith::collectModelInfo(TheoryModel* m,
+ const std::set<Node>& termSet)
{
- std::set<Node> termSet;
- // Work out which variables are needed
- const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
- computeAssertedTerms(termSet, irrKinds);
// this overrides behavior to not assert equality engine
return collectModelValues(m, termSet);
}
void propagate(Effort e) override;
TrustNode explain(TNode n) override;
- bool collectModelInfo(TheoryModel* m) override;
+ bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet) override;
/**
* Collect model values in m based on the relevant terms given by termSet.
*/
if(n.isConst()){
d_partialModel.invalidateDelta();
}
- d_congruenceManager.addSharedTerm(n);
if(!n.isConst() && !isSetup(n)){
Polynomial poly = Polynomial::parsePolynomial(n);
Polynomial::iterator it = poly.begin();
Debug("arrays::sharing") << spaces(getSatContext()->getLevel())
<< "TheoryArrays::notifySharedTerm(" << t << ")"
<< std::endl;
- d_equalityEngine->addTriggerTerm(t, THEORY_ARRAYS);
if (t.getType().isArray()) {
d_sharedArrays.insert(t);
}
void TheoryBV::notifySharedTerm(TNode t)
{
d_internal->notifySharedTerm(t);
- // temporary, will be built into Theory::addSharedTerm
- if (d_equalityEngine != nullptr)
- {
- d_equalityEngine->addTriggerTerm(t, THEORY_BV);
- }
}
void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
return d_conv.getValue(d_valuation, var);
}
-bool TheoryFp::collectModelInfo(TheoryModel* m)
+bool TheoryFp::collectModelInfo(TheoryModel* m,
+ const std::set<Node>& relevantTerms)
{
- std::set<Node> relevantTerms;
- // Work out which variables are needed
- const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
- computeAssertedTerms(relevantTerms, irrKinds);
// this override behavior to not assert equality engine
return collectModelValues(m, relevantTerms);
}
//--------------------------------- end standard check
Node getModelValue(TNode var) override;
- bool collectModelInfo(TheoryModel* m) override;
+ bool collectModelInfo(TheoryModel* m,
+ const std::set<Node>& relevantTerms) override;
/** Collect model values in m based on the relevant terms given by
* relevantTerms */
bool collectModelValues(TheoryModel* m,
Theory* t = d_te.theoryOf(theoryId);
Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
<< std::endl;
- if (!t->collectModelInfo(d_model))
+ // collect the asserted terms
+ std::set<Node> termSet;
+ collectAssertedTerms(theoryId, termSet);
+ // also get relevant terms
+ t->computeRelevantTerms(termSet);
+ if (!t->collectModelInfo(d_model, termSet))
{
Trace("model-builder")
<< "ModelManagerDistributed: fail collect model info" << std::endl;
d_equalityEngine->addTriggerPredicate(node);
}
break;
- case kind::CARD: d_equalityEngine->addTriggerTerm(node, THEORY_SETS); break;
default: d_equalityEngine->addTerm(node); break;
}
}
{
Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " "
<< t.getType().isBoolean() << endl;
- d_equalityEngine->addTriggerTerm(t, THEORY_STRINGS);
if (options::stringExp())
{
d_esolver.addSharedTerm(t);
void Theory::notifySharedTerm(TNode n)
{
- // TODO (project #39): this will move to addSharedTerm, as every theory with
- // an equality does this in their notifySharedTerm method.
- // if we have an equality engine, add the trigger term
- if (d_equalityEngine != nullptr)
- {
- d_equalityEngine->addTriggerTerm(n, d_id);
- }
+ // do nothing
}
void Theory::computeCareGraph() {
return currentlyShared;
}
-bool Theory::collectModelInfo(TheoryModel* m)
+bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
{
- // NOTE: the computation of termSet will be moved to model manager
- // and passed as an argument to collectModelInfo.
- std::set<Node> termSet;
- // Compute terms appearing in assertions and shared terms
- TheoryModel* tm = d_valuation.getModel();
- Assert(tm != nullptr);
- const std::set<Kind>& irrKinds = tm->getIrrelevantKinds();
- computeAssertedTerms(termSet, irrKinds, true);
- // Compute additional relevant terms (theory-specific)
- computeRelevantTerms(termSet);
// if we are using an equality engine, assert it to the model
if (d_equalityEngine != nullptr)
{
return collectModelValues(m, termSet);
}
-void Theory::collectTerms(TNode n,
- const std::set<Kind>& irrKinds,
- set<Node>& termSet) const
-{
- if (termSet.find(n) != termSet.end()) {
- return;
- }
- Kind nk = n.getKind();
- if (irrKinds.find(nk) == irrKinds.end())
- {
- Trace("theory::collectTerms")
- << "Theory::collectTerms: adding " << n << endl;
- termSet.insert(n);
- }
- if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
- {
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- collectTerms(*child_it, irrKinds, termSet);
- }
- }
-}
-
-void Theory::computeAssertedTerms(std::set<Node>& termSet,
- const std::set<Kind>& irrKinds,
- bool includeShared) const
-{
- // Collect all terms appearing in assertions
- context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
- assert_it_end = facts_end();
- for (; assert_it != assert_it_end; ++assert_it)
- {
- collectTerms(*assert_it, irrKinds, termSet);
- }
-
- if (!includeShared)
- {
- return;
- }
- // Add terms that are shared terms
- std::set<Kind> kempty;
- context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
- shared_it_end = shared_terms_end();
- for (; shared_it != shared_it_end; ++shared_it)
- {
- collectTerms(*shared_it, kempty, termSet);
- }
-}
-
void Theory::computeRelevantTerms(std::set<Node>& termSet)
{
// by default, there are no additional relevant terms
// standard calls for resource, stats
d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
TimerStat::CodeTimer checkTimer(d_checkTime);
+ Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
+ << std::endl;
// pre-check at level
if (preCheck(level))
{
// check aborted for a theory-specific reason
return;
}
+ Assert(d_theoryState != nullptr);
+ Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
// process the pending fact queue
while (!done() && !d_theoryState->isInConflict())
{
// Get the next assertion from the fact queue
Assertion assertion = get();
TNode fact = assertion.d_assertion;
+ Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
+ << std::endl;
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
// call the pre-notify method
// handled in theory-specific way that doesn't involve equality engine
continue;
}
+ Trace("theory-check") << "Theory::assert " << fact << " " << d_id
+ << std::endl;
// Theories that don't have an equality engine should always return true
// for preNotifyFact
Assert(d_equalityEngine != nullptr);
{
d_equalityEngine->assertPredicate(atom, polarity, fact);
}
+ Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
+ << std::endl;
// notify the theory of the new fact, which is not internal
notifyFact(atom, polarity, fact, false);
}
+ Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
// post-check at level
postCheck(level);
+ Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
}
bool Theory::preCheck(Effort level) { return false; }
d_sharedTerms.push_back(n);
// now call theory-specific method notifySharedTerm
notifySharedTerm(n);
+ // if we have an equality engine, add the trigger term
+ if (d_equalityEngine != nullptr)
+ {
+ d_equalityEngine->addTriggerTerm(n, d_id);
+ }
}
eq::EqualityEngine* Theory::getEqualityEngine()
*/
context::CDList<TNode> d_sharedTerms;
- //---------------------------------- private collect model info
- /**
- * Helper function for computeRelevantTerms
- */
- void collectTerms(TNode n,
- const std::set<Kind>& irrKinds,
- std::set<Node>& termSet) const;
- //---------------------------------- end private collect model info
-
/**
* Construct a Theory.
*
/** Get the decision manager associated to this theory. */
DecisionManager* getDecisionManager() { return d_decManager; }
+ /**
+ * @return The theory state associated with this theory.
+ */
+ TheoryState* getTheoryState() { return d_theoryState; }
+
+ /**
+ * @return The theory inference manager associated with this theory.
+ */
+ TheoryInferenceManager* getInferenceManager() { return d_inferManager; }
+
/**
* Expand definitions in the term node. This returns a term that is
* equivalent to node. It wraps this term in a TrustNode of kind
*
* Theories that use this check method must use an official theory
* state object (d_theoryState).
- *
- * TODO (project #39): this method should be non-virtual, once all theories
- * conform to the new standard
*/
- virtual void check(Effort level = EFFORT_FULL);
+ void check(Effort level = EFFORT_FULL);
/**
* Pre-check, called before the fact queue of the theory is processed.
* If this method returns false, then the theory will process its fact
* then calls computeModelValues.
*
* TODO (project #39): this method should be non-virtual, once all theories
- * conform to the new standard
- */
- virtual bool collectModelInfo(TheoryModel* m);
- /**
- * Scans the current set of assertions and shared terms top-down
- * until a theory-leaf is reached, and adds all terms found to
- * termSet. This is used by collectModelInfo to delimit the set of
- * terms that should be used when constructing a model.
- *
- * @param irrKinds The kinds of terms that appear in assertions that should *not*
- * be included in termSet. Note that the kinds EQUAL and NOT are always
- * treated as irrelevant kinds.
- *
- * @param includeShared Whether to include shared terms in termSet. Notice that
- * shared terms are not influenced by irrKinds.
- *
- * TODO (project #39): this method will be deleted. The version in
- * model manager will be used.
+ * conform to the new standard, delete, move to model manager distributed.
*/
- void computeAssertedTerms(std::set<Node>& termSet,
- const std::set<Kind>& irrKinds,
- bool includeShared = true) const;
+ virtual bool collectModelInfo(TheoryModel* m, const std::set<Node>& termSet);
/**
* Compute terms that are not necessarily part of the assertions or
* shared terms that should be considered relevant, add them to termSet.
/** assert equality engine */
bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee,
- set<Node>* termSet)
+ const std::set<Node>* termSet)
{
Assert(d_equalityEngine->consistent());
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
* is consistent after asserting the equality engine to this model.
*/
bool assertEqualityEngine(const eq::EqualityEngine* ee,
- std::set<Node>* termSet = NULL);
+ const std::set<Node>* termSet = NULL);
/** assert skeleton
*
* This method gives a "skeleton" for the model value of the equivalence
void preRegisterTerm(TNode) override { Unimplemented(); }
void registerTerm(TNode) { Unimplemented(); }
- void check(Theory::Effort) override { Unimplemented(); }
void propagate(Theory::Effort) override { Unimplemented(); }
TrustNode explain(TNode) override
{
projects / cvc5.git / commitdiff