projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d281fb) | patch
Partial merge from datatypes-merge branch:
authorMorgan Deters <mdeters@gmail.com>
Mon, 18 Apr 2011 08:59:09 +0000 (08:59 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 18 Apr 2011 08:59:09 +0000 (08:59 +0000)
commitb90081962840584bb9eeda368ea232a7d42a292b
treec0f568bc787744a5d53b79a818c0f1bd819596cftree
parent7d281fba79b1c9f3ae646d3371a0e52e2efd3bbacommit | diff
Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.
58 files changed:
src/expr/command.cpp diff | blob | history
src/expr/command.h diff | blob | history
src/expr/expr_manager_template.cpp diff | blob | history
src/expr/expr_manager_template.h diff | blob | history
src/expr/expr_template.h diff | blob | history
src/expr/mkexpr diff | blob | history
src/expr/mkkind diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | 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/parser/input.h diff | blob | history
src/parser/parser.cpp diff | blob | history
src/parser/parser.h diff | blob | history
src/parser/smt/Smt.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/builtin/theory_builtin_rewriter.h diff | blob | history
src/theory/datatypes/Makefile [new file with mode: 0644] blob
src/theory/datatypes/Makefile.am [new file with mode: 0644] blob
src/theory/datatypes/datatypes_rewriter.h [new file with mode: 0644] blob
src/theory/datatypes/kinds [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes.cpp [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes.h [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes_type_rules.h [new file with mode: 0644] blob
src/theory/datatypes/union_find.cpp [new file with mode: 0644] blob
src/theory/datatypes/union_find.h [new file with mode: 0644] blob
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/Assert.h diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/bitvector.h diff | blob | history
src/util/datatype.cpp [new file with mode: 0644] blob
src/util/datatype.h [new file with mode: 0644] blob
test/Makefile.am diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/datatypes/Makefile [new file with mode: 0644] blob
test/regress/regress0/datatypes/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype0.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype1.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype13.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype2.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype3.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/datatype4.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/error.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/mutually-recursive.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/rewriter.cvc [new file with mode: 0644] blob
test/regress/regress0/datatypes/typed_v1l50016-simp.cvc [new file with mode: 0644] blob
test/unit/Makefile.am diff | blob | history
test/unit/util/bitvector_black.h diff | blob | history
test/unit/util/datatype_black.h [new file with mode: 0644] blob