From: Haniel Barbosa Date: Fri, 15 Mar 2019 23:35:43 +0000 (-0500) Subject: New beta-reduction for HOL solving (#2869) X-Git-Tag: cvc5-1.0.0~4238 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2989780f0242d14712927bd4c01c4a521a8fe399;p=cvc5.git New beta-reduction for HOL solving (#2869) --- diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 3eb59e5fc..0583cfa1a 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -20,8 +20,10 @@ #ifndef __CVC4__THEORY__UF__THEORY_UF_REWRITER_H #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H +#include "expr/node_algorithm.h" #include "theory/rewriter.h" #include "theory/substitutions.h" +#include "options/uf_options.h" namespace CVC4 { namespace theory { @@ -46,19 +48,52 @@ public: } if(node.getKind() == kind::APPLY_UF) { if( node.getOperator().getKind() == kind::LAMBDA ){ + Trace("uf-ho-beta") + << "uf-ho-beta : beta-reducing all args of : " << node << "\n"; TNode lambda = node.getOperator(); - std::vector vars; - std::vector subs; - for (const TNode& v : lambda[0]) + Node ret; + // build capture-avoiding substitution since in HOL shadowing may have + // been introduced + if (options::ufHo()) { - vars.push_back(v); + std::vector vars; + std::vector subs; + for (const Node& v : lambda[0]) + { + vars.push_back(v); + } + for (const Node& s : node) + { + subs.push_back(s); + } + if (Trace.isOn("uf-ho-beta")) + { + Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size() + << " vars into " << subs.size() << " terms :\n"; + for (unsigned i = 0, size = subs.size(); i < size; ++i) + { + Trace("uf-ho-beta") << "uf-ho-beta: .... " << vars[i] << " |-> " + << subs[i] << "\n"; + } + } + ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs); + Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n"; } - for (const TNode& s : node) + else { - subs.push_back(s); + std::vector vars; + std::vector subs; + for (const TNode& v : lambda[0]) + { + vars.push_back(v); + } + for (const TNode& s : node) + { + subs.push_back(s); + } + ret = lambda[1].substitute( + vars.begin(), vars.end(), subs.begin(), subs.end()); } - Node ret = lambda[1].substitute( - vars.begin(), vars.end(), subs.begin(), subs.end()); return RewriteResponse(REWRITE_AGAIN_FULL, ret); }else if( !canUseAsApplyUfOperator( node.getOperator() ) ){ return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node)); @@ -66,9 +101,12 @@ public: }else if( node.getKind() == kind::HO_APPLY ){ if( node[0].getKind() == kind::LAMBDA ){ // resolve one argument of the lambda - TNode arg = Rewriter::rewrite( node[1] ); - TNode var = node[0][0][0]; - Node new_body = node[0][1].substitute( var, arg ); + Trace("uf-ho-beta") + << "uf-ho-beta : beta-reducing one argument of : " << node[0] + << " with " << node[1] << "\n"; + + // reconstruct the lambda first to avoid variable shadowing + Node new_body = node[0][1]; if( node[0][0].getNumChildren()>1 ){ std::vector< Node > new_vars; for( unsigned i=1; imkNode( kind::BOUND_VAR_LIST, new_vars ) ); largs.push_back( new_body ); new_body = NodeManager::currentNM()->mkNode( kind::LAMBDA, largs ); + Trace("uf-ho-beta") + << "uf-ho-beta : ....new lambda : " << new_body << "\n"; + } + + // build capture-avoiding substitution since in HOL shadowing may have + // been introduced + if (options::ufHo()) + { + Node arg = Rewriter::rewrite(node[1]); + Node var = node[0][0][0]; + new_body = expr::substituteCaptureAvoiding(new_body, var, arg); + } + else + { + TNode arg = Rewriter::rewrite(node[1]); + TNode var = node[0][0][0]; + new_body = new_body.substitute(var, arg); } + Trace("uf-ho-beta") + << "uf-ho-beta : ..new body : " << new_body << "\n"; return RewriteResponse( REWRITE_AGAIN_FULL, new_body ); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9b1ce17e4..fb0e358e2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -476,6 +476,7 @@ set(regress_0_tests regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/modulo-func-equality.smt2 + regress0/ho/shadowing-defs.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2 new file mode 100644 index 000000000..722e970b6 --- /dev/null +++ b/test/regress/regress0/ho/shadowing-defs.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unknown +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort mu 0) + +(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W))))) + +(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (Phi W) (Psi W))))) + +(declare-fun mand ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mand (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mor (mnot Phi) (mnot Psi)) __flatten_var_0)))) + +(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0)))) + +(declare-fun mforall_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_ind (lambda ((Phi (-> mu $$unsorted Bool)) (W $$unsorted)) (forall ((X mu)) (Phi X W) )))) + +(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) + +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) + +(declare-fun a1 ($$unsorted $$unsorted) Bool) +(declare-fun a2 ($$unsorted $$unsorted) Bool) +(declare-fun a3 ($$unsorted $$unsorted) Bool) + +(declare-fun jan () mu) +(declare-fun cola () mu) + +(declare-fun likes (mu mu $$unsorted) Bool) + +(declare-fun very_much_likes (mu mu $$unsorted) Bool) + +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mbox a3 (mimplies (mand (likes X Y) (mand (mbox a1 (likes X Y)) (mbox a2 (likes X Y)))) (very_much_likes X Y)) __flatten_var_0)) __flatten_var_0))))) + +(check-sat) \ No newline at end of file