diff options
| author | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
|---|---|---|
| committer | PaulMeng <baolmeng@gmail.com> | 2016-08-24 11:24:57 -0400 |
| commit | dc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch) | |
| tree | 7516d3d5d43f0dadb943bb186615e0903cbd9f7f /src/theory/quantifiers/quantifiers_rewriter.h | |
| parent | 74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff) | |
| parent | 6b355496aaf27d46d6a33402814753589b755842 (diff) | |
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
| -rwxr-xr-x | src/theory/quantifiers/quantifiers_rewriter.h | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 776517109..60dc8ab10 100755 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -35,8 +35,6 @@ public: static bool isClause( Node n ); static bool isLiteral( Node n ); static bool isCube( Node n ); - static int getPurifyId( Node n ); - static int getPurifyIdLit( Node n ); 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 ); @@ -49,12 +47,12 @@ private: std::vector< Node >& new_vars, std::vector< Node >& new_conds ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); - static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); + static bool isVariableElim( Node v, Node s ); + static void isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, + std::map< Node, bool >& elig_vars ); static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs, - std::map< Node, std::vector< int > >& var_parent ); - static Node computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, - std::map< Node, std::vector< int > >& var_parent, int parentId ); - static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ); + std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds ); + static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ); private: static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); @@ -65,8 +63,6 @@ private: static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); - static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); - static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ); private: enum{ COMPUTE_ELIM_SYMBOLS = 0, @@ -76,7 +72,6 @@ private: COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, COMPUTE_COND_SPLIT, - COMPUTE_PURIFY_EXPAND, //COMPUTE_FLATTEN_ARGS_UF, //COMPUTE_CNF, COMPUTE_LAST |