projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5e9ca9) | patch
Fix issues involving multiple sources of model substitutions in NL (#8300)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Mar 2022 21:12:55 +0000 (16:12 -0500)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 21:12:55 +0000 (21:12 +0000)
commit509ecd23cff74a68ba5971308cfc5313bc6c202f
tree91423540a4246f2dcb3a1ab4c886f1431a4a5504tree
parente5e9ca94a9171914694bcf009cb2968af93af624commit | diff
Fix issues involving multiple sources of model substitutions in NL (#8300)

Fixes #8294.

The first benchmark times out, the second is added as a regression.

The issues center around 2 sources of substitutions (coverings and sine solvers) for model substitutions.

Also does minor cleanup to nl model.
src/theory/arith/nl/coverings_solver.cpp diff | blob | history
src/theory/arith/nl/nl_model.cpp diff | blob | history
src/theory/arith/nl/nl_model.h diff | blob | history
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/nta/issue8294-2-double-solve.smt2 [new file with mode: 0644] blob