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

use simplex conflicts in LRA

Browse source
This commit is contained in:
Simon Cruanes 2020-12-22 10:55:55 -05:00
parent 4be726db43
commit 3b3a2e1caf
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/arith/lra/sidekick_arith_lra.ml
View file

@ -286,17 +286,16 @@ module Make(A : ARG) : S with module A = A = struct
Log.debug 5 "lra: solver returns SAT"; Log.debug 5 "lra: solver returns SAT";
() (* TODO: get a model + model combination *) () (* TODO: get a model + model combination *)
| SimpSolver.Unsatisfiable cert -> | SimpSolver.Unsatisfiable cert ->
begin match SimpSolver.check_cert simplex cert with let unsat_core =
| `Ok _unsat_core -> assert false (* TODO *) match SimpSolver.check_cert simplex cert with
| `Ok unsat_core -> unsat_core (* TODO *)
| _ -> assert false (* some kind of fatal error ? *) | _ -> assert false (* some kind of fatal error ? *)
(* TODO in
Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a" Log.debugf 5 (fun k->k"lra: solver returns UNSAT@ with cert %a"
(Fmt.Dump.list Lit.pp) lits); (Fmt.Dump.list Lit.pp) unsat_core);
let confl = List.rev_map Lit.neg lits in
(* TODO: produce and store a proper LRA resolution proof *) (* TODO: produce and store a proper LRA resolution proof *)
let confl = List.rev_map Lit.neg unsat_core in
SI.raise_conflict si acts confl SI.P.default SI.raise_conflict si acts confl SI.P.default
*)
end
end; end;
() ()