diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 09:45:46 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-11 11:29:45 -0500 |
| commit | 38d149261763e5f2f65abb21c2b647f2befa7807 (patch) | |
| tree | 51c3019eff61c7f3702f3dc888fb88d3a714f68a /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 3ed865aa12a94e935038d70b130701045b84a8b8 (diff) | |
Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
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 */ |