projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 98f80e6) | patch
Add extensionality option for strings disequalities (#7229)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 22 Sep 2021 18:03:38 +0000 (13:03 -0500)
committerGitHub <noreply@github.com>
Wed, 22 Sep 2021 18:03:38 +0000 (18:03 +0000)
commit4cd199a554bd6a5247ab8143e1a3fb2d7eff88f3
tree16d07c8fa5c410c2d34c8d035299d6629862633ctree
parent98f80e6ccc23df7d17f452a3259dd4c3d7aff4c6commit | diff
Add extensionality option for strings disequalities (#7229)

Towards the strings array solver.

Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.
src/options/strings_options.toml diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/core_solver.h diff | blob | history
src/theory/strings/skolem_cache.h diff | blob | history