This commit merges the branch arithmetic/propagation-again into trunk.
authorTim King <taking@cs.nyu.edu>
Mon, 18 Apr 2011 16:48:52 +0000 (16:48 +0000)
committerTim King <taking@cs.nyu.edu>
Mon, 18 Apr 2011 16:48:52 +0000 (16:48 +0000)
commitabe849b486ea3707fd51a612c7982554f3d6581f
tree8f3967f644f9098079c778dd60cf9feb36e1ab2b
parentb90081962840584bb9eeda368ea232a7d42a292b
This commit merges the branch arithmetic/propagation-again into trunk.
- This adds code for bounds refinement, and conflict weakening.
- This adds util/boolean_simplification.h.
- This adds a propagation manager to theory of arithmetic.
- Propagation is disabled by default.
- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.
22 files changed:
src/theory/arith/Makefile.am
src/theory/arith/arith_priority_queue.cpp
src/theory/arith/arith_prop_manager.cpp [new file with mode: 0644]
src/theory/arith/arith_prop_manager.h [new file with mode: 0644]
src/theory/arith/arith_utilities.h
src/theory/arith/arithvar_node_map.h [new file with mode: 0644]
src/theory/arith/arithvar_set.h
src/theory/arith/ordered_set.h
src/theory/arith/partial_model.cpp
src/theory/arith/partial_model.h
src/theory/arith/simplex.cpp
src/theory/arith/simplex.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/unate_propagator.cpp
src/theory/arith/unate_propagator.h
src/theory/theory_engine.h
src/util/Makefile.am
src/util/boolean_simplification.h [new file with mode: 0644]
src/util/options.cpp
src/util/options.h
test/unit/theory/theory_arith_white.h