projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Update test results.
[tatoo.git]
/
src
/
ata.ml
diff --git
a/src/ata.ml
b/src/ata.ml
index
6a3570c
..
8b51a08
100644
(file)
--- a/
src/ata.ml
+++ b/
src/ata.ml
@@
-14,7
+14,7
@@
(***********************************************************************)
(*
(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-2
2 17:22:38
CEST by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-2
4 18:10:13
CEST by Kim Nguyen>
*)
INCLUDE "utils.ml"
*)
INCLUDE "utils.ml"
@@
-199,6
+199,10
@@
type config = {
unsat : StateSet.t;
todo : TransList.t;
summary : node_summary;
unsat : StateSet.t;
todo : TransList.t;
summary : node_summary;
+ (** optimization infos,
+ not taken into account during hashconsing *)
+ mutable round : int;
+ mutable unstable_subtree : bool;
}
module Config = Hcons.Make(struct
}
module Config = Hcons.Make(struct
@@
-238,7
+242,9
@@
let dummy2 = TransList.cons
let dummy_config = Config.make { sat = StateSet.empty;
unsat = StateSet.empty;
todo = TransList.nil;
let dummy_config = Config.make { sat = StateSet.empty;
unsat = StateSet.empty;
todo = TransList.nil;
- summary = dummy_summary
+ summary = dummy_summary;
+ round = 0;
+ unstable_subtree = true;
}
}
@@
-377,7
+383,6
@@
let simplify_atom atom pos q { Config.node=config; _ } =
|| ((not pos) && StateSet.mem q config.sat) then SFormula.false_
else atom
|| ((not pos) && StateSet.mem q config.sat) then SFormula.false_
else atom
-
let eval_form phi fcs nss ps ss summary =
let rec loop phi =
begin match SFormula.expr phi with
let eval_form phi fcs nss ps ss summary =
let rec loop phi =
begin match SFormula.expr phi with
@@
-441,7
+446,7
@@
let eval_trans auto fcs nss ps ss =
let unsat = StateSet.union unsat (StateSet.diff removed kept) in
(* States that were found once to be satisfiable remain so *)
let unsat = StateSet.diff unsat sat in
let unsat = StateSet.union unsat (StateSet.diff removed kept) in
(* States that were found once to be satisfiable remain so *)
let unsat = StateSet.diff unsat sat in
- let new_config = Config.make {
sat; unsat; todo ; summary = old_summary
} in
+ let new_config = Config.make {
old_config.Config.node with sat; unsat; todo;
} in
Cache.N4.add auto.cache4 oid fcsid nssid psid new_config;
new_config
in
Cache.N4.add auto.cache4 oid fcsid nssid psid new_config;
new_config
in