projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 90267f8) | patch
Partial merge of integers work; this is simple B&B and some pseudoboolean
authorMorgan Deters <mdeters@gmail.com>
Fri, 2 Sep 2011 17:56:43 +0000 (17:56 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 2 Sep 2011 17:56:43 +0000 (17:56 +0000)
commit487e610b88f2a634e3285886ff96717c103338de
tree7f034b5c9f537195df72ac9ecd7666226dc2ed9ftree
parent90267f8729799f44c6fb33ace11b971a16e78dffcommit | diff
Partial merge of integers work; this is simple B&B and some pseudoboolean
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
148 files changed:
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/printer/cvc/cvc_printer.cpp diff | blob | history
src/prop/cnf_stream.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/arith/Makefile.am diff | blob | history
src/theory/arith/arith_rewriter.cpp diff | blob | history
src/theory/arith/arith_static_learner.cpp diff | blob | history
src/theory/arith/arith_static_learner.h diff | blob | history
src/theory/arith/arith_utilities.h diff | blob | history
src/theory/arith/arithvar_node_map.h diff | blob | history
src/theory/arith/arithvar_set.h diff | blob | history
src/theory/arith/dio_solver.cpp [new file with mode: 0644] blob
src/theory/arith/dio_solver.h [new file with mode: 0644] blob
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/ordered_set.h diff | blob | history
src/theory/arith/partial_model.h diff | blob | history
src/theory/arith/tableau.cpp diff | blob | history
src/theory/arith/tableau.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/booleans/theory_bool_type_rules.h diff | blob | history
src/theory/builtin/theory_builtin_type_rules.h diff | blob | history
src/theory/output_channel.h diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/Makefile.am diff | blob | history
src/util/integer_cln_imp.h diff | blob | history
src/util/integer_gmp_imp.h diff | blob | history
src/util/pseudoboolean.cpp [new file with mode: 0644] blob
src/util/pseudoboolean.h [new file with mode: 0644] blob
src/util/rational_cln_imp.h diff | blob | history
src/util/rational_gmp_imp.h diff | blob | history
test/Makefile.am diff | blob | history
test/regress/regress0/arith/Makefile [new file with mode: 0644] blob
test/regress/regress0/arith/Makefile.am diff | blob | history
test/regress/regress0/arith/integers/Makefile [new file with mode: 0644] blob
test/regress/regress0/arith/integers/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-001.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-002.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-003.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-004.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-005.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-006.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-007.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-008.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-009.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-010.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-011.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-012.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-013.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-014.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-015.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-016.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-017.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-018.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-019.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-020.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-021.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-022.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-023.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-024.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-025.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-026.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-027.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-028.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-029.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-030.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-031.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-032.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-033.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-034.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-035.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-036.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-037.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-038.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-039.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-040.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-041.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-042.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-042.min.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-043.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-044.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-045.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-046.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-047.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-048.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-049.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-050.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-051.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-052.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-053.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-054.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-055.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-056.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-057.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-058.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-059.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-060.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-061.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-062.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-063.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-064.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-065.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-066.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-067.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-068.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-069.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-070.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-071.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-072.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-073.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-074.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-075.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-076.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-077.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-078.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-079.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-080.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-081.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-082.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-083.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-084.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-085.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-086.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-087.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-088.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-089.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-090.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-091.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-092.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-093.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-094.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-095.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-096.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-097.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-098.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-099.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-int-100.cvc [new file with mode: 0644] blob
test/regress/regress0/arith/integers/arith-interval.cvc [new file with mode: 0644] blob