projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bea30aa) | patch
Add support for eqrange predicate (#4562)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 23 Jun 2020 16:55:01 +0000 (09:55 -0700)
committerGitHub <noreply@github.com>
Tue, 23 Jun 2020 16:55:01 +0000 (09:55 -0700)
commit0539b0342b46e9fb96467a23f703bf2317692bb2
tree1c2d54f7791ee472daa40efc63ce88e13b9e4cc8tree
parentbea30aa5dd6b36fc5a206c4742abadf8c3fab5c1commit | diff
Add support for eqrange predicate (#4562)

This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
14 files changed:
src/api/cvc4cpp.cpp diff | blob | history
src/api/cvc4cppkind.h diff | blob | history
src/options/arrays_options.toml diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arrays/kinds diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/arrays/theory_arrays_type_rules.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/eqrange1.smt2 [new file with mode: 0644] blob
test/regress/regress0/eqrange2.smt2 [new file with mode: 0644] blob
test/regress/regress0/eqrange3.smt2 [new file with mode: 0644] blob