/*! \file theory.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Mathias Preiner, Dejan Jovanovic
+ ** Andrew Reynolds, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
#include "base/check.h"
#include "expr/node_algorithm.h"
+#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/ext_theory.h"
os << "EFFORT_STANDARD"; break;
case Theory::EFFORT_FULL:
os << "EFFORT_FULL"; break;
- case Theory::EFFORT_COMBINATION:
- os << "EFFORT_COMBINATION"; break;
case Theory::EFFORT_LAST_CALL:
os << "EFFORT_LAST_CALL"; break;
default:
d_satContext(satContext),
d_userContext(userContext),
d_logicInfo(logicInfo),
- d_pnm(pnm),
d_facts(satContext),
d_factsHead(satContext, 0),
d_sharedTermsIndex(satContext, 0),
d_equalityEngine(nullptr),
d_allocEqualityEngine(nullptr),
d_theoryState(nullptr),
- d_proofsEnabled(false)
+ d_inferManager(nullptr),
+ d_pnm(pnm)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
{
// set the equality engine pointer
d_equalityEngine = ee;
+ if (d_theoryState != nullptr)
+ {
+ d_theoryState->setEqualityEngine(ee);
+ }
+ if (d_inferManager != nullptr)
+ {
+ d_inferManager->setEqualityEngine(ee);
+ }
}
+
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
{
Assert(d_quantEngine == nullptr);
+ // quantifiers engine may be null if not in quantified logic
d_quantEngine = qe;
}
d_allocEqualityEngine.reset(new eq::EqualityEngine(
*esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
// use it as the official equality engine
- d_equalityEngine = d_allocEqualityEngine.get();
+ setEqualityEngine(d_allocEqualityEngine.get());
}
finishInit();
}
tid = Theory::theoryOf(node.getType());
}
}
- else if (node.isConst())
- {
- tid = Theory::theoryOf(node.getType());
- }
else if (node.getKind() == kind::EQUAL)
{
// Equality is owned by the theory that owns the domain
}
else
{
- // Regular nodes are owned by the kind
+ // Regular nodes are owned by the kind. Notice that constants are a
+ // special case here, where the theory of the kind of a constant
+ // always coincides with the type of that constant.
tid = kindToTheoryId(node.getKind());
}
break;
}
}
}
- else if (node.isConst())
- {
- // Constants go to the theory of the type
- tid = Theory::theoryOf(node.getType());
- }
else if (node.getKind() == kind::EQUAL)
{ // Equality
// If one of them is an ITE, it's irelevant, since they will get
}
else
{
- // Regular nodes are owned by the kind
+ // Regular nodes are owned by the kind, which includes constants as a
+ // special case.
tid = kindToTheoryId(node.getKind());
}
break;
return tid;
}
-void Theory::addSharedTermInternal(TNode n) {
- Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
- Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
- d_sharedTerms.push_back(n);
- addSharedTerm(n);
+void Theory::notifySharedTerm(TNode n)
+{
+ // do nothing
}
void Theory::computeCareGraph() {
switch (d_valuation.getEqualityStatus(a, b)) {
case EQUALITY_TRUE_AND_PROPAGATED:
case EQUALITY_FALSE_AND_PROPAGATED:
- // If we know about it, we should have propagated it, so we can skip
- break;
+ // If we know about it, we should have propagated it, so we can skip
+ break;
default:
- // Let's split on it
- addCarePair(a, b);
- break;
+ // Let's split on it
+ addCarePair(a, b);
+ break;
}
}
}
return currentlyShared;
}
-bool Theory::collectModelInfo(TheoryModel* m)
+bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
{
- std::set<Node> termSet;
- // Compute terms appearing in assertions and shared terms
- 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,
- set<Kind>& irrKinds,
- set<Node>& termSet) const
+void Theory::computeRelevantTerms(std::set<Node>& termSet)
{
- 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);
- }
- }
+ // by default, there are no additional relevant terms
}
-void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
- std::set<Kind>& irrKinds,
- bool includeShared) const
-{
- // Collect all terms appearing in assertions
- irrKinds.insert(kind::EQUAL);
- irrKinds.insert(kind::NOT);
- 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
- 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, bool includeShared)
-{
- std::set<Kind> irrKinds;
- computeRelevantTermsInternal(termSet, irrKinds, includeShared);
-}
-
-bool Theory::collectModelValues(TheoryModel* m, std::set<Node>& termSet)
+bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
{
return true;
}
-Theory::PPAssertStatus Theory::ppAssert(TNode in,
- SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
+ TrustSubstitutionMap& outSubstitutions)
{
+ TNode in = tin.getNode();
if (in.getKind() == kind::EQUAL)
{
// (and (= x t) phi) can be replaced by phi[x/t] if
if (in[0].isVar() && isLegalElimination(in[0], in[1])
&& in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
{
- outSubstitutions.addSubstitution(in[0], in[1]);
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
return PP_ASSERT_STATUS_SOLVED;
}
if (in[1].isVar() && isLegalElimination(in[1], in[0])
&& in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
{
- outSubstitutions.addSubstitution(in[1], in[0]);
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
return PP_ASSERT_STATUS_SOLVED;
}
if (in[0].isConst() && in[1].isConst())
d_careGraph = NULL;
}
+EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
+{
+ // if not using an equality engine, then by default we don't know the status
+ if (d_equalityEngine == nullptr)
+ {
+ return EQUALITY_UNKNOWN;
+ }
+ Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
+ Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
+
+ // Check for equality (simplest)
+ if (d_equalityEngine->areEqual(a, b))
+ {
+ // The terms are implied to be equal
+ return EQUALITY_TRUE;
+ }
+
+ // Check for disequality
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
+ }
+
+ // All other terms are unknown, which is conservative. A theory may override
+ // this method if it knows more information.
+ return EQUALITY_UNKNOWN;
+}
+
+void Theory::check(Effort level)
+{
+ // see if we are already done (as an optimization)
+ if (done() && level < EFFORT_FULL)
+ {
+ return;
+ }
+ Assert(d_theoryState!=nullptr);
+ // 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
+ if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
+ {
+ // 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);
+ // assert to the equality engine
+ if (atom.getKind() == kind::EQUAL)
+ {
+ d_equalityEngine->assertEquality(atom, polarity, fact);
+ }
+ else
+ {
+ 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; }
+
+void Theory::postCheck(Effort level) {}
+
+bool Theory::preNotifyFact(
+ TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+ return false;
+}
+
+void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
+{
+}
+
+void Theory::preRegisterTerm(TNode node) {}
+
+void Theory::addSharedTerm(TNode n)
+{
+ Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
+ << std::endl;
+ Debug("theory::assertions")
+ << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
+ 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()
{
// get the assigned equality engine, which is a pointer stored in this class
projects / cvc5.git / blobdiff