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/theory_arith.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/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0c15c824c..7e14f6b06 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,6 +38,7 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_prop_manager.h" #include "theory/arith/arithvar_node_map.h" +#include "theory/arith/dio_solver.h" #include "util/stats.h" @@ -69,6 +70,21 @@ private: ArithVarNodeMap d_arithvarNodeMap; /** + * List of the types of variables in the system. + * "True" means integer, "false" means (non-integer) real. + */ + std::vector<short> d_integerVars; + + /** + * On full effort checks (after determining LA(Q) satisfiability), we + * consider integer vars, but we make sure to do so fairly to avoid + * nontermination (although this isn't a guarantee). To do it fairly, + * we consider variables in round-robin fashion. This is the + * round-robin index. + */ + ArithVar d_nextIntegerCheckVar; + + /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that * can be used to determine the value of n using getValue(). @@ -86,8 +102,6 @@ private: */ ArithVarSet d_userVariables; - - /** * List of all of the inequalities asserted in the current context. */ @@ -98,6 +112,23 @@ private: */ Tableau d_tableau; + /** + * A Diophantine equation solver. Accesses the tableau and partial + * model (each in a read-only fashion). + */ + DioSolver d_diosolver; + + /** + * Some integer variables can be replaced with pseudoboolean + * variables internally. This map is built up at static learning + * time for top-level asserted expressions of the shape "x = 0 OR x + * = 1". This substitution map is then applied in preprocess(). + * + * Note that expressions of the shape "x >= 0 AND x <= 1" are + * already substituted for PB versions at solve() time and won't + * appear here. + */ + SubstitutionMap d_pbSubstitutions; /** Counts the number of notifyRestart() calls to the theory. */ uint32_t d_restartsCounter; |