diff options
Diffstat (limited to 'Jennisys')
| -rw-r--r-- | Jennisys/Jennisys/Analyzer.fs | 2 | ||||
| -rw-r--r-- | Jennisys/Jennisys/FixpointSolver.fs | 14 |
2 files changed, 9 insertions, 7 deletions
diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs index eb29e4d1..8172718b 100644 --- a/Jennisys/Jennisys/Analyzer.fs +++ b/Jennisys/Jennisys/Analyzer.fs @@ -746,7 +746,7 @@ and TryInferConditionals indent prog comp m unifs heapInst callGraph premises = let newSol = sol |> Utils.MapReplaceKey (c,m) (c,newMeth) newLst
if newSol = sol then Logger.TraceLine "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa sol aaaaaaaaaaaaaaaaaaaaaaaaaa" else ()
newMeth,newSol
- if i >= List.length guardList then
+ if i >= List.length guardList || List.length guardList <= 1 then
guard,m,sol
else
let newGuardList = Utils.ListRemoveNth i guardList
diff --git a/Jennisys/Jennisys/FixpointSolver.fs b/Jennisys/Jennisys/FixpointSolver.fs index 34a9b070..efb09485 100644 --- a/Jennisys/Jennisys/FixpointSolver.fs +++ b/Jennisys/Jennisys/FixpointSolver.fs @@ -237,12 +237,14 @@ let rec ComputeClosure heapInst expandExprFunc premises = // __fff lhs r
// | _ -> [binInExpr]
///////////////////////////////
- [BinaryOr (BinaryIn lhs l) (BinaryIn lhs r)]
-// let opt1 = BinaryIn lhs l
-// let opt2 = BinaryIn lhs r
-// match EvalFull heapInst opt1 with
-// | BoolLiteral(true) -> [opt1]
-// | _ -> [opt2]
+// [BinaryOr (BinaryIn lhs l) (BinaryIn lhs r)]
+ let opt1 = BinaryIn lhs l
+ let opt2 = BinaryIn lhs r
+ match EvalFull heapInst opt1 with
+ | BoolLiteral(true) -> [opt1]
+ | _ -> match EvalFull heapInst opt2 with
+ | BoolLiteral(true) -> [opt2]
+ | _ -> [BinaryOr (BinaryIn lhs l)(BinaryIn lhs r)]
| SequenceExpr(elist) ->
let len = elist |> List.length
if len = 0 then
|