diff options
author | Tim King <taking@cs.nyu.edu> | 2013-05-02 17:15:53 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2013-05-02 17:15:53 -0400 |
commit | d1783a6d2fa6c48418fcf6a28f84e321061c0507 (patch) | |
tree | 3b30fe95e0d24526a2ad538d83512b159f841fba /src/theory/arith/soi_simplex.h | |
parent | 9098391fe334d829ec4101f190b8f1fa21c30752 (diff) |
Adding quick explain for soi simplex.
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 1a6becccb..86b9276ed 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -193,6 +193,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); |