diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-11 23:48:11 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 22:48:11 +0000 |
| commit | a22deeb091673226a1edb5a89bc8a596a3d51fc7 (patch) | |
| tree | f51d6edc2fe374cb0001681c3f882e1a1e7f4a3a /src/theory/arith/simplex.cpp | |
| parent | 5998d7f5a9168b0dd1c26f3aa1b85e570fe72af8 (diff) | |
Make linear arithmetic use its inference manager (#5934)
This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
Diffstat (limited to 'src/theory/arith/simplex.cpp')
| -rw-r--r-- | src/theory/arith/simplex.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index df399d686..d93e42215 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -94,7 +94,7 @@ void SimplexDecisionProcedure::reportConflict(ArithVar basic){ ConstraintCP conflicted = generateConflictForBasic(basic); Assert(conflicted != NullConstraint); - d_conflictChannel.raiseConflict(conflicted); + d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); d_conflictVariables.add(basic); } @@ -117,7 +117,7 @@ ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const { if(checkBasicForConflict(basic)){ ConstraintCP conflicted = generateConflictForBasic(basic); - d_conflictChannel.raiseConflict(conflicted); + d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN); return true; }else{ return false; |