Simplify alpha equivalence module (#5839)

This class uses a discrimination tree which can compute subsumption as well as alpha-equivalence. This class was initially designed to also support subsumption. However, we were only using this class for alpha-equivalence and hence (canonized) Node comparison suffices and the class can be simplified. It also makes minor cosmetic updates to the module.

If we plan to support subsumption checking later, we will write a new module, and use this class https://github.com/CVC4/CVC4/blob/master/src/expr/match_trie.h which is a more mature version of the class deleted by this PR.

Note: I verified that the new and old implementation was equivalent using a temporary AlwaysAssert.

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 643a652e70693793debc61abbc69a3792017cd65..4c0acd9982ba021c49f9ee09214b88520f7090f6 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -30,77 +30,31 @@ struct sortTypeOrder {
   }
 };
 
-Node AlphaEquivalenceNode::registerNode(Node q, Node t)
-{
-  AlphaEquivalenceNode* aen = this;
-  std::vector<Node> tt;
-  std::vector<int> arg_index;
-  tt.push_back(t);
-  std::map< Node, bool > visited;
-  while( !tt.empty() ){
-    if( tt.size()==arg_index.size()+1 ){
-      Node tb = tt.back();
-      Node op;
-      if (tb.hasOperator())
-      {
-        if (visited.find(tb) == visited.end())
-        {
-          visited[tb] = true;
-          op = tb.getOperator();
-          arg_index.push_back( 0 );
-        }
-        else
-        {
-          op = tb;
-          arg_index.push_back( -1 );
-        }
-      }
-      else
-      {
-        op = tb;
-        arg_index.push_back( 0 );
-      }
-      Trace("aeq-debug") << op << " ";
-      aen = &(aen->d_children[op][tb.getNumChildren()]);
-    }else{
-      Node tb = tt.back();
-      int i = arg_index.back();
-      if (i == -1 || i == (int)tb.getNumChildren())
-      {
-        tt.pop_back();
-        arg_index.pop_back();
-      }
-      else
-      {
-        tt.push_back(tb[i]);
-        arg_index[arg_index.size()-1]++;
-      }
-    }
-  }
-  Trace("aeq-debug") << std::endl;
-  if( aen->d_quant.isNull() ){
-    aen->d_quant = q;
-  }
-  return aen->d_quant;
-}
-
-Node AlphaEquivalenceTypeNode::registerNode(Node q,
-                                            Node t,
-                                            std::vector<TypeNode>& typs,
-                                            std::map<TypeNode, int>& typ_count)
+Node AlphaEquivalenceTypeNode::registerNode(
+    Node q,
+    Node t,
+    std::vector<TypeNode>& typs,
+    std::map<TypeNode, size_t>& typCount)
 {
   AlphaEquivalenceTypeNode* aetn = this;
-  unsigned index = 0;
+  size_t index = 0;
   while (index < typs.size())
   {
     TypeNode curr = typs[index];
-    Assert(typ_count.find(curr) != typ_count.end());
-    Trace("aeq-debug") << "[" << curr << " " << typ_count[curr] << "] ";
-    aetn = &(aetn->d_children[curr][typ_count[curr]]);
+    Assert(typCount.find(curr) != typCount.end());
+    Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] ";
+    std::pair<TypeNode, size_t> key(curr, typCount[curr]);
+    aetn = &(aetn->d_children[key]);
     index = index + 1;
   }
   Trace("aeq-debug") << " : ";
-  return aetn->d_data.registerNode(q, t);
+  std::map<Node, Node>::iterator it = aetn->d_quant.find(t);
+  if (it != aetn->d_quant.end())
+  {
+    return it->second;
+  }
+  aetn->d_quant[t] = q;
+  return q;
 }
 
 Node AlphaEquivalenceDb::addTerm(Node q)
@@ -111,11 +65,11 @@ Node AlphaEquivalenceDb::addTerm(Node q)
   Node t = d_tc->getCanonicalTerm(q[1], true);
   Trace("aeq") << "  canonical form: " << t << std::endl;
   //compute variable type counts
-  std::map< TypeNode, int > typ_count;
+  std::map<TypeNode, size_t> typCount;
   std::vector< TypeNode > typs;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    typ_count[tn]++;
+    typCount[tn]++;
     if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
       typs.push_back( tn );
     }
@@ -124,7 +78,7 @@ Node AlphaEquivalenceDb::addTerm(Node q)
   sto.d_tu = d_tc;
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  Node ret = d_ae_typ_trie.registerNode(q, t, typs, typ_count);
+  Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount);
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 987864317d131b3779f16d6d358b0990b48c9568..5f69eee414d2d88029e21d3737966158fbd3c794 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -25,30 +25,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/**
- * This is a discrimination tree index for terms. It handles variadic
- * operators by indexing based on operator arity, and flattens multiple
- * occurrences of subterms.
- *
- * For example, the term
- * +( f( x ), +( a, f(x), b ) )
- *   is stored at:
- * d_children[+][2].d_children[f][1].
- *   d_children[x][0].d_children[+][3].
- *     d_children[a][0].d_children[f(x)][0].
- *       d_children[b][0]
- * Notice that the second occurrence of f(x) is flattened.
- */
-class AlphaEquivalenceNode {
-public:
- /** children of this node */
- std::map<Node, std::map<int, AlphaEquivalenceNode> > d_children;
- /** the data at this node */
- Node d_quant;
- /** Registers term q to this trie. The term t is the canonical form of q. */
- Node registerNode(Node q, Node t);
-};
-
 /**
  * This trie stores a trie of the above form for each multi-set of types. For
  * each term t registered to this node, we store t in the appropriate
@@ -59,18 +35,21 @@ public:
 class AlphaEquivalenceTypeNode {
 public:
  /** children of this node */
- std::map<TypeNode, std::map<int, AlphaEquivalenceTypeNode> > d_children;
- /** the database of terms at this node */
- AlphaEquivalenceNode d_data;
+ std::map<std::pair<TypeNode, size_t>, AlphaEquivalenceTypeNode> d_children;
+ /**
+  * map from canonized quantifier bodies to a quantified formula whose
+  * canonized body is that term.
+  */
+ std::map<Node, Node> d_quant;
  /** register node
   *
   * This registers term q to this trie. The term t is the canonical form of
-  * q, typs/typ_count represent a multi-set of types of free variables in t.
+  * q, typs/typCount represent a multi-set of types of free variables in t.
   */
  Node registerNode(Node q,
                    Node t,
                    std::vector<TypeNode>& typs,
-                   std::map<TypeNode, int>& typ_count);
+                   std::map<TypeNode, size_t>& typCount);
 };
 
 /**