diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-17 20:38:32 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-17 20:38:32 +0000 |
commit | 232042b3e2e265dbfe9c693d018d48388be91018 (patch) | |
tree | 55dc6d39bbd5eff9b0b1c220ed33dac3d4bdd316 /src/theory/arith/Makefile.am | |
parent | 68f8b6b2589320dac3a022a1e5058e5a65cc570b (diff) |
- Removes arith_constants.h
- Adds ArithStaticLearner. Consolidates and cleans up the code for static learning in arithmetic. Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick. The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.
Diffstat (limited to 'src/theory/arith/Makefile.am')
-rw-r--r-- | src/theory/arith/Makefile.am | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 48be16f90..2c00f5d4d 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -9,10 +9,11 @@ libarith_la_SOURCES = \ theory_arith_type_rules.h \ arith_rewriter.h \ arith_rewriter.cpp \ + arith_static_learner.h \ + arith_static_learner.cpp \ normal_form.h\ normal_form.cpp \ arith_utilities.h \ - arith_constants.h \ delta_rational.h \ delta_rational.cpp \ partial_model.h \ |