simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 12:45:48 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: proper negation when raising an acyclicity conflict

Browse source
This commit is contained in:
Simon Cruanes 2022-07-22 21:54:22 -04:00
parent c8800fe3e2
commit 2922cca78f
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/th-data/Sidekick_th_data.ml
View file

@ -630,7 +630,9 @@ module Make (A : ARG) : S with module A = A = struct
k "(@[%s.acyclicity.raise_confl@ %a@ @[:path %a@]@])" name Expl.pp
expl pp_path path);
let lits, pr = SI.cc_resolve_expl solver expl in
SI.raise_conflict solver acts lits pr
(* negate lits *)
let c = List.rev_map SI.Lit.neg lits in
SI.raise_conflict solver acts c pr
| { flag = New; _ } as node_r ->
node_r.flag <- Open;
let path = (n, node_r) :: path in