Boogie: Get rid of {:ignore} feature on axioms

8 files changed, 6 insertions, 24 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index f23f4833..de1fdb00 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1846,7 +1846,6 @@ namespace Microsoft.Boogie {
 

     {:ignore}

       Ignore the declaration (after checking for duplicate names).

-      See also below for more options when :ignore is used with axioms.

 

     {:extern}

       If two top-level declarations introduce the same name (for example, two

@@ -1865,14 +1864,6 @@ namespace Microsoft.Boogie {
       Makes Boogie replace f(VARS) with expr(VARS) everywhere just before

       doing VC generation.

 

-    {:ignore ""p,q..""}

-      Exclude the axiom when generating VC for a prover supporting any

-      of the features 'p', 'q', ...

-      All the provers support the feature 'all'.

-      Simplify supports 'simplify' and 'simplifyLike'.

-      Z3 supports 'z3', 'simplifyLike' and either 'bvInt' (if the /bv:i

-      option is passed) or 'bvDefSem' (for /bv:z).

-

   ---- On implementations and procedures -------------------------------------

 

      {:inline N}

diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs
index 8bf6bbf0..35913019 100644
--- a/Source/Provers/Isabelle/Prover.cs
+++ b/Source/Provers/Isabelle/Prover.cs
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.Isabelle {
     public readonly bool AllTypes;

 

     public IsabelleContext(string outputFilename, bool allTypes)

-      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "bvInt", "bvDefSem", "bvint", "bvz", "external" })) {

+      : base(new VCExpressionGenerator(), new VCGenerationOptions(new List<string/*!*/> { "isabelle", "external" })) {

       Contract.Requires(outputFilename != null);

 

       this.OutputFilename = outputFilename;

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index cd5cdb31..d5e9b797 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -863,11 +863,12 @@ namespace Microsoft.Boogie.SMTLib
 

       VCExpressionGenerator gen = new VCExpressionGenerator();

       List<string>/*!>!*/ proverCommands = new List<string/*!*/>();

-      proverCommands.Add("all");

       proverCommands.Add("smtlib");

       var opts = (SMTLibProverOptions)options ;

       if (opts.UseZ3)

         proverCommands.Add("z3");

+      else

+        proverCommands.Add("external");

       VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

       return new SMTLibProverContext(gen, genOptions);

     }

diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs
index 497911ab..4584b2e7 100644
--- a/Source/Provers/Simplify/ProverInterface.cs
+++ b/Source/Provers/Simplify/ProverInterface.cs
@@ -848,9 +848,7 @@ namespace Microsoft.Boogie.Simplify {
       Contract.Assert(gen != null);

       List<string>/*!>!*/ proverCommands = new List<string> ();

       Contract.Assert(cce.NonNullElements(proverCommands));

-      proverCommands.Add("all");

       proverCommands.Add("simplify");

-      proverCommands.Add("simplifyLike");

       return new DeclFreeProverContext(gen, new VCGenerationOptions(proverCommands));

     }

 

diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index d18535e2..424e36ac 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -323,10 +323,8 @@ USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool
 

       VCExpressionGenerator gen = new VCExpressionGenerator();

       List<string>/*!>!*/ proverCommands = new List<string/*!*/>();

-      // TODO: what is supported?

-      //      proverCommands.Add("all");

-      //      proverCommands.Add("simplify");

-      //      proverCommands.Add("simplifyLike");

+      proverCommands.Add("tptp");

+      proverCommands.Add("external");

       VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

       Contract.Assert(genOptions != null);

 

diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 3194fa63..388cf91b 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -393,10 +393,8 @@ REVERSE_IMPLIES=<bool>    Encode P==>Q as Q||!P.
       Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)options);

       VCExpressionGenerator gen = new VCExpressionGenerator ();

       List<string/*!>!*/> proverCommands = new List<string/*!*/> ();

-      proverCommands.Add("all");

       proverCommands.Add("z3");

       proverCommands.Add("simplifyLike");

-      proverCommands.Add("bvDefSem");

       VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);

       

       return NewProverContext(gen, genOptions, opts);

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 4d8fed6a..4555f18c 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -17,6 +17,7 @@ using Microsoft.Basetypes;
 namespace Microsoft.Boogie.VCExprAST {

   using Microsoft.Boogie;

 

+  // TODO: in future we might use that for defining symbols for Boogie's conditional compilation 

   public class VCGenerationOptions {

     private readonly List<string/*!*/>/*!*/ SupportedProverCommands;

     [ContractInvariantMethod]

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 7cb9a404..bf27144b 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -158,11 +158,6 @@ public abstract class ProverContextContracts:ProverContext{
     public override void AddAxiom(Axiom ax, string attributes) {//Contract.Requires(ax != null);

       base.AddAxiom(ax, attributes);

 

-      string ignore = ax.FindStringAttribute("ignore");

-      if (ignore != null && genOptions.IsAnyProverCommandSupported(ignore)) {

-        return;

-      }

-

       axiomConjuncts.Add(translator.Translate(ax.Expr));

     }