API/Smt2 parser: refactor termAtomic (#2674)

2 files changed, 269 insertions, 15 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index c0818f54f..dbbb4b535 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1461,6 +1461,14 @@ DatatypeConstructor::DatatypeConstructor(const CVC4::DatatypeConstructor& ctor)
 
 DatatypeConstructor::~DatatypeConstructor() {}
 
+bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); }
+
+Term DatatypeConstructor::getConstructorTerm() const
+{
+  CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor.";
+  return Term(d_ctor->getConstructor());
+}
+
 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
 {
   // CHECK: selector with name exists?
@@ -1583,6 +1591,13 @@ Datatype::Datatype(const CVC4::Datatype& dtype)
 
 Datatype::~Datatype() {}
 
+DatatypeConstructor Datatype::operator[](size_t idx) const
+{
+  // CHECK (maybe): is resolved?
+  CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
+  return (*d_dtype)[idx];
+}
+
 DatatypeConstructor Datatype::operator[](const std::string& name) const
 {
   // CHECK: cons with name exists?
@@ -1735,6 +1750,8 @@ Solver::~Solver() {}
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
+Sort Solver::getNullSort(void) const { return Type(); }
+
 Sort Solver::getBooleanSort(void) const { return d_exprMgr->booleanType(); }
 
 Sort Solver::getIntegerSort(void) const { return d_exprMgr->integerType(); }
@@ -2051,14 +2068,14 @@ Term Solver::mkSepNil(Sort sort) const
   }
 }
 
-Term Solver::mkString(const char* s) const
+Term Solver::mkString(const char* s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
+  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
-Term Solver::mkString(const std::string& s) const
+Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
+  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const unsigned char c) const
@@ -2078,7 +2095,8 @@ Term Solver::mkUniverseSet(Sort sort) const
     CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
     Term res =
         d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
-    (void)res.d_expr->getType(true); /* kick off type checking */
+    // TODO(#2771): Reenable?
+    // (void)res.d_expr->getType(true); /* kick off type checking */
     return res;
   }
   catch (TypeCheckingException& e)
@@ -2105,7 +2123,8 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
   try
   {
     CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
-    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 16, s) << "base 2 or 16";
+    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+        << "base 2, 10, or 16";
     return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
   }
   catch (std::invalid_argument& e)
@@ -2114,6 +2133,28 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
   }
 }
 
+Term Solver::mkBVFromStrHelper(uint32_t size,
+                               std::string s,
+                               uint32_t base) const
+{
+  try
+  {
+    CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
+    CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, s)
+        << "base 2, 10, or 16";
+
+    Integer val(s, base);
+    CVC4_API_CHECK(val.modByPow2(size) == val)
+        << "Overflow in bitvector construction (specified bitvector size "
+        << size << " too small to hold value " << s << ")";
+    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+  }
+  catch (std::invalid_argument& e)
+  {
+    throw CVC4ApiException(e.what());
+  }
+}
+
 Term Solver::mkBitVector(const char* s, uint32_t base) const
 {
   CVC4_API_ARG_CHECK_NOT_NULL(s);
@@ -2125,6 +2166,57 @@ Term Solver::mkBitVector(const std::string& s, uint32_t base) const
   return mkBVFromStrHelper(s, base);
 }
 
+Term Solver::mkBitVector(uint32_t size, const char* s, uint32_t base) const
+{
+  CVC4_API_ARG_CHECK_NOT_NULL(s);
+  return mkBVFromStrHelper(size, s, base);
+}
+
+Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
+{
+  return mkBVFromStrHelper(size, s, base);
+}
+
+Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
+{
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
+  return mkConstHelper<CVC4::FloatingPoint>(
+      FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
+}
+
+Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
+{
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
+  return mkConstHelper<CVC4::FloatingPoint>(
+      FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
+}
+
+Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
+{
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
+  return mkConstHelper<CVC4::FloatingPoint>(
+      FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
+}
+
+Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
+{
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
+  return mkConstHelper<CVC4::FloatingPoint>(
+      FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
+}
+
+Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
+{
+  CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
+      << "Expected CVC4 to be compiled with SymFPU support";
+  return mkConstHelper<CVC4::FloatingPoint>(
+      FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
+}
+
 Term Solver::mkConst(RoundingMode rm) const
 {
   try
@@ -2655,6 +2747,23 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector<Term>& children) const
   }
 }
 
+Term Solver::mkTuple(const std::vector<Sort>& sorts,
+                     const std::vector<Term>& terms) const
+{
+  CVC4_API_CHECK(sorts.size() == terms.size())
+      << "Expected the same number of sorts and elements";
+  std::vector<Term> args;
+  for (size_t i = 0, size = sorts.size(); i < size; i++)
+  {
+    args.push_back(ensureTermSort(terms[i], sorts[i]));
+  }
+
+  Sort s = mkTupleSort(sorts);
+  Datatype dt = s.getDatatype();
+  args.insert(args.begin(), dt[0].getConstructorTerm());
+  return mkTerm(APPLY_CONSTRUCTOR, args);
+}
+
 std::vector<Expr> Solver::termVectorToExprs(
     const std::vector<Term>& terms) const
 {
@@ -3359,6 +3468,31 @@ void Solver::setOption(const std::string& option,
   d_smtEngine->setOption(option, value);
 }
 
+Term Solver::ensureTermSort(const Term& t, const Sort& s) const
+{
+  CVC4_API_CHECK(t.getSort() == s || (t.getSort().isInteger() && s.isReal()))
+      << "Expected conversion from Int to Real";
+
+  if (t.getSort() == s)
+  {
+    return t;
+  }
+
+  // Integers are reals, too
+  Assert(t.getSort().isReal());
+  Term res = t;
+  if (t.getSort().isInteger())
+  {
+    // Must cast to Real to ensure correct type is passed to parametric type
+    // constructors. We do this cast using division with 1. This has the
+    // advantage wrt using TO_REAL since (constant) division is always included
+    // in the theory.
+    res = mkTerm(DIVISION, *t.d_expr, mkReal(1));
+  }
+  Assert(res.getSort() == s);
+  return res;
+}
+
 /**
  * !!! This is only temporarily available until the parser is fully migrated to
  * the new API. !!!
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 1f74a34a9..ef82a9174 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1135,7 +1135,7 @@ class CVC4_PUBLIC DatatypeConstructor
   /**
    * Constructor.
    * @param ctor the internal datatype constructor to be wrapped
-   * @return thte DatatypeConstructor
+   * @return the DatatypeConstructor
    */
   DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
 
@@ -1145,6 +1145,17 @@ class CVC4_PUBLIC DatatypeConstructor
   ~DatatypeConstructor();
 
   /**
+   * @return true if this datatype constructor has been resolved.
+   */
+  bool isResolved() const;
+
+  /**
+   * Get the constructor operator of this datatype constructor.
+   * @return the constructor operator
+   */
+  Term getConstructorTerm() const;
+
+  /**
    * Get the datatype selector with the given name.
    * This is a linear search through the selectors, so in case of
    * multiple, similarly-named selectors, the first is returned.
@@ -1286,6 +1297,13 @@ class CVC4_PUBLIC Datatype
   ~Datatype();
 
   /**
+   * Get the datatype constructor at a given index.
+   * @param idx the index of the datatype constructor to return
+   * @return the datatype constructor with the given index
+   */
+  DatatypeConstructor operator[](size_t idx) const;
+
+  /**
    * Get the datatype constructor with the given name.
    * This is a linear search through the constructors, so in case of multiple,
    * similarly-named constructors, the first is returned.
@@ -1521,6 +1539,11 @@ class CVC4_PUBLIC Solver
   /* .................................................................... */
 
   /**
+   * @return sort null
+   */
+  Sort getNullSort() const;
+
+  /**
    * @return sort Boolean
    */
   Sort getBooleanSort() const;
@@ -1739,6 +1762,16 @@ class CVC4_PUBLIC Solver
    */
   Term mkTerm(OpTerm opTerm, const std::vector<Term>& children) const;
 
+  /**
+   * Create a tuple term. Terms are automatically converted if sorts are
+   * compatible.
+   * @param sorts The sorts of the elements in the tuple
+   * @param terms The elements in the tuple
+   * @return the tuple Term
+   */
+  Term mkTuple(const std::vector<Sort>& sorts,
+               const std::vector<Term>& terms) const;
+
   /* .................................................................... */
   /* Create Operator Terms                                                */
   /* .................................................................... */
@@ -1827,7 +1860,7 @@ class CVC4_PUBLIC Solver
   Term mkPi() const;
 
   /**
-   * Create a real constant.
+   * Create a real constant from a string.
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
    * @return a constant of sort Real or Integer (if 's' represents an integer)
@@ -1835,7 +1868,7 @@ class CVC4_PUBLIC Solver
   Term mkReal(const char* s) const;
 
   /**
-   * Create a real constant.
+   * Create a real constant from a string.
    * @param s the string representation of the constant, may represent an
    *          integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
    * @return a constant of sort Real or Integer (if 's' represents an integer)
@@ -1931,16 +1964,20 @@ class CVC4_PUBLIC Solver
   /**
    * Create a String constant.
    * @param s the string this constant represents
+   * @param useEscSequences determines whether escape sequences in \p s should
+   * be converted to the corresponding character
    * @return the String constant
    */
-  Term mkString(const char* s) const;
+  Term mkString(const char* s, bool useEscSequences = false) const;
 
   /**
    * Create a String constant.
    * @param s the string this constant represents
+   * @param useEscSequences determines whether escape sequences in \p s should
+   * be converted to the corresponding character
    * @return the String constant
    */
-  Term mkString(const std::string& s) const;
+  Term mkString(const std::string& s, bool useEscSequences = false) const;
 
   /**
    * Create a String constant.
@@ -1973,21 +2010,84 @@ class CVC4_PUBLIC Solver
 
   /**
    * Create a bit-vector constant from a given string.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
+   * @param s the string representation of the constant
+   * @param base the base of the string representation (2, 10, or 16)
    * @return the bit-vector constant
    */
   Term mkBitVector(const char* s, uint32_t base = 2) const;
 
   /**
    * Create a bit-vector constant from a given string.
-   * @param s the string represetntation of the constant
-   * @param base the base of the string representation
+   * @param s the string representation of the constant
+   * @param base the base of the string representation (2, 10, or 16)
    * @return the bit-vector constant
    */
   Term mkBitVector(const std::string& s, uint32_t base = 2) const;
 
   /**
+   * Create a bit-vector constant of a given bit-width from a given string.
+   * @param size the bit-width of the constant
+   * @param s the string representation of the constant
+   * @param base the base of the string representation (2, 10, or 16)
+   * @return the bit-vector constant
+   */
+  Term mkBitVector(uint32_t size, const char* s, uint32_t base) const;
+
+  /**
+   * Create a bit-vector constant of a given bit-width from a given string.
+   * @param size the bit-width of the constant
+   * @param s the string representation of the constant
+   * @param base the base of the string representation (2, 10, or 16)
+   * @return the bit-vector constant
+   */
+  Term mkBitVector(uint32_t size, std::string& s, uint32_t base) const;
+
+  /**
+   * Create a positive infinity floating-point constant. Requires CVC4 to be
+   * compiled with SymFPU support.
+   * @param exp Number of bits in the exponent
+   * @param sig Number of bits in the significand
+   * @return the floating-point constant
+   */
+  Term mkPosInf(uint32_t exp, uint32_t sig) const;
+
+  /**
+   * Create a negative infinity floating-point constant. Requires CVC4 to be
+   * compiled with SymFPU support.
+   * @param exp Number of bits in the exponent
+   * @param sig Number of bits in the significand
+   * @return the floating-point constant
+   */
+  Term mkNegInf(uint32_t exp, uint32_t sig) const;
+
+  /**
+   * Create a not-a-number (NaN) floating-point constant. Requires CVC4 to be
+   * compiled with SymFPU support.
+   * @param exp Number of bits in the exponent
+   * @param sig Number of bits in the significand
+   * @return the floating-point constant
+   */
+  Term mkNaN(uint32_t exp, uint32_t sig) const;
+
+  /**
+   * Create a positive zero (+0.0) floating-point constant. Requires CVC4 to be
+   * compiled with SymFPU support.
+   * @param exp Number of bits in the exponent
+   * @param sig Number of bits in the significand
+   * @return the floating-point constant
+   */
+  Term mkPosZero(uint32_t exp, uint32_t sig) const;
+
+  /**
+   * Create a negative zero (-0.0) floating-point constant. Requires CVC4 to be
+   * compiled with SymFPU support.
+   * @param exp Number of bits in the exponent
+   * @param sig Number of bits in the significand
+   * @return the floating-point constant
+   */
+  Term mkNegZero(uint32_t exp, uint32_t sig) const;
+
+  /**
    * Create constant of kind:
    *   - CONST_ROUNDINGMODE
    * @param rm the floating point rounding mode this constant represents
@@ -2507,6 +2607,15 @@ class CVC4_PUBLIC Solver
    */
   void setOption(const std::string& option, const std::string& value) const;
 
+  /**
+   * If needed, convert this term to a given sort. Note that the sort of the
+   * term must be convertible into the target sort. Currently only Int to Real
+   * conversions are supported.
+   * @param s the target sort
+   * @return the term wrapped into a sort conversion if needed
+   */
+  Term ensureTermSort(const Term& t, const Sort& s) const;
+
   // !!! This is only temporarily available until the parser is fully migrated
   // to the new API. !!!
   ExprManager* getExprManager(void) const;
@@ -2530,6 +2639,9 @@ class CVC4_PUBLIC Solver
   Term mkRealFromStrHelper(std::string s) const;
   /* Helper for mkBitVector functions that take a string as argument. */
   Term mkBVFromStrHelper(std::string s, uint32_t base) const;
+  /* Helper for mkBitVector functions that take a string and a size as
+   * arguments. */
+  Term mkBVFromStrHelper(uint32_t size, std::string s, uint32_t base) const;
   /* Helper for mkBitVector functions that take an integer as argument. */
   Term mkBVFromIntHelper(uint32_t size, uint64_t val) const;
   /* Helper for mkConst functions that take a string as argument. */
@@ -2539,6 +2651,14 @@ class CVC4_PUBLIC Solver
   template <typename T>
   Term mkConstFromIntHelper(Kind kind, T a) const;
 
+  /**
+   * Helper function that ensures that a given term is of sort real (as opposed
+   * to being of sort integer).
+   * @param term a term of sort integer or real
+   * @return a term of sort real
+   */
+  Term ensureRealSort(Term expr) const;
+
   /* The expression manager of this solver. */
   std::unique_ptr<ExprManager> d_exprMgr;
   /* The SMT engine of this solver. */