From 72bf82dade6b72cea4cb8bf86d03a7f6b875b3a9 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Feb 2022 15:14:38 -0800 Subject: [PATCH] Improve theory combination over real algebraic models (#8045) Though we support real algebraic models now for theory combination, cvc5/cvc5-projects#451 uncovered the possibility to assert if an equality was in fact not equal during theory combination and the difference was real algebraic. This PR fixes this issue by adding the proper check. Fixes cvc5/cvc5-projects#451. --- src/theory/arith/arith_evaluator.cpp | 5 ++++- test/regress/CMakeLists.txt | 2 ++ .../regress0/nl/proj-issue-451-ran-combination-1.smt2 | 7 +++++++ .../regress0/nl/proj-issue-451-ran-combination-2.smt2 | 10 ++++++++++ 4 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 create mode 100644 test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 diff --git a/src/theory/arith/arith_evaluator.cpp b/src/theory/arith/arith_evaluator.cpp index d9fe7db47..155a6cdce 100644 --- a/src/theory/arith/arith_evaluator.cpp +++ b/src/theory/arith/arith_evaluator.cpp @@ -37,7 +37,10 @@ std::optional isExpressionZero(Env& env, { return expr.getConst().isZero(); } - Assert(expr.getKind() != Kind::REAL_ALGEBRAIC_NUMBER); + if (expr.getKind() == Kind::REAL_ALGEBRAIC_NUMBER) + { + return isZero(expr.getOperator().getConst()); + } return std::nullopt; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 67603be82..3bdecf556 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -780,6 +780,8 @@ set(regress_0_tests regress0/nl/pow2-pow-isabelle.smt2 regress0/nl/proj-issue-348.smt2 regress0/nl/proj-issue-444-memout-eqelim.smt2 + regress0/nl/proj-issue-451-ran-combination-1.smt2 + regress0/nl/proj-issue-451-ran-combination-2.smt2 regress0/nl/real-as-int.smt2 regress0/nl/real-div-ufnra.smt2 regress0/nl/sin-cos-346-b-chunk-0169.smt2 diff --git a/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 b/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 new file mode 100644 index 000000000..c126e5b29 --- /dev/null +++ b/test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: poly +; EXPECT: sat +(set-option :global-declarations true) +(set-logic QF_NRA) +(set-option :produce-unsat-cores true) +(declare-const _x0 Real) +(check-sat-assuming ( (>= (/ _x0 _x0) (/ (/ 2079598914 691107) _x0)) (and (> (/ (/ (/ 2079598914 691107) _x0) _x0) _x0) (> (- _x0) _x0)))) diff --git a/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 b/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 new file mode 100644 index 000000000..0cd8f2645 --- /dev/null +++ b/test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 @@ -0,0 +1,10 @@ +; REQUIRES: poly +; EXPECT: sat +(set-logic QF_NRA) +(declare-const x6 Real) +(set-option :produce-unsat-cores true) +(declare-const x Real) +(assert (= x6 (/ x x))) +(assert (> (- x) 0.0)) +(assert (> (/ 2 x x) x)) +(check-sat) -- 2.30.2