From: Andrew Reynolds Date: Fri, 13 Apr 2018 00:59:59 +0000 (-0500) Subject: Fix alpha equivalence for higher-order (#1769) X-Git-Tag: cvc5-1.0.0~5157 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=781bfd65daec2932b7836259b3484ac500edb46a;p=cvc5.git Fix alpha equivalence for higher-order (#1769) --- 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)