diff options
Diffstat (limited to 'src/theory/bv/bv_inequality_graph.h')
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 20 |
1 files changed, 4 insertions, 16 deletions
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 860302aa4..d402b1561 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -190,7 +190,7 @@ class InequalityGraph : public context::ContextNotifyObj{ * @param explanation */ void computeExplanation(TermId from, TermId to, std::vector<ReasonId>& explanation); - void splitDisequality(TNode diseq); + // void splitDisequality(TNode diseq); /** Disequality reasoning @@ -198,11 +198,8 @@ class InequalityGraph : public context::ContextNotifyObj{ /*** The currently asserted disequalities */ context::CDQueue<TNode> d_disequalities; - context::CDQueue<TNode> d_disequalitiesToSplit; - context::CDO<unsigned> d_diseqToSplitIndex; - TNodeSet d_lemmasAdded; - TNodeSet d_disequalitiesAlreadySplit; - + NodeSet d_disequalitiesAlreadySplit; + Node makeDiseqSplitLemma(TNode diseq); /** Backtracking mechanisms **/ std::vector<std::pair<TermId, InequalityEdge> > d_undoStack; context::CDO<unsigned> d_undoStackIndex; @@ -225,8 +222,6 @@ public: d_signed(s), d_modelValues(c), d_disequalities(c), - d_disequalitiesToSplit(c), - d_diseqToSplitIndex(c, 0), d_disequalitiesAlreadySplit(), d_undoStack(), d_undoStackIndex(c) @@ -255,17 +250,10 @@ public: void getConflict(std::vector<TNode>& conflict); virtual ~InequalityGraph() throw(AssertionException) {} /** - * Get any new lemmas (resulting from disequalities splits) that need - * to be added. - * - * @param new_lemmas - */ - void getNewLemmas(std::vector<Node>& new_lemmas); - /** * Check that the currently asserted disequalities that have not been split on * are still true in the current model. */ - void checkDisequalities(); + void checkDisequalities(std::vector<Node>& lemmas); /** * Return true if a < b is entailed by the current set of assertions. * |