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

Tautological input clauses are now accepted

Browse source
This commit is contained in:
Guillaume Bury 2015-03-10 18:02:31 +01:00
parent a17d83eb1d
commit 9b41aab1b1
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
solver/mcproof.ml
View file

@ -77,9 +77,10 @@ module Make(St : Mcsolver_types.S) = struct
for i = 0 to Vec.size v - 1 do for i = 0 to Vec.size v - 1 do
l := (Vec.get v i) :: !l l := (Vec.get v i) :: !l
done; done;
let l, res = resolve (List.sort_uniq compare_atoms !l) in let res = List.sort_uniq compare_atoms !l in
let l, _ = resolve res in
if l <> [] then if l <> [] then
raise (Resolution_error "Input clause is a tautology"); Log.debug 3 "Input clause is a tautology";
res res
(* Adding hyptoheses *) (* Adding hyptoheses *)