projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4e1c078) | patch
Inferences and model construction taking into account seq.unit (#4607)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Jul 2020 13:46:07 +0000 (08:46 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Jul 2020 13:46:07 +0000 (08:46 -0500)
commit04154c08c1af81bb751376ae9379c071a95c5a3f
tree7a89b64878297c2a5009271ceb58023b4e76c8b1tree
parent4e1c078cfc49030b7e96485d777509ce4bc57a5acommit | diff
 Inferences and model construction taking into account seq.unit (#4607)

Towards theory of sequences.

This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction.

It also fixes a bug in the best content heuristic, which previously failed to update the best score.
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/infer_info.cpp diff | blob | history
src/theory/strings/infer_info.h diff | blob | history
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
src/theory/strings/theory_strings_utils.h diff | blob | history