diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 44 |
1 files changed, 34 insertions, 10 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e44672d66..7703f01fd 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -16,11 +16,10 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H -#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #include "theory/rewriter.h" -#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -36,13 +35,28 @@ 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 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 ); + static void computeArgs(const std::vector<Node>& args, + std::map<Node, bool>& activeMap, + Node n, + std::map<Node, bool>& visited); + static void computeArgVec(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n); + static void computeArgVec2(const std::vector<Node>& args, + std::vector<Node>& activeArgs, + Node n, + Node ipl); static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); + /** datatype expand + * + * If v occurs in args and has a datatype type whose index^th constructor is + * C, this method returns a node of the form C( x1, ..., xn ), removes v from + * args and adds x1...xn to args. + */ + static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args); //-------------------------------------variable elimination /** is variable elimination * @@ -62,12 +76,22 @@ private: std::vector<Node>& args, std::vector<Node>& vars, std::vector<Node>& subs); - /** variable eliminate for bit-vector literals + /** variable eliminate for bit-vector equalities + * + * If this returns a non-null value ret, then var is updated to a member of + * args, lit is equivalent to ( var = ret ). + */ + static Node getVarElimLitBv(Node lit, + const std::vector<Node>& args, + Node& var); + /** variable eliminate for string equalities * * If this returns a non-null value ret, then var is updated to a member of - * args, lit is equivalent to ( var = ret ), and var is removed from args. + * args, lit is equivalent to ( var = ret ). */ - static Node getVarElimLitBv(Node lit, std::vector<Node>& args, Node& var); + static Node getVarElimLitString(Node lit, + const std::vector<Node>& args, + Node& var); /** get variable elimination * * If n asserted with polarity pol entails a literal lit that corresponds @@ -188,6 +212,6 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ |