Preprocessing step for finding finite runs of well-defined function definitions using FMF.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index c2d8aeb65..22adf427d 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -30,6 +30,17 @@ namespace quantifiers {
 
 //find finite models for well-defined functions
 class FunDefFmf {
+private:
+  //defined functions to input sort
+  std::map< Node, TypeNode > d_sorts;
+  //defined functions to injections input -> argument elements
+  std::map< Node, std::vector< Node > > d_input_arg_inj;
+  //flatten ITE
+  void flattenITE( Node lhs, Node n, std::vector< std::vector< Node > >& conds, std::vector< Node >& terms );
+  //simplify
+  Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false );
+  //simplify term
+  void simplifyTerm( Node n, std::vector< Node >& constraints );
 public:
   FunDefFmf(){}
   ~FunDefFmf(){}