Fix alpha equivalence for higher-order (#1769)

3 files changed, 37 insertions, 2 deletions

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 9aa4561ce..a8abd41eb 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -452,8 +452,13 @@ Node TermUtil::getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_co
         cchildren[i] = getCanonicalTerm( cchildren[i], var_count, subs, apply_torder, visited );
       }
       if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        Trace("canon-term-debug") << "Insert operator " << n.getOperator() << std::endl;
-        cchildren.insert( cchildren.begin(), n.getOperator() );
+        Node op = n.getOperator();
+        if (options::ufHo())
+        {
+          op = getCanonicalTerm(op, var_count, subs, apply_torder, visited);
+        }
+        Trace("canon-term-debug") << "Insert operator " << op << std::endl;
+        cchildren.insert(cchildren.begin(), op);
       }
       Trace("canon-term-debug") << "...constructing for " << n << "." << std::endl;
       Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cchildren );
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 3899ff367..76185044e 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -444,6 +444,7 @@ REG0_TESTS = \
 	regress0/ho/ext-sat-partial-eval.smt2 \
 	regress0/ho/ext-sat.smt2 \
 	regress0/ho/finite-fun-ext.smt2 \
+	regress0/ho/fta0144-alpha-eq.smt2 \
 	regress0/ho/ho-match-fun-suffix.smt2 \
 	regress0/ho/ho-matching-enum.smt2 \
 	regress0/ho/ho-matching-nested-app.smt2 \
diff --git a/test/regress/regress0/ho/fta0144-alpha-eq.smt2 b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
new file mode 100644
index 000000000..0fc536bd9
--- /dev/null
+++ b/test/regress/regress0/ho/fta0144-alpha-eq.smt2
@@ -0,0 +1,29 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort Nat$ 0)
+(declare-sort Complex$ 0)
+(declare-sort Real_set$ 0)
+(declare-fun g$ (Nat$) Complex$)
+(declare-fun r$ () Real)
+(declare-fun uu$ (Real Real) Real)
+(declare-fun uua$ (Real_set$ Real) Bool)
+(declare-fun less$ (Nat$ Nat$) Bool)
+(declare-fun norm$ (Complex$) Real)
+(declare-fun zero$ () Complex$)
+(declare-fun minus$ (Complex$ Complex$) Complex$)
+(declare-fun norm$a (Real) Real)
+(declare-fun zero$a () Nat$)
+(declare-fun member$ (Real Real_set$) Bool)
+(declare-fun minus$a (Nat$ Nat$) Nat$)
+(declare-fun thesis$ () Bool)
+(declare-fun collect$ ((-> Real Bool)) Real_set$)
+(declare-fun less_eq$ (Nat$ Nat$) Bool)
+(declare-fun strict_mono$ ((-> Nat$ Nat$)) Bool)
+(declare-fun strict_mono$a ((-> Real Real)) Bool)
+(declare-fun strict_mono$b ((-> Nat$ Real)) Bool)
+(declare-fun strict_mono$c ((-> Real Nat$)) Bool)
+(assert (! (not thesis$) :named a2))
+(assert (! (forall ((?v0 (-> Nat$ Nat$)) (?v1 Complex$)) (=> (and true (forall ((?v2 Real)) (=> true (exists ((?v3 Nat$)) (forall ((?v4 Nat$)) (=> (less_eq$ ?v3 ?v4) (< (norm$ (minus$ (g$ (?v0 ?v4)) ?v1)) ?v2))))))) thesis$)) :named a3))
+(assert (! (exists ((?v0 (-> Nat$ Nat$)) (?v1 Complex$)) (and true (forall ((?v2 Real)) (=> true (exists ((?v3 Nat$)) (forall ((?v4 Nat$)) (=> (less_eq$ ?v3 ?v4) (< (norm$ (minus$ (g$ (?v0 ?v4)) ?v1)) ?v2)))))))) :named a4))
+(check-sat)