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.

1 files changed, 29 insertions, 7 deletions

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 );
 };