Fix char overflow issues in regular expression solver (#2275)

1 files changed, 28 insertions, 26 deletions

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index ecf294fc6..a646f0e6f 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -38,8 +38,9 @@ class RegExpOpr {
   typedef std::set< Node > SetNodes;
   typedef std::pair< Node, Node > PairNodes;
 
-private:
-  unsigned char d_lastchar;
+ private:
+  /** the code point of the last character in the alphabet we are using */
+  unsigned d_lastchar;
   Node d_emptyString;
   Node d_true;
   Node d_false;
@@ -49,39 +50,40 @@ private:
   Node d_one;
   CVC4::Rational RMAXINT;
 
-  unsigned char d_char_start;
-  unsigned char d_char_end;
   Node d_sigma;
   Node d_sigma_star;
 
-  std::map< PairNodes, Node > d_simpl_cache;
-  std::map< PairNodes, Node > d_simpl_neg_cache;
-  std::map< Node, std::pair< int, Node > > d_delta_cache;
-  std::map< PairNodeStr, Node > d_dv_cache;
-  std::map< PairNodeStr, std::pair< Node, int > > d_deriv_cache;
-  std::map< Node, std::pair< Node, int > > d_compl_cache;
-  std::map< Node, bool > d_cstre_cache;
-  std::map< Node, std::pair< std::set<unsigned char>, std::set<Node> > > d_cset_cache;
-  std::map< Node, std::pair< std::set<unsigned char>, std::set<Node> > > d_fset_cache;
-  std::map< PairNodes, Node > d_inter_cache;
-  std::map< Node, Node > d_rm_inter_cache;
-  std::map< Node, bool > d_norv_cache;
-  std::map< Node, std::vector< PairNodes > > d_split_cache;
-  //bool checkStarPlus( Node t );
-  void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );
-  void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );
-  std::string niceChar( Node r );
-  Node mkAllExceptOne( unsigned char c );
-  bool isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2);
+  std::map<PairNodes, Node> d_simpl_cache;
+  std::map<PairNodes, Node> d_simpl_neg_cache;
+  std::map<Node, std::pair<int, Node> > d_delta_cache;
+  std::map<PairNodeStr, Node> d_dv_cache;
+  std::map<PairNodeStr, std::pair<Node, int> > d_deriv_cache;
+  std::map<Node, std::pair<Node, int> > d_compl_cache;
+  std::map<Node, bool> d_cstre_cache;
+  std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_cset_cache;
+  std::map<Node, std::pair<std::set<unsigned>, std::set<Node> > > d_fset_cache;
+  std::map<PairNodes, Node> d_inter_cache;
+  std::map<Node, Node> d_rm_inter_cache;
+  std::map<Node, bool> d_norv_cache;
+  std::map<Node, std::vector<PairNodes> > d_split_cache;
+  void simplifyPRegExp(Node s, Node r, std::vector<Node> &new_nodes);
+  void simplifyNRegExp(Node s, Node r, std::vector<Node> &new_nodes);
+  std::string niceChar(Node r);
+  Node mkAllExceptOne(unsigned c);
+  bool isPairNodesInSet(std::set<PairNodes> &s, Node n1, Node n2);
 
   bool containC2(unsigned cnt, Node n);
   Node convert1(unsigned cnt, Node n);
   void convert2(unsigned cnt, Node n, Node &r1, Node &r2);
   bool testNoRV(Node r);
-  Node intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > cache, unsigned cnt );
+  Node intersectInternal(Node r1,
+                         Node r2,
+                         std::map<PairNodes, Node> cache,
+                         unsigned cnt);
   Node removeIntersection(Node r);
-  void firstChars( Node r, std::set<unsigned char> &pcset, SetNodes &pvset );
-public:
+  void firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset);
+
+ public:
   RegExpOpr();
   ~RegExpOpr();