projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 47c9c2f) | patch
Improve getValue for non-evaluated operators (#6436)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 24 Apr 2021 01:45:01 +0000 (20:45 -0500)
committerGitHub <noreply@github.com>
Sat, 24 Apr 2021 01:45:01 +0000 (01:45 +0000)
commit8f50a5600e0664330128d2ac824092a685ef965e
treece3e08fbaa21cee663604e3da5981374d5b8da1atree
parent47c9c2f42696a1e04577c1a79ac78f4186657818commit | diff
Improve getValue for non-evaluated operators (#6436)

This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.

This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
47 files changed:
src/theory/theory_model.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/div-chainable.smt2 diff | blob | history
test/regress/regress0/arith/issue3413.smt2 diff | blob | history
test/regress/regress0/bug484.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_5293_2.smt2 diff | blob | history
test/regress/regress0/decision/quant-ex1.smt2 diff | blob | history
test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 diff | blob | history
test/regress/regress0/fmf/fmc_unsound_model.smt2 diff | blob | history
test/regress/regress0/fmf/sc_bad_model_1221.smt2 diff | blob | history
test/regress/regress0/fp/issue3619.smt2 diff | blob | history
test/regress/regress0/push-pop/real-as-int-incremental.smt2 diff | blob | history
test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 diff | blob | history
test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 diff | blob | history
test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 diff | blob | history
test/regress/regress1/arith/issue4985-model-success.smt2 diff | blob | history
test/regress/regress1/arith/issue4985b-model-success.smt2 diff | blob | history
test/regress/regress1/fmf/Hoare-z3.931718.smtv1.smt2 diff | blob | history
test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2 diff | blob | history
test/regress/regress1/fmf/am-bad-model.cvc diff | blob | history
test/regress/regress1/fmf/german169.smt2 diff | blob | history
test/regress/regress1/fmf/issue3626.smt2 diff | blob | history
test/regress/regress1/fmf/jasmin-cdt-crash.smt2 diff | blob | history
test/regress/regress1/fmf/loopy_coda.smt2 diff | blob | history
test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 diff | blob | history
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc diff | blob | history
test/regress/regress1/fmf/nun-0208-to.smt2 diff | blob | history
test/regress/regress1/fmf/refcount24.cvc.smt2 diff | blob | history
test/regress/regress1/quantifiers/horn-simple.smt2 diff | blob | history
test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue3664.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue4849-nqe.smt2 diff | blob | history
test/regress/regress1/quantifiers/issue5470-aext.smt2 diff | blob | history
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 diff | blob | history
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 diff | blob | history
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 diff | blob | history
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 diff | blob | history
test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2 diff | blob | history
test/regress/regress1/sets/is_singleton1.smt2 diff | blob | history
test/regress/regress1/sets/issue5271.smt2 diff | blob | history
test/regress/regress1/sets/sets-tuple-poly.cvc diff | blob | history
test/regress/regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 diff | blob | history
test/regress/regress1/sygus/issue3944-div-rewrite.smt2 diff | blob | history
test/regress/regress1/trim.cvc diff | blob | history
test/regress/regress2/issue3687-check-models.smt2 diff | blob | history
test/regress/regress2/quantifiers/net-policy-no-time.smt2 diff | blob | history
test/regress/regress2/sygus/issue4022-conjecture-gen.smt2 diff | blob | history