From 42e970e822ec3d0adaacbff40e0aee02a32372cc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Sep 2017 07:23:33 -0500 Subject: Improve finite model finding for recursive predicates (#1150) * Optimization for model finding for recursive functions involving branching positions. Update documentation, add regressions. * Simplifications, update comments. --- src/theory/quantifiers/fun_def_process.cpp | 57 +++++++++++++++++++++++------- src/theory/quantifiers/fun_def_process.h | 36 +++++++++++++++---- 2 files changed, 74 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 064d6c8d9..5bbd4c48e 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -11,7 +11,7 @@ ** ** \brief Sort inference module ** - ** This class implements pre-process steps for well-defined functions + ** This class implements pre-process steps for admissible recursive function definitions (Reynolds et al IJCAR2016) **/ #include @@ -29,7 +29,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; -void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { +void FunDefFmf::simplify( std::vector< Node >& assertions ) { std::vector< int > fd_assertions; std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers @@ -97,12 +97,12 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { std::map< int, std::map< Node, Node > > visited; std::map< int, std::map< Node, Node > > visited_cons; for( unsigned i=0; i constraints; - Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; - Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd, visited, visited_cons ); + Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is function definition = " << is_fd << std::endl; + Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd ? subs_head[i] : Node::null(), is_fd, visited, visited_cons ); Assert( constraints.empty() ); if( n!=assertions[i] ){ n = Rewriter::rewrite( n ); @@ -116,12 +116,11 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { } } -//is_fun_def 1 : top of fun-def, 2 : top of fun-def body, 0 : not top -Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def, +Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, std::map< int, std::map< Node, Node > >& visited, std::map< int, std::map< Node, Node > >& visited_cons ) { Assert( constraints.empty() ); - int index = is_fun_def + 3*( hasPol ? ( pol ? 1 : -1 ) : 0 ); + int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 ); std::map< Node, Node >::iterator itv = visited[index].find( n ); if( itv!=visited[index].end() ){ //constraints.insert( visited_cons[index] @@ -148,19 +147,29 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod }else{ Node nn = n; bool isBool = n.getType().isBoolean(); - if( isBool && n.getKind()!=APPLY_UF && is_fun_def!=2 ){ + if( isBool && n.getKind()!=APPLY_UF ){ std::vector< Node > children; bool childChanged = false; + // are we at a branch position (not all children are necessarily relevant)? + bool branch_pos = ( n.getKind()==ITE || n.getKind()==OR || n.getKind()==AND ); + std::vector< Node > branch_constraints; for( unsigned i=0; i cconstraints; - c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, is_fun_def==1 ? 2 : 0, visited, visited_cons ); + c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, false, visited, visited_cons ); + if( branch_pos ){ + // if at a branching position, the other constraints don't matter if this is satisfied + Node bcons = cconstraints.empty() ? NodeManager::currentNM()->mkConst( true ) : + ( cconstraints.size()==1 ? cconstraints[0] : NodeManager::currentNM()->mkNode( AND, cconstraints ) ); + branch_constraints.push_back( bcons ); + Trace("fmf-fun-def-debug2") << "Branching constraint at arg " << i << " is " << bcons << std::endl; + } constraints.insert( constraints.end(), cconstraints.begin(), cconstraints.end() ); } children.push_back( c ); @@ -169,6 +178,29 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod if( childChanged ){ nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); } + if( branch_pos && !constraints.empty() ){ + // if we are at a branching position in the formula, we can + // minimize recursive constraints on recursively defined predicates if we know one child forces + // the overall evaluation of this formula. + Node branch_cond; + if( n.getKind()==ITE ){ + // always care about constraints on the head of the ITE, but only care about one of the children depending on how it evaluates + branch_cond = NodeManager::currentNM()->mkNode( kind::AND, branch_constraints[0], + NodeManager::currentNM()->mkNode( kind::ITE, n[0], branch_constraints[1], branch_constraints[2] ) ); + }else{ + // in the default case, we care about all conditions + branch_cond = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints ); + for( unsigned i=0; imkNode( kind::ITE, + ( n.getKind()==OR ? n[i] : n[i].negate() ), branch_constraints[i], branch_cond ); + } + } + Trace("fmf-fun-def-debug2") << "Made branching condition " << branch_cond << std::endl; + constraints.clear(); + constraints.push_back( branch_cond ); + } }else{ //simplify term std::map< Node, bool > visited; @@ -182,6 +214,7 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod }else{ ret = NodeManager::currentNM()->mkNode( OR, nn, cons.negate() ); } + Trace("fmf-fun-def-debug2") << "Add constraint to obtain " << ret << std::endl; constraints.clear(); }else{ ret = nn; diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index e7a53324d..a4e0bdfa3 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Pre-process steps for well-defined functions + ** \brief Pre-process step for admissible recursively defined functions **/ #include "cvc4_private.h" @@ -28,14 +28,31 @@ namespace CVC4 { namespace theory { namespace quantifiers { -//find finite models for well-defined functions +//Preprocessing pass to allow finite model finding for admissible recursive function definitions +// For details, see Reynolds et al "Model Finding for Recursive Functions" IJCAR 2016 class FunDefFmf { private: - //simplify - Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, int is_fun_def, + /** simplify formula + * This is A_0 in Figure 1 of Reynolds et al "Model Finding for Recursive Functions". + * The input of A_0 in that paper is a pair ( term t, polarity p ) + * The return value of A_0 in that paper is a pair ( term t', set of formulas X ). + * + * This function implements this such that : + * n is t + * pol/hasPol is p + * the return value is t' + * the set of formulas X are stored in "constraints" + * + * Additionally, is_fun_def is whether we are currently processing the top of a function defintion, + * since this affects whether we process the head of the definition. + */ + Node simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, std::map< int, std::map< Node, Node > >& visited, std::map< int, std::map< Node, Node > >& visited_cons ); - //simplify term + /** simplify term + * This computes constraints for the final else branch of A_0 in Figure 1 + * of Reynolds et al "Model Finding for Recursive Functions". + */ void simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited ); public: FunDefFmf(){} @@ -46,8 +63,13 @@ public: std::map< Node, std::vector< Node > > d_input_arg_inj; // (newly) defined functions std::vector< Node > d_funcs; - //simplify - void simplify( std::vector< Node >& assertions, bool doRewrite = false ); + /** simplify, which does the following: + * (1) records all top-level recursive function definitions in assertions, + * (2) runs Figure 1 of Reynolds et al "Model Finding for Recursive Functions" + * IJCAR 2016 on all formulas in assertions based on the definitions from part (1), + * which are Sigma^{dfn} in that paper. + */ + void simplify( std::vector< Node >& assertions ); }; -- cgit v1.2.3