summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2010-08-23 06:02:26 +0000
committerGravatar qadeer <unknown>2010-08-23 06:02:26 +0000
commitb70795fd8b275d77ca5ee9056233c0742bd50c35 (patch)
treeb72ce87546abd103de52961492771238249b0ed4
parentd2dbcb56f7b92ca7684182d120d02a697bfa368d (diff)
further fixes to Z3api project trying to make it work; still a long way off.
-rw-r--r--Source/BoogieDriver/BoogieDriver.csproj6
-rw-r--r--Source/Provers/Z3/ProverInterface.cs18
-rw-r--r--Source/Provers/Z3api/ContextLayer.cs41
-rw-r--r--Source/Provers/Z3api/ProverLayer.cs147
-rw-r--r--Source/Provers/Z3api/SafeContext.cs35
-rw-r--r--Source/Provers/Z3api/StubContext.cs4
-rw-r--r--Source/Provers/Z3api/TypeAdapter.cs65
-rw-r--r--Source/Provers/Z3api/VCExprVisitor.cs88
-rw-r--r--Source/Provers/Z3api/Z3api.csproj14
9 files changed, 142 insertions, 276 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 51cb7f2f..b572dd6f 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -3,7 +3,7 @@
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.30729</ProductVersion>
+ <ProductVersion>9.0.21022</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}</ProjectGuid>
<OutputType>Exe</OutputType>
@@ -121,6 +121,10 @@
<Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
<Name>SMTLib</Name>
</ProjectReference>
+ <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">
+ <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>
+ <Name>Z3api</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\Z3\Z3.csproj">
<Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
<Name>Z3</Name>
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index bcf55c4c..3813c63b 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -155,7 +155,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
}
}
- internal class Z3LineariserOptions : LineariserOptions {
+ public class Z3LineariserOptions : LineariserOptions {
private readonly Z3InstanceOptions opts;
[ContractInvariantMethod]
@@ -169,7 +169,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
return opts.BitVectors;
} }
- internal Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {
+ public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {
Contract.Requires(opts != null);
Contract.Requires(cce.NonNullElements(letVariables));
@@ -415,8 +415,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
proverCommands.Add("bvInt");
VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
-
- return new DeclFreeProverContext(gen, genOptions);
+ return NewProverContext(gen, genOptions, opts);
}
public override ProverOptions BlankProverOptions()
@@ -426,8 +425,8 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
}
protected virtual Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx,
- Z3InstanceOptions opts) {
+ DeclFreeProverContext ctx,
+ Z3InstanceOptions opts) {
Contract.Requires(gen != null);
Contract.Requires(ctx != null);
Contract.Requires(opts != null);
@@ -435,5 +434,12 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
return new Z3ProcessTheoremProver(gen, ctx, opts);
}
+
+ protected virtual DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,
+ VCGenerationOptions genOptions,
+ Z3InstanceOptions opts)
+ {
+ return new DeclFreeProverContext(gen, genOptions);
+ }
}
}
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs
index 532b1932..e3ba1fa7 100644
--- a/Source/Provers/Z3api/ContextLayer.cs
+++ b/Source/Provers/Z3api/ContextLayer.cs
@@ -15,30 +15,20 @@ namespace Microsoft.Boogie.Z3
{
public class Z3Config
{
+ ~Z3Config()
+ {
+ config.Dispose();
+ }
private Config config = new Config();
private int counterexamples;
private string logFilename;
private List<string> debugTraces = new List<string>();
- public void SetPartialModels(bool enabled)
- {
- config.SetParamValue("PARTIAL_MODELS", (enabled ? "true" : "false"));
- }
public void SetModelCompletion(bool enabled)
{
config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));
}
- public void SetHideUnusedPartitions(bool enabled)
- {
- config.SetParamValue("HIDE_UNUSED_PARTITIONS", (enabled ? "true" : "false"));
- }
-
- public void SetMAM(string mamNumber)
- {
- config.SetParamValue("MAM", mamNumber);
- }
-
public void SetModel(bool enabled)
{
config.SetParamValue("MODEL", (enabled ? "true" : "false"));
@@ -54,11 +44,6 @@ namespace Microsoft.Boogie.Z3
config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));
}
- public void SetReflectBvOps(bool enabled)
- {
- config.SetParamValue("REFLECT_BV_OPS", (enabled ? "true" : "false"));
- }
-
public void SetCounterExample(int counterexample)
{
this.counterexamples = counterexample;
@@ -93,16 +78,6 @@ namespace Microsoft.Boogie.Z3
}
}
- public abstract class Z3ContextFactory
- {
-
- public static Z3Context BuildZ3Context(Z3Config config, VCExpressionGenerator gen)
- {
- return new Z3SafeContext(config, gen);
- }
- }
-
-
public abstract class Z3TermAst { }
public abstract class Z3PatternAst { }
public abstract class Z3ConstDeclAst { }
@@ -112,8 +87,8 @@ namespace Microsoft.Boogie.Z3
{
void CreateBacktrackPoint();
void Backtrack();
- void AddAxiom(VCExpr vc);
- void AddConjecture(VCExpr vc);
+ void AddAxiom(VCExpr vc, LineariserOptions linOptions);
+ void AddConjecture(VCExpr vc, LineariserOptions linOptions);
void AddSmtlibString(string smtlibString);
string GetDeclName(Z3ConstDeclAst constDeclAst);
Z3PatternAst MakePattern(List<Z3TermAst> exprs);
@@ -142,7 +117,7 @@ namespace Microsoft.Boogie.Z3
private int partitionCounter = FAKE_PARTITION;
public int GetPartition(int valueHash)
{
- if (partitionToValueHash.ContainsKey(valueHash))
+ if (!partitionToValueHash.ContainsKey(valueHash))
{
partitionCounter++;
partitionToValueHash.Add(valueHash, partitionCounter);
@@ -234,7 +209,7 @@ namespace Microsoft.Boogie.Z3
string c_name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
Term v = z3Model.Eval(c, new Term[0]);
Sort s = v.GetSort();
- Context ctx = new Context(null); // placeholder.
+ Context ctx = ((Z3SafeContext)container).z3;
Sort boolSort = ctx.MkBoolSort();
Sort intSort = ctx.MkIntSort();
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 02362edf..f3dfab69 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -20,84 +20,31 @@ using PatternAst = System.IntPtr;
namespace Microsoft.Boogie.Z3
{
- public class Z3ThreadTheoremProver : ProverInterface
+ public class Z3apiProcessTheoremProver : Z3ProcessTheoremProver
{
- protected DeclFreeProverContext ctx;
- protected VCExpressionGenerator gen;
- public override ProverContext Context
+ public Z3apiProcessTheoremProver(VCExpressionGenerator gen,
+ DeclFreeProverContext ctx,
+ Z3InstanceOptions opts)
+ : base(gen, ctx, opts)
{
- get { return this.ctx; }
- }
- public override VCExpressionGenerator VCExprGen
- {
- get { return this.gen; }
- }
-
- private int timeout;
- private Z3Context cm;
-
- public Z3ThreadTheoremProver(Z3InstanceOptions proverOptions)
- : base()
- {
- gen = new VCExpressionGenerator();
-
- string codebaseString = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
- string backgroundPredicates;
-
- // Initialize '_backgroundPredicates'
- string univBackPredPath = Path.Combine(codebaseString,
- // yes, using .NeedsTypes here is an ugly hack...
- "Z3API_UnivBackPred.smt");
- using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
- {
- backgroundPredicates = reader.ReadToEnd();
- }
-
- Z3Config config = BuildConfig(timeout, true);
- Z3Context cm = Z3ContextFactory.BuildZ3Context(config, gen);
- Z3ThreadProverContext ctx = new Z3ThreadProverContext(gen, cm);
-
- this.cm = cm;
- cm.AddSmtlibString(backgroundPredicates);
this.z3ContextIsUsed = false;
}
- private static Z3Config BuildConfig(int timeout, bool nativeBv)
- {
- Z3Config config = new Z3Config();
- config.SetPartialModels(true);
- config.SetModelCompletion(false);
- config.SetHideUnusedPartitions(false);
- config.SetModel(true);
-
- if (0 <= CommandLineOptions.Clo.ProverCCLimit)
- {
- config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);
- }
-
- if (0 <= timeout)
- {
- config.SetSoftTimeout(timeout.ToString());
- }
-
- config.SetTypeCheck(true);
- if (nativeBv)
- config.SetReflectBvOps(true);
-
- return config;
- }
-
private bool z3ContextIsUsed;
public void PushAxiom(VCExpr axiom)
{
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
cm.CreateBacktrackPoint();
- cm.AddAxiom((VCExpr)axiom);
+ LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+ cm.AddAxiom((VCExpr)axiom, linOptions);
}
private void PushConjecture(VCExpr conjecture)
{
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
cm.CreateBacktrackPoint();
- cm.AddConjecture((VCExpr)conjecture);
+ LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+ cm.AddConjecture((VCExpr)conjecture, linOptions);
}
public void PrepareCheck(string descriptiveName, VCExpr vc)
@@ -108,31 +55,33 @@ namespace Microsoft.Boogie.Z3
public void BeginPreparedCheck()
{
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
outcome = Outcome.Undetermined;
outcome = cm.Check(out z3LabelModels);
}
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
+ LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
if (z3ContextIsUsed)
{
cm.Backtrack();
}
else
{
- cm.AddAxiom((VCExpr)ctx.Axioms);
+ cm.AddAxiom((VCExpr)ctx.Axioms, linOptions);
z3ContextIsUsed = true;
}
cm.CreateBacktrackPoint();
- cm.AddConjecture((VCExpr)vc);
+ cm.AddConjecture((VCExpr)vc, linOptions);
BeginPreparedCheck();
}
private Outcome outcome;
private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();
- private UnexpectedProverOutputException proverException = null;
[NoDefaultContract]
public override Outcome CheckOutcome(ErrorHandler handler)
@@ -141,7 +90,7 @@ namespace Microsoft.Boogie.Z3
{
foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
{
- List<string> unprefixedLabels = RemovePreffixes(z3LabelModel.RelevantLabels);
+ List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
}
}
@@ -150,14 +99,16 @@ namespace Microsoft.Boogie.Z3
public void CreateBacktrackPoint()
{
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
cm.CreateBacktrackPoint();
}
override public void Pop()
{
+ Z3SafeContext cm = ((Z3apiProverContext)ctx).cm;
cm.Backtrack();
}
- private List<string> RemovePreffixes(List<string> labels)
+ private List<string> RemovePrefixes(List<string> labels)
{
List<string> result = new List<string>();
foreach (string label in labels)
@@ -175,22 +126,42 @@ namespace Microsoft.Boogie.Z3
result.Add(label.Substring(1));
}
else
- throw new Exception("Unknown preffix in label " + label);
+ throw new Exception("Unknown prefix in label " + label);
}
return result;
}
-
}
- public class Z3ThreadProverContext : DeclFreeProverContext
+ public class Z3apiProverContext : DeclFreeProverContext
{
+ public Z3SafeContext cm;
+
+ public Z3apiProverContext(VCExpressionGenerator gen,
+ VCGenerationOptions genOptions,
+ Z3InstanceOptions opts)
+ : base(gen, genOptions)
+ {
+ Z3Config config = BuildConfig(opts.Timeout, true);
+ this.cm = new Z3SafeContext(config, gen);
+ }
+ private static Z3Config BuildConfig(int timeout, bool nativeBv)
+ {
+ Z3Config config = new Z3Config();
+ config.SetModelCompletion(false);
+ config.SetModel(true);
- private Z3Context cm;
+ if (0 <= CommandLineOptions.Clo.ProverCCLimit)
+ {
+ config.SetCounterExample(CommandLineOptions.Clo.ProverCCLimit);
+ }
- public Z3ThreadProverContext(VCExpressionGenerator gen, Z3Context cm)
- : base(gen, null)
- {
- this.cm = cm;
+ if (0 <= timeout)
+ {
+ config.SetSoftTimeout(timeout.ToString());
+ }
+
+ config.SetTypeCheck(true);
+ return config;
}
public override void DeclareType(TypeCtorDecl t, string attributes)
@@ -205,7 +176,6 @@ namespace Microsoft.Boogie.Z3
cm.DeclareConstant(c.Name, c.TypedIdent.Type);
}
-
public override void DeclareFunction(Function f, string attributes)
{
base.DeclareFunction(f, attributes);
@@ -231,23 +201,20 @@ namespace Microsoft.Boogie.Z3
namespace Microsoft.Boogie.Z3api
{
-
- public class Factory : ProverFactory
+ public class Factory : Microsoft.Boogie.Z3.Factory
{
- public override object SpawnProver(ProverOptions popts, object ctxt)
+ protected override Z3ProcessTheoremProver SpawnProver(VCExpressionGenerator gen,
+ DeclFreeProverContext ctx,
+ Z3InstanceOptions opts)
{
- Z3InstanceOptions options = (Z3InstanceOptions) popts;
- if (CommandLineOptions.Clo.BracketIdsInVC < 0)
- {
- CommandLineOptions.Clo.BracketIdsInVC = 0;
- }
-
- return new Z3ThreadTheoremProver(options);
+ return new Z3apiProcessTheoremProver(gen, ctx, opts);
}
- public override object NewProverContext(ProverOptions options)
+ protected override DeclFreeProverContext NewProverContext(VCExpressionGenerator gen,
+ VCGenerationOptions genOptions,
+ Z3InstanceOptions opts)
{
- throw new NotImplementedException();
+ return new Z3apiProverContext(gen, genOptions, opts);
}
}
} \ No newline at end of file
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs
index 26e7385d..70b7f35c 100644
--- a/Source/Provers/Z3api/SafeContext.cs
+++ b/Source/Provers/Z3api/SafeContext.cs
@@ -81,13 +81,16 @@ namespace Microsoft.Boogie.Z3
public class Z3SafeContext : Z3Context
{
-
private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
internal BacktrackDictionary<string, Z3TypeSafeTerm> constants = new BacktrackDictionary<string, Z3TypeSafeTerm>();
internal BacktrackDictionary<string, Z3TypeSafeConstDecl> functions = new BacktrackDictionary<string, Z3TypeSafeConstDecl>();
internal BacktrackDictionary<string, Z3TypeSafeTerm> labels = new BacktrackDictionary<string, Z3TypeSafeTerm>();
- private Context z3;
+ ~Z3SafeContext()
+ {
+ z3.Dispose();
+ }
+ public Context z3;
private Z3Config config;
public void CreateBacktrackPoint()
@@ -108,19 +111,19 @@ namespace Microsoft.Boogie.Z3
symbols.Backtrack();
}
- public void AddAxiom(VCExpr vc)
+ public void AddAxiom(VCExpr vc, LineariserOptions linOptions)
{
Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);
- Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, null);
+ Z3TermAst z3ast = (Z3TermAst)vc.Accept(visitor, linOptions);
Term term = Unwrap(z3ast);
z3.AssertCnstr(term);
}
- public void AddConjecture(VCExpr vc)
+ public void AddConjecture(VCExpr vc, LineariserOptions linOptions)
{
VCExpr not_vc = (VCExpr)this.gen.Not(vc);
Z3apiExprLineariser visitor = new Z3apiExprLineariser(this);
- Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, null);
+ Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);
Term term = Unwrap(z3ast);
z3.AssertCnstr(term);
}
@@ -281,7 +284,7 @@ namespace Microsoft.Boogie.Z3
return false;
for (int i = 0; i < l.Count; i++)
- if (l[i].Equals(r[i]))
+ if (!l[i].Equals(r[i]))
return false;
return true;
}
@@ -295,7 +298,7 @@ namespace Microsoft.Boogie.Z3
{
Symbol sym = relevantLabels.GetLabel(i);
string labelName = z3.GetSymbolString(sym);
- if (labelName.StartsWith("@"))
+ if (!labelName.StartsWith("@"))
{
relevantLabels.Disable(i);
}
@@ -322,7 +325,6 @@ namespace Microsoft.Boogie.Z3
System.Console.WriteLine("---");
}
-
public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors)
{
boogieErrors = new List<Z3ErrorModelAndLabels>();
@@ -380,7 +382,7 @@ namespace Microsoft.Boogie.Z3
private VCExpressionGenerator gen;
- internal Z3SafeContext(Z3Config config, VCExpressionGenerator gen)
+ public Z3SafeContext(Z3Config config, VCExpressionGenerator gen)
{
Context z3 = new Context(config.Config);
// TBD: z3.EnableArithmetic();
@@ -390,7 +392,7 @@ namespace Microsoft.Boogie.Z3
z3.EnableDebugTrace(tag);
this.z3 = z3;
this.config = config;
- this.tm = new Z3TransformerTypeCache(new Z3SafeTypeBuilder(z3), new IntTransformer());
+ this.tm = new Z3TypeCachedBuilder(new Z3SafeTypeBuilder(z3));
this.gen = gen;
}
@@ -448,13 +450,13 @@ namespace Microsoft.Boogie.Z3
private Symbol GetSymbol(string symbolName)
{
- if (symbols.ContainsKey(symbolName))
+ if (!symbols.ContainsKey(symbolName))
{
Symbol symbolAst = z3.MkSymbol(symbolName);
symbols.Add(symbolName, symbolAst);
}
Symbol result;
- if (symbols.TryGetValue(symbolName, out result))
+ if (!symbols.TryGetValue(symbolName, out result))
throw new Exception("symbol " + symbolName + " is undefined");
return result;
}
@@ -462,10 +464,10 @@ namespace Microsoft.Boogie.Z3
public Z3TermAst GetConstant(string constantName, Type constantType)
{
Z3TypeSafeTerm typeSafeTerm;
- if (constants.ContainsKey(constantName))
+ if (!constants.ContainsKey(constantName))
this.DeclareConstant(constantName, constantType);
- if (constants.TryGetValue(constantName, out typeSafeTerm))
+ if (!constants.TryGetValue(constantName, out typeSafeTerm))
throw new Exception("constant " + constantName + " is not defined");
return typeSafeTerm;
}
@@ -548,7 +550,7 @@ namespace Microsoft.Boogie.Z3
private FuncDecl GetFunction(string functionName)
{
Z3TypeSafeConstDecl function;
- if (functions.TryGetValue(functionName, out function))
+ if (!functions.TryGetValue(functionName, out function))
throw new Exception("function " + functionName + " is undefined");
FuncDecl unwrapFunction = Unwrap(function);
return unwrapFunction;
@@ -557,7 +559,6 @@ namespace Microsoft.Boogie.Z3
public class Z3SafeTypeBuilder : Z3TypeBuilder
{
-
protected Context z3;
public Z3SafeTypeBuilder(Context z3)
diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index 80f1776e..e4dd9318 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -19,8 +19,8 @@ namespace Microsoft.Boogie.Z3 {
public void CreateBacktrackPoint(){}
public void Backtrack(){}
- public void AddAxiom(VCExpr vc) {}
- public void AddConjecture(VCExpr vc){}
+ public void AddAxiom(VCExpr vc, LineariserOptions linOptions) {}
+ public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}
public void AddSmtlibString(string smtlibString) {}
public string GetDeclName(Z3ConstDeclAst constDeclAst) {
return "";
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs
index 553205b1..280e93e9 100644
--- a/Source/Provers/Z3api/TypeAdapter.cs
+++ b/Source/Provers/Z3api/TypeAdapter.cs
@@ -57,7 +57,7 @@ namespace Microsoft.Boogie.Z3
private Z3Type GetBvType(BvType bvType)
{
- if (bvTypes.ContainsKey(bvType))
+ if (!bvTypes.ContainsKey(bvType))
{
Z3Type typeAst = builder.BuildBvType(bvType);
bvTypes.Add(bvType, typeAst);
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie.Z3
private Z3Type GetBasicType(BasicType basicType)
{
- if (basicTypes.ContainsKey(basicType))
+ if (!basicTypes.ContainsKey(basicType))
{
Z3Type typeAst = builder.BuildBasicType(basicType);
basicTypes.Add(basicType, typeAst);
@@ -99,65 +99,4 @@ namespace Microsoft.Boogie.Z3
Z3Type BuildBvType(BvType bvType);
Z3Type BuildBasicType(BasicType basicType);
}
-
-
- internal class Z3TransformerTypeCache : Z3TypeCachedBuilder
- {
-
- private BoogieTypeTransformer transformer;
-
- public Z3TransformerTypeCache(Z3TypeBuilder builder, BoogieTypeTransformer transformer)
- : base(builder)
- {
- this.transformer = transformer;
- }
-
- public override Z3Type GetType(Type boogieType)
- {
- Type resolvedBoogieType = transformer.TransformType(boogieType);
- return base.GetType(resolvedBoogieType);
- }
- }
-
- internal abstract class BoogieTypeTransformer
- {
-
- protected abstract Type TransformBvType(BvType boogieType);
- protected abstract Type TransformBasicType(BasicType boogieType);
-
- public Type TransformType(Type boogieType)
- {
- return Dispatch(boogieType);
- }
-
- private Type Dispatch(Type boogieType)
- {
- if (boogieType.GetType().Equals(typeof(BvType)))
- return TransformBvType((BvType)boogieType);
- else if (boogieType.GetType().Equals(typeof(BasicType)))
- return TransformBasicType((BasicType)boogieType);
- else
- throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
- }
-
- }
-
- internal class IntTransformer : BoogieTypeTransformer
- {
-
- protected override Type TransformBvType(BvType bvType)
- {
- // registerBvType(bvType.Bits)
- return BasicType.Int;
- }
-
- protected override Type TransformBasicType(BasicType boogieType)
- {
- if (boogieType.IsBool)
- {
- // registerBool()
- }
- return BasicType.Int;
- }
- }
} \ No newline at end of file
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index ca32a824..25b674a7 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -14,7 +14,6 @@ using Microsoft.Boogie.VCExprAST;
namespace Microsoft.Boogie.Z3
{
- // Lineariser for expressions. The result (bool) is currently not used for anything
public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>
{
private Z3apiOpLineariser OpLinObject = null;
@@ -30,18 +29,12 @@ namespace Microsoft.Boogie.Z3
}
internal readonly UniqueNamer Namer;
- private readonly TextWriter wr;
-
protected Z3Context cm;
- protected Stack<Dictionary<string, VCExpr>> lets;
- protected Stack<List<string>> binders;
-
public Z3apiExprLineariser(Z3Context cm)
{
this.cm = cm;
- Stack<Dictionary<string, VCExpr>> lets = new Stack<Dictionary<string, VCExpr>>();
- Stack<List<string>> binders = new Stack<List<string>>();
+ this.Namer = new UniqueNamer();
}
public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)
@@ -53,39 +46,6 @@ namespace Microsoft.Boogie.Z3
/////////////////////////////////////////////////////////////////////////////////////
- private bool DeBruijnIndex(string variableName, out int deBruijnIndex)
- {
- deBruijnIndex = -1;
- foreach (List<string> binder in binders)
- {
- for (int i = binder.Count - 1; i >= 0; i--)
- {
- deBruijnIndex++;
- if (binder[i].Equals(variableName))
- return true;
- }
- }
- deBruijnIndex = -1;
- return false;
- }
-
- protected Z3TermAst FindDefinition(string variableName, Type variableType)
- {
- Z3TermAst termAst;
- int deBruijnIndex;
- if (DeBruijnIndex(variableName, out deBruijnIndex))
- {
- return cm.MakeBoundVariable((uint)deBruijnIndex, variableType);
- }
- else
- {
- termAst = cm.GetConstant(variableName, variableType);
- return termAst;
- }
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)
{
Contract.Requires(options != null);
@@ -142,8 +102,8 @@ namespace Microsoft.Boogie.Z3
{
Contract.Requires(options != null);
Contract.Requires(node != null);
-
- return FindDefinition(node.Name, node.Type);
+ string varName = Namer.GetName(node, node.Name);
+ return cm.GetConstant(varName, node.Type);
}
/////////////////////////////////////////////////////////////////////////////////////
@@ -154,7 +114,7 @@ namespace Microsoft.Boogie.Z3
Contract.Requires(node != null);
Contract.Assert(node.TypeParameters.Count == 0);
- binders.Push(new List<string>());
+ Namer.PushScope();
try
{
List<string> varNames;
@@ -211,7 +171,7 @@ namespace Microsoft.Boogie.Z3
}
finally
{
- binders.Pop();
+ Namer.PopScope();
}
}
@@ -221,9 +181,9 @@ namespace Microsoft.Boogie.Z3
varTypes = new List<Type>();
foreach (VCExprVar var in boundVars)
{
- varNames.Add(var.Name);
+ string varName = Namer.GetLocalName(var, var.Name);
+ varNames.Add(varName);
varTypes.Add(var.Type);
- binders.Peek().Add(var.Name);
}
}
@@ -260,24 +220,32 @@ namespace Microsoft.Boogie.Z3
public Z3TermAst Visit(VCExprLet node, LineariserOptions options)
{
+ Namer.PushScope();
try
{
- Dictionary<string, VCExpr> let = new Dictionary<string, VCExpr>();
- lets.Push(let);
+ List<Z3TermAst> equations = new List<Z3TermAst>();
foreach (VCExprLetBinding b in node)
{
- let.Add(b.V.Name, b.E);
+ string varName = Namer.GetLocalName(b.V, b.V.Name);
+ Z3TermAst varAst = cm.GetConstant(varName, b.V.Type);
+ Z3TermAst defAst = Linearise(b.E, options);
+ List<Z3TermAst> args = new List<Z3TermAst>();
+ args.Add(varAst);
+ args.Add(defAst);
+ equations.Add(cm.Make("EQ", args));
}
- Z3TermAst letAST = Linearise(node.Body, options);
- return letAST;
+ System.Diagnostics.Debug.Assert(equations.Count > 0);
+ Z3TermAst eqAst = cm.Make("AND", equations);
+ List<Z3TermAst> t = new List<Z3TermAst>();
+ t.Add(eqAst);
+ t.Add(Linearise(node.Body, options));
+ return cm.Make("IMPLIES", t);
}
finally
{
- lets.Pop();
+ Namer.PopScope();
}
- }
-
-
+ }
/////////////////////////////////////////////////////////////////////////////////////
@@ -546,28 +514,28 @@ namespace Microsoft.Boogie.Z3
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("intLess", node, options); // arguments are always terms
+ return WriteApplication("<", node, options); // arguments are always terms
}
public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("intAtMost", node, options); // arguments are always terms
+ return WriteApplication("<=", node, options); // arguments are always terms
}
public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("intGreater", node, options); // arguments are always terms
+ return WriteApplication(">", node, options); // arguments are always terms
}
public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("intAtLeast", node, options); // arguments are always terms
+ return WriteApplication(">=", node, options); // arguments are always terms
}
public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj
index 15dfa133..fb01ce94 100644
--- a/Source/Provers/Z3api/Z3api.csproj
+++ b/Source/Provers/Z3api/Z3api.csproj
@@ -3,13 +3,13 @@
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.30729</ProductVersion>
+ <ProductVersion>9.0.21022</ProductVersion>
<SchemaVersion>2.0</SchemaVersion>
<ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Z3api</RootNamespace>
- <AssemblyName>Z3api</AssemblyName>
+ <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace>
+ <AssemblyName>Provers.Z3api</AssemblyName>
<TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<StartupObject>
@@ -81,6 +81,10 @@
<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>
@@ -91,7 +95,9 @@
<Compile Include="ProverLayer.cs" />
<Compile Include="SafeContext.cs" />
<Compile Include="StubContext.cs" />
- <Compile Include="TypeAdapter.cs" />
+ <Compile Include="TypeAdapter.cs">
+ <SubType>Code</SubType>
+ </Compile>
<Compile Include="VCExprVisitor.cs" />
</ItemGroup>
</Project> \ No newline at end of file