projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3428c0e) | patch
Simplify and fix how purified terms are managed in the trancendental solver (#8167)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 25 Feb 2022 18:45:43 +0000 (12:45 -0600)
committerGitHub <noreply@github.com>
Fri, 25 Feb 2022 18:45:43 +0000 (18:45 +0000)
commit5e7107f378f917731acbd017c854829f25ac8bdf
treeb71dbf842dd68c3e098a8dd0266fdc0907b0a618tree
parent3428c0e156cdb3b079ae57bc8ba3805edb5d9c88commit | diff
Simplify and fix how purified terms are managed in the trancendental solver (#8167)

Simplification is leftover from the sine symmetry heuristic, now the mapping from terms to what purifies them is injective.
Also makes the mapping context-dependent.

It also ensures that we keep model values for purification arguments. Fixes #8160.
src/theory/arith/nl/transcendental/exponential_solver.h diff | blob | history
src/theory/arith/nl/transcendental/sine_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/nta/issue8160-model-purify.smt2 [new file with mode: 0644] blob