diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e97d84701..4cbdb0cd1 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,14 +38,16 @@ public: private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); - static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); + static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ); + static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static bool hasArg( std::vector< Node >& args, Node n ); static void setNestedQuantifiers( Node n, Node q ); static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); + static void setAttributes( Node in, Node n ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); + static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); static Node computeNNF( Node body ); static Node computeSimpleIteLift( Node body ); @@ -79,6 +81,10 @@ private: static bool doMiniscopingAnd(); static bool doOperation( Node f, bool isNested, int computeOption ); public: + static Node rewriteRewriteRule( Node r ); + static bool containsQuantifiers(Node n); + static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs); +public: //static Node rewriteQuants( Node n, bool isNested = false ); //static Node rewriteQuant( Node n, bool isNested = false ); };/* class QuantifiersRewriter */ |