diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-28 15:19:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-28 15:19:41 -0600 |
commit | 6473c66b039c933c433d2dec4a475780ebb72953 (patch) | |
tree | 24a8a34db88c384076668b953d24417add2d3dbe /src | |
parent | 9bb84e49df11dd669db1fff22cb69a08dfaa7bb4 (diff) |
Do not insist on bound values being constant in arithmetic instantiation (#3643)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 0a3775807..2984c23be 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -236,9 +236,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, // since the quantifier-free arithmetic solver may pass full // effort with no lemmas even when we are not guaranteed to have a // model. By convention, we use GEQ to compare the values here. + // It also may be the case that cmp is non-constant, in the case + // where lhs or rhs contains a transcendental function. We consider + // the bound to be an upper bound in this case. Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); cmp = Rewriter::rewrite(cmp); - Assert(cmp.isConst()); is_upper = !cmp.isConst() || !cmp.getConst<bool>(); } } @@ -466,8 +468,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, cmp_bound = Rewriter::rewrite(cmp_bound); // Should be comparing two constant values which should rewrite // to a constant. If a step failed, we assume that this is not - // the new best bound. - Assert(cmp_bound.isConst()); + // the new best bound. We might not be comparing constant + // values (for instance if transcendental functions are + // involved), in which case we do update the best bound value. if (!cmp_bound.isConst() || !cmp_bound.getConst<bool>()) { new_best = false; |