projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ed42d7) | patch
Fixes for unconstrained variables in nonlinear model (#5351)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 28 Oct 2020 20:17:05 +0000 (15:17 -0500)
committerGitHub <noreply@github.com>
Wed, 28 Oct 2020 20:17:05 +0000 (15:17 -0500)
commiteb812afac2884131b21948aee3da9d8c1e92ba98
tree86833576ff15aeafb135a0f186fa4333e160d2fbtree
parent3ed42d7aba07db5801cf8245890035192aa06b15commit | diff
Fixes for unconstrained variables in nonlinear model (#5351)

This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0.

This fixes #5348.
src/theory/arith/nl/nl_model.cpp diff | blob | history
src/theory/arith/nl/nl_model.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/iand-no-init.smt2 [new file with mode: 0644] blob