diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-03 13:15:26 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-03 13:15:26 -0400 |
commit | 5100b3d2e8e870f85aaa753b25bd8e1fa2349e39 (patch) | |
tree | fc7d1c6d01a6bb6872b77c13e81b5a673edde1a0 /src/theory/arith/soi_simplex.h | |
parent | cb09a647dc2524772e13946299f7b29ae627ae60 (diff) | |
parent | d1783a6d2fa6c48418fcf6a28f84e321061c0507 (diff) |
Merging branch 'soiquickexplain'.
Diffstat (limited to 'src/theory/arith/soi_simplex.h')
-rw-r--r-- | src/theory/arith/soi_simplex.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 006839a55..de565df64 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -195,6 +195,19 @@ private: IntStat& conflictStat = d_statistics.d_initialConflicts; return standardProcessSignals(timer, conflictStat); } + + void quickExplain(); + DenseSet d_qeInSoi; + DenseSet d_qeInUAndNotInSoi; + ArithVarVec d_qeConflict; + ArithVarVec d_qeGreedyOrder; + sgn_table d_qeSgns; + + uint32_t quickExplainRec(uint32_t cEnd, uint32_t uEnd); + void qeAddRange(uint32_t begin, uint32_t end); + void qeRemoveRange(uint32_t begin, uint32_t end); + void qeSwapRange(uint32_t N, uint32_t r, uint32_t s); + unsigned trySet(const ArithVarVec& set); unsigned tryAllSubsets(const ArithVarVec& set, unsigned depth, ArithVarVec& tmp); |