Properly parse numerals as real when integers are disabled (#8591)

SMT-LIB says numerals are real when integers are not included in the logic.

Due to subtyping, we don't complain internally, although if subtyping is eliminated, this fix is necessary.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d40f5d94c98313458267de2c7b2eb3a8f2eae537..edde6489ef5a8733b57b02bc16f7a1cc40e1c9aa 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1704,7 +1704,7 @@ termAtomic[cvc5::Term& atomTerm]
   : INTEGER_LITERAL
     {
       std::string intStr = AntlrInput::tokenText($INTEGER_LITERAL);
-      atomTerm = SOLVER->mkInteger(intStr);
+      atomTerm = PARSER_STATE->mkRealOrIntFromNumeral(intStr);
     }
   | DECIMAL_LITERAL
     {

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d9ab184f3709b45b8fef7c68662222cb813e2417..3ad63d20b922a15244ed0477794b9a64e0f9c639 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -839,6 +839,17 @@ bool Smt2::isAbstractValue(const std::string& name)
          && name.find_first_not_of("0123456789", 1) == std::string::npos;
 }
 
+cvc5::Term Smt2::mkRealOrIntFromNumeral(const std::string& str)
+{
+  // if arithmetic is enabled, and integers are disabled
+  if (d_logic.isTheoryEnabled(internal::theory::THEORY_ARITH)
+      && !d_logic.areIntegersUsed())
+  {
+    return d_solver->mkReal(str);
+  }
+  return d_solver->mkInteger(str);
+}
+
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, cvc5::Sort type)
 {
   Trace("parser") << "parseOpApplyTypeAscription : " << p << " " << type

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 48345f8357cd0677af1e250c3c6044fb43bed992..febbae176838e1e1d7d3caa78880ba88607292b5 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -292,12 +292,13 @@ class Smt2 : public Parser
   /** Does name denote an abstract value? (of the form '@n' for numeral n). */
   bool isAbstractValue(const std::string& name);
 
-  /** Make abstract value
+  /**
+   * Make real or int from numeral string.
    *
-   * Abstract values are used for processing get-value calls. The argument
-   * name should be such that isUninterpretedSortValue(name) is true.
+   * In particular, if arithmetic is enabled, but integers are disabled, then
+   * we construct a real. Otherwise, we construct an integer.
    */
-  cvc5::Term mkUninterpretedSortValue(const std::string& name);
+  cvc5::Term mkRealOrIntFromNumeral(const std::string& str);
 
   /**
    * Smt2 parser provides its own checkDeclaration, which does the