diff options
Diffstat (limited to 'Source/Provers/Z3api')
-rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 153 | ||||
-rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 8 |
2 files changed, 151 insertions, 10 deletions
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 947d4eae..3b7b8f43 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -8,7 +8,7 @@ using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie;
using Microsoft.Boogie.Z3;
using Microsoft.Boogie.VCExprAST;
-using Microsoft.Boogie.Simplify;
+using System.Diagnostics.Contracts;
using TypeAst = System.IntPtr;
using TermAst = System.IntPtr;
@@ -19,7 +19,146 @@ using PatternAst = System.IntPtr; namespace Microsoft.Boogie.Z3
{
- public class Z3apiProcessTheoremProver : ApiProverInterface
+ public class Z3InstanceOptions : ProverOptions {
+ public int Timeout { get { return TimeLimit / 1000; } }
+ public int Lets {
+ get {
+ Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
+ return CommandLineOptions.Clo.Z3lets;
+ }
+ }
+ public bool DistZ3 = false;
+ public string ExeName = "z3.exe";
+ public bool InverseImplies = false;
+ public string Inspector = null;
+ public bool OptimizeForBv = false;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(ExeName != null);
+ }
+
+ protected override bool Parse(string opt) {
+ //Contract.Requires(opt!=null);
+ 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);
+ }
+
+ public override void PostParse() {
+ base.PostParse();
+
+ if (DistZ3) {
+ ExeName = "z3-dist.exe";
+ CommandLineOptions.Clo.RestartProverPerVC = true;
+ }
+ }
+
+ public override string Help {
+ get {
+ return
+@"
+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.
+
+" + base.Help;
+ // DIST requires non-public binaries
+ }
+ }
+ }
+
+ public class Z3LineariserOptions : LineariserOptions {
+ private readonly Z3InstanceOptions opts;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(opts != null);
+ }
+
+
+ public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables)
+ : base(asTerm) {
+ Contract.Requires(opts != null);
+ Contract.Requires(cce.NonNullElements(letVariables));
+
+ this.opts = opts;
+ this.LetVariablesAttr = letVariables;
+ }
+
+ public override bool UseWeights {
+ get {
+ return true;
+ }
+ }
+
+ public override bool UseTypes {
+ get {
+ return true;
+ }
+ }
+
+ public override bool QuantifierIds {
+ get {
+ return true;
+ }
+ }
+
+ public override bool InverseImplies {
+ get {
+ return opts.InverseImplies;
+ }
+ }
+
+ public override LineariserOptions SetAsTerm(bool newVal) {
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+ if (newVal == AsTerm)
+ return this;
+ return new Z3LineariserOptions(newVal, opts, LetVariables);
+ }
+
+ // variables representing formulas in let-bindings have to be
+ // printed in a different way than other variables
+ private readonly List<VCExprVar/*!>!*/> LetVariablesAttr;
+ public override List<VCExprVar/*!>!*/> LetVariables {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+
+ return LetVariablesAttr;
+ }
+ }
+
+ public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
+ //Contract.Requires(furtherVar != null);
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+ List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
+ allVars.AddRange(LetVariables);
+ allVars.Add(furtherVar);
+ return new Z3LineariserOptions(AsTerm, opts, allVars);
+ }
+
+ public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
+ //Contract.Requires(furtherVars != null);
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+ List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
+ allVars.AddRange(LetVariables);
+ allVars.AddRange(furtherVars);
+ return new Z3LineariserOptions(AsTerm, opts, allVars);
+ }
+ }
+
+ public class Z3apiProcessTheoremProver : ProverInterface
{
public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)
{
@@ -152,6 +291,16 @@ namespace Microsoft.Boogie.Z3 return outcome;
}
+ public override Outcome CheckOutcomeCore(ErrorHandler handler) {
+ if (outcome == Outcome.Invalid) {
+ foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {
+ List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
+ handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
+ }
+ }
+ return outcome;
+ }
+
private List<string> RemovePrefixes(List<string> labels)
{
List<string> result = new List<string>();
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 94184957..7c481438 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -162,14 +162,6 @@ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
<Name>VCGeneration</Name>
</ProjectReference>
- <ProjectReference Include="..\Simplify\Simplify.csproj">
- <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
- <Name>Simplify</Name>
- </ProjectReference>
- <ProjectReference Include="..\Z3\Z3.csproj">
- <Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
- <Name>Z3</Name>
- </ProjectReference>
</ItemGroup>
<ItemGroup>
<Compile Include="..\..\version.cs">
|