Some changes to support expanded use of z3api.

Should not affect function
of other provers. There is an option added in Check.cs to  allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).

1 files changed, 5 insertions, 4 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9b7b6e36..bb225071 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -100,8 +100,9 @@ namespace Microsoft.Boogie {
 

     /// <summary>

     /// Constructor.  Initialize a checker with the program and log file.

+    /// Optionally, use prover context provided by parameter "ctx". 

     /// </summary>

-    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {

+    public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {

       Contract.Requires(vcgen != null);

       Contract.Requires(prog != null);

       this.timeout = timeout;

@@ -121,7 +122,6 @@ namespace Microsoft.Boogie {
       options.Parse(CommandLineOptions.Clo.ProverOptions);

 

       ContextCacheKey key = new ContextCacheKey(prog);

-      ProverContext ctx;

       ProverInterface prover;

 

       if (vcgen.CheckerCommonState == null) {

@@ -129,12 +129,13 @@ namespace Microsoft.Boogie {
       }

       IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;

 

-      if (cachedContexts.TryGetValue(key, out ctx)) {

+      if (ctx == null && cachedContexts.TryGetValue(key, out ctx))

+      {

         ctx = (ProverContext)cce.NonNull(ctx).Clone();

         prover = (ProverInterface)

           CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);

       } else {

-        ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

+        if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);

 

         // set up the context

         foreach (Declaration decl in prog.TopLevelDeclarations) {