projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 35ea6f4) | patch
Improve theory combination in the presence of real algebraic numbers (#7883)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 6 Jan 2022 21:09:10 +0000 (13:09 -0800)
committerGitHub <noreply@github.com>
Thu, 6 Jan 2022 21:09:10 +0000 (21:09 +0000)
commit868a62d550966065f8afdfc5b39715ca6c06314a
tree2b66c1d96a3c96369af6947c611542f777693c29tree
parent35ea6f4cb9b3915d1720b668e98236d453c1d682commit | diff
Improve theory combination in the presence of real algebraic numbers (#7883)

This PR changes how we handle real algebraic numbers in theory combination and model construction.
The goal is to improve getEqualityStatus() and produce proper models more often.
We now use a RAN-aware evaluator for getEqualityStatus() and change the way how the nonlinear extension finalizes its model.
src/CMakeLists.txt diff | blob | history
src/theory/arith/arith_evaluator.cpp [new file with mode: 0644] blob
src/theory/arith/arith_evaluator.h [new file with mode: 0644] blob
src/theory/arith/nl/cad_solver.cpp diff | blob | history
src/theory/arith/nl/cad_solver.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/combined-uf.smt2 [new file with mode: 0644] blob