Use proper RAN nodes for nl model (#7939)

This PR finally uses proper RealAlgebraicNumber (wrapped in nodes) to represent nonlinear model values. This simplifies the implementation of getEqualityStatus, and should make theory combination much more robust.
Also, we reintroduce the possibility to have getEqualityStatus return unknown, though this should only happen in the presence of witness terms.

diff --git a/src/theory/arith/arith_evaluator.cpp b/src/theory/arith/arith_evaluator.cpp
index 0fe045a61d02b943195d8b180f3fc61bb1015cad..d9fe7db470ba9c935473d87976eede430d6c9087 100644 (file)
--- a/src/theory/arith/arith_evaluator.cpp
+++ b/src/theory/arith/arith_evaluator.cpp
@@ -9,53 +9,9 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-namespace {
-
-RealAlgebraicNumber evaluate(TNode expr,
-                             const std::map<Node, RealAlgebraicNumber>& rans)
-{
-  switch (expr.getKind())
-  {
-    case Kind::PLUS:
-    {
-      RealAlgebraicNumber aggr;
-      for (const auto& n : expr)
-      {
-        aggr += evaluate(n, rans);
-      }
-      return aggr;
-    }
-    case Kind::MULT:
-    case Kind::NONLINEAR_MULT:
-    {
-      RealAlgebraicNumber aggr(Integer(1));
-      for (const auto& n : expr)
-      {
-        aggr *= evaluate(n, rans);
-      }
-      return aggr;
-    }
-    case Kind::MINUS:
-      Assert(expr.getNumChildren() == 2);
-      return evaluate(expr[0], rans) - evaluate(expr[1], rans);
-    case Kind::UMINUS: return -evaluate(expr[0], rans);
-    case Kind::CONST_RATIONAL:
-      return RealAlgebraicNumber(expr.getConst<Rational>());
-    default:
-      auto it = rans.find(expr);
-      if (it != rans.end())
-      {
-        return it->second;
-      }
-      Assert(false) << "Unsupported expression kind for RAN evaluation: "
-                    << expr.getKind();
-      return RealAlgebraicNumber();
-  }
-}
-
-}  // namespace
-
-bool isExpressionZero(Env& env, Node expr, const std::map<Node, Node>& model)
+std::optional<bool> isExpressionZero(Env& env,
+                                     Node expr,
+                                     const std::map<Node, Node>& model)
 {
   // Substitute constants and rewrite
   expr = env.getRewriter()->rewrite(expr);
@@ -63,7 +19,6 @@ bool isExpressionZero(Env& env, Node expr, const std::map<Node, Node>& model)
   {
     return expr.getConst<Rational>().isZero();
   }
-  std::map<Node, RealAlgebraicNumber> rans;
   std::vector<TNode> nodes;
   std::vector<TNode> repls;
   for (const auto& [node, repl] : model)
@@ -74,10 +29,6 @@ bool isExpressionZero(Env& env, Node expr, const std::map<Node, Node>& model)
       nodes.emplace_back(node);
       repls.emplace_back(repl);
     }
-    else
-    {
-      rans.emplace(node, nl::node_to_ran(repl, node));
-    }
   }
   expr =
       expr.substitute(nodes.begin(), nodes.end(), repls.begin(), repls.end());
@@ -86,7 +37,8 @@ bool isExpressionZero(Env& env, Node expr, const std::map<Node, Node>& model)
   {
     return expr.getConst<Rational>().isZero();
   }
-  return isZero(evaluate(expr, rans));
+  Assert(expr.getKind() != Kind::REAL_ALGEBRAIC_NUMBER);
+  return std::nullopt;
 }
 
 }  // namespace arith

diff --git a/src/theory/arith/arith_evaluator.h b/src/theory/arith/arith_evaluator.h
index cc50c670cd7cfbb5c429c1160a4aee216f61deb8..efc143df7b0cd89cd965b7af5fdc6deac695a1eb 100644 (file)
--- a/src/theory/arith/arith_evaluator.h
+++ b/src/theory/arith/arith_evaluator.h
@@ -4,6 +4,8 @@
 #ifndef CVC5__THEORY__ARITH__ARITH_EVALUATOR_H
 #define CVC5__THEORY__ARITH__ARITH_EVALUATOR_H
 
+#include <optional>
+
 #include "expr/node.h"
 #include "smt/env.h"
 
@@ -15,11 +17,16 @@ namespace arith {
  * Check if the expression `expr` is zero over the given model.
  * The model may contain real algebraic numbers in standard witness form.
  * The environment is used for rewriting.
+ *
+ * The result is true or false, if the expression could be evaluated. If it
+ * could not, possibly in the presence of a transcendental model, the result is
+ * std::nullopt.
  */
-bool isExpressionZero(Env& env, Node expr, const std::map<Node, Node>& model);
-
+std::optional<bool> isExpressionZero(Env& env,
+                                     Node expr,
+                                     const std::map<Node, Node>& model);
 }
 }  // namespace theory
 }  // namespace cvc5
 
-#endif
\ No newline at end of file
+#endif

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index ebe76e0180150c2508f743b8c1abccb24691c8b1..4a636ac60ef2dc64e055e693f292d3546adf551f 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -402,11 +402,12 @@ Node value_to_node(const poly::Value& v, const Node& ran_variable)
   Assert(!is_none(v)) << "Can not convert none.";
   Assert(!is_plus_infinity(v)) << "Can not convert plus infinity.";
 
+  auto* nm = NodeManager::currentNM();
   if (is_algebraic_number(v))
   {
-    return ran_to_node(as_algebraic_number(v), ran_variable);
+    auto ran = as_algebraic_number(v);
+    return nm->mkRealAlgebraicNumber(RealAlgebraicNumber(std::move(ran)));
   }
-  auto* nm = NodeManager::currentNM();
   if (is_dyadic_rational(v))
   {
     return nm->mkConst(CONST_RATIONAL,

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 899bbfe0ee014fc71d5b662f29530bcab3468188..61dbe4fce08c0d9d0fb823321c3baabb1dbf37ac 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -343,11 +343,12 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
     return d_internal->getEqualityStatus(a,b);
   }
   Node diff = d_env.getNodeManager()->mkNode(Kind::MINUS, a, b);
-  if (isExpressionZero(d_env, diff, d_arithModelCache))
+  std::optional<bool> isZero = isExpressionZero(d_env, diff, d_arithModelCache);
+  if (isZero)
   {
-    return EQUALITY_TRUE_IN_MODEL;
+    return *isZero ? EQUALITY_TRUE_IN_MODEL : EQUALITY_FALSE_IN_MODEL;
   }
-  return EQUALITY_FALSE_IN_MODEL;
+  return EQUALITY_UNKNOWN;
 }
 
 Node TheoryArith::getModelValue(TNode var) {

diff --git a/test/regress/regress0/nl/issue3652.smt2 b/test/regress/regress0/nl/issue3652.smt2
index ff496a334a12293f0061a795c625ab278ad0a612..4b3bdd067203ea8e326c154d41238937f308ae5d 100644 (file)
--- a/test/regress/regress0/nl/issue3652.smt2
+++ b/test/regress/regress0/nl/issue3652.smt2
@@ -1,7 +1,6 @@
 ;COMMAND-LINE: --check-models
 ;REQUIRES: poly
-;EXIT: 1
-;EXPECT: (error "Cannot run check-model on a model with approximate values.")
+;EXPECT: sat
 (set-logic QF_NRA)
 (declare-fun a () Real)
 (assert (= (* a a) 2))

diff --git a/test/regress/regress0/nl/sqrt2-value.smt2 b/test/regress/regress0/nl/sqrt2-value.smt2
index 915122140252c653127d8e6c622d03040f1d9ae5..217d12cd3412a27073c510d52e56fe569c8957f1 100644 (file)
--- a/test/regress/regress0/nl/sqrt2-value.smt2
+++ b/test/regress/regress0/nl/sqrt2-value.smt2
@@ -1,8 +1,8 @@
-; SCRUBBER: sed -e 's/witness.*/witness/'
+; SCRUBBER: sed -e 's/(_ real_algebraic_number.*/(_ real_algebraic_number/'
 ; COMMAND-LINE: --no-check-models
 ; REQUIRES: poly
 ; EXPECT: sat
-; EXPECT: ((x (witness
+; EXPECT: ((x (_ real_algebraic_number
 (set-option :produce-models true)
 (set-logic QF_NRA)
 (declare-fun x () Real)

diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
index 16f24ac0d6a9ea05471f5e3beb44f478295f4362..5348fb239e57a913f3a653d50827f5ecd24eaed1 100644 (file)
--- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
+++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -1,8 +1,8 @@
-; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (.*/SUCCESS/'
+; SCRUBBER: sed -e 's/((x (_ real_algebraic_number .*/((x (_ real_algebraic_number/'
 ; COMMAND-LINE: --produce-models --model-witness-value --no-check-models
 ; REQUIRES: poly
 ; EXPECT: sat
-; EXPECT: SUCCESS
+; EXPECT: ((x (_ real_algebraic_number
 (set-logic QF_NRA)
 (set-info :status sat)
 (declare-fun x () Real)