diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 37 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 44 |
2 files changed, 32 insertions, 49 deletions
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index d52a7f99..cffcd9bf 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -109,7 +109,8 @@ namespace Microsoft.Boogie.Z3 this.tm = new Z3TypeCachedBuilder(this);
this.gen = gen;
this.namer = new UniqueNamer();
- this.z3.SetPrintMode(PrintMode.SmtlibFull);
+ this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);
+ this.z3.TraceToFile("trace.c");
this.z3log = null;
try
@@ -130,7 +131,10 @@ namespace Microsoft.Boogie.Z3 {
if (z3log != null)
{
- z3log.WriteLine(format, args);
+ var str = string.Format(format, args);
+ // Do standard string replacement
+ str = str.Replace("array", "Array");
+ z3log.WriteLine(str);
z3log.Flush();
}
}
@@ -151,7 +155,7 @@ namespace Microsoft.Boogie.Z3 functions.CreateBacktrackPoint();
labels.CreateBacktrackPoint();
z3.Push();
- log("Push");
+ log("(push)");
}
public void Backtrack()
@@ -161,7 +165,7 @@ namespace Microsoft.Boogie.Z3 functions.Backtrack();
constants.Backtrack();
symbols.Backtrack();
- log("Pop");
+ log("(pop)");
}
public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)
@@ -169,7 +173,7 @@ namespace Microsoft.Boogie.Z3 Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions);
Term term = Unwrap(z3ast);
- log("assert {0}", term);
+ log("(assert {0})", term);
z3.AssertCnstr(term);
}
@@ -179,7 +183,7 @@ namespace Microsoft.Boogie.Z3 Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);
Term term = Unwrap(z3ast);
- log("assert {0}", term);
+ log("(assert {0})", term);
z3.AssertCnstr(term);
}
@@ -202,7 +206,7 @@ namespace Microsoft.Boogie.Z3 }
foreach (Term assumption in assumptions)
{
- log("assert {0}", assumption);
+ log("(assert {0})", assumption);
z3.AssertCnstr(assumption);
}
}
@@ -347,7 +351,7 @@ namespace Microsoft.Boogie.Z3 {
Model z3Model;
outcome = z3.CheckAndGetModel(out z3Model);
- log("check-and-get-model");
+ log("(check-sat)");
if (outcome == LBool.False)
break;
@@ -406,17 +410,18 @@ namespace Microsoft.Boogie.Z3 Term proof;
Term[] core;
Term[] assumption_terms = new Term[assumptions.Count];
-
+ var logstring = "";
for (int i = 0; i < assumptions.Count; i++)
{
Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
Z3TermAst z3ast = (Z3TermAst)assumptions[i].Accept(visitor, linOptions);
assumption_terms[i] = Unwrap(z3ast);
+ logstring += string.Format("({0}) ", assumption_terms[i]);
}
- log("check-assumptions ...");
+ log("(get-core {0})", logstring);
outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
-
+
if (outcome != LBool.False)
{
Debug.Assert(z3Model != null);
@@ -440,7 +445,7 @@ namespace Microsoft.Boogie.Z3 labels.Dispose();
z3Model.Dispose();
}
-
+
if (boogieErrors.Count > 0)
{
return ProverInterface.Outcome.Invalid;
@@ -474,7 +479,7 @@ namespace Microsoft.Boogie.Z3 public void DeclareType(string typeName)
{
- log("declare-type: {0}", typeName);
+ log("(declare-sort {0})", typeName);
}
public void DeclareConstant(string constantName, Type boogieType)
@@ -485,26 +490,28 @@ namespace Microsoft.Boogie.Z3 Term constAst = z3.MkConst(symbolAst, unwrapTypeAst);
constants.Add(constantName, Wrap(constAst));
- log("declare-const: {0}: {1}", constantName, unwrapTypeAst);
+ log("(declare-funs (({0} {1})))", constAst, unwrapTypeAst);
}
public void DeclareFunction(string functionName, List<Type> domain, Type range)
{
Symbol symbolAst = GetSymbol(functionName);
+ var domainStr = "";
List<Sort> domainAst = new List<Sort>();
foreach (Type domainType in domain)
{
Z3Type type = tm.GetType(domainType);
Sort unwrapType = Unwrap(type);
domainAst.Add(unwrapType);
+ domainStr += unwrapType.ToString() + " ";
}
Z3Type rangeAst = tm.GetType(range);
Sort unwrapRangeAst = Unwrap(rangeAst);
FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), unwrapRangeAst);
Z3TypeSafeConstDecl typeSafeConstDecl = Wrap(constDeclAst);
functions.Add(functionName, typeSafeConstDecl);
- log("declare-fun: {0}: {1}", functionName, constDeclAst);
+ log("(declare-funs (({0} {1} {2})))", functionName, domainStr, unwrapRangeAst);
}
private List<Symbol> GetSymbols(List<string> symbolNames)
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index ef8a4c80..7002ad61 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -682,12 +682,19 @@ namespace VC {
checker.TheoremProver.LogComment(str);
}
- /*
+
public override Outcome CheckAssumptions(List<VCExpr> assumptions)
{
+ if (assumptions.Count == 0)
+ {
+ return CheckVC();
+ }
+
+ //TheoremProver.Push();
TheoremProver.AssertAxioms();
TheoremProver.CheckAssumptions(assumptions);
ProverInterface.Outcome outcome = TheoremProver.CheckOutcome(reporter);
+ //TheoremProver.Pop();
numQueries++;
switch (outcome)
@@ -707,7 +714,7 @@ namespace VC throw new cce.UnreachableException();
}
}
- */
+
}
// Store important information related to a single VerifyImplementation query
@@ -1009,21 +1016,6 @@ namespace VC assumptions.Add(calls.getFalseExpr(id));
}
- /*
- checker.Push();
-
- foreach (int id in calls.currCandidates)
- {
- checker.AddAxiom(calls.getFalseExpr(id));
- }
-
- // Check!
- ret = checker.CheckVC();
-
- // Pop
- checker.Pop();
- */
-
ret = checker.CheckAssumptions(assumptions);
checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");
@@ -1079,31 +1071,15 @@ namespace VC if (allFalse)
{
- ret = Outcome.Correct;
- }
- else
- {
- ret = checker.CheckAssumptions(assumptions);
- }
- /*
- checker.Push();
-
- // Check
- if (allFalse)
- {
// If we made all candidates false, then this is the same
// as the underapprox query. We already know the answer.
ret = Outcome.Correct;
}
else
{
- ret = checker.CheckVC();
+ ret = checker.CheckAssumptions(assumptions);
}
- // Pop
- checker.Pop();
- */
-
if (ret != Outcome.Correct && ret != Outcome.Errors)
{
// The query ran out of memory or time, that's it,
|