Minor changes to E-matching utilities (#7062)

diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 12c667fb56823a4636429422e8cf46474d2dc327..4272c048466dfc88b2850564159e5eee14821578 100644 (file)
--- 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 5f76d5289cdb13d9644dfa1b3371b76b69bdeffe..5380fc7d5f21b32afb6753625c13ba292159e7ec 100644 (file)
--- 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 83234d1153a8d2db96c05e76d1e610b86a2138de..332346f3fea699389f3b5dd0d4f2d36fbb22d250 100644 (file)
--- 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
       {