projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e33582f) | patch
Fixes and improvement for IAND solver (#8771)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 13 May 2022 18:52:59 +0000 (13:52 -0500)
committerGitHub <noreply@github.com>
Fri, 13 May 2022 18:52:59 +0000 (18:52 +0000)
commitead6d41a4cbfd0d99a80201cd1197943c63428ee
tree7523b1a512dcbd423d69851d78c842310594fbd8tree
parente33582f42b0998170bc4f30f54290808fc9cf4accommit | diff
Fixes and improvement for IAND solver (#8771)

This fixes a model soundness bug in the non-linear solver for IAND, which was caused by the core NL model solving for an IAND term. This adds 2 delta debugged variants of a benchmark from an application.

It also improves the value-based refinement scheme for IAND significantly by ensuring we take the modulus of model values. This should make it terminating.
src/options/smt_options.toml diff | blob | history
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/nl_model.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/dd.iand-wrong-0513-pp.smt2 [new file with mode: 0644] blob
test/regress/cli/regress1/bv/dd.iand-wrong-0513.smt2 [new file with mode: 0644] blob