diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.h')
-rw-r--r-- | src/theory/quantifiers/fun_def_process.h | 36 |
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 ); }; |