projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cdb5c6e) | patch
Formalize more skolems (#6307)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 13 Apr 2021 19:30:03 +0000 (14:30 -0500)
committerGitHub <noreply@github.com>
Tue, 13 Apr 2021 19:30:03 +0000 (19:30 +0000)
commit10308c88ae5de234eb62c08380d53d4967112ccd
treec60187541a2e5aabda5fd1141ab210900e690126tree
parentcdb5c6e7e03e4717f21c5726f02763962c23a7b2commit | diff
Formalize more skolems (#6307)

This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.

It also adds proof support for datatypes purification.
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/datatypes/infer_proof_cons.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/strings/skolem_cache.cpp diff | blob | history
src/theory/strings/skolem_cache.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history