summaryrefslogtreecommitdiff
path: root/src/theory/arith/soi_simplex.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/soi_simplex.h')
-rw-r--r--src/theory/arith/soi_simplex.h13
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback