projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b7be76b) | patch
Correct subtyping for arrays, disable subtyping for predicate subtypes. Bug fixes...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 18 Feb 2016 21:21:34 +0000 (15:21 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 18 Feb 2016 21:21:40 +0000 (15:21 -0600)
commit793361d81f0766c6a28ff699ed5447d9b8f8c123
treefff4d0f9c809400abb22edc13403867558b7426ftree
parentb7be76b58846a68dea4c1fcae19d6c3f087994b9commit | diff
Correct subtyping for arrays, disable subtyping for predicate subtypes.  Bug fixes in quantifiers related to subtypes/parametric sorts.  Make macros trace dependencies for get-unsat-core. Add regressions.
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/macro-subtype-param.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/macros-real-arg.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/subtype-param-unk.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/subtype-param.smt2 [new file with mode: 0644] blob