From d94ee09f56c82be899dd796c91c767a8711302e4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Apr 2022 21:48:35 -0500 Subject: [PATCH] Ignore irrelevant exponential terms (#8534) Fixes #8517. --- .../arith/nl/transcendental/exponential_solver.cpp | 11 ++++++++++- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress1/quantifiers/issue8517-exp-exp.smt2 | 6 ++++++ 3 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 93786f646..3e5fb2b4a 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -153,6 +153,14 @@ void ExponentialSolver::checkMonotonic() for (const Node& tf : it->second) { + Node mva = d_data->d_model.computeAbstractModelValue(tf); + if (mva == tf) + { + // if it was not assigned a model value by the linear solver, it is + // not a relevant term. This can happen for terms like (exp (exp 1.0)), + // where (exp 1.0) is not relevant until we purify (exp (exp 1.0)). + continue; + } Node a = tf[0]; Node mvaa = d_data->d_model.computeAbstractModelValue(a); if (mvaa.isConst()) @@ -178,7 +186,8 @@ void ExponentialSolver::checkMonotonic() Assert(sargval.isConst()); Node s = tf_arg_to_term[sarg]; Node sval = d_data->d_model.computeAbstractModelValue(s); - Assert(sval.isConst()); + Assert(sval.isConst()) << "non-constant model value " << sval << " for " + << s; // store the concavity region d_data->d_tf_region[s] = 1; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 8fda24a13..d6be8cafd 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2229,6 +2229,7 @@ set(regress_1_tests regress1/quantifiers/issue8456-2-syqi-ic.smt2 regress1/quantifiers/issue8456-syqi-ic.smt2 regress1/quantifiers/issue8497-syqi-str-fmf.smt2 + regress1/quantifiers/issue8517-exp-exp.smt2 regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 diff --git a/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 new file mode 100644 index 000000000..a98c6e5c2 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/issue8517-exp-exp.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic ALL) +(declare-const x Bool) +(declare-const x1 Bool) +(assert (forall ((r Real)) (= x (and x1 (= r 2) (= 0.0 (exp (exp 1.0))) (= 3 (/ (- r) (- r))))))) +(check-sat) -- 2.30.2