diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 20 |
3 files changed, 14 insertions, 14 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 5e5a896a..ed80f6ac 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -565,6 +565,7 @@ namespace Microsoft.Boogie { public bool StratifiedInliningWithoutModels = false; // disable model generation for SI
public int StratifiedInliningVerbose = 0; // verbosity level
public int RecursionBound = 500;
+ public bool NonUniformUnfolding = false;
public string inferLeastForUnsat = null;
public string CoverageReporterPath = null;
public Process coverageReporter = null; // used internally for debugging
@@ -1223,7 +1224,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||
ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||
ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||
- ps.CheckBooleanFlag("printAssignment", ref PrintAssignment)
+ ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||
+ ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding)
) {
// one of the boolean flags matched
return true;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 9987e6f4..5667429a 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -864,9 +864,9 @@ namespace Microsoft.Boogie.SMTLib }
Check();
outcome = CheckOutcomeCore(handler);
- Pop();
if (outcome != Outcome.Valid)
break;
+ Pop();
string relaxVar = "relax_" + k;
relaxVars.Add(relaxVar);
SendThisVC("(declare-fun " + relaxVar + " () Int)");
@@ -882,6 +882,7 @@ namespace Microsoft.Boogie.SMTLib if (outcome == Outcome.Invalid) {
foreach (var relaxVar in relaxVars) {
SendThisVC("(get-value (" + relaxVar + "))");
+ FlushLogFile();
var resp = Process.GetProverResponse();
if (resp == null) break;
if (!(resp.Name == "" && resp.ArgCount == 1)) break;
@@ -896,6 +897,7 @@ namespace Microsoft.Boogie.SMTLib else
break;
}
+ Pop();
}
Pop();
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 12be00b2..98f20d21 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -1106,7 +1106,8 @@ namespace VC checker.TheoremProver.LogComment(str);
}
- public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions, out List<int> unsatisfiedSoftAssumptions) {
+ public Outcome CheckAssumptions(List<VCExpr> hardAssumptions, List<VCExpr> softAssumptions) {
+ List<int> unsatisfiedSoftAssumptions;
ProverInterface.Outcome outcome = TheoremProver.CheckAssumptions(hardAssumptions, softAssumptions, out unsatisfiedSoftAssumptions, reporter);
switch (outcome) {
case ProverInterface.Outcome.Valid:
@@ -1613,7 +1614,7 @@ namespace VC // bool underApproxNeeded = true;
// The recursion bound for stratified search
- int bound = 1;
+ int bound = CommandLineOptions.Clo.NonUniformUnfolding ? CommandLineOptions.Clo.RecursionBound : 1;
int done = 0;
@@ -1720,13 +1721,7 @@ namespace VC if (block.Count == 0)
{
// Increment bound
- var minRecReached = CommandLineOptions.Clo.RecursionBound + 1;
- foreach (var id in calls.currCandidates)
- {
- var rb = calls.getRecursionBound(id);
- if (bound < rb && rb < minRecReached) minRecReached = rb;
- }
- bound = minRecReached;
+ bound++;
if (useSummary) summaryComputation.boundChanged();
if (bound > CommandLineOptions.Clo.RecursionBound)
@@ -2210,7 +2205,6 @@ namespace VC bool allTrue = true;
bool allFalse = true;
List<VCExpr> softAssumptions = new List<VCExpr>();
- List<int> unsatisfiedSoftAssumptions;
assumptions = new List<VCExpr>();
procsThatReachedRecBound.Clear();
@@ -2220,7 +2214,7 @@ namespace VC int idBound = calls.getRecursionBound(id);
if (idBound <= bound)
{
- if (idBound > 0)
+ if (idBound > 1)
softAssumptions.Add(calls.getFalseExpr(id));
if (block.Contains(id))
{
@@ -2249,7 +2243,9 @@ namespace VC }
else
{
- ret = checker.CheckAssumptions(assumptions, softAssumptions, out unsatisfiedSoftAssumptions);
+ ret = CommandLineOptions.Clo.NonUniformUnfolding
+ ? checker.CheckAssumptions(assumptions, softAssumptions)
+ : checker.CheckAssumptions(assumptions);
}
if (ret != Outcome.Correct && ret != Outcome.Errors)
|