/*! \file theory.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Andrew Reynolds, Dejan Jovanovic
+ ** Andrew Reynolds, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** 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 "theory/theory.h"
-#include <vector>
-#include <sstream>
#include <iostream>
+#include <sstream>
#include <string>
+#include <vector>
-#include "base/cvc4_assert.h"
+#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/substitutions.h"
+#include "theory/ext_theory.h"
#include "theory/quantifiers_engine.h"
-
+#include "theory/substitutions.h"
+#include "theory/theory_rewriter.h"
using namespace std;
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:
return os;
}/* ostream& operator<<(ostream&, Theory::Effort) */
-
-Theory::Theory(TheoryId id, context::Context* satContext,
- context::UserContext* userContext, OutputChannel& out,
- Valuation valuation, const LogicInfo& logicInfo,
- std::string name) throw()
- : d_id(id)
- , d_instanceName(name)
- , d_satContext(satContext)
- , d_userContext(userContext)
- , d_logicInfo(logicInfo)
- , d_facts(satContext)
- , d_factsHead(satContext, 0)
- , d_sharedTermsIndex(satContext, 0)
- , d_careGraph(NULL)
- , d_quantEngine(NULL)
- , d_extTheory(NULL)
- , d_checkTime(getFullInstanceName() + "::checkTime")
- , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
- , d_sharedTerms(satContext)
- , d_out(&out)
- , d_valuation(valuation)
- , d_proofsEnabled(false)
+Theory::Theory(TheoryId id,
+ context::Context* satContext,
+ context::UserContext* userContext,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo,
+ ProofNodeManager* pnm,
+ std::string name)
+ : d_id(id),
+ d_satContext(satContext),
+ d_userContext(userContext),
+ d_logicInfo(logicInfo),
+ d_facts(satContext),
+ d_factsHead(satContext, 0),
+ d_sharedTermsIndex(satContext, 0),
+ d_careGraph(NULL),
+ d_quantEngine(NULL),
+ d_decManager(nullptr),
+ d_instanceName(name),
+ d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
+ d_computeCareGraphTime(getStatsPrefix(id) + name
+ + "::computeCareGraphTime"),
+ d_sharedTerms(satContext),
+ d_out(&out),
+ d_valuation(valuation),
+ d_equalityEngine(nullptr),
+ d_allocEqualityEngine(nullptr),
+ d_theoryState(nullptr),
+ d_inferManager(nullptr),
+ d_pnm(pnm)
{
smtStatisticsRegistry()->registerStat(&d_checkTime);
smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
Theory::~Theory() {
smtStatisticsRegistry()->unregisterStat(&d_checkTime);
smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
+}
- delete d_extTheory;
+bool Theory::needsEqualityEngine(EeSetupInfo& esi)
+{
+ // by default, this theory does not use an (official) equality engine
+ return false;
+}
+
+void Theory::setEqualityEngine(eq::EqualityEngine* ee)
+{
+ // 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;
+}
+
+void Theory::setDecisionManager(DecisionManager* dm)
+{
+ Assert(d_decManager == nullptr);
+ Assert(dm != nullptr);
+ d_decManager = dm;
}
-TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
+void Theory::finishInitStandalone()
+{
+ EeSetupInfo esi;
+ if (needsEqualityEngine(esi))
+ {
+ // always associated with the same SAT context as the theory (d_satContext)
+ d_allocEqualityEngine.reset(new eq::EqualityEngine(
+ *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
+ // use it as the official equality engine
+ setEqualityEngine(d_allocEqualityEngine.get());
+ }
+ finishInit();
+}
+
+TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
+{
TheoryId tid = THEORY_BUILTIN;
switch(mode) {
- case THEORY_OF_TYPE_BASED:
- // Constants, variables, 0-ary constructors
- if (node.isVar()) {
- if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
- tid = THEORY_UF;
- }else{
- 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
- tid = Theory::theoryOf(node[0].getType());
- } else {
- // Regular nodes are owned by the kind
- tid = kindToTheoryId(node.getKind());
- }
- break;
- case THEORY_OF_TERM_BASED:
- // Variables
- if (node.isVar()) {
- if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
- // We treat the variables as uninterpreted
- tid = s_uninterpretedSortOwner;
- } else {
- if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
- //Boolean vars go to UF
+ case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
+ // Constants, variables, 0-ary constructors
+ if (node.isVar())
+ {
+ if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+ {
tid = THEORY_UF;
- }else{
- // Except for the Boolean ones
- tid = THEORY_BOOL;
+ }
+ else
+ {
+ tid = Theory::theoryOf(node.getType());
}
}
- } 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 replaced out anyhow
- if (node[0].getKind() == kind::ITE) {
+ else if (node.getKind() == kind::EQUAL)
+ {
+ // Equality is owned by the theory that owns the domain
tid = Theory::theoryOf(node[0].getType());
- } else if (node[1].getKind() == kind::ITE) {
- tid = Theory::theoryOf(node[1].getType());
- } else {
- TNode l = node[0];
- TNode r = node[1];
- TypeNode ltype = l.getType();
- TypeNode rtype = r.getType();
- if( ltype != rtype ){
- tid = Theory::theoryOf(l.getType());
- }else {
- // If both sides belong to the same theory the choice is easy
- TheoryId T1 = Theory::theoryOf(l);
- TheoryId T2 = Theory::theoryOf(r);
- if (T1 == T2) {
- tid = T1;
- } else {
- TheoryId T3 = Theory::theoryOf(ltype);
- // This is a case of
- // * x*y = f(z) -> UF
- // * x = c -> UF
- // * f(x) = read(a, y) -> either UF or ARRAY
- // at least one of the theories has to be parametric, i.e. theory of the type is different
- // from the theory of the term
- if (T1 == T3) {
- tid = T2;
- } else if (T2 == T3) {
+ }
+ else
+ {
+ // 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;
+ case options::TheoryOfMode::THEORY_OF_TERM_BASED:
+ // Variables
+ if (node.isVar())
+ {
+ if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
+ {
+ // We treat the variables as uninterpreted
+ tid = s_uninterpretedSortOwner;
+ }
+ else
+ {
+ if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+ {
+ // Boolean vars go to UF
+ tid = THEORY_UF;
+ }
+ else
+ {
+ // Except for the Boolean ones
+ tid = THEORY_BOOL;
+ }
+ }
+ }
+ else if (node.getKind() == kind::EQUAL)
+ { // Equality
+ // If one of them is an ITE, it's irelevant, since they will get
+ // replaced out anyhow
+ if (node[0].getKind() == kind::ITE)
+ {
+ tid = Theory::theoryOf(node[0].getType());
+ }
+ else if (node[1].getKind() == kind::ITE)
+ {
+ tid = Theory::theoryOf(node[1].getType());
+ }
+ else
+ {
+ TNode l = node[0];
+ TNode r = node[1];
+ TypeNode ltype = l.getType();
+ TypeNode rtype = r.getType();
+ if (ltype != rtype)
+ {
+ tid = Theory::theoryOf(l.getType());
+ }
+ else
+ {
+ // If both sides belong to the same theory the choice is easy
+ TheoryId T1 = Theory::theoryOf(l);
+ TheoryId T2 = Theory::theoryOf(r);
+ if (T1 == T2)
+ {
tid = T1;
- } else {
- // If both are parametric, we take the smaller one (arbitrary)
- tid = T1 < T2 ? T1 : T2;
+ }
+ else
+ {
+ TheoryId T3 = Theory::theoryOf(ltype);
+ // This is a case of
+ // * x*y = f(z) -> UF
+ // * x = c -> UF
+ // * f(x) = read(a, y) -> either UF or ARRAY
+ // at least one of the theories has to be parametric, i.e. theory
+ // of the type is different from the theory of the term
+ if (T1 == T3)
+ {
+ tid = T2;
+ }
+ else if (T2 == T3)
+ {
+ tid = T1;
+ }
+ else
+ {
+ // If both are parametric, we take the smaller one (arbitrary)
+ tid = T1 < T2 ? T1 : T2;
+ }
}
}
}
}
- } else {
- // Regular nodes are owned by the kind
- tid = kindToTheoryId(node.getKind());
- }
+ else
+ {
+ // Regular nodes are owned by the kind, which includes constants as a
+ // special case.
+ tid = kindToTheoryId(node.getKind());
+ }
break;
default:
Unreachable();
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;
}
}
}
printFacts(DebugChannel.getStream());
}
+bool Theory::isLegalElimination(TNode x, TNode val)
+{
+ Assert(x.isVar());
+ if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
+ || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+ {
+ return false;
+ }
+ if (expr::hasSubterm(val, x))
+ {
+ return false;
+ }
+ if (!val.getType().isSubtypeOf(x.getType()))
+ {
+ return false;
+ }
+ if (!options::produceModels())
+ {
+ // don't care about the model, we are fine
+ return true;
+ }
+ // if there is a model object
+ TheoryModel* tm = d_valuation.getModel();
+ Assert(tm != nullptr);
+ return tm->isLegalElimination(x, val);
+}
+
std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
for (shared_terms_iterator i = shared_terms_begin(),
return currentlyShared;
}
-
-void Theory::collectTerms(TNode n, set<Node>& termSet) const
+bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
{
- if (termSet.find(n) != termSet.end()) {
- return;
- }
- Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
- termSet.insert(n);
- if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- collectTerms(*child_it, termSet);
+ // if we are using an equality engine, assert it to the model
+ if (d_equalityEngine != nullptr)
+ {
+ if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
+ {
+ return false;
}
}
+ // now, collect theory-specific value assigments
+ return collectModelValues(m, termSet);
}
-
-void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
+void Theory::computeRelevantTerms(std::set<Node>& termSet)
{
- // 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, termSet);
- }
-
- if (!includeShared) return;
-
- // Add terms that are shared terms
- 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, termSet);
- }
+ // by default, there are no additional relevant terms
}
+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)
{
- if (in.getKind() == kind::EQUAL) {
+ TNode in = tin.getNode();
+ if (in.getKind() == kind::EQUAL)
+ {
// (and (= x t) phi) can be replaced by phi[x/t] if
// 1) x is a variable
// 2) x is not in the term t
// 3) x : T and t : S, then S <: T
- if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
- (in[1].getType()).isSubtypeOf(in[0].getType()) ){
- outSubstitutions.addSubstitution(in[0], in[1]);
+ if (in[0].isVar() && isLegalElimination(in[0], in[1])
+ && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
+ {
+ outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
return PP_ASSERT_STATUS_SOLVED;
}
- if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
- (in[0].getType()).isSubtypeOf(in[1].getType())){
- outSubstitutions.addSubstitution(in[1], in[0]);
+ if (in[1].isVar() && isLegalElimination(in[1], in[0])
+ && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
+ {
+ outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
return PP_ASSERT_STATUS_SOLVED;
}
- if (in[0].isConst() && in[1].isConst()) {
- if (in[0] != in[1]) {
+ if (in[0].isConst() && in[1].isConst())
+ {
+ if (in[0] != in[1])
+ {
return PP_ASSERT_STATUS_CONFLICT;
}
}
return PP_ASSERT_STATUS_UNSOLVED;
}
-std::pair<bool, Node> Theory::entailmentCheck(
- TNode lit,
- const EntailmentCheckParameters* params,
- EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
+{
return make_pair(false, Node::null());
}
-ExtTheory* Theory::getExtTheory() {
- Assert(d_extTheory != NULL);
- return d_extTheory;
-}
-
void Theory::addCarePair(TNode t1, TNode t2) {
if (d_careGraph) {
d_careGraph->insert(CarePair(t1, t2, d_id));
d_careGraph = NULL;
}
-void Theory::setQuantifiersEngine(QuantifiersEngine* qe) {
- Assert(d_quantEngine == NULL);
- Assert(qe != NULL);
- d_quantEngine = qe;
-}
-
-void Theory::setupExtTheory() {
- Assert(d_extTheory == NULL);
- d_extTheory = new ExtTheory(this);
-}
-
-
-EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
- : d_tid(tid) {
-}
-
-std::string Theory::getFullInstanceName() const {
- std::stringstream ss;
- ss << "theory<" << d_id << ">" << d_instanceName;
- return ss.str();
-}
-
-EntailmentCheckParameters::~EntailmentCheckParameters(){}
-
-TheoryId EntailmentCheckParameters::getTheoryId() const {
- return d_tid;
-}
-
-EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
- : d_tid(tid)
-{}
-
-TheoryId EntailmentCheckSideEffects::getTheoryId() const {
- return d_tid;
-}
-
-EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
-}
-
-
-
-ExtTheory::ExtTheory( Theory * p, bool cacheEnabled ) : d_parent( p ),
-d_ext_func_terms( p->getSatContext() ), d_ci_inactive( p->getUserContext() ), d_has_extf( p->getSatContext() ),
-d_lemmas( p->getUserContext() ), d_pp_lemmas( p->getUserContext() ), d_cacheEnabled( cacheEnabled ){
- d_true = NodeManager::currentNM()->mkConst( true );
-}
-
-// Gets all leaf terms in n.
-std::vector<Node> ExtTheory::collectVars(Node n) {
- std::vector<Node> vars;
- std::set<Node> visited;
- std::vector<Node> worklist;
- worklist.push_back(n);
- while (!worklist.empty()) {
- Node current = worklist.back();
- worklist.pop_back();
- if (current.isConst() || visited.count(current) > 0) {
- continue;
- }
- visited.insert(current);
- // Treat terms not belonging to this theory as leaf
- // AJR TODO : should include terms not belonging to this theory
- // (commented below)
- if (current.getNumChildren() > 0) {
- //&& Theory::theoryOf(n)==d_parent->getId() ){
- worklist.insert(worklist.end(), current.begin(), current.end());
- } else {
- vars.push_back(current);
- }
+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;
}
- return vars;
-}
-
-Node ExtTheory::getSubstitutedTerm( int effort, Node term, std::vector< Node >& exp, bool useCache ) {
- if( useCache ){
- Assert( d_gst_cache[effort].find( term )!=d_gst_cache[effort].end() );
- exp.insert( exp.end(), d_gst_cache[effort][term].d_exp.begin(), d_gst_cache[effort][term].d_exp.end() );
- return d_gst_cache[effort][term].d_sterm;
- }else{
- std::vector< Node > terms;
- terms.push_back( term );
- std::vector< Node > sterms;
- std::vector< std::vector< Node > > exps;
- getSubstitutedTerms( effort, terms, sterms, exps, useCache );
- Assert( sterms.size()==1 );
- Assert( exps.size()==1 );
- exp.insert( exp.end(), exps[0].begin(), exps[0].end() );
- return sterms[0];
+ 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;
}
-}
-//do inferences
-void ExtTheory::getSubstitutedTerms(int effort, const std::vector<Node>& terms,
- std::vector<Node>& sterms,
- std::vector<std::vector<Node> >& exp,
- bool useCache) {
- if (useCache) {
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- Assert( d_gst_cache[effort].find( n )!=d_gst_cache[effort].end() );
- sterms.push_back( d_gst_cache[effort][n].d_sterm );
- exp.push_back( std::vector< Node >() );
- exp[0].insert( exp[0].end(), d_gst_cache[effort][n].d_exp.begin(), d_gst_cache[effort][n].d_exp.end() );
- }
- }else{
- Trace("extt-debug") << "getSubstitutedTerms for " << terms.size() << " / " << d_ext_func_terms.size() << " extended functions." << std::endl;
- if( !terms.empty() ){
- //all variables we need to find a substitution for
- std::vector< Node > vars;
- std::vector< Node > sub;
- std::map< Node, std::vector< Node > > expc;
- for( unsigned i=0; i<terms.size(); i++ ){
- //do substitution, rewrite
- Node n = terms[i];
- std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
- Assert( iti!=d_extf_info.end() );
- for( unsigned i=0; i<iti->second.d_vars.size(); i++ ){
- if( std::find( vars.begin(), vars.end(), iti->second.d_vars[i] )==vars.end() ){
- vars.push_back( iti->second.d_vars[i] );
- }
- }
- }
- bool useSubs = d_parent->getCurrentSubstitution( effort, vars, sub, expc );
- //get the current substitution for all variables
- Assert( !useSubs || vars.size()==sub.size() );
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- Node ns = n;
- std::vector< Node > expn;
- if( useSubs ){
- //do substitution
- ns = n.substitute( vars.begin(), vars.end(), sub.begin(), sub.end() );
- if( ns!=n ){
- //build explanation: explanation vars = sub for each vars in FV( n )
- std::map< Node, ExtfInfo >::iterator iti = d_extf_info.find( n );
- Assert( iti!=d_extf_info.end() );
- for( unsigned j=0; j<iti->second.d_vars.size(); j++ ){
- Node v = iti->second.d_vars[j];
- std::map< Node, std::vector< Node > >::iterator itx = expc.find( v );
- if( itx!=expc.end() ){
- for( unsigned k=0; k<itx->second.size(); k++ ){
- if( std::find( expn.begin(), expn.end(), itx->second[k] )==expn.end() ){
- expn.push_back( itx->second[k] );
- }
- }
- }
- }
- }
- Trace("extt-debug") << " have " << n << " == " << ns << ", exp size=" << expn.size() << "." << std::endl;
- }
- //add to vector
- sterms.push_back( ns );
- exp.push_back( expn );
- //add to cache
- if( d_cacheEnabled ){
- d_gst_cache[effort][n].d_sterm = ns;
- d_gst_cache[effort][n].d_exp.clear();
- d_gst_cache[effort][n].d_exp.insert( d_gst_cache[effort][n].d_exp.end(), expn.begin(), expn.end() );
- }
- }
- }
+ // Check for disequality
+ if (d_equalityEngine->areDisequal(a, b, false))
+ {
+ // The terms are implied to be dis-equal
+ return EQUALITY_FALSE;
}
-}
-bool ExtTheory::doInferencesInternal(int effort, const std::vector<Node>& terms,
- std::vector<Node>& nred, bool batch,
- bool isRed) {
- if (batch) {
- bool addedLemma = false;
- if( isRed ){
- for( unsigned i=0; i<terms.size(); i++ ){
- Node n = terms[i];
- Node nr;
- //TODO: reduction with substitution?
- int ret = d_parent->getReduction( effort, n, nr );
- if( ret==0 ){
- nred.push_back( n );
- }else{
- if( !nr.isNull() && n!=nr ){
- Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr );
- if( sendLemma( lem, true ) ){
- Trace("extt-lemma") << "ExtTheory : reduction lemma : " << lem << std::endl;
- addedLemma = true;
- }
- }
- markReduced( terms[i], ret<0 );
- }
- }
- }else{
- std::vector< Node > sterms;
- std::vector< std::vector< Node > > exp;
- getSubstitutedTerms( effort, terms, sterms, exp );
- std::map< Node, unsigned > sterm_index;
- for( unsigned i=0; i<terms.size(); i++ ){
- bool processed = false;
- if( sterms[i]!=terms[i] ){
- Node sr = Rewriter::rewrite( sterms[i] );
- //ask the theory if this term is reduced, e.g. is it constant or it is a non-extf term.
- if( d_parent->isExtfReduced( effort, sr, terms[i], exp[i] ) ){
- processed = true;
- markReduced( terms[i] );
- Node eq = terms[i].eqNode( sr );
- Node expn = exp[i].size()>1 ? NodeManager::currentNM()->mkNode( kind::AND, exp[i] ) : ( exp[i].size()==1 ? exp[i][0] : d_true );
- Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq << " by " << expn << std::endl;
- Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, expn, eq );
- Trace("extt-debug") << "...send lemma " << lem << std::endl;
- if( sendLemma( lem ) ){
- Trace("extt-lemma") << "ExtTheory : substitution + rewrite lemma : " << lem << std::endl;
- addedLemma = true;
- }
- }else{
- //check if we have already reduced this
- std::map< Node, unsigned >::iterator itsi = sterm_index.find( sr );
- if( itsi!=sterm_index.end() ){
- //unsigned j = itsi->second;
- //can add (non-reducing) lemma : exp[j] ^ exp[i] => sterms[i] = sterms[j]
- //TODO
- }else{
- sterm_index[sr] = i;
- }
- //check if we reduce to another active term?
-
- Trace("extt-nred") << "Non-reduced term : " << sr << std::endl;
- }
- }else{
- Trace("extt-nred") << "Non-reduced term : " << sterms[i] << std::endl;
- }
- if( !processed ){
- nred.push_back( terms[i] );
- }
- }
- }
- return addedLemma;
- }else{
- std::vector< Node > nnred;
- if( terms.empty() ){
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
- std::vector< Node > nterms;
- nterms.push_back( (*it).first );
- if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
- return true;
- }
- }
- }
- }else{
- for( unsigned i=0; i<terms.size(); i++ ){
- std::vector< Node > nterms;
- nterms.push_back( terms[i] );
- if( doInferencesInternal( effort, nterms, nnred, true, isRed ) ){
- return true;
- }
- }
- }
- return false;
- }
+ // All other terms are unknown, which is conservative. A theory may override
+ // this method if it knows more information.
+ return EQUALITY_UNKNOWN;
}
-bool ExtTheory::sendLemma( Node lem, bool preprocess ) {
- if( preprocess ){
- if( d_pp_lemmas.find( lem )==d_pp_lemmas.end() ){
- d_pp_lemmas.insert( lem );
- d_parent->getOutputChannel().lemma( lem, false, true );
- return true;
- }
- }else{
- if( d_lemmas.find( lem )==d_lemmas.end() ){
- d_lemmas.insert( lem );
- d_parent->getOutputChannel().lemma( lem );
- return true;
- }
- }
- return false;
-}
-
-bool ExtTheory::doInferences(int effort, const std::vector<Node>& terms,
- std::vector<Node>& nred, bool batch) {
- if (!terms.empty()) {
- return doInferencesInternal( effort, terms, nred, batch, false );
- }else{
- return false;
- }
-}
-
-bool ExtTheory::doInferences( int effort, std::vector< Node >& nred, bool batch ) {
- std::vector< Node > terms = getActive();
- return doInferencesInternal( effort, terms, nred, batch, false );
-}
-
-bool ExtTheory::doReductions(int effort, const std::vector<Node>& terms,
- std::vector<Node>& nred, bool batch) {
- if (!terms.empty()) {
- return doInferencesInternal( effort, terms, nred, batch, true );
- }else{
- return false;
+void Theory::check(Effort level)
+{
+ // see if we are already done (as an optimization)
+ if (done() && level < EFFORT_FULL)
+ {
+ return;
}
-}
-
-bool ExtTheory::doReductions(int effort, std::vector<Node>& nred, bool batch) {
- const std::vector<Node> terms = getActive();
- return doInferencesInternal(effort, terms, nred, batch, true);
-}
-
-// Register term.
-void ExtTheory::registerTerm(Node n) {
- if (d_extf_kind.find(n.getKind()) != d_extf_kind.end()) {
- if (d_ext_func_terms.find(n) == d_ext_func_terms.end()) {
- Trace("extt-debug") << "Found extended function : " << n << " in "
- << d_parent->getId() << std::endl;
- d_ext_func_terms[n] = true;
- d_has_extf = n;
- d_extf_info[n].d_vars = collectVars(n);
- }
+ 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;
}
-}
-
-void ExtTheory::registerTermRec(Node n) {
- std::set<Node> visited;
- registerTermRec(n, &visited);
-}
-
-void ExtTheory::registerTermRec(Node n, std::set<Node>* visited) {
- if (visited->find(n) == visited->end()) {
- visited->insert(n);
- registerTerm(n);
- for (unsigned i = 0; i < n.getNumChildren(); i++) {
- registerTermRec(n[i], visited);
+ 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;
}
- }
-}
-
-//mark reduced
-void ExtTheory::markReduced( Node n, bool contextDepend ) {
- registerTerm( n );
- Assert( d_ext_func_terms.find( n )!=d_ext_func_terms.end() );
- d_ext_func_terms[n] = false;
- if( !contextDepend ){
- d_ci_inactive.insert( n );
- }
-
- //update has_extf
- if( d_has_extf.get()==n ){
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- //if not already reduced
- if( (*it).second && !isContextIndependentInactive( (*it).first ) ){
- d_has_extf = (*it).first;
- }
+ 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);
}
-
- }
-}
-
-//mark congruent
-void ExtTheory::markCongruent( Node a, Node b ) {
- Trace("extt-debug") << "Mark congruent : " << a << " " << b << std::endl;
- registerTerm( a );
- registerTerm( b );
- NodeBoolMap::const_iterator it = d_ext_func_terms.find( b );
- if( it!=d_ext_func_terms.end() ){
- if( d_ext_func_terms.find( a )!=d_ext_func_terms.end() ){
- d_ext_func_terms[a] = d_ext_func_terms[a] && (*it).second;
- }else{
- Assert( false );
+ else
+ {
+ d_equalityEngine->assertPredicate(atom, polarity, fact);
}
- d_ext_func_terms[b] = false;
- }else{
- Assert( false );
+ 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 ExtTheory::isContextIndependentInactive(Node n) const {
- return d_ci_inactive.find(n) != d_ci_inactive.end();
-}
+bool Theory::preCheck(Effort level) { return false; }
+void Theory::postCheck(Effort level) {}
-void ExtTheory::getTerms( std::vector< Node >& terms ) {
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- terms.push_back( (*it).first );
- }
+bool Theory::preNotifyFact(
+ TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
+{
+ return false;
}
-bool ExtTheory::hasActiveTerm() {
- return !d_has_extf.get().isNull();
-}
-
-//is active
-bool ExtTheory::isActive( Node n ) {
- NodeBoolMap::const_iterator it = d_ext_func_terms.find( n );
- if( it!=d_ext_func_terms.end() ){
- return (*it).second && !isContextIndependentInactive( n );
- }else{
- return false;
- }
+void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
+{
}
-// get active
-std::vector<Node> ExtTheory::getActive() const {
- std::vector<Node> active;
- for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
- it != d_ext_func_terms.end(); ++it) {
- // if not already reduced
- if ((*it).second && !isContextIndependentInactive((*it).first)) {
- active.push_back((*it).first);
- }
- }
- return active;
-}
+void Theory::preRegisterTerm(TNode node) {}
-std::vector<Node> ExtTheory::getActive(Kind k) const {
- std::vector<Node> active;
- for (NodeBoolMap::iterator it = d_ext_func_terms.begin();
- it != d_ext_func_terms.end(); ++it) {
- // if not already reduced
- if ((*it).first.getKind() == k && (*it).second &&
- !isContextIndependentInactive((*it).first)) {
- active.push_back((*it).first);
- }
+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);
}
- return active;
}
-void ExtTheory::clearCache() {
- d_gst_cache.clear();
+eq::EqualityEngine* Theory::getEqualityEngine()
+{
+ // get the assigned equality engine, which is a pointer stored in this class
+ return d_equalityEngine;
}
}/* CVC4::theory namespace */
projects / cvc5.git / blobdiff