From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Provers/Z3api/ProverLayer.cs | 706 ++++++++++++++++++------------------ 1 file changed, 353 insertions(+), 353 deletions(-) (limited to 'Source/Provers/Z3api/ProverLayer.cs') diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index d72705f3..cb7df8d7 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -1,354 +1,354 @@ -using System; -using System.Collections; -using System.Collections.Generic; -using System.Threading; -using System.IO; -using System.Diagnostics; -using Microsoft.Boogie.AbstractInterpretation; -using Microsoft.Boogie; -using Microsoft.Boogie.Z3; -using Microsoft.Boogie.VCExprAST; -using System.Diagnostics.Contracts; - -using TypeAst = System.IntPtr; -using TermAst = System.IntPtr; -using ConstDeclAst = System.IntPtr; -using ConstAst = System.IntPtr; -using Value = System.IntPtr; -using PatternAst = System.IntPtr; - -namespace Microsoft.Boogie.Z3 -{ - public class Z3InstanceOptions : ProverOptions { - public int Timeout { get { return TimeLimit / 1000; } } - public int Lets { - get { - Contract.Ensures(0 <= Contract.Result() && Contract.Result() < 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= Use the specified Z3Inspector binary. -OPTIMIZE_FOR_BV= Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. - -Obscure options: -~~~~~~~~~~~~~~~~ -DIST= Use z3-dist.exe binary. -REVERSE_IMPLIES= 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!*/> 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() != 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!*/> LetVariablesAttr; - public override List!*/> LetVariables { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - return LetVariablesAttr; - } - } - - public override LineariserOptions AddLetVariable(VCExprVar furtherVar) { - //Contract.Requires(furtherVar != null); - Contract.Ensures(Contract.Result() != null); - - List!*/> allVars = new List(); - allVars.AddRange(LetVariables); - allVars.Add(furtherVar); - return new Z3LineariserOptions(AsTerm, opts, allVars); - } - - public override LineariserOptions AddLetVariables(List!*/> furtherVars) { - //Contract.Requires(furtherVars != null); - Contract.Ensures(Contract.Result() != null); - - List!*/> allVars = new List(); - allVars.AddRange(LetVariables); - allVars.AddRange(furtherVars); - return new Z3LineariserOptions(AsTerm, opts, allVars); - } - } - - public class Z3apiProcessTheoremProver : ProverInterface - { - public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt) - { - this.options = opts; - this.context = (Z3apiProverContext) ctxt; - this.numAxiomsPushed = 0; - } - - private Z3InstanceOptions options; - - private Z3apiProverContext context; - public override ProverContext Context - { - get { return context; } - } - - public override VCExpressionGenerator VCExprGen - { - get { return context.ExprGen; } - } - - private int numAxiomsPushed; - - public override void Close() - { - base.Close(); - context.CloseLog(); - context.z3.Dispose(); - context.config.Dispose(); - } - - public void PushAxiom(VCExpr axiom) - { - context.CreateBacktrackPoint(); - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - context.AddAxiom(axiom, linOptions); - } - - private void PushConjecture(VCExpr conjecture) - { - context.CreateBacktrackPoint(); - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - context.AddConjecture(conjecture, linOptions); - } - - public override void PushVCExpression(VCExpr vc) - { - PushAxiom(vc); - numAxiomsPushed++; - } - - public void CreateBacktrackPoint() - { - context.CreateBacktrackPoint(); - } - - public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) - { - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - Push(); - context.AddAxiom(context.Axioms, linOptions); - context.AddConjecture(vc, linOptions); - outcome = context.Check(out z3LabelModels); - Pop(); - } - - public override void Check() - { - outcome = context.Check(out z3LabelModels); - } - - public override ProverInterface.Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) - { - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore); - } - - public override void Push() - { - context.CreateBacktrackPoint(); - } - - public override void Pop() - { - context.Backtrack(); - } - - public override void Assert(VCExpr vc, bool polarity) - { - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - if (polarity) - context.AddAxiom(vc, linOptions); - else - context.AddConjecture(vc, linOptions); - } - - public override void AssertAxioms() - { - LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); - context.AddAxiom(context.Axioms, linOptions); - } - - // Number of axioms pushed since the last call to FlushAxioms - public override int NumAxiomsPushed() - { - return numAxiomsPushed; - } - - public override int FlushAxiomsToTheoremProver() - { - var ret = numAxiomsPushed; - numAxiomsPushed = 0; - return ret; - } - - private Outcome outcome; - private List z3LabelModels = new List(); - - [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler) - { - if (outcome == Outcome.Invalid) - { - foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) - { - List unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); - handler.OnModel(unprefixedLabels, z3LabelModel.Model); - } - } - return outcome; - } - - public override Outcome CheckOutcomeCore(ErrorHandler handler) { - if (outcome == Outcome.Invalid) { - foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) { - List unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); - handler.OnModel(unprefixedLabels, z3LabelModel.Model); - } - } - return outcome; - } - - private List RemovePrefixes(List labels) - { - List result = new List(); - foreach (string label in labels) - { - if (label.StartsWith("+")) - { - result.Add(label.Substring(1)); - } - else if (label.StartsWith("|")) - { - result.Add(label.Substring(1)); - } - else if (label.StartsWith("@")) - { - result.Add(label.Substring(1)); - } - else - throw new Exception("Unknown prefix in label " + label); - } - return result; - } - } -} - -namespace Microsoft.Boogie.Z3api -{ - public class Factory : ProverFactory - { - public override object SpawnProver(ProverOptions options, object ctxt) - { - return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt); - } - - public override object NewProverContext(ProverOptions opts) - { - if (CommandLineOptions.Clo.BracketIdsInVC < 0) - { - CommandLineOptions.Clo.BracketIdsInVC = 0; - } - - VCExpressionGenerator gen = new VCExpressionGenerator(); - return new Z3apiProverContext((Z3InstanceOptions)opts, gen); - } - - public override ProverOptions BlankProverOptions() - { - return new Z3InstanceOptions(); - } - } +using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Boogie.VCExprAST; +using System.Diagnostics.Contracts; + +using TypeAst = System.IntPtr; +using TermAst = System.IntPtr; +using ConstDeclAst = System.IntPtr; +using ConstAst = System.IntPtr; +using Value = System.IntPtr; +using PatternAst = System.IntPtr; + +namespace Microsoft.Boogie.Z3 +{ + public class Z3InstanceOptions : ProverOptions { + public int Timeout { get { return TimeLimit / 1000; } } + public int Lets { + get { + Contract.Ensures(0 <= Contract.Result() && Contract.Result() < 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= Use the specified Z3Inspector binary. +OPTIMIZE_FOR_BV= Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. + +Obscure options: +~~~~~~~~~~~~~~~~ +DIST= Use z3-dist.exe binary. +REVERSE_IMPLIES= 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!*/> 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() != 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!*/> LetVariablesAttr; + public override List!*/> LetVariables { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + + return LetVariablesAttr; + } + } + + public override LineariserOptions AddLetVariable(VCExprVar furtherVar) { + //Contract.Requires(furtherVar != null); + Contract.Ensures(Contract.Result() != null); + + List!*/> allVars = new List(); + allVars.AddRange(LetVariables); + allVars.Add(furtherVar); + return new Z3LineariserOptions(AsTerm, opts, allVars); + } + + public override LineariserOptions AddLetVariables(List!*/> furtherVars) { + //Contract.Requires(furtherVars != null); + Contract.Ensures(Contract.Result() != null); + + List!*/> allVars = new List(); + allVars.AddRange(LetVariables); + allVars.AddRange(furtherVars); + return new Z3LineariserOptions(AsTerm, opts, allVars); + } + } + + public class Z3apiProcessTheoremProver : ProverInterface + { + public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt) + { + this.options = opts; + this.context = (Z3apiProverContext) ctxt; + this.numAxiomsPushed = 0; + } + + private Z3InstanceOptions options; + + private Z3apiProverContext context; + public override ProverContext Context + { + get { return context; } + } + + public override VCExpressionGenerator VCExprGen + { + get { return context.ExprGen; } + } + + private int numAxiomsPushed; + + public override void Close() + { + base.Close(); + context.CloseLog(); + context.z3.Dispose(); + context.config.Dispose(); + } + + public void PushAxiom(VCExpr axiom) + { + context.CreateBacktrackPoint(); + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + context.AddAxiom(axiom, linOptions); + } + + private void PushConjecture(VCExpr conjecture) + { + context.CreateBacktrackPoint(); + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + context.AddConjecture(conjecture, linOptions); + } + + public override void PushVCExpression(VCExpr vc) + { + PushAxiom(vc); + numAxiomsPushed++; + } + + public void CreateBacktrackPoint() + { + context.CreateBacktrackPoint(); + } + + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + Push(); + context.AddAxiom(context.Axioms, linOptions); + context.AddConjecture(vc, linOptions); + outcome = context.Check(out z3LabelModels); + Pop(); + } + + public override void Check() + { + outcome = context.Check(out z3LabelModels); + } + + public override ProverInterface.Outcome CheckAssumptions(List assumptions, out List unsatCore, ErrorHandler handler) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore); + } + + public override void Push() + { + context.CreateBacktrackPoint(); + } + + public override void Pop() + { + context.Backtrack(); + } + + public override void Assert(VCExpr vc, bool polarity) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + if (polarity) + context.AddAxiom(vc, linOptions); + else + context.AddConjecture(vc, linOptions); + } + + public override void AssertAxioms() + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); + context.AddAxiom(context.Axioms, linOptions); + } + + // Number of axioms pushed since the last call to FlushAxioms + public override int NumAxiomsPushed() + { + return numAxiomsPushed; + } + + public override int FlushAxiomsToTheoremProver() + { + var ret = numAxiomsPushed; + numAxiomsPushed = 0; + return ret; + } + + private Outcome outcome; + private List z3LabelModels = new List(); + + [NoDefaultContract] + public override Outcome CheckOutcome(ErrorHandler handler) + { + if (outcome == Outcome.Invalid) + { + foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) + { + List unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); + handler.OnModel(unprefixedLabels, z3LabelModel.Model); + } + } + return outcome; + } + + public override Outcome CheckOutcomeCore(ErrorHandler handler) { + if (outcome == Outcome.Invalid) { + foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) { + List unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); + handler.OnModel(unprefixedLabels, z3LabelModel.Model); + } + } + return outcome; + } + + private List RemovePrefixes(List labels) + { + List result = new List(); + foreach (string label in labels) + { + if (label.StartsWith("+")) + { + result.Add(label.Substring(1)); + } + else if (label.StartsWith("|")) + { + result.Add(label.Substring(1)); + } + else if (label.StartsWith("@")) + { + result.Add(label.Substring(1)); + } + else + throw new Exception("Unknown prefix in label " + label); + } + return result; + } + } +} + +namespace Microsoft.Boogie.Z3api +{ + public class Factory : ProverFactory + { + public override object SpawnProver(ProverOptions options, object ctxt) + { + return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt); + } + + public override object NewProverContext(ProverOptions opts) + { + if (CommandLineOptions.Clo.BracketIdsInVC < 0) + { + CommandLineOptions.Clo.BracketIdsInVC = 0; + } + + VCExpressionGenerator gen = new VCExpressionGenerator(); + return new Z3apiProverContext((Z3InstanceOptions)opts, gen); + } + + public override ProverOptions BlankProverOptions() + { + return new Z3InstanceOptions(); + } + } } \ No newline at end of file -- cgit v1.2.3