Represent (a subset of) real numbers as algebraic numbers

This representation is used by Z3 for it covers a subset of irrational
numbers in addition to rational numbers.

Author: tautschnig

regression/cbmc/real-irrational1/test.desc

@@ -1,11 +1,8 @@
-KNOWNBUG
+CORE smt-backend broken-cprover-smt-backend no-new-smt
 main.c
 --trace --smt2
+^  a=x ∈ ℝ\.\(x\^2 \+ -2 = 0\)
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
-This currently fails an invariant in parse_literal, but really requires
-adjusting the implementation of realt to be coefficients of a polynomial. We can
-then parse, e.g., (root-obj (+ (^ x 2) (- 2)) 1), which Z3 returns as part of
-the model.

src/solvers/smt2/smt2_conv.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2_conv.h"
 
+#include <util/algebraic_number.h>
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
@@ -31,7 +32,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/range.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
-#include <util/real.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
@@ -447,10 +447,11 @@ constant_exprt smt2_convt::parse_literal(
         }
         else if(type.id() == ID_real)
         {
-          mp_integer first = string2integer(s.substr(0, pos));
-          mp_integer second = string2integer(s.substr(pos, std::string::npos));
-          realt real{first, second};
-          return real.as_expr();
+          rationalt rational_value;
+          bool failed = to_rational(
+            constant_exprt{src.id(), rational_typet{}}, rational_value);
+          CHECK_RETURN(!failed);
+          return algebraic_numbert{rational_value}.as_expr();
         }
         else
         {
@@ -538,6 +539,37 @@ constant_exprt smt2_convt::parse_literal(
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
     return ieee_float_valuet::NaN(ieee_float_spect(s - 1, e)).to_expr();
   }
+  else if(
+    src.get_sub().size() == 3 &&
+    src.get_sub()[0].id() == "root-obj") // (root-obj (+ ...) 1)
+  {
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      src.get_sub()[1].id().empty() && src.get_sub()[1].get_sub().size() == 3 &&
+        src.get_sub()[1].get_sub()[0].id() == "+" &&
+        src.get_sub()[2].id() == "1",
+      "unexpected root-obj expression",
+      src.pretty());
+    irept sum_rhs = src.get_sub()[1].get_sub()[2];
+    rationalt constant_coeff;
+    bool failed =
+      to_rational(parse_literal(sum_rhs, rational_typet{}), constant_coeff);
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      !failed, "failed to parse rational constant coefficient", src.pretty());
+    irept sum_lhs = src.get_sub()[1].get_sub()[1];
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      sum_lhs.id().empty() && sum_lhs.get_sub().size() == 3 &&
+        sum_lhs.get_sub()[0].id() == "^" && sum_lhs.get_sub()[1].id() == "x",
+      "unexpected first operand to root-obj",
+      src.pretty());
+    std::size_t degree = unsafe_string2size_t(sum_lhs.get_sub()[2].id_string());
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      degree > 0, "polynomial degree must be positive", src.pretty());
+    std::vector<rationalt> coefficients{degree + 1, rationalt{}};
+    coefficients.front() = constant_coeff;
+    coefficients.back() = rationalt{1};
+    algebraic_numbert a{coefficients};
+    return a.as_expr();
+  }
 
   if(type.id()==ID_signedbv ||
      type.id()==ID_unsignedbv ||

src/util/Makefile

@@ -1,4 +1,6 @@
-SRC = arith_tools.cpp \
+SRC = \
+      algebraic_number.cpp \
+      arith_tools.cpp \
       array_element_from_pointer.cpp \
       array_name.cpp \
       bitvector_expr.cpp \
@@ -66,7 +68,6 @@ SRC = arith_tools.cpp \
       prefix_filter.cpp \
       rational.cpp \
       rational_tools.cpp \
-      real.cpp \
       ref_expr_set.cpp \
       refined_string_type.cpp \
       rename.cpp \

src/util/algebraic_number.cpp

@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+Module: Algebraic Numbers
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Algebraic numbers
+
+#include "algebraic_number.h"
+
+#include "mathematical_types.h"
+#include "rational_tools.h"
+
+constant_exprt algebraic_numbert::as_expr() const
+{
+  if(coefficients.size() == 2 && coefficients.back().is_one())
+  {
+    // root of x - c
+    auto c = from_rational(-coefficients.front());
+    c.type() = real_typet{};
+    return c;
+  }
+  else
+  {
+    std::ostringstream oss;
+    oss << *this;
+    return constant_exprt{oss.str(), real_typet{}};
+  }
+}
+
+std::ostream &operator<<(std::ostream &out, const algebraic_numbert &a)
+{
+  out << "x ∈ ℝ.(";
+
+  const auto &coefficients = a.get_coefficients();
+
+  bool need_plus = false;
+  for(std::size_t d = coefficients.size(); d > 0; --d)
+  {
+    if(coefficients[d - 1].is_zero())
+      continue;
+    if(need_plus)
+      out << " + ";
+    if(d == 1)
+      out << coefficients[d - 1];
+    else
+    {
+      if(!coefficients[d - 1].is_one())
+        out << coefficients[d - 1] << "*";
+      out << "x^" << d - 1;
+    }
+    need_plus = true;
+  }
+
+  if(!need_plus)
+    out << "0";
+  out << " = 0)";
+
+  return out;
+}

src/util/algebraic_number.h

@@ -0,0 +1,55 @@
+/*******************************************************************\
+
+Module: Algebraic numbers
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_ALGEBRAIC_NUMBER_H
+#define CPROVER_UTIL_ALGEBRAIC_NUMBER_H
+
+#include "rational.h"
+#include "std_expr.h"
+
+/// Represents real numbers as roots (zeros) of a polynomial with rational
+/// coefficients. Cannot represent transcendental numbers.
+class algebraic_numbert
+{
+protected:
+  // the i-th entry is the coefficient of degree i
+  using coefficientst = std::vector<rationalt>;
+  coefficientst coefficients;
+
+public:
+  /// Represent a real number as roots of a polynomial with rational
+  /// coefficients \p coeff.
+  explicit algebraic_numbert(const std::vector<rationalt> &coeff)
+    : coefficients(coeff)
+  {
+    DATA_INVARIANT(coefficients.size() >= 2, "minimum degree is 1");
+  }
+
+  /// The default constructor builds a `algebraic_numbert` representing real
+  /// number 0.
+  algebraic_numbert() : algebraic_numbert({rationalt{0}, rationalt{1}})
+  {
+  }
+
+  /// Represent a rational number as `algebraic_numbert`.
+  explicit algebraic_numbert(const rationalt &r)
+    : algebraic_numbert({-r, rationalt{1}})
+  {
+  }
+
+  constant_exprt as_expr() const;
+
+  const coefficientst &get_coefficients() const
+  {
+    return coefficients;
+  }
+};
+
+std::ostream &operator<<(std::ostream &out, const algebraic_numbert &a);
+
+#endif // CPROVER_UTIL_ALGEBRAIC_NUMBER_H