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.

2 files changed, 74 insertions, 19 deletions

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 <vector>
@@ -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<assertions.size(); i++ ){
-    int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0;
+    bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
     //constant boolean function definitions do not add domain constraints
-    if( is_fd==0 || ( is_fd==1 && assertions[i][1].getKind()==EQUAL ) ){
+    if( !is_fd || ( is_fd && assertions[i][1].getKind()==EQUAL ) ){
       std::vector< Node > 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<n.getNumChildren(); i++ ){
           Node c = n[i];
           //do not process LHS of definition
-          if( is_fun_def!=1 || c!=hd ){
+          if( !is_fun_def || c!=hd ){
             bool newHasPol;
             bool newPol;
             QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
             //get child constraints
             std::vector< Node > 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; i<n.getNumChildren(); i++ ){
+              // if this child holds with forcing polarity (true child of OR or false child of AND), 
+              // then we only care about its associated recursive conditions 
+              branch_cond = NodeManager::currentNM()->mkNode( 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 );
 };