diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /src/theory/arrays | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 12 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 6985aaea8..0aff30d74 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -118,7 +118,7 @@ void TheoryArrays::check(Effort e) { // which can lead to a conflict Node conflict = constructConflict(d_conflict); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } merge(assertion[0], assertion[1]); @@ -139,13 +139,13 @@ void TheoryArrays::check(Effort e) { // after addTerm since we weren't watching a or b before Node conflict = constructConflict(d_conflict); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } else if(find(a) == find(b)) { Node conflict = constructConflict(assertion[0]); d_conflict = Node::null(); - d_out->conflict(conflict, false); + d_out->conflict(conflict); return; } Assert(!d_cc.areCongruent(a,b)); @@ -764,7 +764,7 @@ bool TheoryArrays::isRedundantInContext(TNode a, TNode b, TNode i, TNode j) { nb << literal1.notNode() << literal2.notNode(); literal1 = nb; d_conflict = Node::null(); - d_out->conflict(literal1, false); + d_out->conflict(literal1); Trace("arrays") << "TheoryArrays::isRedundantInContext() " << "conflict via lemma: " << literal1 << endl; return true; @@ -870,7 +870,7 @@ bool TheoryArrays::propagateFromRow(TNode a, TNode b, TNode i, TNode j) { return false; } -void TheoryArrays::explain(TNode n) { +Node TheoryArrays::explain(TNode n) { Trace("arrays")<<"Arrays::explain start for "<<n<<"\n"; @@ -901,7 +901,7 @@ void TheoryArrays::explain(TNode n) { } Node reason = nb; - d_out->explanation(reason); + return reason; /* context::CDMap<TNode, std::pair<TNode, TNode>, TNodeHashFunction>::const_iterator diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 37fffd2ec..a984cb342 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -476,7 +476,7 @@ public: */ } - void explain(TNode n); + Node explain(TNode n); Node getValue(TNode n); SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); |