From db982d9329981683c8d791aadba7e97fa98b0bd3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 28 Oct 2014 17:23:22 +0100 Subject: Preprocessing step for finding finite runs of well-defined function definitions using FMF. --- src/theory/quantifiers/fun_def_process.h | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/theory/quantifiers/fun_def_process.h') 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(){} -- cgit v1.2.3