From 9428079835bca16d4fd04ea4b9fb5d9801e71232 Mon Sep 17 00:00:00 2001 From: Unknown Date: Mon, 10 Oct 2011 18:41:36 -0400 Subject: Jennisys: changed the fixpoint solver to pick only the true clause in a disjunction (if there is one that is true) --- Jennisys/Jennisys/Analyzer.fs | 2 +- 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 -- cgit v1.2.3