summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/alpha_equivalence.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/alpha_equivalence.cpp')
-rw-r--r--src/theory/quantifiers/alpha_equivalence.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index b72f15a01..d49b37e4c 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -79,7 +79,7 @@ bool AlphaEquivalenceTypeNode::registerNode( AlphaEquivalenceTypeNode* aetn,
return AlphaEquivalenceNode::registerNode( &(aetn->d_data), qe, q, tt, arg_index );
}
-bool AlphaEquivalence::registerQuantifier( Node q ) {
+bool AlphaEquivalence::reduceQuantifier( Node q ) {
Assert( q.getKind()==FORALL );
Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
//construct canonical quantified formula
@@ -99,7 +99,7 @@ bool AlphaEquivalence::registerQuantifier( Node q ) {
sto.d_tdb = d_qe->getTermDatabase();
std::sort( typs.begin(), typs.end(), sto );
Trace("aeq-debug") << " ";
- bool ret = AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
+ bool ret = !AlphaEquivalenceTypeNode::registerNode( &d_ae_typ_trie, d_qe, q, t, typs, typ_count );
Trace("aeq") << " ...result : " << ret << std::endl;
return ret;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback