projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 50c31e6) | patch
Support for witnessing choice in models (#3781)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 26 Feb 2020 15:02:15 +0000 (09:02 -0600)
committerGitHub <noreply@github.com>
Wed, 26 Feb 2020 15:02:15 +0000 (09:02 -0600)
commitabd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8
treecffa12338950b4d7b5bfc43e78849684b6058e30tree
parent50c31e61ab240ccd551a0aea732f8b9a88d7fb32commit | diff
Support for witnessing choice in models (#3781)

Fixes #3300.

This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.
src/options/smt_options.toml diff | blob | history
src/theory/arith/nl_model.cpp diff | blob | history
src/theory/arith/nl_model.h diff | blob | history
src/theory/arith/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nonlinear_extension.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 [new file with mode: 0644] blob