From 93160e9f24c78b68d3c2b523cd11a2f71acd77e4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 17 Mar 2022 13:56:15 -0500 Subject: [PATCH] Update care graph computations to use standard node trie algorithm (#8298) Standardizes a few new methods in theory to support this. This should not change the behavior, only refactors. This is in preparation for adding efficient care graph computation for bags, and towards possible fixes for arrays. --- src/CMakeLists.txt | 2 + src/theory/care_pair_argument_callback.cpp | 35 ++++ src/theory/care_pair_argument_callback.h | 56 +++++++ src/theory/datatypes/theory_datatypes.cpp | 126 +------------- src/theory/datatypes/theory_datatypes.h | 4 +- src/theory/sets/theory_sets.cpp | 26 ++- src/theory/sets/theory_sets.h | 7 + src/theory/sets/theory_sets_private.cpp | 185 ++++----------------- src/theory/sets/theory_sets_private.h | 20 ++- src/theory/strings/theory_strings.cpp | 106 +----------- src/theory/strings/theory_strings.h | 13 +- src/theory/theory.cpp | 60 ++++++- src/theory/theory.h | 20 ++- src/theory/uf/theory_uf.cpp | 119 ++----------- src/theory/uf/theory_uf.h | 17 +- 15 files changed, 274 insertions(+), 522 deletions(-) create mode 100644 src/theory/care_pair_argument_callback.cpp create mode 100644 src/theory/care_pair_argument_callback.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b5f34a246..063930fa6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -632,6 +632,8 @@ libcvc5_add_sources( theory/bv/theory_bv_utils.h theory/bv/type_enumerator.h theory/care_graph.h + theory/care_pair_argument_callback.cpp + theory/care_pair_argument_callback.cpp theory/combination_care_graph.cpp theory/combination_care_graph.h theory/combination_engine.cpp diff --git a/src/theory/care_pair_argument_callback.cpp b/src/theory/care_pair_argument_callback.cpp new file mode 100644 index 000000000..e0e459b42 --- /dev/null +++ b/src/theory/care_pair_argument_callback.cpp @@ -0,0 +1,35 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The care pair argument callback. + */ + +#include "theory/care_pair_argument_callback.h" + +namespace cvc5 { +namespace theory { + +CarePairArgumentCallback::CarePairArgumentCallback(Theory& t) : d_theory(t) {} + +bool CarePairArgumentCallback::considerPath(TNode a, TNode b) +{ + // interested in finding pairs that are not disequal + return !d_theory.areCareDisequal(a, b); +} + +void CarePairArgumentCallback::processData(TNode fa, TNode fb) +{ + d_theory.processCarePairArgs(fa, fb); +} + +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/care_pair_argument_callback.h b/src/theory/care_pair_argument_callback.h new file mode 100644 index 000000000..beacf9e43 --- /dev/null +++ b/src/theory/care_pair_argument_callback.h @@ -0,0 +1,56 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * The care pair argument callback. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__CARE_PAIR_ARGUMENT_CALLBACK_H +#define CVC5__THEORY__CARE_PAIR_ARGUMENT_CALLBACK_H + +#include "expr/node_trie_algorithm.h" +#include "theory/theory.h" + +namespace cvc5 { +namespace theory { + +/** + * The standard callback for computing the care pairs from a node trie. + */ +class CarePairArgumentCallback : public NodeTriePathPairProcessCallback +{ + public: + CarePairArgumentCallback(Theory& t); + ~CarePairArgumentCallback() {} + /** + * Call on the arguments a and b of two function applications we are + * computing care pairs for. Returns true if a and b are not already + * disequal according to theory combination (Theory::areCareDisequal). + */ + bool considerPath(TNode a, TNode b) override; + /** + * Called when we have two function applications that do not have pairs + * of disequal arguments at any position. We call Theory::processCarePairArgs + * to add all relevant care pairs. + */ + void processData(TNode fa, TNode fb) override; + + private: + /** Reference to theory */ + Theory& d_theory; +}; + +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__CARE_ARGUMENT_CALLBACK_H */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8bdc92ebd..d2df204a6 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -64,7 +64,8 @@ TheoryDatatypes::TheoryDatatypes(Env& env, d_rewriter(env.getEvaluator()), d_state(env, valuation), d_im(env, *this, d_state), - d_notify(d_im, *this) + d_notify(d_im, *this), + d_cpacb(*this) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -1036,107 +1037,7 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ return EQUALITY_FALSE_IN_MODEL; } -void TheoryDatatypes::addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth, - unsigned& n_pairs) -{ - Trace("dt-cg") << "Process at depth " << depth << "/" << arity << std::endl; - if( depth==arity ){ - Assert(t2 != nullptr); - Node f1 = t1->getData(); - Node f2 = t2->getData(); - if (!areEqual(f1, f2)) - { - Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; - std::vector > currentPairs; - for (size_t k = 0, nchild = f1.getNumChildren(); k < nchild; ++k) - { - TNode x = f1[k]; - TNode y = f2[k]; - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - Assert(!areDisequal(x, y)); - Assert(!areCareDisequal(x, y)); - if (!d_equalityEngine->areEqual(x, y)) - { - Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y - << std::endl; - if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES) - && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES)) - { - TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( - x, THEORY_DATATYPES); - TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( - y, THEORY_DATATYPES); - currentPairs.push_back(make_pair(x_shared, y_shared)); - } - } - } - for (std::pair& p : currentPairs) - { - Trace("dt-cg-pair") - << "Pair : " << p.first << " " << p.second << std::endl; - addCarePair(p.first, p.second); - n_pairs++; - } - } - return; - } - if (t2 == nullptr) - { - if (depth + 1 < arity) - { - // add care pairs internal to each child - for (std::pair& tt : t1->d_data) - { - Trace("dt-cg-debug") << "Traverse into arg " << tt.first << " at depth " - << depth << std::endl; - addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs); - } - } - // add care pairs based on each pair of non-disequal arguments - for (std::map::iterator it = t1->d_data.begin(); - it != t1->d_data.end(); - ++it) - { - std::map::iterator it2 = it; - ++it2; - for (; it2 != t1->d_data.end(); ++it2) - { - if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) - { - if (!areCareDisequal(it->first, it2->first)) - { - addCarePairs(&it->second, &it2->second, arity, depth + 1, n_pairs); - } - } - } - } - return; - } - // add care pairs based on product of indices, non-disequal arguments - for (std::pair& tt1 : t1->d_data) - { - for (std::pair& tt2 : t2->d_data) - { - if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) - { - if (!areCareDisequal(tt1.first, tt2.first)) - { - Trace("dt-cg-debug") - << "Traverse into " << tt1.first << " " << tt2.first - << " at depth " << depth << std::endl; - addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); - } - } - } - } -} - void TheoryDatatypes::computeCareGraph(){ - unsigned n_pairs = 0; Trace("dt-cg-summary") << "Compute graph for dt..." << d_functionTerms.size() << " " << d_sharedTerms.size() << std::endl; Trace("dt-cg") << "Build indices..." << std::endl; std::map > index; @@ -1178,11 +1079,11 @@ void TheoryDatatypes::computeCareGraph(){ { Trace("dt-cg") << "Process index " << tt.first << ", " << t.first << "..." << std::endl; - addCarePairs(&t.second, nullptr, arity[t.first], 0, n_pairs); + nodeTriePathPairProcess(&t.second, arity[t.first], d_cpacb); Trace("dt-cg") << "...finish" << std::endl; } } - Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; + Trace("dt-cg-summary") << "...done" << std::endl; } bool TheoryDatatypes::collectModelValues(TheoryModel* m, @@ -1804,25 +1705,6 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ } } -bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) { - Trace("datatypes-cg") << "areCareDisequal: " << x << " " << y << std::endl; - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - if (d_equalityEngine->isTriggerTerm(x, THEORY_DATATYPES) - && d_equalityEngine->isTriggerTerm(y, THEORY_DATATYPES)) - { - TNode x_shared = - d_equalityEngine->getTriggerTermRepresentative(x, THEORY_DATATYPES); - TNode y_shared = - d_equalityEngine->getTriggerTermRepresentative(y, THEORY_DATATYPES); - EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); - if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ - return true; - } - } - return false; -} - TNode TheoryDatatypes::getRepresentative( TNode a ){ if( hasTerm( a ) ){ return d_equalityEngine->getRepresentative(a); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3463935bb..738c5c303 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -24,6 +24,7 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/node_trie.h" +#include "theory/care_pair_argument_callback.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/inference_manager.h" #include "theory/datatypes/proof_checker.h" @@ -272,7 +273,6 @@ private: bool hasTerm( TNode a ); bool areEqual( TNode a, TNode b ); bool areDisequal( TNode a, TNode b ); - bool areCareDisequal( TNode x, TNode y ); TNode getRepresentative( TNode a ); /** Collect model values in m based on the relevant terms given by termSet */ @@ -298,6 +298,8 @@ private: NotifyClass d_notify; /** Proof checker for datatypes */ DatatypesProofRuleChecker d_checker; + /** The care pair argument callback, used for theory combination */ + CarePairArgumentCallback d_cpacb; };/* class TheoryDatatypes */ } // namespace datatypes diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 7b62f0589..e61881daa 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -32,8 +32,9 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation) d_skCache(env.getRewriter()), d_state(env, valuation, d_skCache), d_im(env, *this, d_state), - d_internal( - new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)), + d_cpacb(*this), + d_internal(new TheorySetsPrivate( + env, *this, d_state, d_im, d_skCache, d_pnm, d_cpacb)), d_notify(*d_internal.get(), d_im) { // use the official theory state and inference manager objects @@ -209,6 +210,27 @@ bool TheorySets::isEntailed( Node n, bool pol ) { return d_internal->isEntailed( n, pol ); } +void TheorySets::processCarePairArgs(TNode a, TNode b) +{ + // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or + // not for the shared variables x, y in the care graph. + // However, this does not apply to the membership operator since the + // equality or disequality between members affects the number of elements + // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER. + // Example: + // Suppose (= (member x S) member(y S)) is true and there are + // no other members in S. We would get S = {x} if (= x y) is true. + // Otherwise we would get S = {x, y}. + if (a.getKind() != SET_MEMBER && d_state.areEqual(a, b)) + { + return; + } + // otherwise, we add pairs for each of their arguments + addCarePairArgs(a, b); + + d_internal->processCarePairArgs(a, b); +} + /**************************** eq::NotifyClass *****************************/ void TheorySets::NotifyClass::eqNotifyNewClass(TNode t) diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index e9510d70e..920a7a4ab 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -21,6 +21,7 @@ #include #include "smt/logic_exception.h" +#include "theory/care_pair_argument_callback.h" #include "theory/sets/inference_manager.h" #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" @@ -85,6 +86,10 @@ class TheorySets : public Theory bool isEntailed(Node n, bool pol); private: + /** + * Overrides to handle a special case of set membership. + */ + void processCarePairArgs(TNode a, TNode b) override; /** Functions to handle callbacks from equality engine */ class NotifyClass : public TheoryEqNotifyClass { @@ -106,6 +111,8 @@ class TheorySets : public Theory SolverState d_state; /** The inference manager */ InferenceManager d_im; + /** The care pair argument callback, used for theory combination */ + CarePairArgumentCallback d_cpacb; /** The internal theory */ std::unique_ptr d_internal; /** Instance of the above class */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index df6f17e80..c6be43d6d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -41,7 +41,8 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env, SolverState& state, InferenceManager& im, SkolemCache& skc, - ProofNodeManager* pnm) + ProofNodeManager* pnm, + CarePairArgumentCallback& cpacb) : EnvObj(env), d_deq(context()), d_termProcessed(userContext()), @@ -55,7 +56,8 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env, d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)), d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)), d_rels_enabled(false), - d_card_enabled(false) + d_card_enabled(false), + d_cpacb(cpacb) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -191,26 +193,6 @@ TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n, } } -bool TheorySetsPrivate::areCareDisequal(Node a, Node b) -{ - if (d_equalityEngine->isTriggerTerm(a, THEORY_SETS) - && d_equalityEngine->isTriggerTerm(b, THEORY_SETS)) - { - TNode a_shared = - d_equalityEngine->getTriggerTermRepresentative(a, THEORY_SETS); - TNode b_shared = - d_equalityEngine->getTriggerTermRepresentative(b, THEORY_SETS); - EqualityStatus eqStatus = - d_external.d_valuation.getEqualityStatus(a_shared, b_shared); - if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE - || eqStatus == EQUALITY_FALSE_IN_MODEL) - { - return true; - } - } - return false; -} - void TheorySetsPrivate::fullEffortReset() { Assert(d_equalityEngine->consistent()); @@ -849,135 +831,6 @@ void TheorySetsPrivate::notifyFact(TNode atom, bool polarity, TNode fact) } //--------------------------------- end standard check -/************************ Sharing ************************/ -/************************ Sharing ************************/ -/************************ Sharing ************************/ - -void TheorySetsPrivate::addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth, - unsigned& n_pairs) -{ - if (depth == arity) - { - if (t2 != NULL) - { - Node f1 = t1->getData(); - Node f2 = t2->getData(); - - // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or - // not for the shared variables x, y in the care graph. - // However, this does not apply to the membership operator since the - // equality or disequality between members affects the number of elements - // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER. - // Example: - // Suppose (= (member x S) member( y, S)) is true and there are - // no other members in S. We would get S = {x} if (= x y) is true. - // Otherwise we would get S = {x, y}. - if (f1.getKind() == SET_MEMBER || !d_state.areEqual(f1, f2)) - { - Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl; - vector > currentPairs; - for (unsigned k = 0; k < f1.getNumChildren(); ++k) - { - TNode x = f1[k]; - TNode y = f2[k]; - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - Assert(!d_state.areDisequal(x, y)); - Assert(!areCareDisequal(x, y)); - if (!d_equalityEngine->areEqual(x, y)) - { - Trace("sets-cg") - << "Arg #" << k << " is " << x << " " << y << std::endl; - if (d_equalityEngine->isTriggerTerm(x, THEORY_SETS) - && d_equalityEngine->isTriggerTerm(y, THEORY_SETS)) - { - TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( - x, THEORY_SETS); - TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( - y, THEORY_SETS); - currentPairs.push_back(make_pair(x_shared, y_shared)); - } - else if (isCareArg(f1, k) && isCareArg(f2, k)) - { - // splitting on sets (necessary for handling set of sets properly) - if (x.getType().isSet()) - { - Assert(y.getType().isSet()); - if (!d_state.areDisequal(x, y)) - { - Trace("sets-cg-lemma") - << "Should split on : " << x << "==" << y << std::endl; - d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT); - } - } - } - } - } - for (unsigned c = 0; c < currentPairs.size(); ++c) - { - Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " - << currentPairs[c].second << std::endl; - d_external.addCarePair(currentPairs[c].first, currentPairs[c].second); - n_pairs++; - } - } - } - } - else - { - if (t2 == NULL) - { - if (depth < (arity - 1)) - { - // add care pairs internal to each child - for (std::pair& t : t1->d_data) - { - addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs); - } - } - // add care pairs based on each pair of non-disequal arguments - for (std::map::iterator it = t1->d_data.begin(); - it != t1->d_data.end(); - ++it) - { - std::map::iterator it2 = it; - ++it2; - for (; it2 != t1->d_data.end(); ++it2) - { - if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) - { - if (!areCareDisequal(it->first, it2->first)) - { - addCarePairs( - &it->second, &it2->second, arity, depth + 1, n_pairs); - } - } - } - } - } - else - { - // add care pairs based on product of indices, non-disequal arguments - for (std::pair& tt1 : t1->d_data) - { - for (std::pair& tt2 : t2->d_data) - { - if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) - { - if (!areCareDisequal(tt1.first, tt2.first)) - { - addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); - } - } - } - } - } - } -} - void TheorySetsPrivate::computeCareGraph() { const std::map >& ol = d_state.getOperatorList(); @@ -1039,7 +892,7 @@ void TheorySetsPrivate::computeCareGraph() { Trace("sets-cg") << "Process index " << tt.first << "..." << std::endl; - addCarePairs(&tt.second, nullptr, arity, 0, n_pairs); + nodeTriePathPairProcess(&tt.second, arity, d_cpacb); } } Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; @@ -1059,10 +912,7 @@ bool TheorySetsPrivate::isCareArg(Node n, unsigned a) { return true; } - else - { - return false; - } + return false; } /******************** Model generation ********************/ @@ -1252,6 +1102,29 @@ bool TheorySetsPrivate::isEntailed(Node n, bool pol) return d_state.isEntailed(n, pol); } +void TheorySetsPrivate::processCarePairArgs(TNode a, TNode b) +{ + for (size_t k = 0, nchild = a.getNumChildren(); k < nchild; ++k) + { + TNode x = a[k]; + TNode y = b[k]; + if (!d_equalityEngine->areEqual(x, y)) + { + if (isCareArg(a, k) && isCareArg(b, k)) + { + // splitting on sets (necessary for handling set of sets properly) + if (x.getType().isSet()) + { + Assert(y.getType().isSet()); + Trace("sets-cg-lemma") + << "Should split on : " << x << "==" << y << std::endl; + d_im.split(x.eqNode(y), InferenceId::SETS_CG_SPLIT); + } + } + } + } +} + Node TheorySetsPrivate::explain(TNode literal) { Trace("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index c75f1a24f..191bf1a99 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -22,6 +22,7 @@ #include "context/cdqueue.h" #include "expr/node_trie.h" #include "smt/env_obj.h" +#include "theory/care_pair_argument_callback.h" #include "theory/sets/cardinality_extension.h" #include "theory/sets/inference_manager.h" #include "theory/sets/solver_state.h" @@ -49,8 +50,6 @@ class TheorySetsPrivate : protected EnvObj void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); private: - /** Are a and b trigger terms in the equality engine that may be disequal? */ - bool areCareDisequal(Node a, Node b); /** * Invoke the decision procedure for this theory, which is run at * full effort. This will either send a lemma or conflict on the output @@ -87,12 +86,6 @@ class TheorySetsPrivate : protected EnvObj */ void checkReduceComprehensions(); - void addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth, - unsigned& n_pairs); - Node d_true; Node d_false; Node d_zero; @@ -140,7 +133,8 @@ class TheorySetsPrivate : protected EnvObj SolverState& state, InferenceManager& im, SkolemCache& skc, - ProofNodeManager* pnm); + ProofNodeManager* pnm, + CarePairArgumentCallback& cpacb); ~TheorySetsPrivate(); @@ -182,6 +176,12 @@ class TheorySetsPrivate : protected EnvObj /** Is formula n entailed to have polarity pol in the current context? */ bool isEntailed(Node n, bool pol); + /** + * Adds inferences for splitting on arguments of a and b that are not + * equal nor disequal and are sets. + */ + void processCarePairArgs(TNode a, TNode b); + private: TheorySets& d_external; /** The state of the sets solver at full effort */ @@ -229,6 +229,8 @@ class TheorySetsPrivate : protected EnvObj /** a map that maps each set to an existential quantifier generated for * operator is_singleton */ std::map d_isSingletonNodes; + /** Reference to care pair argument callback, used for theory combination */ + CarePairArgumentCallback& d_cpacb; }; /* class TheorySetsPrivate */ } // namespace sets diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 740e32434..273b3364c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -85,7 +85,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation) d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()), d_stringsFmf(env, valuation, d_termReg), d_strat(d_env), - d_absModelCounter(0) + d_absModelCounter(0), + d_cpacb(*this) { d_termReg.finishInit(&d_im); @@ -165,24 +166,6 @@ std::string TheoryStrings::identify() const return std::string("TheoryStrings"); } -bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS) - && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS)) - { - TNode x_shared = - d_equalityEngine->getTriggerTermRepresentative(x, THEORY_STRINGS); - TNode y_shared = - d_equalityEngine->getTriggerTermRepresentative(y, THEORY_STRINGS); - EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); - if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ - return true; - } - } - return false; -} - bool TheoryStrings::propagateLit(TNode literal) { return d_im.propagateLit(literal); @@ -1004,89 +987,6 @@ void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2) } } -void TheoryStrings::addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth) -{ - if( depth==arity ){ - if( t2!=NULL ){ - Node f1 = t1->getData(); - Node f2 = t2->getData(); - if (!d_equalityEngine->areEqual(f1, f2)) - { - Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; - vector< pair > currentPairs; - for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { - TNode x = f1[k]; - TNode y = f2[k]; - Assert(d_equalityEngine->hasTerm(x)); - Assert(d_equalityEngine->hasTerm(y)); - Assert(!d_equalityEngine->areDisequal(x, y, false)); - Assert(!areCareDisequal(x, y)); - if (!d_equalityEngine->areEqual(x, y)) - { - if (d_equalityEngine->isTriggerTerm(x, THEORY_STRINGS) - && d_equalityEngine->isTriggerTerm(y, THEORY_STRINGS)) - { - TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( - x, THEORY_STRINGS); - TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( - y, THEORY_STRINGS); - currentPairs.push_back(make_pair(x_shared, y_shared)); - } - } - } - for (unsigned c = 0; c < currentPairs.size(); ++ c) { - Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; - addCarePair(currentPairs[c].first, currentPairs[c].second); - } - } - } - }else{ - if( t2==NULL ){ - if( depth<(arity-1) ){ - //add care pairs internal to each child - for (std::pair& tt : t1->d_data) - { - addCarePairs(&tt.second, nullptr, arity, depth + 1); - } - } - //add care pairs based on each pair of non-disequal arguments - for (std::map::iterator it = t1->d_data.begin(); - it != t1->d_data.end(); - ++it) - { - std::map::iterator it2 = it; - ++it2; - for( ; it2 != t1->d_data.end(); ++it2 ){ - if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) - { - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1 ); - } - } - } - } - }else{ - //add care pairs based on product of indices, non-disequal arguments - for (std::pair& tt1 : t1->d_data) - { - for (std::pair& tt2 : t2->d_data) - { - if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) - { - if (!areCareDisequal(tt1.first, tt2.first)) - { - addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); - } - } - } - } - } - } -} - void TheoryStrings::computeCareGraph(){ //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl; @@ -1122,7 +1022,7 @@ void TheoryStrings::computeCareGraph(){ Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << ti.first << "..." << std::endl; Node op = ti.first.second; - addCarePairs(&ti.second, nullptr, arity[op], 0); + nodeTriePathPairProcess(&ti.second, arity[op], d_cpacb); } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ac04d0ed6..89c2a8bdc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -24,6 +24,7 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "expr/node_trie.h" +#include "theory/care_pair_argument_callback.h" #include "theory/ext_theory.h" #include "theory/strings/array_solver.h" #include "theory/strings/base_solver.h" @@ -167,16 +168,6 @@ class TheoryStrings : public Theory { };/* class TheoryStrings::NotifyClass */ /** compute care graph */ void computeCareGraph() override; - /** - * Are x and y shared terms that are not equal? This is used for constructing - * the care graph in the above function. - */ - bool areCareDisequal(TNode x, TNode y); - /** Add care pairs */ - void addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, - unsigned arity, - unsigned depth); /** Collect model info for type tn * * Assigns model values (in m) to all relevant terms of the string-like type @@ -322,6 +313,8 @@ class TheoryStrings : public Theory { * we have built, so that unique debug names can be assigned. */ size_t d_absModelCounter; + /** The care pair argument callback, used for theory combination */ + CarePairArgumentCallback d_cpacb; };/* class TheoryStrings */ } // namespace strings diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 8d90f25a6..8f4c9ee6d 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -494,19 +494,71 @@ std::pair Theory::entailmentCheck(TNode lit) } void Theory::addCarePair(TNode t1, TNode t2) { - if (d_careGraph) { - d_careGraph->insert(CarePair(t1, t2, d_id)); + Assert(d_careGraph != nullptr); + Trace("sharing") << "Theory::addCarePair: add pair " << d_id << " " << t1 + << " " << t2 << std::endl; + d_careGraph->insert(CarePair(t1, t2, d_id)); +} +void Theory::addCarePairArgs(TNode a, TNode b) +{ + Assert(d_careGraph != nullptr); + Assert(d_equalityEngine != nullptr); + Assert(a.hasOperator() && b.hasOperator()); + Assert(a.getOperator() == b.getOperator()); + Assert(a.getNumChildren() == b.getNumChildren()); + Trace("sharing") << "Theory::addCarePairArgs: checking function " << d_id + << " " << a << " " << b << std::endl; + for (size_t k = 0, nchildren = a.getNumChildren(); k < nchildren; ++k) + { + TNode x = a[k]; + TNode y = b[k]; + if (d_equalityEngine->isTriggerTerm(x, d_id) + && d_equalityEngine->isTriggerTerm(y, d_id) + && !d_equalityEngine->areEqual(x, y)) + { + TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id); + TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id); + addCarePair(x_shared, y_shared); + } + } +} + +void Theory::processCarePairArgs(TNode a, TNode b) +{ + // if a and b are already equal, we ignore this pair + if (d_theoryState->areEqual(a, b)) + { + return; + } + // otherwise, we add pairs for each of their arguments + addCarePairArgs(a, b); +} + +bool Theory::areCareDisequal(TNode x, TNode y) +{ + Assert(d_equalityEngine != nullptr); + Assert(d_equalityEngine->hasTerm(x)); + Assert(d_equalityEngine->hasTerm(y)); + if (!d_equalityEngine->isTriggerTerm(x, d_id) + || !d_equalityEngine->isTriggerTerm(y, d_id)) + { + return false; } + TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(x, d_id); + TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(y, d_id); + EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); + return eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE + || eqStatus == EQUALITY_FALSE_IN_MODEL; } void Theory::getCareGraph(CareGraph* careGraph) { - Assert(careGraph != NULL); + Assert(careGraph != nullptr); Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl; TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime); d_careGraph = careGraph; computeCareGraph(); - d_careGraph = NULL; + d_careGraph = nullptr; } bool Theory::proofsEnabled() const diff --git a/src/theory/theory.h b/src/theory/theory.h index f0d147d07..cd6b7f431 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -47,6 +47,7 @@ class ProofRuleChecker; namespace theory { +class CarePairArgumentCallback; class DecisionManager; struct EeSetupInfo; class OutputChannel; @@ -97,6 +98,7 @@ namespace eq { */ class Theory : protected EnvObj { + friend class CarePairArgumentCallback; friend class ::cvc5::TheoryEngine; protected: @@ -112,10 +114,24 @@ class Theory : protected EnvObj /** time spent in theory combination */ TimerStat d_computeCareGraphTime; + /** Add (t1, t2) to the care graph */ + void addCarePair(TNode t1, TNode t2); /** - * The only method to add suff to the care graph. + * Assuming a is f(a1, ..., an) and b is f(b1, ..., bn), this method adds + * (ai, bi) to the care graph for each i where ai is not equal to bi. */ - void addCarePair(TNode t1, TNode t2); + void addCarePairArgs(TNode a, TNode b); + /** + * Process care pair arguments for a and b. By default, this calls the + * method above if a and b are not equal according to the equality engine + * of this theory. + */ + virtual void processCarePairArgs(TNode a, TNode b); + /** + * Are care disequal? Return true if x and y are shared terms that are + * disequal according to the valuation. + */ + virtual bool areCareDisequal(TNode x, TNode y); /** * The function should compute the care graph over the shared terms. diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1b1624598..cdd2e0501 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -55,7 +55,8 @@ TheoryUF::TheoryUF(Env& env, d_rewriter(logicInfo().isHigherOrder()), d_state(env, valuation), d_im(env, *this, d_state, "theory::uf::" + instanceName, false), - d_notify(d_im, *this) + d_notify(d_im, *this), + d_cpacb(*this) { d_true = NodeManager::currentNM()->mkConst( true ); // indicate we are using the default theory state and inference managers @@ -107,28 +108,6 @@ void TheoryUF::finishInit() { } } -static Node mkAnd(const std::vector& conjunctions) { - Assert(conjunctions.size() > 0); - - std::set all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - NodeBuilder conjunction(kind::AND); - std::set::const_iterator it = all.begin(); - std::set::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - //--------------------------------- standard check bool TheoryUF::needsCheckLastEffort() @@ -352,7 +331,7 @@ void TheoryUF::explain(TNode literal, Node& exp) { d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr); } - exp = mkAnd(assumptions); + exp = NodeManager::currentNM()->mkAnd(assumptions); } TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); } @@ -569,89 +548,15 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y) return false; } -void TheoryUF::addCarePairs(const TNodeTrie* t1, - const TNodeTrie* t2, - unsigned arity, - unsigned depth) +void TheoryUF::processCarePairArgs(TNode a, TNode b) { - // Note we use d_state instead of d_equalityEngine in this method in several - // places to be robust to cases where the tries have terms that do not - // exist in the equality engine, which can be the case if higher order. - if( depth==arity ){ - if( t2!=NULL ){ - Node f1 = t1->getData(); - Node f2 = t2->getData(); - if (!d_state.areEqual(f1, f2)) - { - Trace("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; - vector< pair > currentPairs; - for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k) - { - TNode x = f1[k]; - TNode y = f2[k]; - Assert(!d_state.areDisequal(x, y)); - Assert(!areCareDisequal(x, y)); - if (!d_state.areEqual(x, y)) - { - if (d_equalityEngine->isTriggerTerm(x, THEORY_UF) - && d_equalityEngine->isTriggerTerm(y, THEORY_UF)) - { - TNode x_shared = - d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF); - TNode y_shared = - d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF); - currentPairs.push_back(make_pair(x_shared, y_shared)); - } - } - } - for (unsigned c = 0; c < currentPairs.size(); ++ c) { - Trace("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl; - addCarePair(currentPairs[c].first, currentPairs[c].second); - } - } - } - }else{ - if( t2==NULL ){ - if( depth<(arity-1) ){ - //add care pairs internal to each child - for (const std::pair& tt : t1->d_data) - { - addCarePairs(&tt.second, NULL, arity, depth + 1); - } - } - //add care pairs based on each pair of non-disequal arguments - for (std::map::const_iterator it = t1->d_data.begin(); - it != t1->d_data.end(); - ++it) - { - std::map::const_iterator it2 = it; - ++it2; - for( ; it2 != t1->d_data.end(); ++it2 ){ - if (!d_state.areDisequal(it->first, it2->first)) - { - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1 ); - } - } - } - } - }else{ - //add care pairs based on product of indices, non-disequal arguments - for (const std::pair& tt1 : t1->d_data) - { - for (const std::pair& tt2 : t2->d_data) - { - if (!d_state.areDisequal(tt1.first, tt2.first)) - { - if (!areCareDisequal(tt1.first, tt2.first)) - { - addCarePairs(&tt1.second, &tt2.second, arity, depth + 1); - } - } - } - } - } + // if a and b are already equal, we ignore this pair + if (d_state.areEqual(a, b)) + { + return; } + // otherwise, we add pairs for each of their arguments + addCarePairArgs(a, b); } void TheoryUF::computeCareGraph() { @@ -723,14 +628,14 @@ void TheoryUF::computeCareGraph() { Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << tt.first << "..." << std::endl; Assert(arity.find(tt.first) != arity.end()); - addCarePairs(&tt.second, nullptr, arity[tt.first], 0); + nodeTriePathPairProcess(&tt.second, arity[tt.first], d_cpacb); } for (std::pair& tt : hoIndex) { Trace("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index " << tt.first << "..." << std::endl; // the arity of HO_APPLY is always two - addCarePairs(&tt.second, nullptr, 2, 0); + nodeTriePathPairProcess(&tt.second, 2, d_cpacb); } Trace("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 58e949aef..ec011ef48 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -21,7 +21,7 @@ #define CVC5__THEORY__UF__THEORY_UF_H #include "expr/node.h" -#include "expr/node_trie.h" +#include "theory/care_pair_argument_callback.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" #include "theory/theory_state.h" @@ -152,11 +152,14 @@ private: /** Explain why this literal is true by building an explanation */ void explain(TNode literal, Node& exp); - bool areCareDisequal(TNode x, TNode y); - void addCarePairs(const TNodeTrie* t1, - const TNodeTrie* t2, - unsigned arity, - unsigned depth); + /** Overrides to ensure that pairs of lambdas are not considered disequal. */ + bool areCareDisequal(TNode x, TNode y) override; + /** + * Overrides to use the theory state instead of the equality engine, since + * for higher-order, some terms that do not occur in the equality engine are + * considered. + */ + void processCarePairArgs(TNode a, TNode b) override; /** * Is t a higher order type? A higher-order type is a function type having * an argument type that is also a function type. This is used for checking @@ -174,6 +177,8 @@ private: NotifyClass d_notify; /** Cache for isHigherOrderType */ std::map d_isHoType; + /** The care pair argument callback, used for theory combination */ + CarePairArgumentCallback d_cpacb; };/* class TheoryUF */ } // namespace uf -- 2.30.2