1 files changed, 33 insertions, 19 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b186c2b2a..19c3527f7 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,6 +135,11 @@ void Smt2::addDatatypesOperators()
   {
     Parser::addOperator(api::APPLY_UPDATER);
     addOperator(api::DT_SIZE, "dt.size");
+    // Notice that tuple operators, we use the generic APPLY_SELECTOR and
+    // APPLY_UPDATER kinds. These are processed based on the context
+    // in which they are parsed, e.g. when parsing identifiers.
+    addIndexedOperator(
+        api::APPLY_SELECTOR, api::APPLY_SELECTOR, "tuple_select");
     addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update");
   }
 }
@@ -258,14 +263,16 @@ void Smt2::addFloatingPointOperators() {
 }
 
 void Smt2::addSepOperators() {
+  defineVar("sep.emp", d_solver->mkSepEmp());
+  // the Boolean sort is a placeholder here since we don't have type info
+  // without type annotation
+  defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
   addOperator(api::SEP_STAR, "sep");
   addOperator(api::SEP_PTO, "pto");
   addOperator(api::SEP_WAND, "wand");
-  addOperator(api::SEP_EMP, "emp");
   Parser::addOperator(api::SEP_STAR);
   Parser::addOperator(api::SEP_PTO);
   Parser::addOperator(api::SEP_WAND);
-  Parser::addOperator(api::SEP_EMP);
 }
 
 void Smt2::addCoreSymbols()
@@ -288,7 +295,7 @@ void Smt2::addOperator(api::Kind kind, const std::string& name)
   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
                   << std::endl;
   Parser::addOperator(kind);
-  operatorKindMap[name] = kind;
+  d_operatorKindMap[name] = kind;
 }
 
 void Smt2::addIndexedOperator(api::Kind tKind,
@@ -302,11 +309,11 @@ void Smt2::addIndexedOperator(api::Kind tKind,
 api::Kind Smt2::getOperatorKind(const std::string& name) const
 {
   // precondition: isOperatorEnabled(name)
-  return operatorKindMap.find(name)->second;
+  return d_operatorKindMap.find(name)->second;
 }
 
 bool Smt2::isOperatorEnabled(const std::string& name) const {
-  return operatorKindMap.find(name) != operatorKindMap.end();
+  return d_operatorKindMap.find(name) != d_operatorKindMap.end();
 }
 
 bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
@@ -437,7 +444,7 @@ void Smt2::reset() {
   d_logicSet = false;
   d_seenSetLogic = false;
   d_logic = LogicInfo();
-  operatorKindMap.clear();
+  d_operatorKindMap.clear();
   d_lastNamedTerm = std::pair<api::Term, std::string>();
 }
 
@@ -509,7 +516,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
     {
       addOperator(api::CARDINALITY_CONSTRAINT, "fmf.card");
-      addOperator(api::CARDINALITY_VALUE, "fmf.card.val");
     }
   }
 
@@ -546,7 +552,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 
     if (d_logic.areTranscendentalsUsed())
     {
-      defineVar("real.pi", d_solver->mkTerm(api::PI));
+      defineVar("real.pi", d_solver->mkPi());
       addTranscendentalOperators();
     }
     if (!strictModeEnabled())
@@ -672,12 +678,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addFloatingPointOperators();
   }
 
-  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
-    // the Boolean sort is a placeholder here since we don't have type info
-    // without type annotation
-    defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
-    defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP));
-
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP))
+  {
     addSepOperators();
   }
 
@@ -953,6 +955,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     {
       // a builtin operator, convert to kind
       kind = getOperatorKind(p.d_name);
+      Debug("parser") << "Got builtin kind " << kind << " for name"
+                      << std::endl;
     }
     else
     {
@@ -1119,17 +1123,27 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
       return ret;
     }
-    if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
-    {
-      parseError(
-          "eqrange predicate requires option --arrays-exp to be enabled.");
-    }
     if (kind == api::SINGLETON && args.size() == 1)
     {
       api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
       Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
       return ret;
     }
+    else if (kind == api::CARDINALITY_CONSTRAINT)
+    {
+      if (args.size() != 2)
+      {
+        parseError("Incorrect arguments for cardinality constraint");
+      }
+      api::Sort sort = args[0].getSort();
+      if (!sort.isUninterpretedSort())
+      {
+        parseError("Expected uninterpreted sort for cardinality constraint");
+      }
+      uint64_t ubound = args[1].getUInt32Value();
+      api::Term ret = d_solver->mkCardinalityConstraint(sort, ubound);
+      return ret;
+    }
     api::Term ret = d_solver->mkTerm(kind, args);
     Debug("parser") << "applyParseOp: return default builtin " << ret
                     << std::endl;