diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 17:56:43 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 17:56:43 +0000 |
commit | 487e610b88f2a634e3285886ff96717c103338de (patch) | |
tree | 7f034b5c9f537195df72ac9ecd7666226dc2ed9f /src/theory/arith/arith_static_learner.h | |
parent | 90267f8729799f44c6fb33ace11b971a16e78dff (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.
Diffstat (limited to 'src/theory/arith/arith_static_learner.h')
-rw-r--r-- | src/theory/arith/arith_static_learner.h | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 0ed9cbe85..c58778215 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -25,6 +25,7 @@ #include "util/stats.h" #include "theory/arith/arith_utilities.h" +#include "theory/substitutions.h" #include <set> #include <list> @@ -45,6 +46,19 @@ private: std::list<TNode> d_miplibTrickKeys; /** + * Some integer variables are eligible to be replaced by + * pseudoboolean variables. This map collects those eligible + * substitutions. + * + * This is a reference to the substitution map in TheoryArith; as + * it's not "owned" by this static learner, it isn't cleared on + * clear(). This makes sense, as the static learner only + * accumulates information in the substitution map, it never uses it + * (i.e., it's write-only). + */ + SubstitutionMap& d_pbSubstitutions; + + /** * Map from a node to it's minimum and maximum. */ typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap; @@ -52,7 +66,7 @@ private: NodeToMinMaxMap d_maxMap; public: - ArithStaticLearner(); + ArithStaticLearner(SubstitutionMap& pbSubstitutions); void staticLearning(TNode n, NodeBuilder<>& learned); void addBound(TNode n); @@ -64,11 +78,14 @@ private: void postProcess(NodeBuilder<>& learned); + void replaceWithPseudoboolean(TNode var); void iteMinMax(TNode n, NodeBuilder<>& learned); void iteConstant(TNode n, NodeBuilder<>& learned); void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); + void checkBoundsForPseudobooleanReplacement(TNode n); + /** These fields are designed to be accessable to ArithStaticLearner methods. */ class Statistics { public: |