projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 223155c) | patch
(proof-new) Clean up uses of witness with skolem lemmas (#6109)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 11 Mar 2021 09:21:06 +0000 (03:21 -0600)
committerGitHub <noreply@github.com>
Thu, 11 Mar 2021 09:21:06 +0000 (09:21 +0000)
commit71e843a8e9e88fc739aaa5a4a5d608004648fafa
tree6f18912dfcb230139bbb6bdb68b38400d23d7efftree
parent223155cfb300458f534f4be6b88e5fdc17b0ff14commit | diff
(proof-new) Clean up uses of witness with skolem lemmas (#6109)

This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.

It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.
src/CMakeLists.txt diff | blob | history
src/theory/arith/operator_elim.cpp diff | blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
src/theory/skolem_lemma.cpp [new file with mode: 0644] blob
src/theory/skolem_lemma.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history