diff options
3 files changed, 21 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index 12c667fb5..4272c0484 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -73,6 +73,8 @@ class CandidateGenerator { virtual Node getNextCandidate() = 0; /** is n a legal candidate? */ bool isLegalCandidate(Node n); + /** Identify this generator (for debugging, etc..) */ + virtual std::string identify() const = 0; protected: /** Reference to the quantifiers state */ @@ -106,6 +108,9 @@ class CandidateGeneratorQE : public CandidateGenerator { return d_exclude_eqc.find(r) != d_exclude_eqc.end(); } + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override { return "CandidateGeneratorQE"; } + protected: /** reset this class for matching operator op in equivalence class eqc */ void resetForOperator(Node eqc, Node op); @@ -153,6 +158,8 @@ class CandidateGeneratorQELitDeq : public CandidateGenerator void reset(Node eqc) override; /** get next candidate */ Node getNextCandidate() override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override { return "CandidateGeneratorQELitDeq"; } private: /** the equality class iterator for false */ @@ -182,6 +189,8 @@ class CandidateGeneratorQEAll : public CandidateGenerator unsigned d_index; //first time bool d_firstTime; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override { return "CandidateGeneratorQEAll"; } public: CandidateGeneratorQEAll(QuantifiersState& qs, TermRegistry& tr, Node mpat); @@ -209,6 +218,11 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE void reset(Node eqc) override; /** get next candidate */ Node getNextCandidate() override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override + { + return "CandidateGeneratorConsExpand"; + } protected: /** the (datatype) type of the input match pattern */ @@ -234,6 +248,9 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE * application of the wrong constructor. */ Node getNextCandidate() override; + /** Identify this generator (for debugging, etc..) */ + std::string identify() const override { return "CandidateGeneratorSelector"; } + protected: /** the selector operator */ Node d_selOp; diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 5f76d5289..5380fc7d5 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -271,6 +271,9 @@ void InstMatchGenerator::initialize(Node q, Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; } + Trace("inst-match-gen") << "Candidate generator is " + << (d_cg != nullptr ? d_cg->identify() : "null") + << std::endl; gens.insert( gens.end(), d_children.begin(), d_children.end() ); } diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 83234d115..332346f3f 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -60,7 +60,6 @@ bool PatternTermSelector::isUsable(Node n, Node q) { return true; } - std::map<Node, Node> coeffs; if (options::purifyTriggers()) { Node x = getInversionVariable(n); @@ -82,7 +81,7 @@ Node PatternTermSelector::getIsUsableEq(Node q, Node n) if (i == 1 && n.getKind() == EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0])) { - return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]); + return NodeManager::currentNM()->mkNode(EQUAL, n[1], n[0]); } else { |