summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/CommandLineOptions.ssc31
-rw-r--r--Source/Provers/Z3/Inspector.cs8
-rw-r--r--Source/Provers/Z3/Prover.cs25
-rw-r--r--Source/Provers/Z3/ProverInterface.cs58
4 files changed, 57 insertions, 65 deletions
diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index c0ba6eaa..92d97fb1 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -95,8 +95,6 @@ namespace Microsoft.Boogie
public bool SimplifyLogFileAppend = false;
public bool SoundnessSmokeTest = false;
- public List<string!>! Z3DebugTraces = new List<string!>();
-
private bool noConsistencyChecks = false;
public bool NoConsistencyChecks {
get {return !Verify ? true : noConsistencyChecks;}
@@ -203,10 +201,8 @@ namespace Microsoft.Boogie
get { if (DebugRefuted) return XmlSink; else return null; }
}
- public int Z3mam = 0;
[Peer] public List<string!>! Z3Options = new List<string!>();
public bool Z3types = false;
- public bool Z3OptimizeForBitvectors = false;
public int Z3lets = 3; // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any
invariant 0 <= Z3lets && Z3lets < 4;
@@ -926,13 +922,6 @@ namespace Microsoft.Boogie
}
break;
- case "-z3DebugTrace":
- case "/z3DebugTrace":
- if (ps.ConfirmArgumentCount(1)) {
- CommandLineOptions.Clo.Z3DebugTraces.Add((!)args[ps.i]);
- }
- break;
-
case "-inline":
case "/inline":
if (ps.ConfirmArgumentCount(1)) {
@@ -1125,19 +1114,6 @@ namespace Microsoft.Boogie
ps.GetNumericArgument(ref ProverCCLimit);
break;
- case "-z3mam":
- case "/z3mam":
- {
- int mam = 0;
- if (ps.GetNumericArgument(ref mam)) {
- if (mam == 0 || mam == 3 || mam == 4) {
- Z3mam = mam;
- } else
- ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);
- }
- }
- break;
-
case "-z3opt":
case "/z3opt":
if (ps.ConfirmArgumentCount(1))
@@ -1237,7 +1213,6 @@ namespace Microsoft.Boogie
ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||
ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||
ps.CheckBooleanFlag("z3types", ref Z3types) ||
- ps.CheckBooleanFlag("z3bv", ref Z3OptimizeForBitvectors) ||
ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||
ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||
ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||
@@ -2086,12 +2061,7 @@ namespace Microsoft.Boogie
/simplifyMatchDepth:<num> : Set Simplify prover's matching depth limit
Z3 specific options:
- /z3mam:<num> : Z3 matching engine: 0 (default) - eager instantiation,
- 3 - lazy instantiation,
- 4 - eager instantiation w/ matching-loop breaking heuristic
/z3opt:<arg> : specify additional Z3 options
- /z3DebugTrace:<arg> : z3 command line options so that Z3 generates debug
- tracing
/z3multipleErrors : report multiple counterexamples for each error
/useArrayTheory : use Z3's native theory (as opposed to axioms). Currently
implies /monomorphize.
@@ -2104,7 +2074,6 @@ namespace Microsoft.Boogie
/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
- /z3bv : use Z3 settings optimized for bitvector reasoning
");
}
}
diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs
index 425de1ff..3675f6a7 100644
--- a/Source/Provers/Z3/Inspector.cs
+++ b/Source/Provers/Z3/Inspector.cs
@@ -53,12 +53,12 @@ void ObjectInvariant()
[Rep] readonly TextReader fromInspector;
[Rep] readonly TextWriter toInspector;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(inspector!=null);
+ void ObjectInvariant()
+ {
+ Contract.Invariant(inspector!=null);
Contract.Invariant(fromInspector!=null);
Contract.Invariant(toInspector != null);
-}
+ }
public Inspector(Z3InstanceOptions opts)
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 36c5c82d..2bb02e64 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -113,25 +113,13 @@ namespace Microsoft.Boogie.Z3
AddOption(result, "MODEL_V1", "true");
AddOption(result, "ASYNC_COMMANDS", "false");
- if (!CommandLineOptions.Clo.Z3OptimizeForBitvectors) {
-
+ if (!opts.OptimizeForBv) {
// Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.
// The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.
AddOption(result, "PHASE_SELECTION", "0");
AddOption(result, "RESTART_STRATEGY", "0");
AddOption(result, "RESTART_FACTOR", "|1.5|");
- // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
- // the foo(x0) will be activated for e-matching when x is skolemized to x0.
- AddOption(result, "NNF_SK_HACK", "true");
-
- // More or less like MAM=0.
- AddOption(result, "QI_EAGER_THRESHOLD", "100");
- // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
-
- // the following will make the :weight option more usable
- AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");
-
// Make the integer model more diverse by default, speeds up some benchmarks a lot.
AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");
@@ -144,6 +132,17 @@ namespace Microsoft.Boogie.Z3
AddOption(result, "DELAY_UNITS_THRESHOLD", "16");
}
+ // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,
+ // the foo(x0) will be activated for e-matching when x is skolemized to x0.
+ AddOption(result, "NNF_SK_HACK", "true");
+
+ // More or less like MAM=0.
+ AddOption(result, "QI_EAGER_THRESHOLD", "100");
+ // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.
+
+ // the following will make the :weight option more usable
+ AddOption(result, "QI_COST", "|\"(+ weight generation)\"|");
+
if (opts.Inspector != null)
AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 172fbf60..bcf55c4c 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -104,11 +104,13 @@ void ObjectInvariant()
public string ExeName = "z3.exe";
public bool InverseImplies = false;
public string Inspector = null;
+ public bool OptimizeForBv = false;
+
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(ExeName!=null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(ExeName!=null);
+ }
protected override bool Parse(string opt)
@@ -117,6 +119,7 @@ void ObjectInvariant()
return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "DIST", ref DistZ3) ||
+ ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
base.Parse(opt);
}
@@ -129,16 +132,37 @@ void ObjectInvariant()
CommandLineOptions.Clo.RestartProverPerVC = true;
}
}
+
+ public string Help
+ {
+ get
+ {
+ return
+ // base.Help +
+@"
+Z3-specific options:
+~~~~~~~~~~~~~~~~~~~~
+INSPECTOR=<string> Use the specified Z3Inspector binary.
+OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
+
+Obscure options:
+~~~~~~~~~~~~~~~~
+DIST=<bool> Use z3-dist.exe binary.
+REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
+";
+ // DIST requires non-public binaries
+ }
+ }
}
internal class Z3LineariserOptions : LineariserOptions {
private readonly Z3InstanceOptions opts;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(opts!=null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(opts!=null);
+ }
public override CommandLineOptions.BvHandling Bitvectors { get {
@@ -250,15 +274,15 @@ void ObjectInvariant()
return new Z3VCExprTranslator(this);
}
-[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Opts!=null);
- Contract.Invariant(Gen != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != null);
-}
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(Opts!=null);
+ Contract.Invariant(Gen != null);
+ Contract.Invariant(AxBuilder != null);
+ Contract.Invariant(Namer != null);
+ Contract.Invariant(DeclCollector != null);
+ }
private readonly Z3InstanceOptions Opts;
private readonly VCExpressionGenerator Gen;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 22:48:00 +0000