From e2cac78d39d20d628a6194f4ed76b6bad5d77f00 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 20 Oct 2015 16:48:43 +0200 Subject: [PATCH] Fixed typos in clause simplification --- solver/internal.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/solver/internal.ml b/solver/internal.ml index 7675a72f..1784618a 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -508,12 +508,12 @@ module Make (L : Log_intf.S)(St : Solver_types.S) if a.is_true then raise Trivial; if a.neg.is_true then begin match a.var.reason with - | Bcp (Some cl) -> atoms, true, max lvl cl.c_level + | Bcp (Some cl) -> atoms, false, max lvl cl.c_level | _ -> assert false end else a::atoms, init, lvl in - let atoms, init, lvl = List.fold_left aux ([], false, level0) atoms in + let atoms, init, lvl = List.fold_left aux ([], true, level0) atoms in List.fast_sort (fun a b -> a.var.vid - b.var.vid) atoms, init, lvl let partition atoms init0 = @@ -527,7 +527,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) if a.var.level = 0 then begin match a.var.reason with | Bcp (Some cl) -> - partition_aux trues unassigned falses true (max lvl cl.c_level) r + partition_aux trues unassigned falses false (max lvl cl.c_level) r | _ -> assert false end else partition_aux trues unassigned (a::falses) init lvl r @@ -542,7 +542,7 @@ module Make (L : Log_intf.S)(St : Solver_types.S) let add_clause ?tag name atoms history = if env.is_unsat then raise Unsat; (* is it necessary ? *) let init_name = name in - let c_level = current_level () in + let c_level = current_level () in let init0 = make_clause ?tag init_name atoms (List.length atoms) (history <> History []) history c_level in L.debug 10 "Adding clause : %a" St.pp_clause init0; try