projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48471e5) | patch
Relax what is generated in the model from NL (#8113)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Feb 2022 17:46:44 +0000 (11:46 -0600)
committerGitHub <noreply@github.com>
Tue, 22 Feb 2022 17:46:44 +0000 (17:46 +0000)
commit4d84681baf668906523d4a8f3543783d638fe1df
tree095bc3ddf87f3b4fd68f45217672ae5d29354094tree
parent48471e5f6202cbe681d7d71c9974da603704160fcommit | diff
Relax what is generated in the model from NL (#8113)

This makes it so that we don't assign concrete values to equivalence classes with transcendental functions.

It also removes some unused infrastructure.
src/theory/arith/nl/cad_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/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
test/regress/regress0/arith/exp-in-model.smt2 diff | blob | history
test/regress/regress0/arith/issue7984-quant-trans.smt2 diff | blob | history