diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-10-27 17:36:29 -0700 |
| commit | a8c04614ad34b4a36c1c739f8838fe4fd6232720 (patch) | |
| tree | 73c080b032638d7e046f7e1d18d5fa7a2273c181 /Source/Provers | |
| parent | 51fe0a74abb863a3bb908e6fced5b9779446d065 (diff) | |
Boogie: Get rid of {:ignore} feature on axioms
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/Isabelle/Prover.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 3 | ||||
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/TPTP/ProverInterface.cs | 6 | ||||
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 2 |
5 files changed, 5 insertions, 10 deletions
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);
|