}
};
-Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index ) {
+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 lem;
Trace("aeq-debug") << std::endl;
if( aen->d_quant.isNull() ){
aen->d_quant = q;
- }else{
- if( q.getNumChildren()==2 ){
- //lemma ( q <=> d_quant )
- Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
- Trace("alpha-eq") << " " << q << std::endl;
- Trace("alpha-eq") << " " << aen->d_quant << std::endl;
- lem = q.eqNode( aen->d_quant );
- }else{
- //do not reduce annotated quantified formulas based on alpha equivalence
- }
}
- return lem;
+ return aen->d_quant;
}
-Node AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
- QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index ){
- while( index<(int)typs.size() ){
+Node AlphaEquivalenceTypeNode::registerNode(Node q,
+ Node t,
+ std::vector<TypeNode>& typs,
+ std::map<TypeNode, int>& typ_count)
+{
+ AlphaEquivalenceTypeNode* aetn = this;
+ unsigned 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]]);
index = index + 1;
}
- std::vector< Node > tt;
- std::vector< int > arg_index;
- tt.push_back( t );
Trace("aeq-debug") << " : ";
- return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
+ return aetn->d_data.registerNode(q, t);
}
-Node AlphaEquivalence::reduceQuantifier( Node q ) {
+Node AlphaEquivalenceDb::addTerm(Node q)
+{
Assert( q.getKind()==FORALL );
Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
//construct canonical quantified formula
- Node t = d_qe->getTermCanonize()->getCanonicalTerm(q[1], true);
+ 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;
}
}
sortTypeOrder sto;
- sto.d_tu = d_qe->getTermCanonize();
+ sto.d_tu = d_tc;
std::sort( typs.begin(), typs.end(), sto );
Trace("aeq-debug") << " ";
- Node ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+ Node ret = d_ae_typ_trie.registerNode(q, t, typs, typ_count);
Trace("aeq") << " ...result : " << ret << std::endl;
return ret;
}
+
+AlphaEquivalence::AlphaEquivalence(QuantifiersEngine* qe)
+ : d_aedb(qe->getTermCanonize())
+{
+}
+
+Node AlphaEquivalence::reduceQuantifier(Node q)
+{
+ Assert(q.getKind() == FORALL);
+ Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
+ Node ret = d_aedb.addTerm(q);
+ Node lem;
+ if (ret != q)
+ {
+ // do not reduce annotated quantified formulas based on alpha equivalence
+ if (q.getNumChildren() == 2)
+ {
+ // lemma ( q <=> d_quant )
+ Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
+ Trace("alpha-eq") << " " << q << std::endl;
+ Trace("alpha-eq") << " " << ret << std::endl;
+ lem = q.eqNode(ret);
+ }
+ }
+ return lem;
+}
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:
- std::map< Node, std::map< int, AlphaEquivalenceNode > > d_children;
- Node d_quant;
- static Node registerNode( AlphaEquivalenceNode* aen, QuantifiersEngine* qe, Node q, std::vector< Node >& tt, std::vector< int >& arg_index );
+ /** 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
+ * AlphaEquivalenceNode trie. For example, if t contains 2 free variables
+ * of type T1 and 3 free variables of type T2, then it is stored at
+ * d_children[T1][2].d_children[T2][3].
+ */
class AlphaEquivalenceTypeNode {
public:
- std::map< TypeNode, std::map< int, AlphaEquivalenceTypeNode > > d_children;
- AlphaEquivalenceNode d_data;
- static Node registerNode( AlphaEquivalenceTypeNode* aetn,
- QuantifiersEngine* qe, Node q, Node t, std::vector< TypeNode >& typs, std::map< TypeNode, int >& typ_count, int index = 0 );
+ /** children of this node */
+ std::map<TypeNode, std::map<int, AlphaEquivalenceTypeNode> > d_children;
+ /** the database of terms at this node */
+ AlphaEquivalenceNode d_data;
+ /** 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.
+ */
+ Node registerNode(Node q,
+ Node t,
+ std::vector<TypeNode>& typs,
+ std::map<TypeNode, int>& typ_count);
};
-class AlphaEquivalence {
-private:
- QuantifiersEngine* d_qe;
- //per # of variables per type
+/**
+ * Stores a database of quantified formulas, which computes alpha-equivalence.
+ */
+class AlphaEquivalenceDb
+{
+ public:
+ AlphaEquivalenceDb(TermCanonize* tc) : d_tc(tc) {}
+ /** adds quantified formula q to this database
+ *
+ * This function returns a quantified formula q' that is alpha-equivalent to
+ * q. If q' != q, then q' was previously added to this database via a call
+ * to addTerm.
+ */
+ Node addTerm(Node q);
+
+ private:
+ /** a trie per # of variables per type */
AlphaEquivalenceTypeNode d_ae_typ_trie;
-public:
- AlphaEquivalence( QuantifiersEngine* qe ) : d_qe( qe ){}
+ /** pointer to the term canonize utility */
+ TermCanonize* d_tc;
+};
+
+/**
+ * A quantifiers module that computes reductions based on alpha-equivalence,
+ * using the above utilities.
+ */
+class AlphaEquivalence
+{
+ public:
+ AlphaEquivalence(QuantifiersEngine* qe);
~AlphaEquivalence(){}
- /** reduce quantifier, return value (if non-null) is lemma justifying why q ia reducible. */
+ /** reduce quantifier
+ *
+ * If non-null, its return value is lemma justifying why q is reducible.
+ * This is of the form ( q = q' ) where q' is a quantified formula that
+ * was previously registered to this class via a call to reduceQuantifier,
+ * and q and q' are alpha-equivalent.
+ */
Node reduceQuantifier( Node q );
+
+ private:
+ /** the database of quantified formulas registered to this class */
+ AlphaEquivalenceDb d_aedb;
};
}