diff options
| author | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
|---|---|---|
| committer | Paul Meng <baolmeng@gmail.com> | 2016-10-11 13:54:20 -0500 |
| commit | 3395c5c13cd61d98aec0d9806e3b9bc3d707968a (patch) | |
| tree | 0eadad9799862ec77d29f7abe03a46c300d80de8 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 773e7d27d606b71ff0f78e84efe1deef2653f016 (diff) | |
| parent | 5f415d4585134612bc24e9a823289fee35541a01 (diff) | |
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
Conflicts:
src/options/quantifiers_options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rwxr-xr-x | src/theory/quantifiers/quantifiers_rewriter.h | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 60dc8ab10..90a22f4b7 100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,7 +38,6 @@ public: private: static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); - static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); @@ -53,14 +52,15 @@ private: static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); -private: +public: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); + static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); + static Node computePrenexAgg( Node n, bool topLevel ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); private: @@ -89,8 +89,11 @@ private: static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs); public: static Node rewriteRewriteRule( Node r ); - static bool containsQuantifiers(Node n); + static bool containsQuantifiers( Node n ); + static bool isPrenexNormalForm( Node n ); static Node preprocess( Node n, bool isInst = false ); + static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); + static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ |