Skip to content

why3
why3
Commit 9c4c6599 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

Add timelimit in database. Fix the Einstein puzzle

parent 1501f43a
Hide whitespace changes
Inline Side-by-side
Showing with 86 additions and 68 deletions
examples/einstein.why
View file @ 9c4c6599
......@@ -48,81 +48,83 @@ theory Einstein "Einstein's problem"
leftof h1 h2 or rightof h1 h2
end
theory EinsteinHints "Hints"
theory EinsteinClues "Clues"
use import Einstein
(* The Englishman lives in a red house *)
axiom Hint1: Color.of (Owner.to_ Englishman) = Red
axiom Clue1: Color.of (Owner.to_ Englishman) = Red
(* The Swede has dogs *)
axiom Hint2: Pet.of Swede = Dogs
axiom Clue2: Pet.of Swede = Dogs
(* The Dane drinks tea *)
axiom Hint3: Drink.of Dane = Tea
axiom Clue3: Drink.of Dane = Tea
(* The green house is on the left of the white one *)
axiom Hint4: leftof (Color.to_ Green) (Color.to_ White)
axiom Clue4: leftof (Color.to_ Green) (Color.to_ White)
(* The green house's owner drinks coffee *)
axiom Hint5: Drink.of (Owner.of (Color.to_ Green)) = Coffee
axiom Clue5: Drink.of (Owner.of (Color.to_ Green)) = Coffee
(* The person who smokes Pall Mall has birds *)
axiom Hint6: Pet.of (Cigar.to_ PallMall) = Birds
axiom Clue6: Pet.of (Cigar.to_ PallMall) = Birds
(* The yellow house's owner smokes Dunhill *)
axiom Hint7: Cigar.of (Owner.of (Color.to_ Yellow)) = Dunhill
axiom Clue7: Cigar.of (Owner.of (Color.to_ Yellow)) = Dunhill
(* In the house in the center lives someone who drinks milk *)
axiom Hint8: Drink.of (Owner.of H3) = Milk
axiom Clue8: Drink.of (Owner.of H3) = Milk
(* The Norwegian lives in the first house *)
axiom Hint9: Owner.of H1 = Norwegian
axiom Clue9: Owner.of H1 = Norwegian
(* The man who smokes Blends lives next to the one who has cats *)
axiom Hint10: neighbour
axiom Clue10: neighbour
(Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Pet.to_ Cats))
(* The man who owns a horse lives next to the one who smokes Dunhills *)
axiom Hint11: neighbour
axiom Clue11: neighbour
(Owner.to_ (Pet.to_ Horse)) (Owner.to_ (Cigar.to_ Dunhill))
(* The man who smokes Blue Masters drinks beer *)
axiom Hint12:
axiom Clue12:
Drink.of (Cigar.to_ BlueMaster) = Beer
(* The German smokes Prince *)
axiom Hint13:
axiom Clue13:
Cigar.of German = Prince
(* The Norwegian lives next to the blue house *)
axiom Hint14:
axiom Clue14:
neighbour (Owner.to_ Norwegian) (Color.to_ Blue)
(* The man who smokes Blends has a neighbour who drinks water *)
axiom Hint15:
axiom Clue15:
neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))
end
theory Goals "Goals about Einstein's problem"
use import Einstein
use import EinsteinHints
(* lemma First_House_Not_White: Color.of H1 <> White *)
(* lemma Last_House_Not_Green: Color.of H5 <> Green *)
(* lemma Blue_not_Red: Blue <> Red *)
(* lemma Englishman_not_H2: Owner.to_ Englishman <> H2 *)
(* lemma Englishman_not_H1: Owner.to_ Englishman <> H1 *)
(* lemma Second_House_Blue: Color.of H2 = Blue *)
(* lemma Green_H4 : Color.of H4 = Green *)
(* lemma White_H5 : Color.of H5 = White *)
(* lemma Red_H3 : Color.of H3 = Red *)
(* lemma Yellow_H1 : Color.of H1 = Yellow *)
use import EinsteinClues
(*
lemma First_House_Not_White: Color.of H1 <> White
lemma Last_House_Not_Green: Color.of H5 <> Green
lemma Blue_not_Red: Blue <> Red
lemma Englishman_not_H2: Owner.to_ Englishman <> H2
lemma Englishman_not_H1: Owner.to_ Englishman <> H1
lemma Second_House_Blue: Color.of H2 = Blue
lemma Green_H4 : Color.of H4 = Green
lemma White_H5 : Color.of H5 = White
lemma Red_H3 : Color.of H3 = Red
lemma Yellow_H1 : Color.of H1 = Yellow
*)
goal G1: Pet.to_ Fish = German
goal G2: Pet.to_ Cats = Swede
goal Wrong: Pet.to_ Cats = Swede
goal G2: Pet.to_ Cats = Norwegian
end
......
examples/einstein/why3session.xml
View file @ 9c4c6599
......@@ -6,29 +6,31 @@
</theory>
<theory name="Einstein" verified="true" expanded="true">
</theory>
<theory name="EinsteinHints" verified="true" expanded="true">
<theory name="EinsteinClues" verified="true" expanded="true">
</theory>
<theory name="Goals" verified="false" expanded="true">
<goal name="G1" sum="3ac4d6944c1b5acf60b54d125510b5ce" proved="true" expanded="true">
<proof prover="z3" edited="" obsolete="false">
<result status="valid" time="0.08"/>
<goal name="G1" sum="0fe9a42b15af9d88af3552c07fd92112" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="G2" sum="1dfddc09f50e2271f110483bc42e7472" proved="false" expanded="true">
<proof prover="cvc3" edited="" obsolete="false">
<result status="unknown" time="0.42"/>
<goal name="Wrong" sum="fd482c10b98c64766b7b7527eeaf36ee" proved="false" expanded="true">
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.02"/>
</proof>
<proof prover="simplify" edited="" obsolete="false">
<result status="timeout" time="10.06"/>
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.37"/>
</proof>
<proof prover="alt-ergo" edited="" obsolete="false">
<result status="unknown" time="1.00"/>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="unknown" time="0.75"/>
</proof>
<proof prover="z3" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="timeout" time="2.09"/>
</proof>
<proof prover="gappa" edited="" obsolete="false">
<result status="unknown" time="0.01"/>
</goal>
<goal name="G2" sum="a6cfd18d6312e82ecf666580fac7945e" proved="true" expanded="true">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.08"/>
</proof>
</goal>
</theory>
......
src/ide/newmain.ml
View file @ 9c4c6599
......@@ -578,6 +578,7 @@ let prover_on_selected_goals pr =
let a = get_any row in
M.run_prover
~context_unproved_goals_only:!context_unproved_goals_only
~timelimit:gconfig.time_limit
pr a)
goals_view#selection#get_selected_rows
......
src/ide/session.ml
View file @ 9c4c6599
......@@ -126,6 +126,7 @@ type proof_attempt =
proof_goal : goal;
proof_key : O.key;
mutable proof_state : proof_attempt_status;
mutable timelimit : int;
mutable proof_obsolete : bool;
mutable edited_as : string;
}
......@@ -269,8 +270,8 @@ let save_status fmt s =
| Done r -> save_result fmt r
let save_proof_attempt fmt _key a =
fprintf fmt "@\n@[<v 1><proof prover=\"%s\" edited=\"%s\" obsolete=\"%b\">"
a.prover.prover_id a.edited_as a.proof_obsolete;
fprintf fmt "@\n@[<v 1><proof prover=\"%s\" timelimit=\"%d\" edited=\"%s\" obsolete=\"%b\">"
a.prover.prover_id a.timelimit a.edited_as a.proof_obsolete;
save_status fmt a.proof_state;
fprintf fmt "@]@\n</proof>"
......@@ -585,13 +586,14 @@ let task_checksum t =
(* raw additions to the model *)
(******************************)
let raw_add_external_proof ~obsolete ~edit (g:goal) p result =
let raw_add_external_proof ~obsolete ~timelimit ~edit (g:goal) p result =
let key = O.create ~parent:g.goal_key () in
let a = { prover = p;
proof_goal = g;
proof_key = key;
proof_obsolete = obsolete;
proof_state = result;
timelimit = timelimit;
edited_as = edit;
}
in
......@@ -760,7 +762,8 @@ let reload_proof ~provers obsolete goal pid old_a =
let obsolete = obsolete or old_a.proof_obsolete in
(* eprintf "proof_obsolete : %b@." obsolete; *)
let a =
raw_add_external_proof ~obsolete ~edit:old_a.edited_as goal p old_res
raw_add_external_proof ~obsolete ~timelimit:old_a.timelimit
~edit:old_a.edited_as goal p old_res
in
!notify_fun (Goal a.proof_goal)
with Not_found ->
......@@ -963,6 +966,11 @@ let bool_attribute field r def =
| _ -> assert false
with Not_found -> def
let int_attribute field r def =
try
int_of_string (List.assoc field r.Xml.attributes)
with Not_found | Invalid_argument _ -> def
let load_result r =
match r.Xml.name with
| "result" ->
......@@ -1043,7 +1051,10 @@ and load_proof_or_transf ~env ~provers mg a =
with Not_found -> assert false
in
let obsolete = bool_attribute "obsolete" a true in
let _pa = raw_add_external_proof ~obsolete ~edit mg p res in
let timelimit = int_attribute "timelimit" a 10 in
let (_ : proof_attempt) =
raw_add_external_proof ~obsolete ~timelimit ~edit mg p res
in
(* already done by raw_add_external_proof
Hashtbl.add mg.external_proofs prover pa *)
()
......@@ -1153,7 +1164,7 @@ let save_session () =
(* method: run a given prover on each unproved goals *)
(*****************************************************)
let redo_external_proof g a =
let redo_external_proof ~timelimit g a =
(* check that the state is not Scheduled or Running *)
let running = match a.proof_state with
| Scheduled | Running -> true
......@@ -1173,55 +1184,56 @@ let redo_external_proof g a =
end
in
schedule_proof_attempt
~debug:false ~timelimit:10 ~memlimit:0
~debug:false ~timelimit ~memlimit:0
?old ~command:p.command ~driver:p.driver
~callback
(get_task g)
let rec prover_on_goal p g =
let rec prover_on_goal ~timelimit p g =
let id = p.prover_id in
let a =
try Hashtbl.find g.external_proofs id
with Not_found ->
raw_add_external_proof ~obsolete:false ~edit:"" g p Undone
raw_add_external_proof ~obsolete:false ~timelimit ~edit:"" g p Undone
in
let () = redo_external_proof g a in
let () = redo_external_proof ~timelimit g a in
Hashtbl.iter
(fun _ t -> List.iter (prover_on_goal p) t.subgoals)
(fun _ t -> List.iter (prover_on_goal ~timelimit p) t.subgoals)
g.transformations
let rec prover_on_goal_or_children ~context_unproved_goals_only p g =
let rec prover_on_goal_or_children ~context_unproved_goals_only ~timelimit p g =
if not (g.proved && context_unproved_goals_only) then
begin
let r = ref true in
Hashtbl.iter
(fun _ t ->
r := false;
List.iter (prover_on_goal_or_children ~context_unproved_goals_only p)
List.iter (prover_on_goal_or_children
~context_unproved_goals_only ~timelimit p)
t.subgoals) g.transformations;
if !r then prover_on_goal p g
if !r then prover_on_goal ~timelimit p g
end
let run_prover ~context_unproved_goals_only pr a =
let run_prover ~context_unproved_goals_only ~timelimit pr a =
match a with
| Goal g ->
prover_on_goal_or_children ~context_unproved_goals_only pr g
prover_on_goal_or_children ~context_unproved_goals_only ~timelimit pr g
| Theory th ->
List.iter
(prover_on_goal_or_children ~context_unproved_goals_only pr)
(prover_on_goal_or_children ~context_unproved_goals_only ~timelimit pr)
th.goals
| File file ->
List.iter
(fun th ->
List.iter
(prover_on_goal_or_children ~context_unproved_goals_only pr)
(prover_on_goal_or_children ~context_unproved_goals_only ~timelimit pr)
th.goals)
file.theories
| Proof_attempt a ->
prover_on_goal_or_children ~context_unproved_goals_only pr a.proof_goal
prover_on_goal_or_children ~context_unproved_goals_only ~timelimit pr a.proof_goal
| Transformation tr ->
List.iter
(prover_on_goal_or_children ~context_unproved_goals_only pr)
(prover_on_goal_or_children ~context_unproved_goals_only ~timelimit pr)
tr.subgoals
(**********************************)
......@@ -1238,7 +1250,7 @@ let rec replay_on_goal_or_children ~obsolete_only ~context_unproved_goals_only g
(fun _ a ->
if not obsolete_only || a.proof_obsolete then
if not context_unproved_goals_only || proof_successful a
then redo_external_proof g a)
then redo_external_proof ~timelimit:a.timelimit g a)
g.external_proofs;
Hashtbl.iter
(fun _ t ->
......
src/ide/session.mli
View file @ 9c4c6599
......@@ -124,6 +124,7 @@ module Make(O: OBSERVER) : sig
proof_goal : goal;
proof_key : O.key;
mutable proof_state : proof_attempt_status;
mutable timelimit : int;
mutable proof_obsolete : bool;
mutable edited_as : string;
}
......@@ -207,7 +208,7 @@ module Make(O: OBSERVER) : sig
transformation_data -> Task.task -> unit
val run_prover : context_unproved_goals_only:bool ->
prover_data -> any -> unit
timelimit:int -> prover_data -> any -> unit
(** [run_prover p a] runs prover [p] on all goals under [a] *)
val transform : context_unproved_goals_only:bool ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment