From fa45dcc9a4c401e5a5491231925df04bccbcafa7 Mon Sep 17 00:00:00 2001 From: Thibaut Cuvelier Date: Wed, 20 May 2020 17:14:37 +0200 Subject: [PATCH 1/5] Update attributes.jl --- src/attributes.jl | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/attributes.jl b/src/attributes.jl index 94b0bf2022..cf4f71e6e8 100644 --- a/src/attributes.jl +++ b/src/attributes.jl @@ -920,15 +920,23 @@ most recent call to [`compute_conflict!`](@ref). Possible values are: * `COMPUTE_CONFLICT_NOT_CALLED`: the function [`compute_conflict!`](@ref) has not yet been called +* `COMPUTE_CONFLICT_FAILED`: the function [`compute_conflict!`](@ref) has been + called and failed to completely execute. In particular, it could not decide + whether a conflict exists or not * `NO_CONFLICT_EXISTS`: there is no conflict because the problem is feasible -* `NO_CONFLICT_FOUND`: the solver could not find a conflict +* `NO_CONFLICT_FOUND`: the solver could not find a conflict, but did not ensure + the problem is feasible * `CONFLICT_FOUND`: at least one conflict could be found +* `MINIMUM_CONFLICT_FOUND`: at least one conflict could be found and the solver + was able to prove this conflict is minimal """ @enum ConflictStatusCode begin COMPUTE_CONFLICT_NOT_CALLED + COMPUTE_CONFLICT_FAILED NO_CONFLICT_EXISTS NO_CONFLICT_FOUND CONFLICT_FOUND + MINIMUM_CONFLICT_FOUND end """ From fff69b3529840f13410c72d2a01d76574ad9103c Mon Sep 17 00:00:00 2001 From: Thibaut Cuvelier Date: Thu, 21 May 2020 00:16:05 +0200 Subject: [PATCH 2/5] Update attributes.jl --- src/attributes.jl | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/attributes.jl b/src/attributes.jl index cf4f71e6e8..778a2b3060 100644 --- a/src/attributes.jl +++ b/src/attributes.jl @@ -923,20 +923,14 @@ Possible values are: * `COMPUTE_CONFLICT_FAILED`: the function [`compute_conflict!`](@ref) has been called and failed to completely execute. In particular, it could not decide whether a conflict exists or not -* `NO_CONFLICT_EXISTS`: there is no conflict because the problem is feasible -* `NO_CONFLICT_FOUND`: the solver could not find a conflict, but did not ensure - the problem is feasible +* `NO_CONFLICT_FOUND`: there is no conflict, maybe because the problem is feasible * `CONFLICT_FOUND`: at least one conflict could be found -* `MINIMUM_CONFLICT_FOUND`: at least one conflict could be found and the solver - was able to prove this conflict is minimal """ @enum ConflictStatusCode begin COMPUTE_CONFLICT_NOT_CALLED COMPUTE_CONFLICT_FAILED - NO_CONFLICT_EXISTS NO_CONFLICT_FOUND CONFLICT_FOUND - MINIMUM_CONFLICT_FOUND end """ From cbd940c95ebf37abc4b569a21e4efe41b7f65419 Mon Sep 17 00:00:00 2001 From: Thibaut Cuvelier Date: Thu, 21 May 2020 03:17:32 +0200 Subject: [PATCH 3/5] Update attributes.jl --- src/attributes.jl | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/attributes.jl b/src/attributes.jl index 778a2b3060..8a86e3d9d3 100644 --- a/src/attributes.jl +++ b/src/attributes.jl @@ -920,15 +920,14 @@ most recent call to [`compute_conflict!`](@ref). Possible values are: * `COMPUTE_CONFLICT_NOT_CALLED`: the function [`compute_conflict!`](@ref) has not yet been called -* `COMPUTE_CONFLICT_FAILED`: the function [`compute_conflict!`](@ref) has been - called and failed to completely execute. In particular, it could not decide - whether a conflict exists or not -* `NO_CONFLICT_FOUND`: there is no conflict, maybe because the problem is feasible +* `NO_CONFLICT_FOUND`: there is no conflict available. There may be several + reasons for this: the function [`compute_conflict!`](@ref) has finished + and decided that the problem is feasible, the function has failed to + completely execute * `CONFLICT_FOUND`: at least one conflict could be found """ @enum ConflictStatusCode begin COMPUTE_CONFLICT_NOT_CALLED - COMPUTE_CONFLICT_FAILED NO_CONFLICT_FOUND CONFLICT_FOUND end From 83a9a9864ac24e498bc404fdc7cc02eaa55c081f Mon Sep 17 00:00:00 2001 From: Thibaut Cuvelier Date: Fri, 22 May 2020 20:06:48 +0200 Subject: [PATCH 4/5] Update attributes.jl --- src/attributes.jl | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/attributes.jl b/src/attributes.jl index 8a86e3d9d3..b343dcf23c 100644 --- a/src/attributes.jl +++ b/src/attributes.jl @@ -920,14 +920,17 @@ most recent call to [`compute_conflict!`](@ref). Possible values are: * `COMPUTE_CONFLICT_NOT_CALLED`: the function [`compute_conflict!`](@ref) has not yet been called +* `NO_CONFLICT_EXISTS`: there is no conflict available, because the solver could + prove that the problem is feasible (i.e. there are no conflicts) * `NO_CONFLICT_FOUND`: there is no conflict available. There may be several reasons for this: the function [`compute_conflict!`](@ref) has finished and decided that the problem is feasible, the function has failed to - completely execute + completely execute (e.g., because it met a time limit) * `CONFLICT_FOUND`: at least one conflict could be found """ @enum ConflictStatusCode begin COMPUTE_CONFLICT_NOT_CALLED + NO_CONFLICT_EXISTS NO_CONFLICT_FOUND CONFLICT_FOUND end From 5d80995cbe7c0cd7c49fc0f2a60fd6f0363806c5 Mon Sep 17 00:00:00 2001 From: Thibaut Cuvelier Date: Tue, 26 May 2020 15:43:04 +0200 Subject: [PATCH 5/5] Update attributes.jl --- src/attributes.jl | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/attributes.jl b/src/attributes.jl index b343dcf23c..ad3ca78f26 100644 --- a/src/attributes.jl +++ b/src/attributes.jl @@ -922,10 +922,9 @@ Possible values are: not yet been called * `NO_CONFLICT_EXISTS`: there is no conflict available, because the solver could prove that the problem is feasible (i.e. there are no conflicts) -* `NO_CONFLICT_FOUND`: there is no conflict available. There may be several - reasons for this: the function [`compute_conflict!`](@ref) has finished - and decided that the problem is feasible, the function has failed to - completely execute (e.g., because it met a time limit) +* `NO_CONFLICT_FOUND`: there is no conflict available, because the function + [`compute_conflict!`](@ref) has failed to completely execute (e.g., because it + met a time limit) * `CONFLICT_FOUND`: at least one conflict could be found """ @enum ConflictStatusCode begin