projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d6d3460) | patch
Make type rules more strict for operators whose type rules involve subtypes. Disable...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 12 Jul 2017 13:35:03 +0000 (08:35 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 12 Jul 2017 13:50:58 +0000 (08:50 -0500)
commit360d6ee8d3cdd5ddb47c328043eaed3a107b8db1
tree9e1fb4d128a62ca3e9152530dbfadb448ed49a45tree
parentd6d34604fa6d4c260edfc10a5b7f543540be75f4commit | diff
Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).
29 files changed:
src/compat/cvc3_compat.cpp diff | blob | history
src/expr/Makefile.am diff | blob | history
src/expr/expr_manager_template.cpp diff | blob | history
src/expr/expr_manager_template.h diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history
src/expr/predicate.cpp [deleted file] blob | history
src/expr/predicate.h [deleted file] blob | history
src/expr/predicate.i [deleted file] blob | history
src/expr/type.cpp diff | blob | history
src/expr/type.h diff | blob | history
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/theory_arith_type_rules.h diff | blob | history
src/theory/arith/type_enumerator.h diff | blob | history
src/theory/arrays/theory_arrays_type_rules.h diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/uf/theory_uf_type_rules.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history