From d39210bb485c13e7f3290e4e7faab9c5830f437d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Feb 2018 22:50:47 -0600 Subject: [PATCH] Minor fixes for rec-fun (#1616) --- .../quantifiers/quantifiers_attributes.cpp | 20 +++++++- .../quantifiers/quantifiers_rewriter.cpp | 50 +++++++++++++++---- test/regress/regress1/quantifiers/Makefile.am | 3 +- .../regress1/quantifiers/arith-rec-fun.smt2 | 6 +++ 4 files changed, 65 insertions(+), 14 deletions(-) create mode 100644 test/regress/regress1/quantifiers/arith-rec-fun.smt2 diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index d80a7cf82..25e5bbb5f 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -14,12 +14,13 @@ #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers_engine.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/arith/arith_msum.h" #include "theory/quantifiers/fun_def_engine.h" #include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" #include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; @@ -146,6 +147,21 @@ Node QuantAttributes::getFunDefBody( Node q ) { }else if( q[1][1]==h ){ return q[1][0]; } + else if (q[1][0].getType().isReal()) + { + // solve for h in the equality + std::map msum; + if (ArithMSum::getMonomialSum(q[1], msum)) + { + Node veq; + int res = ArithMSum::isolate(h, msum, veq, EQUAL); + if (res != 0) + { + Assert(veq.getKind() == EQUAL); + return res == 1 ? veq[0] : veq[1]; + } + } + } }else{ Node atom = q[1].getKind()==NOT ? q[1][0] : q[1]; bool pol = q[1].getKind()!=NOT; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 5586c04fb..bc298fa9c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -517,14 +517,36 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Assert( !h.isNull() ); // if it is a function definition, rewrite the body independently Node fbody = QuantAttributes::getFunDefBody( q ); - Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; - Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false ); - Assert( new_vars.size()==h.getNumChildren() ); - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) ); - }else{ - return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, options::elimExtArithQuant() ); - } + if (!fbody.isNull()) + { + Node r = computeProcessTerms2(fbody, + true, + true, + curr_cond, + 0, + cache, + icache, + new_vars, + new_conds, + false); + Assert(new_vars.size() == h.getNumChildren()); + return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r)); + } + // It can happen that we can't infer the shape of the function definition, + // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to + // forall xy. false. + } + return computeProcessTerms2(body, + true, + true, + curr_cond, + 0, + cache, + icache, + new_vars, + new_conds, + options::elimExtArithQuant()); } Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, @@ -1917,7 +1939,16 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs ); return nn.negate(); }else if( n.getKind()==kind::FORALL ){ - if( polarity ){ + if (n.getNumChildren() == 3) + { + // Do not pre-skolemize quantified formulas with three children. + // This includes non-standard quantified formulas + // like recursive function definitions, or sygus conjectures, and + // quantified formulas with triggers. + return n; + } + else if (polarity) + { if( options::preSkolemQuant() && options::preSkolemQuantNested() ){ vector< Node > children; children.push_back( n[0] ); @@ -1932,9 +1963,6 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v } //process body children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) ); - if( n.getNumChildren()==3 ){ - children.push_back( n[2] ); - } //return processed quantifier return NodeManager::currentNM()->mkNode( kind::FORALL, children ); } diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am index 7d3da3654..159f2e088 100644 --- a/test/regress/regress1/quantifiers/Makefile.am +++ b/test/regress/regress1/quantifiers/Makefile.am @@ -79,7 +79,8 @@ TESTS = \ RND-small.smt2 \ RNDPRE_4_1-dd-nqe.smt2 \ set8.smt2 \ - z3.620661-no-fv-trigger.smt2 + z3.620661-no-fv-trigger.smt2 \ + arith-rec-fun.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress1/quantifiers/arith-rec-fun.smt2 b/test/regress/regress1/quantifiers/arith-rec-fun.smt2 new file mode 100644 index 000000000..8133db8dd --- /dev/null +++ b/test/regress/regress1/quantifiers/arith-rec-fun.smt2 @@ -0,0 +1,6 @@ +(set-logic UFLIA) +(set-info :status unsat) +(define-fun-rec sumr ((x Int)) Int + (+ x (ite (> x 0) (sumr (- x 1)) 0))) +(assert (= (sumr 2) 2)) +(check-sat) -- 2.30.2