projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 811e5c6) | patch
Introduce skolem function to make transcendental function purification consistent...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 17 Feb 2022 21:40:22 +0000 (15:40 -0600)
committerGitHub <noreply@github.com>
Thu, 17 Feb 2022 21:40:22 +0000 (21:40 +0000)
commitcdef52f07aef156ad19dea89862a1b8d4373ea3a
treeee8f806255f7ed9b02db0603d21134c29781cb74tree
parent811e5c602c1445a4a64aa8a90d9b52a769611ebecommit | diff
Introduce skolem function to make transcendental function purification consistent (#8116)

Previously, we could introduce multiple purifications for the same sin term.
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history