From 05c6ae0bda064083efb7941e1ceb0869cb1b1090 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 15:58:46 -0500 Subject: [PATCH] Remove spurious theory methods calls (#4931) This PR removes spurious theory method calls that are not implemented. It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)". --- src/theory/arrays/kinds | 2 +- src/theory/arrays/theory_arrays.cpp | 17 +++++++---------- src/theory/arrays/theory_arrays.h | 11 +++++------ src/theory/datatypes/kinds | 2 +- src/theory/datatypes/theory_datatypes.cpp | 20 ++++++-------------- src/theory/datatypes/theory_datatypes.h | 14 +++++--------- src/theory/sep/kinds | 2 +- src/theory/sep/theory_sep.cpp | 13 ++++--------- src/theory/sep/theory_sep.h | 15 +++++---------- src/theory/sets/kinds | 2 +- src/theory/sets/theory_sets.cpp | 4 ---- src/theory/sets/theory_sets.h | 1 - src/theory/sets/theory_sets_private.cpp | 2 -- src/theory/sets/theory_sets_private.h | 2 -- src/theory/strings/kinds | 2 +- src/theory/strings/theory_strings.cpp | 13 ++++++------- src/theory/strings/theory_strings.h | 13 +++++-------- src/theory/uf/kinds | 2 +- src/theory/uf/theory_uf.cpp | 15 ++++++--------- src/theory/uf/theory_uf.h | 14 +++++--------- 20 files changed, 60 insertions(+), 106 deletions(-) diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 659f05ae8..629064d99 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -8,7 +8,7 @@ theory THEORY_ARRAYS ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_ typechecker "theory/arrays/theory_arrays_type_rules.h" properties polite stable-infinite parametric -properties check propagate presolve +properties check presolve rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h" diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 9c1e22940..d659aff11 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -414,14 +414,17 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - -bool TheoryArrays::propagate(TNode literal) +bool TheoryArrays::propagateLit(TNode literal) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ")" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::propagateLit(" << literal << ")" + << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << "): already in conflict" << std::endl; + Debug("arrays") << spaces(getSatContext()->getLevel()) + << "TheoryArrays::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } @@ -861,12 +864,6 @@ void TheoryArrays::preRegisterTerm(TNode node) } } - -void TheoryArrays::propagate(Effort e) -{ - // direct propagation now -} - TrustNode TheoryArrays::explain(TNode literal) { Node explanation = explain(literal, NULL); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 2d09c55fe..24ebb4916 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -213,7 +213,7 @@ class TheoryArrays : public Theory { context::CDO d_literalsToPropagateIndex; /** Should be called to propagate the literal. */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector& assumptions, @@ -227,7 +227,6 @@ class TheoryArrays : public Theory { public: void preRegisterTerm(TNode n) override; - void propagate(Effort e) override; Node explain(TNode n, eq::EqProof* proof); TrustNode explain(TNode n) override; @@ -306,9 +305,9 @@ class TheoryArrays : public Theory { << (value ? "true" : "false") << ")" << std::endl; // Just forward to arrays if (value) { - return d_arrays.propagate(predicate); + return d_arrays.propagateLit(predicate); } - return d_arrays.propagate(predicate.notNode()); + return d_arrays.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, @@ -324,14 +323,14 @@ class TheoryArrays : public Theory { } } // Propagate equality between shared terms - return d_arrays.propagate(t1.eqNode(t2)); + return d_arrays.propagateLit(t1.eqNode(t2)); } else { if (t1.getType().isArray()) { if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) { return true; } } - return d_arrays.propagate(t1.eqNode(t2).notNode()); + return d_arrays.propagateLit(t1.eqNode(t2).notNode()); } return true; } diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 4b80529d2..26bff20b7 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -7,7 +7,7 @@ theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" typechecker "theory/datatypes/theory_datatypes_type_rules.h" -properties check presolve parametric propagate +properties check parametric rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 08ec4322e..65264bb3f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -701,11 +701,6 @@ TrustNode TheoryDatatypes::expandDefinition(Node n) return TrustNode::null(); } -void TheoryDatatypes::presolve() -{ - Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; -} - TrustNode TheoryDatatypes::ppRewrite(TNode in) { Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl; @@ -739,17 +734,14 @@ void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl; } -/** propagate */ -void TheoryDatatypes::propagate(Effort effort){ - -} - -/** propagate */ -bool TheoryDatatypes::propagate(TNode literal){ - Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << ")" << std::endl; +bool TheoryDatatypes::propagateLit(TNode literal) +{ + Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")" + << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl; + Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } Trace("dt-prop") << "dtPropagate " << literal << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 0465a7788..137aae469 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -62,9 +62,9 @@ class TheoryDatatypes : public Theory { { Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { - return d_dt.propagate(predicate); + return d_dt.propagateLit(predicate); } - return d_dt.propagate(predicate.notNode()); + return d_dt.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, @@ -73,10 +73,9 @@ class TheoryDatatypes : public Theory { { Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { - return d_dt.propagate(t1.eqNode(t2)); - } else { - return d_dt.propagate(t1.eqNode(t2).notNode()); + return d_dt.propagateLit(t1.eqNode(t2)); } + return d_dt.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override { @@ -270,9 +269,7 @@ private: //--------------------------------- end initialization /** propagate */ - void propagate(Effort effort) override; - /** propagate */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** explain */ void addAssumptions( std::vector& assumptions, std::vector& tassumptions ); void explainEquality( TNode a, TNode b, bool polarity, std::vector& assumptions ); @@ -293,7 +290,6 @@ private: void preRegisterTerm(TNode n) override; TrustNode expandDefinition(Node n) override; TrustNode ppRewrite(TNode n) override; - void presolve() override; void addSharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool collectModelInfo(TheoryModel* m) override; diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 235b61172..7a3fb00a4 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -8,7 +8,7 @@ theory THEORY_SEP ::CVC4::theory::sep::TheorySep "theory/sep/theory_sep.h" typechecker "theory/sep/theory_sep_type_rules.h" properties polite stable-infinite parametric -properties check propagate presolve +properties check presolve rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index f75eb4472..cf3cf2f9a 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -111,13 +111,13 @@ Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstit // T-PROPAGATION / REGISTRATION ///////////////////////////////////////////////////////////////////////////// - -bool TheorySep::propagate(TNode literal) +bool TheorySep::propagateLit(TNode literal) { - Debug("sep") << "TheorySep::propagate(" << literal << ")" << std::endl; + Debug("sep") << "TheorySep::propagateLit(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl; + Debug("sep") << "TheorySep::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } bool ok = d_out->propagate(literal); @@ -146,11 +146,6 @@ void TheorySep::explain(TNode literal, std::vector& assumptions) { } } - -void TheorySep::propagate(Effort e){ - -} - TrustNode TheorySep::explain(TNode literal) { Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl; diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b178b97db..bbb37a3a2 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -105,13 +105,12 @@ class TheorySep : public Theory { private: /** Should be called to propagate the literal. */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector& assumptions); public: - void propagate(Effort e) override; TrustNode explain(TNode n) override; public: @@ -163,9 +162,9 @@ class TheorySep : public Theory { // Just forward to sep if (value) { - return d_sep.propagate(predicate); + return d_sep.propagateLit(predicate); } - return d_sep.propagate(predicate.notNode()); + return d_sep.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, @@ -178,13 +177,9 @@ class TheorySep : public Theory { if (value) { // Propagate equality between shared terms - return d_sep.propagate(t1.eqNode(t2)); + return d_sep.propagateLit(t1.eqNode(t2)); } - else - { - return d_sep.propagate(t1.eqNode(t2).notNode()); - } - return true; + return d_sep.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 452acfea0..d3c42ef27 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -12,7 +12,7 @@ rewriter ::CVC4::theory::sets::TheorySetsRewriter \ "theory/sets/theory_sets_rewriter.h" properties parametric -properties check propagate presolve +properties check presolve # constants constant EMPTYSET \ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 2627f72e3..647a7bb47 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -196,10 +196,6 @@ void TheorySets::presolve() { d_internal->presolve(); } -void TheorySets::propagate(Effort e) { - d_internal->propagate(e); -} - bool TheorySets::isEntailed( Node n, bool pol ) { return d_internal->isEntailed( n, pol ); } diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 36e6ac65d..9e04b89a7 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -70,7 +70,6 @@ class TheorySets : public Theory TrustNode expandDefinition(Node n) override; PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void presolve() override; - void propagate(Effort) override; bool isEntailed(Node n, bool pol); private: /** Functions to handle callbacks from equality engine */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f7c7ae7f9..3c9414606 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1392,8 +1392,6 @@ Node mkAnd(const std::vector& conjunctions) return conjunction; } /* mkAnd() */ -void TheorySetsPrivate::propagate(Theory::Effort effort) {} - bool TheorySetsPrivate::propagate(TNode literal) { Debug("sets-prop") << " propagate(" << literal << ")" << std::endl; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 9a786598c..af780eadc 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -219,8 +219,6 @@ class TheorySetsPrivate { void presolve(); - void propagate(Theory::Effort); - /** get default output channel */ OutputChannel* getOutputChannel(); /** get the valuation */ diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 131a48ae9..78c6ab1f1 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -6,7 +6,7 @@ theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h" -properties check parametric propagate presolve +properties check parametric presolve rewriter ::CVC4::theory::strings::SequencesRewriter "theory/strings/sequences_rewriter.h" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6d81c742a..e42796354 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -181,16 +181,15 @@ EqualityStatus TheoryStrings::getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } -void TheoryStrings::propagate(Effort e) { - // direct propagation now -} - -bool TheoryStrings::propagate(TNode literal) { - Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << ")" << std::endl; +bool TheoryStrings::propagateLit(TNode literal) +{ + Debug("strings-propagate") + << "TheoryStrings::propagateLit(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_state.isInConflict()) { - Debug("strings-propagate") << "TheoryStrings::propagate(" << literal << "): already in conflict" << std::endl; + Debug("strings-propagate") << "TheoryStrings::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } // Propagate out diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index da48ece90..8a1afe6b3 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -84,8 +84,6 @@ class TheoryStrings : public Theory { //--------------------------------- end initialization /** Identify this theory */ std::string identify() const override; - /** Propagate */ - void propagate(Effort e) override; /** Explain */ TrustNode explain(TNode literal) override; /** Get current substitution */ @@ -130,9 +128,9 @@ class TheoryStrings : public Theory { { Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { - return d_str.propagate(predicate); + return d_str.propagateLit(predicate); } - return d_str.propagate(predicate.notNode()); + return d_str.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, @@ -141,10 +139,9 @@ class TheoryStrings : public Theory { { Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { - return d_str.propagate(t1.eqNode(t2)); - } else { - return d_str.propagate(t1.eqNode(t2).notNode()); + return d_str.propagateLit(t1.eqNode(t2)); } + return d_str.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override { @@ -175,7 +172,7 @@ class TheoryStrings : public Theory { SolverState& d_state; };/* class TheoryStrings::NotifyClass */ /** propagate method */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** compute care graph */ void computeCareGraph() override; /** diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 109e6d0a1..9564899fe 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -8,7 +8,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" properties stable-infinite parametric -properties check propagate ppStaticLearn presolve +properties check ppStaticLearn presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function" diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0b97d8a5d..29014d33f 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -261,11 +261,14 @@ void TheoryUF::preRegisterTerm(TNode node) { } }/* TheoryUF::preRegisterTerm() */ -bool TheoryUF::propagate(TNode literal) { - Debug("uf::propagate") << "TheoryUF::propagate(" << literal << ")" << std::endl; +bool TheoryUF::propagateLit(TNode literal) +{ + Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal << ")" + << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl; + Debug("uf::propagate") << "TheoryUF::propagateLit(" << literal + << "): already in conflict" << std::endl; return false; } // Propagate out @@ -276,12 +279,6 @@ bool TheoryUF::propagate(TNode literal) { return ok; }/* TheoryUF::propagate(TNode) */ -void TheoryUF::propagate(Effort effort) { - //if (d_thss != NULL) { - // return d_thss->propagate(effort); - //} -} - void TheoryUF::explain(TNode literal, std::vector& assumptions, eq::EqProof* pf) { // Do the work bool polarity = literal.getKind() != kind::NOT; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 7d17fdb86..8efaf79e3 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -49,10 +49,9 @@ public: { Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; if (value) { - return d_uf.propagate(predicate); - } else { - return d_uf.propagate(predicate.notNode()); + return d_uf.propagateLit(predicate); } + return d_uf.propagateLit(predicate.notNode()); } bool eqNotifyTriggerTermEquality(TheoryId tag, @@ -62,10 +61,9 @@ public: { Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; if (value) { - return d_uf.propagate(t1.eqNode(t2)); - } else { - return d_uf.propagate(t1.eqNode(t2).notNode()); + return d_uf.propagateLit(t1.eqNode(t2)); } + return d_uf.propagateLit(t1.eqNode(t2).notNode()); } void eqNotifyConstantTermMerge(TNode t1, TNode t2) override @@ -119,7 +117,7 @@ private: * Should be called to propagate the literal. We use a node here * since some of the propagated literals are not kept anywhere. */ - bool propagate(TNode literal); + bool propagateLit(TNode literal); /** * Explain why this literal is true by adding assumptions @@ -189,8 +187,6 @@ private: void addSharedTerm(TNode n) override; void computeCareGraph() override; - void propagate(Effort effort) override; - EqualityStatus getEqualityStatus(TNode a, TNode b) override; std::string identify() const override { return "THEORY_UF"; } -- 2.30.2