From 42e970e822ec3d0adaacbff40e0aee02a32372cc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Sep 2017 07:23:33 -0500 Subject: [PATCH] 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 +++++++++--- test/regress/regress0/fmf/Makefile.am | 4 +- .../regress/regress0/fmf/issue916-fmf-or.smt2 | 48 ++++++++++++++++ test/regress/regress0/fmf/pow2-bool.smt2 | 17 ++++++ 5 files changed, 142 insertions(+), 20 deletions(-) create mode 100644 test/regress/regress0/fmf/issue916-fmf-or.smt2 create mode 100644 test/regress/regress0/fmf/pow2-bool.smt2 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 ); }; diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 4f81d79aa..b2ed657d0 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -76,7 +76,9 @@ TESTS = \ fmf-fun-no-elim-ext-arith.smt2 \ fmf-fun-no-elim-ext-arith2.smt2 \ cruanes-no-minimal-unk.smt2 \ - no-minimal-sat.smt2 + no-minimal-sat.smt2 \ + issue916-fmf-or.smt2 \ + pow2-bool.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/issue916-fmf-or.smt2 b/test/regress/regress0/fmf/issue916-fmf-or.smt2 new file mode 100644 index 000000000..0c51e39af --- /dev/null +++ b/test/regress/regress0/fmf/issue916-fmf-or.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat + +(set-logic UFDTLIA) +(set-info :smt-lib-version 2.5) + +(define-funs-rec + ( + (validIdValue ((x Int)(v Int)) Bool) + ) + ( + (or + (and (= x 0) (< (- 10) v 10) ) + (and (= x 1) (<= (- 100) v (- 10)) ) + (and (= x 2) (<= 10 v 100) ) + (and (= x 3) (< (- 1000) v (- 100)) ) + (and (= x 4) (< 100 v 1000) ) + (and (= x 5) (<= (- 1000) v) ) + (and (= x 6) (<= v 1000) ) + (validIdValue (- x 7) v) + ) + ) +) + +(declare-datatypes (T) ( (List (Nil) (Cstr (head T) (tail List) ) ) ) ) +(declare-datatypes (T S) ( (Pair (Pair (first T) (second S)) ) ) ) + +(define-funs-rec + ( + (validList ((l (List (Pair Int Int)))) Bool) + ) + ( + (ite (= l (as Nil (List (Pair Int Int))) ) + true + (let ((hd (head l))) (and (>= (first hd) 0) + (validIdValue (first hd) (second hd)) + (validList (tail l)) + ) + ) + ) + ) +) + + +(declare-const myList (List (Pair Int Int))) +(assert (distinct myList (as Nil (List (Pair Int Int))))) +(assert (validList myList)) +(check-sat) diff --git a/test/regress/regress0/fmf/pow2-bool.smt2 b/test/regress/regress0/fmf/pow2-bool.smt2 new file mode 100644 index 000000000..4943c646c --- /dev/null +++ b/test/regress/regress0/fmf/pow2-bool.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic ALL) + +(define-fun-rec pow2 ((n Int) (p Int)) Bool ( + or + (and (= n 0) (= p 1)) + (and (> n 0) (> p 1) (= 0 (mod p 2)) (pow2 (- n 1) (div p 2))) +)) + +(declare-const n Int) +(declare-const p Int) + +(assert (= n 10)) +(assert (pow2 n p)) + +(check-sat) -- 2.30.2