From: Gereon Kremer Date: Mon, 24 Jan 2022 19:58:56 +0000 (-0800) Subject: Use proper RAN nodes for nl model (#7939) X-Git-Tag: cvc5-1.0.0~514 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a077d2781380c485cf5586a0107c8c943185a79b;p=cvc5.git 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 0fe045a61..d9fe7db47 100644 --- 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& 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()); - 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& model) +std::optional isExpressionZero(Env& env, + Node expr, + const std::map& model) { // Substitute constants and rewrite expr = env.getRewriter()->rewrite(expr); @@ -63,7 +19,6 @@ bool isExpressionZero(Env& env, Node expr, const std::map& model) { return expr.getConst().isZero(); } - std::map rans; std::vector nodes; std::vector repls; for (const auto& [node, repl] : model) @@ -74,10 +29,6 @@ bool isExpressionZero(Env& env, Node expr, const std::map& 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& model) { return expr.getConst().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 cc50c670c..efc143df7 100644 --- 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 + #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& model); - +std::optional isExpressionZero(Env& env, + Node expr, + const std::map& 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 ebe76e018..4a636ac60 100644 --- 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 899bbfe0e..61dbe4fce 100644 --- 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 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 ff496a334..4b3bdd067 100644 --- 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 915122140..217d12cd3 100644 --- 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 16f24ac0d..5348fb239 100644 --- 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)