projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 324434a) | patch
Formalize more string skolems (#7554)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 3 Nov 2021 16:12:18 +0000 (11:12 -0500)
committerGitHub <noreply@github.com>
Wed, 3 Nov 2021 16:12:18 +0000 (16:12 +0000)
commitd527b3f2501410770a76977efa180009e06ea172
tree2740aea9ed89c510e5ccb14b89ca91822609978btree
parent324434a74b35d0e58bdb551c9155e9fb32844d07commit | diff
Formalize more string skolems (#7554)

This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules.

Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.
12 files changed:
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/strings/core_solver.cpp 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
test/api/CMakeLists.txt diff | blob | history
test/api/proj-issue306.cpp diff | blob | history
test/api/proj-issue334.cpp [new file with mode: 0644] blob
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/proj-issue331.smt2 [new file with mode: 0644] blob