From: Andrew Reynolds Date: Tue, 28 Aug 2018 22:09:01 +0000 (-0500) Subject: Fix for get constraints method in fmf-fun (#2399) X-Git-Tag: cvc5-1.0.0~4704 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a2148c3cfb20928b2e721726345ea96149154d9;p=cvc5.git Fix for get constraints method in fmf-fun (#2399) --- diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index c40a7c4d9..1671fa1a0 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -211,8 +211,8 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod } }else{ //simplify term - std::map< Node, bool > visited; - simplifyTerm( n, constraints, visited ); + std::map visited; + getConstraints(n, constraints, visited); } if( !constraints.empty() && isBool && hasPol ){ //conjoin with current @@ -247,46 +247,92 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod } } -void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - Trace("fmf-fun-def-debug") << "Simplify term " << n << std::endl; - if( n.getKind()==ITE ){ - simplifyTerm( n[0], constraints, visited ); - std::vector< Node > ccons1; - std::vector< Node > ccons2; - simplifyTerm( n[1], ccons1, visited ); - simplifyTerm( n[2], ccons2, visited ); - if( !ccons1.empty() || !ccons2.empty() ){ - Node n1 = ccons1.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons1.size()==1 ? ccons1[0] : NodeManager::currentNM()->mkNode( AND, ccons1 ) ); - Node n2 = ccons2.empty() ? NodeManager::currentNM()->mkConst( true ) : ( ccons2.size()==1 ? ccons2[0] : NodeManager::currentNM()->mkNode( AND, ccons2 ) ); - constraints.push_back( NodeManager::currentNM()->mkNode( ITE, n[0], n1, n2 ) ); +void FunDefFmf::getConstraints(Node n, + std::vector& constraints, + std::map& visited) +{ + std::map::iterator itv = visited.find(n); + if (itv != visited.end()) + { + // already visited + if (!itv->second.isNull()) + { + // add the cached constraint if it does not already occur + if (std::find(constraints.begin(), constraints.end(), itv->second) + == constraints.end()) + { + constraints.push_back(itv->second); } - }else{ - if( n.getKind()==APPLY_UF ){ - //check if f is defined, if so, we must enforce domain constraints for this f-application - Node f = n.getOperator(); - std::map< Node, TypeNode >::iterator it = d_sorts.find( f ); - if( it!=d_sorts.end() ){ - //create existential - Node z = NodeManager::currentNM()->mkBoundVar("?z", it->second ); - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, z ); - std::vector< Node > children; - for( unsigned j=0; jmkNode( APPLY_UF, d_input_arg_inj[f][j], z ); - children.push_back( uz.eqNode( n[j] ) ); - } - Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); - bd = bd.negate(); - Node ex = NodeManager::currentNM()->mkNode( FORALL, bvl, bd ); - ex = ex.negate(); - constraints.push_back( ex ); - Trace("fmf-fun-def-debug") << "---> add constraint " << ex << std::endl; + } + return; + } + visited[n] = Node::null(); + std::vector currConstraints; + NodeManager* nm = NodeManager::currentNM(); + if (n.getKind() == ITE) + { + // collect constraints for the condition + getConstraints(n[0], currConstraints, visited); + // collect constraints for each branch + Node cs[2]; + for (unsigned i = 0; i < 2; i++) + { + std::vector ccons; + getConstraints(n[i + 1], ccons, visited); + cs[i] = ccons.empty() + ? nm->mkConst(true) + : (ccons.size() == 1 ? ccons[0] : nm->mkNode(AND, ccons)); + } + if (!cs[0].isConst() || !cs[1].isConst()) + { + Node itec = nm->mkNode(ITE, n[0], cs[0], cs[1]); + currConstraints.push_back(itec); + Trace("fmf-fun-def-debug") + << "---> add constraint " << itec << " for " << n << std::endl; + } + } + else + { + if (n.getKind() == APPLY_UF) + { + // check if f is defined, if so, we must enforce domain constraints for + // this f-application + Node f = n.getOperator(); + std::map::iterator it = d_sorts.find(f); + if (it != d_sorts.end()) + { + // create existential + Node z = nm->mkBoundVar("?z", it->second); + Node bvl = nm->mkNode(BOUND_VAR_LIST, z); + std::vector children; + for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) + { + Node uz = nm->mkNode(APPLY_UF, d_input_arg_inj[f][j], z); + children.push_back(uz.eqNode(n[j])); } + Node bd = + children.size() == 1 ? children[0] : nm->mkNode(AND, children); + bd = bd.negate(); + Node ex = nm->mkNode(FORALL, bvl, bd); + ex = ex.negate(); + currConstraints.push_back(ex); + Trace("fmf-fun-def-debug") + << "---> add constraint " << ex << " for " << n << std::endl; } - for( unsigned i=0; imkNode(AND, currConstraints); + visited[n] = finalc; + // add to constraints + getConstraints(n, constraints, visited); } } diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index b59c6199a..78adc710c 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -49,11 +49,6 @@ private: 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 - * 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(){} ~FunDefFmf(){} @@ -70,6 +65,15 @@ public: * which are Sigma^{dfn} in that paper. */ void simplify( std::vector< Node >& assertions ); + /** get constraints + * + * This computes constraints for the final else branch of A_0 in Figure 1 + * of Reynolds et al "Model Finding for Recursive Functions". The range of + * the cache visited stores the constraint (if any) for each node. + */ + void getConstraints(Node n, + std::vector& constraints, + std::map& visited); }; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 1c37669de..6187cb2fa 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1101,6 +1101,7 @@ REG1_TESTS = \ regress1/fmf/fib-core.smt2 \ regress1/fmf/fmf-bound-2dim.smt2 \ regress1/fmf/fmf-bound-int.smt2 \ + regress1/fmf/fmf-fun-divisor-pp.smt2 \ regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 \ regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 \ regress1/fmf/fmf-strange-bounds.smt2 \ diff --git a/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2 b/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2 new file mode 100644 index 000000000..93bfb930d --- /dev/null +++ b/test/regress/regress1/fmf/fmf-fun-divisor-pp.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --fmf-fun +; EXPECT: unsat +(set-logic UFNIA) +(set-info :status unsat) +(define-fun-rec pow ((a Int)(b Int)) Int + (ite (<= b 0) + 1 + (* a (pow a (- b 1))))) + +(declare-fun x () Int) + +(assert (>= x 0)) +(assert (< x (pow 2 2))) +(assert (>= (mod (div x (pow 2 3)) (pow 2 2)) 2)) + +(check-sat)