diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.ssc | 39 | ||||
| -rw-r--r-- | Source/Provers/Simplify/Let2ImpliesVisitor.ssc | 39 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.ssc | 11 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.ssc | 18 | ||||
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 9 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.ssc | 6 |
6 files changed, 76 insertions, 46 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc index 952bad92..d3eb2eba 100644 --- a/Source/Core/CommandLineOptions.ssc +++ b/Source/Core/CommandLineOptions.ssc @@ -197,6 +197,8 @@ namespace Microsoft.Boogie public int Z3mam = 0;
[Peer] public List<string!>! Z3Options = new List<string!>();
public bool Z3types = false;
+ public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
+ invariant 0 <= Z3lets && Z3lets < 4;
// Maximum amount of virtual memory (in bytes) for the prover to use
//
@@ -219,8 +221,8 @@ namespace Microsoft.Boogie public enum TypeEncoding { None, Predicates, Arguments, Monomorphic };
public TypeEncoding TypeEncodingMethod = TypeEncoding.Predicates;
- public bool Monomorphize = false;
-
+ public bool Monomorphize = false;
+
public bool ReflectAdd = false;
// Static constructor
@@ -421,8 +423,8 @@ namespace Microsoft.Boogie case "-launch":
case "/launch":
- System.Diagnostics.Debugger.Launch();
- break;
+ System.Diagnostics.Debugger.Launch();
+ break;
case "-proc":
case "/proc":
@@ -550,8 +552,8 @@ namespace Microsoft.Boogie case "-proverShutdownLimit":
case "/proverShutdownLimit":
- ps.GetNumericArgument(ref ProverShutdownLimit);
- break;
+ ps.GetNumericArgument(ref ProverShutdownLimit);
+ break;
case "-smtOutput":
case "/smtOutput":
@@ -931,11 +933,6 @@ namespace Microsoft.Boogie }
break;
- case "-monomorphize":
- case "/monomorphize":
- Monomorphize = true;
- break;
-
case "-vcBrackets":
case "/vcBrackets":
ps.GetNumericArgument(ref BracketIdsInVC, 2);
@@ -1021,11 +1018,6 @@ namespace Microsoft.Boogie ps.GetNumericArgument(ref ProverCCLimit);
break;
- case "-z3multipleErrors":
- case "/z3multipleErrors":
- z3AtFlag = false;
- break;
-
case "-z3mam":
case "/z3mam":
{
@@ -1047,11 +1039,11 @@ namespace Microsoft.Boogie }
break;
- case "-z3types":
- case "/z3types":
- Z3types = true;
+ case "-z3lets":
+ case "/z3lets":
+ ps.GetNumericArgument(ref Z3lets, 4);
break;
-
+
case "-platform":
case "/platform":
if (ps.ConfirmArgumentCount(1))
@@ -1137,7 +1129,10 @@ namespace Microsoft.Boogie ps.CheckBooleanFlag("vcsDumpSplits", ref VcsDumpSplits) ||
ps.CheckBooleanFlag("dbgRefuted", ref DebugRefuted) ||
ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||
- ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd)
+ ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
+ ps.CheckBooleanFlag("z3types", ref Z3types) ||
+ ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
+ ps.CheckBooleanFlag("monomorphize", ref Monomorphize)
)
{
// one of the boolean flags matched
@@ -1958,6 +1953,8 @@ namespace Microsoft.Boogie macros as in /proverLog can be used.
/z3types : generate multi-sorted VC that make use of Z3 types
+ /z3lets:<n> : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,
+ 3 - (default) any
");
}
}
diff --git a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc index 8443d950..0dc52516 100644 --- a/Source/Provers/Simplify/Let2ImpliesVisitor.ssc +++ b/Source/Provers/Simplify/Let2ImpliesVisitor.ssc @@ -22,8 +22,16 @@ namespace Microsoft.Boogie.Simplify public class Let2ImpliesMutator : SubstitutingVCExprVisitor {
public Let2ImpliesMutator(VCExpressionGenerator! gen) {
+ this(gen, false, false);
+ }
+ public Let2ImpliesMutator(VCExpressionGenerator! gen, bool keepLetTerm, bool keepLetFormula) {
base(gen);
+ this.keepLetTerm = keepLetTerm;
+ this.keepLetFormula = keepLetFormula;
}
+
+ readonly bool keepLetTerm;
+ readonly bool keepLetFormula;
public VCExpr! Mutate(VCExpr! expr) {
return Mutate(expr, new VCExprSubstitution ());
@@ -138,7 +146,8 @@ namespace Microsoft.Boogie.Simplify substitution.PushScope(); try {
// the bindings that remain and that are later handled using an implication
- List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!> ();
+ List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!> ();
+ List<VCExprLetBinding!> keepBindings = new List<VCExprLetBinding!> ();
foreach (VCExprLetBinding! binding in node) {
// in all cases we apply the substitution up to this point
@@ -149,18 +158,30 @@ namespace Microsoft.Boogie.Simplify // a bound formula is handled using an implication; we introduce
// a fresh variable to avoid clashes
assert polarity > 0;
-
- VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
- substitution[binding.V] = newVar;
-
- bindings.Add(Gen.LetBinding(newVar, newE));
+
+ if (keepLetFormula) {
+ keepBindings.Add(Gen.LetBinding(binding.V, newE));
+
+ } else {
+ VCExprVar! newVar = Gen.Variable(binding.V.Name, Type.Bool);
+ substitution[binding.V] = newVar;
+
+ bindings.Add(Gen.LetBinding(newVar, newE));
+ }
} else {
- // a bound term is substituted
- substitution[binding.V] = newE;
+ if (keepLetTerm) {
+ keepBindings.Add(Gen.LetBinding(binding.V, newE));
+ } else {
+ // a bound term is substituted
+ substitution[binding.V] = newE;
+ }
}
}
VCExpr! newBody = Mutate(node.Body, substitution);
+ if (keepBindings.Count > 0) {
+ newBody = Gen.Let(keepBindings, newBody);
+ }
// Depending on the places where the variable occurs, we would
// have to introduce implications or equations to define the
@@ -172,7 +193,7 @@ namespace Microsoft.Boogie.Simplify assert occ == OccurrenceTypes.None || occ == OccurrenceTypes.Pos;
}
- return Gen.Implies(Gen.AsImplications(bindings), newBody);
+ return Gen.ImpliesSimp(Gen.AsImplications(bindings), newBody);
} finally {
substitution.PopScope();
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc index df7f86d6..09873d7e 100644 --- a/Source/Provers/Simplify/ProverInterface.ssc +++ b/Source/Provers/Simplify/ProverInterface.ssc @@ -562,21 +562,24 @@ namespace Microsoft.Boogie.Simplify private readonly BigLiteralAbstracter! LitAbstracter;
public override string! translate(VCExpr! expr, int polarity) {
- Let2ImpliesMutator! letImplier = new Let2ImpliesMutator (Gen);
+ Let2ImpliesMutator! letImplier = new Let2ImpliesMutator(Gen);
// handle the types in the VCExpr
- TypeEraser! eraser;
+ TypeEraser eraser;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
case CommandLineOptions.TypeEncoding.Arguments:
eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, Gen);
break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ eraser = null;
+ break;
default:
eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
break;
}
- VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+ VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
- TermFormulaFlattener! flattener = new TermFormulaFlattener (Gen);
+ TermFormulaFlattener! flattener = new TermFormulaFlattener(Gen);
VCExpr! exprWithLet = flattener.Flatten(exprWithoutTypes);
VCExpr! exprWithoutLet = letImplier.Mutate(exprWithLet);
diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc index 02b4f505..c3a61fe3 100644 --- a/Source/Provers/Z3/ProverInterface.ssc +++ b/Source/Provers/Z3/ProverInterface.ssc @@ -75,6 +75,13 @@ namespace Microsoft.Boogie.Z3 return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
}
}
+ public int Lets {
+ get
+ ensures 0 <= result && result < 4;
+ {
+ return CommandLineOptions.Clo.Z3lets;
+ }
+ }
public bool V1 = false;
public bool V2 = false; // default set in PostParse
public bool DistZ3 = false;
@@ -107,8 +114,8 @@ namespace Microsoft.Boogie.Z3 ExeName = "z3-v1.3.exe";
}
if (DistZ3) {
- ExeName = "z3-dist.exe";
- CommandLineOptions.Clo.RestartProverPerVC = true;
+ ExeName = "z3-dist.exe";
+ CommandLineOptions.Clo.RestartProverPerVC = true;
}
}
@@ -227,7 +234,6 @@ namespace Microsoft.Boogie.Z3 eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, Gen);
break;
}
-
VCExpr! exprWithoutTypes = eraser != null ? eraser.Erase(expr, polarity) : expr;
LetBindingSorter! letSorter = new LetBindingSorter(Gen);
@@ -243,6 +249,12 @@ namespace Microsoft.Boogie.Z3 sortedExpr = flattener.Flatten(sortedExpr);
sortedAxioms = flattener.Flatten(sortedAxioms);
}
+ if (Opts.Lets != 3) {
+ // replace let expressions with implies
+ Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);
+ sortedExpr = letImplier.Mutate(sortedExpr);
+ sortedAxioms = letImplier.Mutate(sortedAxioms);
+ }
//////////////////////////////////////////////////////////////////////////
//SubtermCollector! coll = new SubtermCollector (gen);
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 7b6bb5c8..289dff87 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -93,18 +93,15 @@ namespace Microsoft.Boogie.VCExprAST public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {
- StringWriter sw = new StringWriter();
- SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
- lin.Linearise(e, LineariserOptions.SimplifyDefault);
- return (!)sw.ToString();
+ return ToString(e, LineariserOptions.SimplifyDefault, namer);
}
public static string! ToString(VCExpr! e, LineariserOptions! options,
UniqueNamer! namer) {
StringWriter sw = new StringWriter();
- SimplifyLikeExprLineariser! lin = new SimplifyLikeExprLineariser (sw, namer);
+ SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);
lin.Linearise(e, options);
- return (!)sw.ToString();
+ return sw.ToString();
}
////////////////////////////////////////////////////////////////////////////////////////
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc index 8347d124..f282b342 100644 --- a/Source/VCExpr/TypeErasure.ssc +++ b/Source/VCExpr/TypeErasure.ssc @@ -708,9 +708,9 @@ namespace Microsoft.Boogie.TypeErasure // "AbstractionVariable(int)" delivers variables
TypeSeq! instantiations) {
- if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
- return rawType;
-
+ if (CommandLineOptions.Clo.Monomorphize && AxBuilder.UnchangedType(rawType))
+ return rawType;
+
if (forall{TypeVariable! var in rawType.FreeVariables;
!boundTypeParams.Has(var)}) {
// Bingo!
|