projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 32347c2) | patch
Connect sequences array solver to strategy in theory of strings (#7847)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 21 Dec 2021 00:30:43 +0000 (18:30 -0600)
committerGitHub <noreply@github.com>
Tue, 21 Dec 2021 00:30:43 +0000 (16:30 -0800)
commit160b1f8d35e7bf6441981db3176f18ce077046bd
treef9f58d058d56778001d476701c6e4a2256835c9dtree
parent32347c2043d60dc83cd2a5675d3f7796a42022a2commit | diff
Connect sequences array solver to strategy in theory of strings (#7847)

Also corrects an issue with model construction, where SEQ_NTH should be assignable in addition to SEQ_NTH_TOTAL.

seqArray branch (which has regressions) can be merged to master after this PR.
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/strategy.cpp diff | blob | history
src/theory/strings/strategy.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history