diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 13:03:31 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-03 13:03:45 -0500 |
| commit | 9aaa7ca741199f73e70149f8309cd7cd9a12e69f (patch) | |
| tree | 1dec877f28b4733f9a866620c1e671b4e522faf9 /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 532a228bc718bde32afb3b96ca2cd3abcbd40f48 (diff) | |
Option for prenex normal form
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | 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..bb352f65c 100644 --- 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 ); + static Node computePrenexAgg( Node n ); 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 */ |