projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 265765c) | patch
Fix the way abstract values are typed; fixes some compliance issues.
authorMorgan Deters <mdeters@gmail.com>
Sat, 1 Dec 2012 14:36:14 +0000 (14:36 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 1 Dec 2012 14:36:14 +0000 (14:36 +0000)
commitec29471e427bf25034a93c182b424730d439a90a
treef4ddc215f2e78b72fdff2fa62fc8561b7dec84betree
parent265765c9f5c35c4b65934e574dbfabab97b15f7acommit | diff
Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)
src/expr/node_builder.h diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/smt/boolean_terms.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history