projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eecc1e4) | patch
Commit for the theory engine and rewriter changes. Changes are substantial and not...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 5 Jan 2011 03:21:35 +0000 (03:21 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Wed, 5 Jan 2011 03:21:35 +0000 (03:21 +0000)
commitf9a4fe48a4ec2355f8fec93d3f47242577df2511
treeeb49b7760b16aa17666d59464c96979b445fbcc8tree
parenteecc1e4f301711dbb2bf1508ea0ba6cd20acd593commit | diff
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
78 files changed:
src/expr/Makefile.am diff | blob | history
src/expr/kind_template.h diff | blob | history
src/expr/mkexpr diff | blob | history
src/expr/mkkind diff | blob | history
src/expr/mkmetakind diff | blob | history
src/expr/node_manager.h diff | blob | history
src/expr/type_constant.h [deleted file] blob | history
src/parser/smt/smt.cpp diff | blob | history
src/prop/sat.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_rewriter.h diff | blob | history
src/theory/arith/kinds diff | blob | history
src/theory/arith/normal_form.cpp diff | blob | history
src/theory/arith/normal_form.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arrays/Makefile.am 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_rewriter.h [new file with mode: 0644] blob
src/theory/booleans/Makefile.am diff | blob | history
src/theory/booleans/kinds diff | blob | history
src/theory/booleans/theory_bool.cpp diff | blob | history
src/theory/booleans/theory_bool.h diff | blob | history
src/theory/booleans/theory_bool_rewriter.cpp [new file with mode: 0644] blob
src/theory/booleans/theory_bool_rewriter.h [new file with mode: 0644] blob
src/theory/builtin/Makefile.am diff | blob | history
src/theory/builtin/kinds diff | blob | history
src/theory/builtin/theory_builtin.cpp diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history
src/theory/builtin/theory_builtin_rewriter.cpp [new file with mode: 0644] blob
src/theory/builtin/theory_builtin_rewriter.h [new file with mode: 0644] blob
src/theory/bv/Makefile.am diff | blob | history
src/theory/bv/kinds diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp [new file with mode: 0644] blob
src/theory/bv/theory_bv_rewriter.h [new file with mode: 0644] blob
src/theory/mkrewriter [new file with mode: 0755] blob
src/theory/mktheoryof [deleted file] blob | history
src/theory/mktheorytraits [new file with mode: 0755] blob
src/theory/rewriter.cpp [new file with mode: 0644] blob
src/theory/rewriter.h [new file with mode: 0644] blob
src/theory/rewriter_attributes.h [new file with mode: 0644] blob
src/theory/rewriter_tables_template.h [new file with mode: 0644] blob
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/theory_traits_template.h [new file with mode: 0644] blob
src/theory/theoryof_table_template.h [deleted file] blob | history
src/theory/uf/Makefile.am diff | blob | history
src/theory/uf/kinds diff | blob | history
src/theory/uf/morgan/theory_uf_morgan.cpp diff | blob | history
src/theory/uf/morgan/theory_uf_morgan.h diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
src/theory/uf/theory_uf_rewriter.h [new file with mode: 0644] blob
src/theory/uf/tim/theory_uf_tim.cpp diff | blob | history
src/theory/uf/tim/theory_uf_tim.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/uflra/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0100_10_10.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0100_10_11.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0100_10_15.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0100_10_16.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0100_10_19.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0200_10_22.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0200_10_25.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0200_10_26.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0200_10_27.smt [new file with mode: 0644] blob
test/regress/regress0/uflra/pb_real_10_0200_10_29.smt [new file with mode: 0644] blob
test/unit/expr/attribute_white.h diff | blob | history
test/unit/theory/theory_arith_white.h diff | blob | history
test/unit/theory/theory_black.h diff | blob | history
test/unit/theory/theory_engine_white.h diff | blob | history
test/unit/theory/theory_uf_tim_white.h diff | blob | history