projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6389272) | patch
Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver class...
authorYing Sheng <sqy1415@gmail.com>
Fri, 17 Dec 2021 22:28:12 +0000 (14:28 -0800)
committerGitHub <noreply@github.com>
Fri, 17 Dec 2021 22:28:12 +0000 (22:28 +0000)
commitc67bbf88a0da5c7c066de5ba9e31b58f00594b9b
tree6bf254c05eddd59c189face7b4ac559f5252dc80tree
parent63892729113274410dd974f1d2541aa96d3788d3commit | diff
Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver class and options (#7820)

This commit fixes several issues in the ArrayCoreSolver class and the options:
1. Add range checking for an update rule.
2. Assign different inference ids to different rules.
3. small syntax optimizations.
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/strings/array_core_solver.cpp diff | blob | history