Merge branch 'master' into fixExportTofixExportTo

18 files changed, 848 insertions, 94 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 714d67f5d..488590deb 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -769,7 +769,6 @@ bool Sort::isSortConstructor() const
   return d_type->isSortConstructor();
 }
 
-#if 0
 Datatype Sort::getDatatype() const
 {
   // CHECK: is this a datatype sort?
@@ -791,7 +790,6 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   Assert (d_type->isSortConstructor());
   return static_cast<SortConstructorType*>(d_type.get())->instantiate(tparams);
 }
-#endif
 
 std::string Sort::toString() const
 {
@@ -1209,6 +1207,286 @@ std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
+/* DatatypeSelector --------------------------------------------------------- */
+
+DatatypeSelector::DatatypeSelector()
+{
+  d_stor = nullptr;
+}
+
+DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor)
+    : d_stor(new CVC4::DatatypeConstructorArg(stor))
+{
+}
+
+DatatypeSelector::~DatatypeSelector()
+{
+}
+
+std::string DatatypeSelector::toString() const
+{
+  std::stringstream ss;
+  ss << *d_stor;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
+{
+  out << stor.toString();
+  return out;
+}
+
+/* DatatypeConstructor ------------------------------------------------------ */
+
+DatatypeConstructor::DatatypeConstructor()
+{
+  d_ctor = nullptr;
+}
+
+DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
+: d_ctor(new CVC4::DatatypeConstructor(ctor))
+{
+}
+
+DatatypeConstructor::~DatatypeConstructor()
+{
+}
+
+DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
+{
+  // CHECK: selector with name exists?
+  // CHECK: is resolved?
+  return (*d_ctor)[name];
+}
+
+DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_ctor)[name];
+}
+
+Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return d_ctor->getSelector(name);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
+{
+  return DatatypeConstructor::const_iterator(*d_ctor, true);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::end() const
+{
+  return DatatypeConstructor::const_iterator(*d_ctor, false);
+}
+
+DatatypeConstructor::const_iterator::const_iterator(
+    const CVC4::DatatypeConstructor& ctor, bool begin)
+{
+  d_int_stors = ctor.getArgs();
+  const std::vector<CVC4::DatatypeConstructorArg>* sels =
+      static_cast<const std::vector<CVC4::DatatypeConstructorArg>*>(
+          d_int_stors);
+  for (const auto& s : *sels)
+  {
+    /* Can not use emplace_back here since constructor is private. */
+    d_stors.push_back(DatatypeSelector(s));
+  }
+  d_idx = begin ? 0 : sels->size();
+}
+
+DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
+operator=(const DatatypeConstructor::const_iterator& it)
+{
+  d_int_stors = it.d_int_stors;
+  d_stors = it.d_stors;
+  d_idx = it.d_idx;
+  return *this;
+}
+
+const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const
+{
+  return d_stors[d_idx];
+}
+
+const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const
+{
+  return &d_stors[d_idx];
+}
+
+DatatypeConstructor::const_iterator& DatatypeConstructor::const_iterator::
+operator++()
+{
+  ++d_idx;
+  return *this;
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::const_iterator::
+operator++(int)
+{
+  DatatypeConstructor::const_iterator it(*this);
+  ++d_idx;
+  return it;
+}
+
+bool DatatypeConstructor::const_iterator::operator==(
+    const DatatypeConstructor::const_iterator& other) const
+{
+  return d_int_stors == other.d_int_stors && d_idx == other.d_idx;
+}
+
+bool DatatypeConstructor::const_iterator::operator!=(
+    const DatatypeConstructor::const_iterator& other) const
+{
+  return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
+}
+
+std::string DatatypeConstructor::toString() const
+{
+  std::stringstream ss;
+  ss << *d_ctor;
+  return ss.str();
+}
+
+std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
+{
+  out << ctor.toString();
+  return out;
+}
+
+/* Datatype ----------------------------------------------------------------- */
+
+Datatype::Datatype(const CVC4::Datatype& dtype)
+: d_dtype(new CVC4::Datatype(dtype))
+{
+}
+
+Datatype::~Datatype()
+{
+}
+
+DatatypeConstructor Datatype::operator[](const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_dtype)[name];
+}
+
+DatatypeConstructor Datatype::getConstructor(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return (*d_dtype)[name];
+}
+
+Term Datatype::getConstructorTerm(const std::string& name) const
+{
+  // CHECK: cons with name exists?
+  // CHECK: is resolved?
+  return d_dtype->getConstructor(name);
+}
+
+Datatype::const_iterator Datatype::begin() const
+{
+  return Datatype::const_iterator(*d_dtype, true);
+}
+
+Datatype::const_iterator Datatype::end() const
+{
+  return Datatype::const_iterator(*d_dtype, false);
+}
+
+Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype, bool begin)
+{
+  d_int_ctors = dtype.getConstructors();
+  const std::vector<CVC4::DatatypeConstructor>* cons =
+    static_cast<const std::vector<CVC4::DatatypeConstructor>*>(d_int_ctors);
+  for (const auto& c : *cons)
+  {
+    /* Can not use emplace_back here since constructor is private. */
+    d_ctors.push_back(DatatypeConstructor(c));
+  }
+  d_idx = begin ? 0 : cons->size();
+}
+
+Datatype::const_iterator& Datatype::const_iterator::operator=(
+    const Datatype::const_iterator& it)
+{
+  d_int_ctors = it.d_int_ctors;
+  d_ctors = it.d_ctors;
+  d_idx = it.d_idx;
+  return *this;
+}
+
+const DatatypeConstructor& Datatype::const_iterator::operator*() const
+{
+  return d_ctors[d_idx];
+}
+
+const DatatypeConstructor* Datatype::const_iterator::operator->() const
+{
+  return &d_ctors[d_idx];
+}
+
+Datatype::const_iterator& Datatype::const_iterator::operator++()
+{
+  ++d_idx;
+  return *this;
+}
+
+Datatype::const_iterator Datatype::const_iterator::operator++(int)
+{
+  Datatype::const_iterator it(*this);
+  ++d_idx;
+  return it;
+}
+
+bool Datatype::const_iterator::operator==(
+    const Datatype::const_iterator& other) const
+{
+  return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx;
+}
+
+bool Datatype::const_iterator::operator!=(
+    const Datatype::const_iterator& other) const
+{
+  return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
+}
+
+/* -------------------------------------------------------------------------- */
+/* Rounding Mode for Floating Points                                          */
+/* -------------------------------------------------------------------------- */
+
+const static std::unordered_map<RoundingMode,
+                          CVC4::RoundingMode,
+                          RoundingModeHashFunction> s_rmodes
+{
+  { ROUND_NEAREST_TIES_TO_EVEN,  CVC4::RoundingMode::roundNearestTiesToEven },
+  { ROUND_TOWARD_POSITIVE,       CVC4::RoundingMode::roundTowardPositive },
+  { ROUND_TOWARD_NEGATIVE,       CVC4::RoundingMode::roundTowardNegative },
+  { ROUND_TOWARD_ZERO,           CVC4::RoundingMode::roundTowardZero },
+  { ROUND_NEAREST_TIES_TO_AWAY,  CVC4::RoundingMode::roundNearestTiesToAway },
+};
+
+const static std::unordered_map<CVC4::RoundingMode,
+                          RoundingMode,
+                          CVC4::RoundingModeHashFunction> s_rmodes_internal
+{
+  { CVC4::RoundingMode::roundNearestTiesToEven,  ROUND_NEAREST_TIES_TO_EVEN },
+  { CVC4::RoundingMode::roundTowardPositive,     ROUND_TOWARD_POSITIVE },
+  { CVC4::RoundingMode::roundTowardNegative,     ROUND_TOWARD_NEGATIVE },
+  { CVC4::RoundingMode::roundTowardZero,         ROUND_TOWARD_ZERO },
+  { CVC4::RoundingMode::roundNearestTiesToAway,  ROUND_NEAREST_TIES_TO_AWAY },
+};
+
+size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
+{
+  return size_t(rm);
+}
+
 /* -------------------------------------------------------------------------- */
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
@@ -1363,7 +1641,355 @@ std::vector<Type> Solver::sortVectorToTypes(
   return res;
 }
 
-/* Create terms ------------------------------------------------------- */
+/* Create consts                                                              */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkTrue(void) const { return d_exprMgr->mkConst<bool>(true); }
+
+Term Solver::mkFalse(void) const { return d_exprMgr->mkConst<bool>(false); }
+
+Term Solver::mkBoolean(bool val) const { return d_exprMgr->mkConst<bool>(val); }
+
+Term Solver::mkInteger(const char* s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(Rational(s, base));
+}
+
+Term Solver::mkInteger(const std::string& s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(Rational(s, base));
+}
+
+Term Solver::mkInteger(int32_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkInteger(uint32_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkInteger(int64_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkInteger(uint64_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkPi() const
+{
+  return d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
+}
+
+Term Solver::mkReal(const char* s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(Rational(s, base));
+}
+
+Term Solver::mkReal(const std::string& s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(Rational(s, base));
+}
+
+Term Solver::mkReal(int32_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkReal(int64_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkReal(uint32_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkReal(uint64_t val) const
+{
+  return d_exprMgr->mkConst(Rational(val));
+}
+
+Term Solver::mkReal(int32_t num, int32_t den) const
+{
+  return d_exprMgr->mkConst(Rational(num, den));
+}
+
+Term Solver::mkReal(int64_t num, int64_t den) const
+{
+  return d_exprMgr->mkConst(Rational(num, den));
+}
+
+Term Solver::mkReal(uint32_t num, uint32_t den) const
+{
+  return d_exprMgr->mkConst(Rational(num, den));
+}
+
+Term Solver::mkReal(uint64_t num, uint64_t den) const
+{
+  return d_exprMgr->mkConst(Rational(num, den));
+}
+
+Term Solver::mkRegexpEmpty() const
+{
+  return d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<Expr>());
+}
+
+Term Solver::mkRegexpSigma() const
+{
+  return d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<Expr>());
+}
+
+Term Solver::mkEmptySet(Sort s) const
+{
+  return d_exprMgr->mkConst(EmptySet(*s.d_type));
+}
+
+Term Solver::mkSepNil(Sort sort) const
+{
+  return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
+}
+
+Term Solver::mkString(const char* s) const
+{
+  return d_exprMgr->mkConst(String(s));
+}
+
+Term Solver::mkString(const std::string& s) const
+{
+  return d_exprMgr->mkConst(String(s));
+}
+
+Term Solver::mkString(const unsigned char c) const
+{
+  return d_exprMgr->mkConst(String(c));
+}
+
+Term Solver::mkString(const std::vector<unsigned>& s) const
+{
+  return d_exprMgr->mkConst(String(s));
+}
+
+Term Solver::mkUniverseSet(Sort sort) const
+{
+  return d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
+}
+
+Term Solver::mkBitVector(uint32_t size) const
+{
+  return d_exprMgr->mkConst(BitVector(size));
+}
+
+Term Solver::mkBitVector(uint32_t size, uint32_t val) const
+{
+  return d_exprMgr->mkConst(BitVector(size, val));
+}
+
+Term Solver::mkBitVector(uint32_t size, uint64_t val) const
+{
+  return d_exprMgr->mkConst(BitVector(size, val));
+}
+
+Term Solver::mkBitVector(const char* s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(BitVector(s, base));
+}
+
+Term Solver::mkBitVector(std::string& s, uint32_t base) const
+{
+  return d_exprMgr->mkConst(BitVector(s, base));
+}
+
+Term Solver::mkConst(RoundingMode rm) const
+{
+  // CHECK: kind == CONST_ROUNDINGMODE
+  // CHECK: valid rm?
+  return d_exprMgr->mkConst(s_rmodes.at(rm));
+}
+
+Term Solver::mkConst(Kind kind, Sort arg) const
+{
+  // CHECK: kind == EMPTYSET
+  return d_exprMgr->mkConst(CVC4::EmptySet(*arg.d_type));
+}
+
+Term Solver::mkConst(Kind kind, Sort arg1, int32_t arg2) const
+{
+  // CHECK: kind == UNINTERPRETED_CONSTANT
+  return d_exprMgr->mkConst(CVC4::UninterpretedConstant(*arg1.d_type, arg2));
+}
+
+Term Solver::mkConst(Kind kind, bool arg) const
+{
+  // CHECK: kind == CONST_BOOLEAN
+  return d_exprMgr->mkConst<bool>(arg);
+}
+
+Term Solver::mkConst(Kind kind, const char* arg) const
+{
+  // CHECK: kind == CONST_STRING
+  return d_exprMgr->mkConst(CVC4::String(arg));
+}
+
+Term Solver::mkConst(Kind kind, const std::string& arg) const
+{
+  // CHECK: kind == CONST_STRING
+  return d_exprMgr->mkConst(CVC4::String(arg));
+}
+
+Term Solver::mkConst(Kind kind, const char* arg1, uint32_t arg2) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  //           || kind == CONST_BITVECTOR
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
+  }
+  if (kind == CONST_RATIONAL)
+  {
+    return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  }
+  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, const std::string& arg1, uint32_t arg2) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  //           || kind == CONST_BITVECTOR
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg1, arg2)));
+  }
+  if (kind == CONST_RATIONAL)
+  {
+    return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+  }
+  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, uint32_t arg) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  //           || kind == CONST_BITVECTOR
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
+  }
+  if (kind == CONST_RATIONAL)
+  {
+    return d_exprMgr->mkConst(CVC4::Rational(arg));
+  }
+  return d_exprMgr->mkConst(CVC4::BitVector(arg));
+}
+
+Term Solver::mkConst(Kind kind, int32_t arg) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
+  }
+  return d_exprMgr->mkConst(CVC4::Rational(arg));
+}
+
+Term Solver::mkConst(Kind kind, int64_t arg) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
+  }
+  return d_exprMgr->mkConst(CVC4::Rational(arg));
+}
+
+Term Solver::mkConst(Kind kind, uint64_t arg) const
+{
+  // CHECK: kind == ABSTRACT_VALUE
+  //           || kind == CONST_RATIONAL
+  if (kind == ABSTRACT_VALUE)
+  {
+    return d_exprMgr->mkConst(CVC4::AbstractValue(Integer(arg)));
+  }
+  return d_exprMgr->mkConst(CVC4::Rational(arg));
+}
+
+Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const
+{
+  // CHECK: kind == CONST_RATIONAL
+  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, int32_t arg1, int32_t arg2) const
+{
+  // CHECK: kind == CONST_RATIONAL
+  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, int64_t arg1, int64_t arg2) const
+{
+  // CHECK: kind == CONST_RATIONAL
+  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const
+{
+  // CHECK: kind == CONST_RATIONAL
+  return d_exprMgr->mkConst(CVC4::Rational(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const
+{
+  // CHECK: kind == CONST_BITVECTOR
+  return d_exprMgr->mkConst(CVC4::BitVector(arg1, arg2));
+}
+
+Term Solver::mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const
+{
+  // CHECK: kind == CONST_FLOATINGPOINT
+  // CHECK: arg 3 is bit-vector constant
+  return d_exprMgr->mkConst(
+      CVC4::FloatingPoint(arg1, arg2, arg3.d_expr->getConst<BitVector>()));
+}
+
+/* Create variables                                                           */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkVar(const std::string& symbol, Sort sort) const
+{
+  // CHECK: sort exists?
+  return d_exprMgr->mkVar(symbol, *sort.d_type);
+}
+
+Term Solver::mkVar(Sort sort) const
+{
+  // CHECK: sort exists?
+  return d_exprMgr->mkVar(*sort.d_type);
+}
+
+Term Solver::mkBoundVar(const std::string& symbol, Sort sort) const
+{
+  // CHECK: sort exists?
+  return d_exprMgr->mkBoundVar(symbol, *sort.d_type);
+}
+
+Term Solver::mkBoundVar(Sort sort) const
+{
+  // CHECK: sort exists?
+  return d_exprMgr->mkBoundVar(*sort.d_type);
+}
+
+/* Create terms                                                               */
+/* -------------------------------------------------------------------------- */
 
 Term Solver::mkTerm(Kind kind) const
 {
@@ -1586,5 +2212,6 @@ std::vector<Expr> Solver::termVectorToExprs(
   }
   return res;
 }
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 9b33b314c..8747c530e 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -695,6 +695,11 @@ bool Datatype::involvesUninterpretedType() const{
   return d_involvesUt;
 }
 
+const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
+{
+  return &d_constructors;
+}
+
 void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
                                   const std::map<std::string, DatatypeType>& resolutions,
                                   const std::vector<Type>& placeholders,
@@ -834,6 +839,12 @@ void DatatypeConstructor::setSygus(Expr op,
   d_sygus_pc = spc;
 }
 
+const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
+    const
+{
+  return &d_args;
+}
+
 void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
   // We don't want to introduce a new data member, because eventually
   // we're going to be a constant stuffed inside a node.  So we stow
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index a56a4f993..c2cf80158 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -450,6 +450,11 @@ class CVC4_PUBLIC DatatypeConstructor {
    */
   void setSygus(Expr op, std::shared_ptr<SygusPrintCallback> spc);
 
+  /**
+   * Get the list of arguments to this constructor.
+   */
+  const std::vector<DatatypeConstructorArg>* getArgs() const;
+
  private:
   /** the name of the constructor */
   std::string d_name;
@@ -938,6 +943,11 @@ public:
    */
   bool involvesUninterpretedType() const;
 
+  /**
+   * Get the list of constructors.
+   */
+  const std::vector<DatatypeConstructor>* getConstructors() const;
+
  private:
   /** name of this datatype */
   std::string d_name;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4b8c52841..b52be77bb 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -353,8 +353,17 @@ command [std::unique_ptr<CVC4::Command>* cmd]
                                       "be declared in logic ");
       }
       // we allow overloading for function declarations
-      Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
-      cmd->reset(new DeclareFunctionCommand(name, func, t));
+      if (PARSER_STATE->sygus())
+      {
+        // it is a higher-order universal variable
+        PARSER_STATE->mkSygusVar(name, t);
+        cmd->reset(new EmptyCommand());
+      }
+      else
+      {
+        Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+        cmd->reset(new DeclareFunctionCommand(name, func, t));
+      }
     }
   | /* function definition */
     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 33ac69c63..257ee1171 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -625,10 +625,12 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
   d_sygusVars.push_back(e);
   d_sygusVarPrimed[e] = false;
   if( isPrimed ){
+    d_sygusInvVars.push_back(e);
     std::stringstream ss;
     ss << name << "'";
     Expr ep = mkBoundVar(ss.str(), type);
     d_sygusVars.push_back(ep);
+    d_sygusInvVars.push_back(ep);
     d_sygusVarPrimed[ep] = true;
   }
   return e;
@@ -1228,15 +1230,14 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
 }
 
 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
-  for( unsigned i=0; i<d_sygusVars.size(); i++ ){
-    Expr v = d_sygusVars[i];
+  for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++)
+  {
+    Expr v = d_sygusInvVars[i];
     std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
     if( it!=d_sygusVarPrimed.end() ){
       if( it->second==isPrimed ){
         vars.push_back( v );
       }
-    }else{
-      //should never happen
     }
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 85d9b112e..c9b224d39 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -64,7 +64,8 @@ private:
   std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // for sygus
-  std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
+  std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints,
+      d_sygusFunSymbols;
   std::map< Expr, bool > d_sygusVarPrimed;
 
 protected:
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index d7672f1b4..016198735 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -161,10 +161,14 @@ void CnfProof::setCnfDependence(Node from, Node to) {
 }
 
 void CnfProof::pushCurrentAssertion(Node assertion) {
-  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
-                     << assertion  << std::endl;
+  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
+                     << std::endl;
 
   d_currentAssertionStack.push_back(assertion);
+
+  Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
+                     << "new stack size = " << d_currentAssertionStack.size()
+                     << std::endl;
 }
 
 void CnfProof::popCurrentAssertion() {
@@ -174,6 +178,10 @@ void CnfProof::popCurrentAssertion() {
                      << d_currentAssertionStack.back() << std::endl;
 
   d_currentAssertionStack.pop_back();
+
+  Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
+                     << "new stack size = " << d_currentAssertionStack.size()
+                     << std::endl;
 }
 
 Node CnfProof::getCurrentAssertion() {
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 99a347744..32833d9a1 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -127,6 +127,11 @@ public:
   void popCurrentDefinition();
   Node getCurrentDefinition();
 
+  /**
+   * Checks whether the assertion stack is empty.
+   */
+  bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
+
   void setProofRecipe(LemmaProofRecipe* proofRecipe);
   LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
   bool haveProofRecipe(const std::set<Node> &lemma);
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d8ab811bc..f2205e2ed 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -332,6 +332,9 @@ void ProofManager::traceUnsatCore() {
   d_satProof->collectClausesUsed(used_inputs,
                                  used_lemmas);
 
+  // At this point, there should be no assertions without a clause id
+  Assert(d_cnfProof->isAssertionStackEmpty());
+
   IdToSatClause::const_iterator it = used_inputs.begin();
   for(; it != used_inputs.end(); ++it) {
     Node node = d_cnfProof->getAssertionForClause(it->first);
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 68050d93c..82e7cb7b2 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -565,6 +565,9 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
 
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
+                          "input (UNIT CLAUSE): "
+                       << lit << std::endl;
       d_inputClauses.insert(newId);
     }
     if (kind == THEORY_LEMMA) {
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8f5b37e74..c312ac146 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -236,33 +236,34 @@ void Solver::resizeVars(int newSize) {
 }
 
 CRef Solver::reason(Var x) {
+  Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl;
 
-    // If we already have a reason, just return it
-    if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
+  // If we already have a reason, just return it
+  if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
 
-    // What's the literal we are trying to explain
-    Lit l = mkLit(x, value(x) != l_True);
+  // What's the literal we are trying to explain
+  Lit l = mkLit(x, value(x) != l_True);
 
-    // Get the explanation from the theory
-    SatClause explanation_cl;
-    // FIXME: at some point return a tag with the theory that spawned you
-    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
-                              explanation_cl);
-    vec<Lit> explanation;
-    MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+  // Get the explanation from the theory
+  SatClause explanation_cl;
+  // FIXME: at some point return a tag with the theory that spawned you
+  proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+  vec<Lit> explanation;
+  MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
-    Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
+  Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl
+                   << std::endl;
 
-    // Sort the literals by trail index level
-    lemma_lt lt(*this);
-    sort(explanation, lt);
-    Assert(explanation[0] == l);
+  // Sort the literals by trail index level
+  lemma_lt lt(*this);
+  sort(explanation, lt);
+  Assert(explanation[0] == l);
 
-    // Compute the assertion level for this clause
-    int explLevel = 0;
-    if (assertionLevelOnly())
-    {
-      explLevel = assertionLevel;
+  // Compute the assertion level for this clause
+  int explLevel = 0;
+  if (assertionLevelOnly())
+  {
+    explLevel = assertionLevel;
     }
     else
     {
@@ -321,10 +322,15 @@ CRef Solver::reason(Var x) {
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
     Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
-    PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
-           ProofManager::getCnfProof()->registerConvertedClause(id, true);
-           // no need to pop current assertion as this is not converted to cnf
-           );
+    PROOF(ClauseId id = ProofManager::getSatProof()->registerClause(
+              real_reason, THEORY_LEMMA);
+          ProofManager::getCnfProof()->registerConvertedClause(id, true);
+          // explainPropagation() pushes the explanation on the assertion stack
+          // in CnfProof, so we need to pop it here. This is important because
+          // reason() may be called indirectly while adding a clause, which can
+          // lead to a wrong assertion being associated with the clause being
+          // added (see issue #2137).
+          ProofManager::getCnfProof()->popCurrentAssertion(););
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -1021,6 +1027,9 @@ void Solver::propagateTheory() {
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
         ClauseId id; // FIXME: mark it as explanation here somehow?
         addClause(explanation, true, id);
+        // explainPropagation() pushes the explanation on the assertion
+        // stack in CnfProof, so we need to pop it here.
+        PROOF(ProofManager::getCnfProof()->popCurrentAssertion();)
       }
     }
   }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bfd7a5509..e3b48a4da 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2226,35 +2226,53 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >&
 
 void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
   // Compute terms appearing in assertions and shared terms
-  computeRelevantTerms(termSet);
-  
+  std::set<Kind> irr_kinds;
+  // testers are not relevant for model construction
+  irr_kinds.insert(APPLY_TESTER);
+  computeRelevantTerms(termSet, irr_kinds);
+
+  Trace("dt-cmi") << "Have " << termSet.size() << " relevant terms..."
+                  << std::endl;
+
   //also include non-singleton equivalence classes  TODO : revisit this
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
   while( !eqcs_i.isFinished() ){
     TNode r = (*eqcs_i);
     bool addedFirst = false;
     Node first;
-    eq::EqClassIterator eqc_i = eq::EqClassIterator( r, &d_equalityEngine );
-    while( !eqc_i.isFinished() ){
-      TNode n = (*eqc_i);
-      if( first.isNull() ){
-        first = n;
-        //always include all datatypes
-        if( n.getType().isDatatype() ){
-          addedFirst = true;
-          termSet.insert( n );
+    TypeNode rtn = r.getType();
+    if (!rtn.isBoolean())
+    {
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, &d_equalityEngine);
+      while (!eqc_i.isFinished())
+      {
+        TNode n = (*eqc_i);
+        if (first.isNull())
+        {
+          first = n;
+          // always include all datatypes
+          if (rtn.isDatatype())
+          {
+            addedFirst = true;
+            termSet.insert(n);
+          }
         }
-      }else{
-        if( !addedFirst ){
-          addedFirst = true;
-          termSet.insert( first );
+        else
+        {
+          if (!addedFirst)
+          {
+            addedFirst = true;
+            termSet.insert(first);
+          }
+          termSet.insert(n);
         }
-        termSet.insert( n );
+        ++eqc_i;
       }
-      ++eqc_i;
     }
     ++eqcs_i;
   }
+  Trace("dt-cmi") << "After adding non-singletons, has " << termSet.size()
+                  << " relevant terms..." << std::endl;
 }
 
 std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index f4cdc22c5..8a415cc10 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -106,36 +106,6 @@ void SygusGrammarNorm::TypeObject::buildDatatype(SygusGrammarNorm* sygus_norm,
                 sygus_norm->d_sygus_vars.toExpr(),
                 dt.getSygusAllowConst(),
                 dt.getSygusAllowAll());
-  if (dt.getSygusAllowConst())
-  {
-    TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
-    // must be handled by counterexample-guided instantiation
-    // don't do it for Boolean (not worth the trouble, since it has only
-    // minimal gain (1 any constant vs 2 constructors for true/false), and
-    // we need to do a lot of special symmetry breaking, e.g. for ensuring
-    // any constant constructors are not the 1st children of ITEs.
-    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
-        && !sygus_type.isBoolean())
-    {
-      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
-      // add an "any constant" proxy variable
-      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
-      // mark that it represents any constant
-      SygusAnyConstAttribute saca;
-      av.setAttribute(saca, true);
-      std::stringstream ss;
-      ss << d_unres_tn << "_any_constant";
-      std::string cname(ss.str());
-      std::vector<Type> builtin_arg;
-      builtin_arg.push_back(dt.getSygusType());
-      // we add this constructor first since we use left associative chains
-      // and our symmetry breaking should group any constants together
-      // beneath the same application
-      // we set its weight to zero since it should be considered at the
-      // same level as constants.
-      d_dt.addSygusConstructor(av.toExpr(), cname, builtin_arg, nullptr, 0);
-    }
-  }
   for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
   {
     d_dt.addSygusConstructor(d_ops[i].toExpr(),
@@ -462,6 +432,41 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
     Assert(op_pos[i] < dt.getNumConstructors());
     to.addConsInfo(this, dt[op_pos[i]]);
   }
+  if (dt.getSygusAllowConst())
+  {
+    TypeNode sygus_type = TypeNode::fromType(dt.getSygusType());
+    // must be handled by counterexample-guided instantiation
+    // don't do it for Boolean (not worth the trouble, since it has only
+    // minimal gain (1 any constant vs 2 constructors for true/false), and
+    // we need to do a lot of special symmetry breaking, e.g. for ensuring
+    // any constant constructors are not the 1st children of ITEs.
+    if (CegInstantiator::isCbqiSort(sygus_type) >= CEG_HANDLED
+        && !sygus_type.isBoolean())
+    {
+      Trace("sygus-grammar-normalize") << "...add any constant constructor.\n";
+      // add an "any constant" proxy variable
+      Node av = NodeManager::currentNM()->mkSkolem("_any_constant", sygus_type);
+      // mark that it represents any constant
+      SygusAnyConstAttribute saca;
+      av.setAttribute(saca, true);
+      std::stringstream ss;
+      ss << to.d_unres_tn << "_any_constant";
+      std::string cname(ss.str());
+      std::vector<Type> builtin_arg;
+      builtin_arg.push_back(dt.getSygusType());
+      // we add this constructor first since we use left associative chains
+      // and our symmetry breaking should group any constants together
+      // beneath the same application
+      // we set its weight to zero since it should be considered at the
+      // same level as constants.
+      to.d_ops.insert(to.d_ops.begin(), av.toExpr());
+      to.d_cons_names.insert(to.d_cons_names.begin(), cname);
+      to.d_cons_args_t.insert(to.d_cons_args_t.begin(), builtin_arg);
+      to.d_pc.insert(to.d_pc.begin(),
+                     printer::SygusEmptyPrintCallback::getEmptyPC());
+      to.d_weight.insert(to.d_weight.begin(), 0);
+    }
+  }
   /* Build normalize datatype */
   if (Trace.isOn("sygus-grammar-normalize"))
   {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 10504b487..311776693 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -232,17 +232,24 @@ std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() cons
   return currentlyShared;
 }
 
-
-void Theory::collectTerms(TNode n, set<Node>& termSet) const
+void Theory::collectTerms(TNode n,
+                          set<Kind>& irrKinds,
+                          set<Node>& termSet) const
 {
   if (termSet.find(n) != termSet.end()) {
     return;
   }
-  Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
-  termSet.insert(n);
-  if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
+  Kind nk = n.getKind();
+  if (irrKinds.find(nk) == irrKinds.end())
+  {
+    Trace("theory::collectTerms")
+        << "Theory::collectTerms: adding " << n << endl;
+    termSet.insert(n);
+  }
+  if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
+  {
     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-      collectTerms(*child_it, termSet);
+      collectTerms(*child_it, irrKinds, termSet);
     }
   }
 }
@@ -250,18 +257,29 @@ void Theory::collectTerms(TNode n, set<Node>& termSet) const
 
 void Theory::computeRelevantTerms(set<Node>& termSet, bool includeShared) const
 {
+  set<Kind> irrKinds;
+  computeRelevantTerms(termSet, irrKinds, includeShared);
+}
+
+void Theory::computeRelevantTerms(set<Node>& termSet,
+                                  set<Kind>& irrKinds,
+                                  bool includeShared) const
+{
   // Collect all terms appearing in assertions
+  irrKinds.insert(kind::EQUAL);
+  irrKinds.insert(kind::NOT);
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
   for (; assert_it != assert_it_end; ++assert_it) {
-    collectTerms(*assert_it, termSet);
+    collectTerms(*assert_it, irrKinds, termSet);
   }
 
   if (!includeShared) return;
 
   // Add terms that are shared terms
+  set<Kind> kempty;
   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
   for (; shared_it != shared_it_end; ++shared_it) {
-    collectTerms(*shared_it, termSet);
+    collectTerms(*shared_it, kempty, termSet);
   }
 }
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3721806ad..2c3c727cb 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -161,14 +161,27 @@ private:
   /**
    * Helper function for computeRelevantTerms
    */
-  void collectTerms(TNode n, std::set<Node>& termSet) const;
+  void collectTerms(TNode n,
+                    std::set<Kind>& irrKinds,
+                    std::set<Node>& termSet) const;
 
   /**
    * Scans the current set of assertions and shared terms top-down
    * until a theory-leaf is reached, and adds all terms found to
    * termSet.  This is used by collectModelInfo to delimit the set of
-   * terms that should be used when constructing a model
+   * terms that should be used when constructing a model.
+   *
+   * irrKinds: The kinds of terms that appear in assertions that should *not*
+   * be included in termSet. Note that the kinds EQUAL and NOT are always
+   * treated as irrelevant kinds.
+   *
+   * includeShared: Whether to include shared terms in termSet. Notice that
+   * shared terms are not influenced by irrKinds.
    */
+  void computeRelevantTerms(std::set<Node>& termSet,
+                            std::set<Kind>& irrKinds,
+                            bool includeShared = true) const;
+  /** same as above, but with empty irrKinds */
   void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const;
 
   /**
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 3c02ea13c..377e91897 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -580,6 +580,7 @@ REG0_TESTS = \
 	regress0/push-pop/inc-double-u.smt2 \
 	regress0/push-pop/incremental-subst-bug.cvc \
 	regress0/push-pop/issue1986.smt2 \
+	regress0/push-pop/issue2137.min.smt2 \
 	regress0/push-pop/quant-fun-proc-unfd.smt2 \
 	regress0/push-pop/simple_unsat_cores.smt2 \
 	regress0/push-pop/test.00.cvc \
diff --git a/test/regress/regress0/push-pop/issue2137.min.smt2 b/test/regress/regress0/push-pop/issue2137.min.smt2
new file mode 100644
index 000000000..372e8f1f3
--- /dev/null
+++ b/test/regress/regress0/push-pop/issue2137.min.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Real)
+(declare-fun b () Bool)
+(assert (< 0 a))
+(assert (xor b (< 0 a 0) false))
+(check-sat)
+(assert (not b))
+(check-sat)
diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p
index 922a6cfc3..f30db563a 100644
--- a/test/regress/regress0/tptp/DAT001=1.p
+++ b/test/regress/regress0/tptp/DAT001=1.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --no-finite-model-find
 %------------------------------------------------------------------------------
 % File     : DAT001=1 : TPTP v5.5.0. Released v5.0.0.
 % Domain   : Data Structures