From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 8 Apr 2022 20:38:52 +0000 (-0500)
Subject: Properly parse numerals as real when integers are disabled (#8591)
X-Git-Tag: cvc5-1.0.1~283
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80959b3c2c4ace7a7a06b996418776b554e3f184;p=cvc5.git

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 d40f5d94c..edde6489e 100644
--- 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 d9ab184f3..3ad63d20b 100644
--- 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 48345f835..febbae176 100644
--- 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