Merge branch 'master' of https://github.com/CVC4/CVC4

10 files changed, 211 insertions, 59 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 4475554b1..84f674d2b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -142,6 +142,11 @@ StringType ExprManager::stringType() const {
   return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType())));
 }
 
+RegExpType ExprManager::regExpType() const {
+  NodeManagerScope nms(d_nodeManager);
+  return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType())));
+}
+
 RealType ExprManager::realType() const {
   NodeManagerScope nms(d_nodeManager);
   return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType())));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 72fa5d1b6..04f2f4289 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -121,6 +121,9 @@ public:
   /** Get the type for strings. */
   StringType stringType() const;
 
+  /** Get the type for regular expressions. */
+  RegExpType regExpType() const;
+
   /** Get the type for reals. */
   RealType realType() const;
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7fa93d38d..7d2b13e4c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -705,7 +705,7 @@ public:
   inline TypeNode stringType();
 
   /** Get the (singleton) type for RegExp. */
-  inline TypeNode regexpType();
+  inline TypeNode regExpType();
 
   /** Get the (singleton) type for rounding modes. */
   inline TypeNode roundingModeType();
@@ -1001,7 +1001,7 @@ inline TypeNode NodeManager::stringType() {
 }
 
 /** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regexpType() {
+inline TypeNode NodeManager::regExpType() {
   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 }
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5b4fef395..0c4d554ef 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -223,6 +223,12 @@ bool Type::isString() const {
   return d_typeNode->isString();
 }
 
+/** Is this the regexp type? */
+bool Type::isRegExp() const {
+  NodeManagerScope nms(d_nodeManager);
+  return d_typeNode->isRegExp();
+}
+
 /** Is this the rounding mode type? */
 bool Type::isRoundingMode() const {
   NodeManagerScope nms(d_nodeManager);
@@ -427,6 +433,11 @@ StringType::StringType(const Type& t) throw(IllegalArgumentException) :
   PrettyCheckArgument(isNull() || isString(), this);
 }
 
+RegExpType::RegExpType(const Type& t) throw(IllegalArgumentException) :
+  Type(t) {
+  PrettyCheckArgument(isNull() || isRegExp(), this);
+}
+
 RoundingModeType::RoundingModeType(const Type& t) throw(IllegalArgumentException) :
   Type(t) {
   PrettyCheckArgument(isNull() || isRoundingMode(), this);
diff --git a/src/expr/type.h b/src/expr/type.h
index a2d6207fb..43cb3ffbf 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -47,6 +47,7 @@ class BooleanType;
 class IntegerType;
 class RealType;
 class StringType;
+class RegExpType;
 class RoundingModeType;
 class BitVectorType;
 class ArrayType;
@@ -258,6 +259,12 @@ public:
   bool isString() const;
 
   /**
+   * Is this the regexp type?
+   * @return true if the type is the regexp type
+   */
+  bool isRegExp() const;
+
+  /**
    * Is this the rounding mode type?
    * @return true if the type is the rounding mode type
    */
@@ -424,6 +431,18 @@ public:
 };/* class StringType */
 
 /**
+ * Singleton class encapsulating the string type.
+ */
+class CVC4_PUBLIC RegExpType : public Type {
+
+public:
+
+  /** Construct from the base type */
+  RegExpType(const Type& type) throw(IllegalArgumentException);
+};/* class RegExpType */
+
+
+/**
  * Singleton class encapsulating the rounding mode type.
  */
 class CVC4_PUBLIC RoundingModeType : public Type {
diff --git a/src/options/arith_options b/src/options/arith_options
index 9f4003004..f38e377ba 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -162,4 +162,7 @@ option pbRewrites --pb-rewrites bool :default false
 option pbRewriteThreshold --pb-rewrite-threshold int :default 256
  threshold of number of pseudoboolean variables to have before doing rewrites
 
+option sNormInferEq --snorm-infer-eq bool :default false
+ infer equalities based on Shostak normalization
+
 endmodule
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 470fc5253..5c37a5372 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -205,16 +205,35 @@ tokens {
   // Strings
 
   STRING_TOK = 'STRING';
-  SCONCAT_TOK = 'SCONCAT';
-  SCONTAINS_TOK = 'CONTAINS';
-  SSUBSTR_TOK = 'SUBSTR';
-  SINDEXOF_TOK = 'INDEXOF';
-  SREPLACE_TOK = 'REPLACE';
-  SPREFIXOF_TOK = 'PREFIXOF';
-  SSUFFIXOF_TOK = 'SUFFIXOF';
-  STOINTEGER_TOK = 'TO_INTEGER';
-  STOSTRING_TOK = 'TO_STRING';
-  STORE_TOK = 'TO_RE';
+  STRING_CONCAT_TOK = 'CONCAT';
+  STRING_LENGTH_TOK = 'LENGTH';
+  STRING_CONTAINS_TOK = 'CONTAINS';
+  STRING_SUBSTR_TOK = 'SUBSTR';
+  STRING_CHARAT_TOK = 'CHARAT';
+  STRING_INDEXOF_TOK = 'INDEXOF';
+  STRING_REPLACE_TOK = 'REPLACE';
+  STRING_PREFIXOF_TOK = 'PREFIXOF';
+  STRING_SUFFIXOF_TOK = 'SUFFIXOF';
+  STRING_STOI_TOK = 'STRING_TO_INTEGER';
+  STRING_ITOS_TOK = 'INTEGER_TO_STRING';
+  STRING_U16TOS_TOK = 'UINT16_TO_STRING';
+  STRING_STOU16_TOK = 'STRING_TO_UINT16';
+  STRING_U32TOS_TOK = 'UINT32_TO_STRING';
+  STRING_STOU32_TOK = 'STRING_TO_UINT32';
+  //Regular expressions (TODO)
+  //STRING_IN_REGEXP_TOK
+  //STRING_TO_REGEXP_TOK
+  //REGEXP_CONCAT_TOK 
+  //REGEXP_UNION_TOK 
+  //REGEXP_INTER_TOK 
+  //REGEXP_STAR_TOK 
+  //REGEXP_PLUS_TOK 
+  //REGEXP_OPT_TOK 
+  //REGEXP_RANGE_TOK 
+  //REGEXP_LOOP_TOK 
+  //REGEXP_EMPTY_TOK
+  //REGEXP_SIGMA_TOK
+  
   
   FMF_CARD_TOK = 'HAS_CARD';
 
@@ -351,6 +370,7 @@ Kind getOperatorKind(int type, bool& negate) {
   case CONCAT_TOK: return kind::BITVECTOR_CONCAT;
   case BAR: return kind::BITVECTOR_OR;
   case BVAND_TOK: return kind::BITVECTOR_AND;
+  
   }
 
   std::stringstream ss;
@@ -1662,7 +1682,6 @@ postfixTerm[CVC4::Expr& f]
           f = MK_EXPR(CVC4::kind::SELECT, f, f2);
         }
       }
-
       /* left- or right-shift */
     | ( LEFTSHIFT_TOK { left = true; }
       | RIGHTSHIFT_TOK { left = false; } ) k=numeral
@@ -1888,7 +1907,6 @@ bvTerm[CVC4::Expr& f]
     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
   | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
-
   | stringTerm[f]
   ;
 
@@ -1900,27 +1918,35 @@ stringTerm[CVC4::Expr& f]
   std::vector<Expr> args;
 }
     /* String prefix operators */
-  : SCONCAT_TOK LPAREN formula[f] { args.push_back(f); }
+  : STRING_CONCAT_TOK LPAREN formula[f] { args.push_back(f); }
     ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_CONCAT, args); }
-  | SCONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+  | STRING_LENGTH_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_LENGTH, f); }
+  | STRING_CONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STRCTN, f, f2); }
-  | SSUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+  | STRING_SUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_SUBSTR, f, f2, f3); }
-  | SINDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+  | STRING_INDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STRIDOF, f, f2, f3); }
-  | SREPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
+  | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STRREPL, f, f2, f3); }
-  | SPREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+  | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_PREFIX, f, f2); }
-  | SSUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+  | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_SUFFIX, f, f2); }
-  | STOINTEGER_TOK LPAREN formula[f] RPAREN
+  | STRING_STOI_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_STOI, f); }
-  | STOSTRING_TOK LPAREN formula[f] RPAREN
+  | STRING_ITOS_TOK LPAREN formula[f] RPAREN
     { f = MK_EXPR(CVC4::kind::STRING_ITOS, f); }
-  | STORE_TOK LPAREN formula[f] RPAREN
-    { f = MK_EXPR(CVC4::kind::STRING_TO_REGEXP, f); }
+  | STRING_U16TOS_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_U16TOS, f); }
+  | STRING_STOU16_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STOU16, f); }
+  | STRING_U32TOS_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_U32TOS, f); }
+  | STRING_STOU32_TOK LPAREN formula[f] RPAREN
+    { f = MK_EXPR(CVC4::kind::STRING_STOU32, f); }    
 
     /* string literal */
   | str[s]
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 833565c9e..cb8cd8dca 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file congruence_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Dejan Jovanovic, Morgan Deters
+ **   Tim King, Dejan Jovanovic, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -15,27 +15,14 @@
  ** \todo document this file
  **/
 
-/*! \file congruence_manager.cpp
- ** \verbatim
- ** Original author: Tim King
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
 #include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
+#include "theory/quantifiers/equality_infer.h"
+#include "options/arith_options.h"
 
 namespace CVC4 {
 namespace theory {
@@ -45,6 +32,8 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
   : d_inConflict(c),
     d_raiseConflict(raiseConflict),
     d_notify(*this),
+    d_eq_infer(NULL),
+    d_eqi_counter(0,c),
     d_keepAlive(c),
     d_propagatations(c),
     d_explanationMap(c),
@@ -52,7 +41,19 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
     d_setupLiteral(setup),
     d_avariables(avars),
     d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
-{}
+{
+  //module to infer additional equalities based on normalization
+  if( options::sNormInferEq() ){
+    d_eq_infer = new quantifiers::EqualityInference(c, true);
+    d_true = NodeManager::currentNM()->mkConst( true );
+  }
+}
+
+ArithCongruenceManager::~ArithCongruenceManager() {
+  if( d_eq_infer ){
+    delete d_eq_infer;
+  }
+}
 
 ArithCongruenceManager::Statistics::Statistics():
   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
@@ -115,10 +116,12 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TN
   }
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) {
+  d_acm.eqNotifyNewClass(t);
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPreMerge(TNode t1, TNode t2) {
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyPostMerge(TNode t1, TNode t2) {
+  d_acm.eqNotifyPostMerge(t1,t2);
 }
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 }
@@ -314,9 +317,9 @@ bool ArithCongruenceManager::propagate(TNode x){
     c->setEqualityEngineProof();
   }else if(c->hasProof() && x != rewritten){
     if(c->assertedToTheTheory()){
-      pushBack(x, rewritten, c->getWitness());
+      pushBack(x);
     }else{
-      pushBack(x, rewritten);
+      pushBack(x);
     }
   }else{
     Assert(c->hasProof() && x == rewritten);
@@ -356,8 +359,24 @@ Node ArithCongruenceManager::explainInternal(TNode internal){
     return conjunction;
   }
 }
+
+void ArithCongruenceManager::eqNotifyNewClass(TNode t) {
+  if( d_eq_infer ){
+    d_eq_infer->eqNotifyNewClass(t);
+    fixpointInfer();
+  }
+}
+void ArithCongruenceManager::eqNotifyPostMerge(TNode t1, TNode t2) {
+  if( d_eq_infer ){
+    d_eq_infer->eqNotifyMerge(t1, t2);
+    fixpointInfer();
+  }
+}
+
 Node ArithCongruenceManager::explain(TNode external){
+  Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
   Node internal = externalToInternal(external);
+  Trace("arith-ee") << "...internal = " << internal << std::endl;
   return explainInternal(internal);
 }
 
@@ -393,6 +412,7 @@ void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar
   TNode eq = d_watchedEqualities[s];
   Assert(eq.getKind() == kind::EQUAL);
 
+  Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl;
   if(isEquality){
     d_ee.assertEquality(eq, true, reason);
   }else{
@@ -418,6 +438,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){
   Node reason = c->externalExplainByAssertions();
   d_keepAlive.push_back(reason);
 
+  Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl;
   d_ee.assertEquality(eq, true, reason);
 }
 
@@ -441,7 +462,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
   d_keepAlive.push_back(eq);
   d_keepAlive.push_back(reason);
 
-
+  Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl;
   d_ee.assertEquality(eq, true, reason);
 }
 
@@ -449,6 +470,55 @@ void ArithCongruenceManager::addSharedTerm(Node x){
   d_ee.addTriggerTerm(x, THEORY_ARITH);
 }
 
+bool ArithCongruenceManager::fixpointInfer() {
+  if( d_eq_infer ){
+    while(! inConflict() && d_eqi_counter.get()<d_eq_infer->getNumPendingMerges() ) {
+      Trace("snorm-infer-eq-debug") << "Processing " << d_eqi_counter.get() << " / " << d_eq_infer->getNumPendingMerges() << std::endl;
+      Node eq = d_eq_infer->getPendingMerge( d_eqi_counter.get() );
+      Trace("snorm-infer-eq") << "ArithCongruenceManager : Infer by normalization : " << eq << std::endl;
+      if( !d_ee.areEqual( eq[0], eq[1] ) ){
+        Node eq_exp = d_eq_infer->getPendingMergeExplanation( d_eqi_counter.get() );
+        Trace("snorm-infer-eq") << "           explanation : " << eq_exp << std::endl;
+        //regress explanation
+        std::vector<TNode> assumptions;
+        if( eq_exp.getKind()==kind::AND ){
+          for( unsigned i=0; i<eq_exp.getNumChildren(); i++ ){
+            explain( eq_exp[i], assumptions );
+          }
+        }else if( eq_exp.getKind()==kind::EQUAL ){
+          explain( eq_exp, assumptions );
+        }else{
+          //eq_exp should be true
+          Assert( eq_exp==d_true );
+        }
+        Node req_exp;
+        if( assumptions.empty() ){
+          req_exp = d_true;
+        }else{
+          std::set<TNode> assumptionSet;
+          assumptionSet.insert(assumptions.begin(), assumptions.end());
+          if( assumptionSet.size()==1 ){
+            req_exp = assumptions[0];
+          }else{
+            NodeBuilder<> conjunction(kind::AND);
+            enqueueIntoNB(assumptionSet, conjunction);
+            req_exp = conjunction;
+          }
+        }
+        Trace("snorm-infer-eq") << " regressed explanation : " << req_exp << std::endl;
+        d_ee.assertEquality( eq, true, req_exp );
+        d_keepAlive.push_back( req_exp );
+      }else{
+        Trace("snorm-infer-eq") << "...already equal." << std::endl;
+      }
+      d_eqi_counter = d_eqi_counter.get() + 1;
+    }
+  }
+  return inConflict();
+}
+
+
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 32e683509..a02f36a0f 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,7 +2,7 @@
 /*! \file congruence_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Dejan Jovanovic
+ **   Tim King, Morgan Deters, Dejan Jovanovic, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -33,6 +33,11 @@
 
 namespace CVC4 {
 namespace theory {
+
+namespace quantifiers {
+class EqualityInference;
+}
+
 namespace arith {
 
 class ArithCongruenceManager {
@@ -69,6 +74,11 @@ private:
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
   };
   ArithCongruenceNotify d_notify;
+  
+  /** module for shostak normalization, d_eqi_counter is how many pending merges in d_eq_infer we have processed */
+  quantifiers::EqualityInference * d_eq_infer;
+  context::CDO< unsigned > d_eqi_counter;
+  Node d_true;
 
   context::CDList<Node> d_keepAlive;
 
@@ -127,9 +137,12 @@ private:
 
   Node explainInternal(TNode internal);
 
+  void eqNotifyNewClass(TNode t);
+  void eqNotifyPostMerge(TNode t1, TNode t2);
 public:
 
   ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
+  ~ArithCongruenceManager();
 
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
@@ -160,6 +173,8 @@ public:
 
   void addSharedTerm(Node x);
 
+  /** process inferred equalities based on Shostak normalization */
+  bool fixpointInfer();
 private:
   class Statistics {
   public:
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index e304fb794..eae993545 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -239,7 +239,7 @@ class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -262,7 +262,7 @@ public:
          throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -280,7 +280,7 @@ public:
          }
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -298,7 +298,7 @@ public:
        }
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -312,7 +312,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -326,7 +326,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -340,7 +340,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -373,7 +373,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting standard ASCII characters in regexp range, or please set the option strings-std-ascii to be false");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -409,7 +409,7 @@ public:
         //}
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -426,7 +426,7 @@ public:
       //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
       //}
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -456,7 +456,7 @@ public:
     throw (TypeCheckingExceptionPrivate, AssertionException) {
 
     Assert(n.getKind() == kind::REGEXP_EMPTY);
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -466,7 +466,7 @@ public:
     throw (TypeCheckingExceptionPrivate, AssertionException) {
 
     Assert(n.getKind() == kind::REGEXP_SIGMA);
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };
 
@@ -480,7 +480,7 @@ public:
         throw TypeCheckingExceptionPrivate(n, "expecting an integer term in RV");
       }
     }
-    return nodeManager->regexpType();
+    return nodeManager->regExpType();
   }
 };