Merge branch 'master' into splitEqRew

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 */