Commit 5ebac877 authored by Thorsten Wißmann's avatar Thorsten Wißmann 🐧 Committed by Thorsten Wißmann
Browse files

Some partial progress, DONT MERGE TO MASTER

parent f71032c3
......@@ -121,7 +121,10 @@ and setCnstr = unit GHt.t
(* Types that are hard coded into the algorithm *)
(*****************************************************************************)
and stateExpander = unit -> ruleEnumeration
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
| Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
and stateExpander = unit -> ruleEnumeration junction
and sort = C.sort
......@@ -132,9 +135,12 @@ and nodeStatus =
| Unsat
and dependencies = bset list -> bset
and rule = (dependencies * (sort * bset) list)
and ruleEnumeration =
| AllInOne of (dependencies * (sort * bset) list) list
| NextRule of dependencies * (sort * bset) list
| AllInOne of rule list
| NextRule of rule
| NoMoreRules
type nominal = sort * localFormula
......
......@@ -60,7 +60,10 @@ type setCnstr
(* Types that are hard coded into the algorithm *)
(*****************************************************************************)
and stateExpander = unit -> ruleEnumeration
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
| Conjunctive of 'a (*specifies that all of the 'a need to be satifsfied *)
and stateExpander = unit -> ruleEnumeration junction
and sort = CoAlgFormula.sort
......@@ -71,9 +74,12 @@ and nodeStatus =
| Unsat
and dependencies = bset list -> bset
and rule = (dependencies * (sort * bset) list)
and ruleEnumeration =
| AllInOne of (dependencies * (sort * bset) list) list
| NextRule of dependencies * (sort * bset) list
| AllInOne of rule list
| NextRule of rule
| NoMoreRules
type nominal = sort * localFormula
......@@ -176,7 +182,7 @@ val stateGetRules : state -> (dependencies * core list) list
val stateAddRule : state -> dependencies -> core list -> int
val stateGetConstraints : state -> csetSet
val stateSetConstraints : state -> csetSet -> unit
val stateNextRule : state -> ruleEnumeration
val stateNextRule : state -> ruleEnumeration junction
(*****************************************************************************)
......
......@@ -530,14 +530,19 @@ let insertRule state dep chldrn =
false
end else true
let rec insertAllRules state = function
let rec insertAllRules state : rule list junction -> bool = function (* tells whether it is notUnsat *)
| [] -> true
| (dep, chldrn)::tl ->
let notUnsat = insertRule state dep chldrn in
if notUnsat then insertAllRules state tl else false
let expandState state =
match stateNextRule state with
let (junction, rules) =
match stateNextRule state with
| Disjunctive r -> (fun x -> Disjunctive x, r)
| Conjunctive r -> (fun x -> Conjunctive x, r)
in
match rules with
| AllInOne rules ->
let notUnsat = insertAllRules state rules in
if notUnsat then stateSetStatus state Open
......
Supports Markdown
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