From 0e84c5bfb3521c6fe80a7c9dd4969806d5396ad1 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 29 Jan 2015 15:49:01 +0100 Subject: [PATCH] Revert "Removed an error that was raised for tautological conflict clauses" This reverts commit 803b61c7dc8646071034d4d8dd7e233f0d00a67e. --- solver/mcproof.ml | 5 ++++- solver/mcsolver.ml | 5 +---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/solver/mcproof.ml b/solver/mcproof.ml index f9e620db..bd440a50 100644 --- a/solver/mcproof.ml +++ b/solver/mcproof.ml @@ -78,7 +78,10 @@ module Make(St : Mcsolver_types.S) = struct for i = 0 to Vec.size v - 1 do l := (Vec.get v i) :: !l done; - List.sort_uniq compare_atoms !l + let l, res = resolve (List.sort_uniq compare_atoms !l) in + if l <> [] then + raise (Resolution_error "Input cause is a tautology"); + res (* Adding hyptoheses *) let is_unit_hyp = function diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 9df6cd9f..d2368cd7 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -370,10 +370,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) var_bump_activity a.var; history := d :: !history; c := res - | _ -> - L.debug 0 "Found %d resolution lits" (List.length tmp); - List.iter (fun c -> L.debug 0 " |- %a" St.pp_atom c) tmp; - assert false + | _ -> assert false end | Bcp None -> L.debug 15 "Decision : %a" St.pp_atom a | Semantic _ -> L.debug 15 "Semantic propagation : %a" St.pp_atom a)