projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dfc685b) | patch
Use proper RAN nodes for nl model (#7939)
authorGereon Kremer <gkremer@stanford.edu>
Mon, 24 Jan 2022 19:58:56 +0000 (11:58 -0800)
committerGitHub <noreply@github.com>
Mon, 24 Jan 2022 19:58:56 +0000 (19:58 +0000)
commita077d2781380c485cf5586a0107c8c943185a79b
tree558b0e0b545f96753802cb747073a7c2e9f9ec5btree
parentdfc685b86237a56b1a54801bafa343b5139aaac0commit | diff
Use proper RAN nodes for nl model (#7939)

This PR finally uses proper RealAlgebraicNumber (wrapped in nodes) to represent nonlinear model values. This simplifies the implementation of getEqualityStatus, and should make theory combination much more robust.
Also, we reintroduce the possibility to have getEqualityStatus return unknown, though this should only happen in the presence of witness terms.
src/theory/arith/arith_evaluator.cpp diff | blob | history
src/theory/arith/arith_evaluator.h diff | blob | history
src/theory/arith/nl/poly_conversion.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/regress0/nl/issue3652.smt2 diff | blob | history
test/regress/regress0/nl/sqrt2-value.smt2 diff | blob | history
test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 diff | blob | history