diff options
| author |  Unknown <aleks@aleks-PC.csail.mit.edu> | 2011-10-10 18:41:36 -0400 |
|---|---|---|
| committer | Unknown <aleks@aleks-PC.csail.mit.edu> | 2011-10-10 18:41:36 -0400 |
| commit | 9428079835bca16d4fd04ea4b9fb5d9801e71232 (patch) | |
| tree | e4562b8d90785c6114ea1aaf5e51813b924428ed /Jennisys/Jennisys | |
| parent | 280a1f0644ab07863b09ef80c8b96d9a4c8a7371 (diff) | |
Jennisys: changed the fixpoint solver to pick only the true clause in a disjunction (if there is one that is true)
Diffstat (limited to 'Jennisys/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
|