summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/CommandLineOptions.cs5
-rw-r--r--Source/Core/VCExp.cs1
-rw-r--r--Source/Provers/Z3/Prover.cs7
-rw-r--r--Source/Provers/Z3/ProverInterface.cs33
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs19
-rw-r--r--Source/VCGeneration/Check.cs21
6 files changed, 14 insertions, 72 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 8647e79e..f23f4833 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -236,11 +236,6 @@ namespace Microsoft.Boogie {
public string/*?*/ ModelViewFile = null;
public int EnhancedErrorMessages = 0;
public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present
- public enum BvHandling {
- None,
- Z3Native,
- ToInt
- }
public bool UseArrayTheory = false;
public bool MonomorphicArrays {
get {
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index f6a976e5..6bc43e14 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -29,7 +29,6 @@ namespace Microsoft.Boogie {
public bool ForceLogStatus = false;
public int TimeLimit = 0;
public int MemoryLimit = 0;
- public CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;
public int Verbosity = 0;
public string ProverPath;
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 8929e732..6a066f1f 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -156,11 +156,8 @@ namespace Microsoft.Boogie.Z3
if (opts.Inspector != null)
AddOption(result, "PROGRESS_SAMPLING_FREQ", "100");
- if (opts.Typed) {
- AddOption(result, "TYPE_CHECK", "true");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
- AddOption(result, "BV_REFLECT", "true");
- }
+ AddOption(result, "TYPE_CHECK", "true");
+ AddOption(result, "BV_REFLECT", "true");
foreach (string opt in CommandLineOptions.Clo.Z3Options) {
Contract.Assert(opt != null);
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs
index 19097f8c..3194fa63 100644
--- a/Source/Provers/Z3/ProverInterface.cs
+++ b/Source/Provers/Z3/ProverInterface.cs
@@ -35,7 +35,7 @@ void ObjectInvariant()
[NotDelayed]
public Z3ProcessTheoremProver(VCExpressionGenerator gen,
- DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName,opts.Typed ? "TypedUnivBackPred2.sx" : "UnivBackPred2.sx")
+ DeclFreeProverContext ctx, Z3InstanceOptions opts):base(opts, gen, ctx, opts.ExeName, "TypedUnivBackPred2.sx")
{
Contract.Requires(gen != null);
Contract.Requires(ctx != null);
@@ -88,11 +88,6 @@ void ObjectInvariant()
public class Z3InstanceOptions : ProverOptions
{
public int Timeout { get { return TimeLimit / 1000; } }
- public bool Typed {
- get {
- return CommandLineOptions.Clo.Z3types || BitVectors == CommandLineOptions.BvHandling.Z3Native;
- }
- }
public int Lets {
get
{
@@ -164,10 +159,6 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
}
- public override CommandLineOptions.BvHandling Bitvectors { get {
- return opts.BitVectors;
- } }
-
public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables):base(asTerm) {
Contract.Requires(opts != null);
Contract.Requires(cce.NonNullElements(letVariables));
@@ -181,7 +172,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
} }
public override bool UseTypes { get {
- return opts.Typed;
+ return true;
} }
public override bool QuantifierIds { get {
@@ -254,7 +245,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
UniqueNamer namer = new UniqueNamer ();
Namer = namer;
this.DeclCollector =
- new TypeDeclCollector (namer, opts.BitVectors == CommandLineOptions.BvHandling.Z3Native);
+ new TypeDeclCollector (namer, true);
}
private Z3VCExprTranslator(Z3VCExprTranslator tl) :base(tl){
@@ -332,16 +323,9 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
Contract.Assert(sortedAxioms!=null);
- if (Opts.Typed) {
- DeclCollector.Collect(sortedAxioms);
- DeclCollector.Collect(sortedExpr);
- FeedTypeDeclsToProver();
- } else {
- TermFormulaFlattener flattener = new TermFormulaFlattener (Gen);
- Contract.Assert(flattener!=null);
- sortedExpr = flattener.Flatten(sortedExpr);
- sortedAxioms = flattener.Flatten(sortedAxioms);
- }
+ DeclCollector.Collect(sortedAxioms);
+ DeclCollector.Collect(sortedExpr);
+ FeedTypeDeclsToProver();
if (Opts.Lets != 3) {
// replace let expressions with implies
Let2ImpliesMutator letImplier = new Let2ImpliesMutator(Gen, Opts.Lets == 1, Opts.Lets == 2);
@@ -412,10 +396,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
proverCommands.Add("all");
proverCommands.Add("z3");
proverCommands.Add("simplifyLike");
- if (opts.BitVectors == CommandLineOptions.BvHandling.Z3Native)
- proverCommands.Add("bvDefSem");
- if (opts.BitVectors == CommandLineOptions.BvHandling.ToInt)
- proverCommands.Add("bvInt");
+ proverCommands.Add("bvDefSem");
VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
return NewProverContext(gen, genOptions, opts);
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 58c6ad7a..848fafcb 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -56,12 +56,6 @@ namespace Microsoft.Boogie.VCExprAST {
get;
}
- public virtual CommandLineOptions.BvHandling Bitvectors {
- get {
- return CommandLineOptions.BvHandling.None;
- }
- }
-
// variables representing formulas in let-bindings have to be
// printed in a different way than other variables
public virtual List<VCExprVar/*!*/>/*!*/ LetVariables {
@@ -89,19 +83,6 @@ namespace Microsoft.Boogie.VCExprAST {
Contract.Invariant(EmptyList != null);
}
-
- public bool NativeBv {
- get {
- return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
- }
- }
-
- public bool IntBv {
- get {
- return Bitvectors == CommandLineOptions.BvHandling.ToInt;
- }
- }
-
////////////////////////////////////////////////////////////////////////////////////////
protected LineariserOptions(bool asTerm) {
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 24e083d0..ff691828 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -33,7 +33,6 @@ namespace Microsoft.Boogie {
private readonly VCExpressionGenerator gen;
private ProverInterface thmProver;
- private CommandLineOptions.BvHandling bitvectors;
private int timeout;
// state for the async interface
@@ -48,12 +47,8 @@ namespace Microsoft.Boogie {
public readonly AutoResetEvent ProverDone = new AutoResetEvent(false);
- private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) {
- return CommandLineOptions.BvHandling.Z3Native;
- }
-
public bool WillingToHandle(Implementation impl, int timeout) {
- return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);
+ return !closed && timeout == this.timeout;
}
public VCExpressionGenerator VCExprGen {
@@ -79,13 +74,10 @@ namespace Microsoft.Boogie {
}
public readonly Program program;
- public readonly CommandLineOptions.BvHandling bitvectors;
- public ContextCacheKey(Program prog,
- CommandLineOptions.BvHandling bitvectors) {
+ public ContextCacheKey(Program prog) {
Contract.Requires(prog != null);
this.program = prog;
- this.bitvectors = bitvectors;
}
[Pure]
@@ -93,15 +85,14 @@ namespace Microsoft.Boogie {
public override bool Equals(object that) {
if (that is ContextCacheKey) {
ContextCacheKey thatKey = (ContextCacheKey)that;
- return this.program.Equals(thatKey.program) &&
- this.bitvectors.Equals(thatKey.bitvectors);
+ return this.program.Equals(thatKey.program);
}
return false;
}
[Pure]
public override int GetHashCode() {
- return this.program.GetHashCode() + this.bitvectors.GetHashCode();
+ return this.program.GetHashCode();
}
}
@@ -113,7 +104,6 @@ namespace Microsoft.Boogie {
public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
- this.bitvectors = BvHandlingForImpl(impl);
this.timeout = timeout;
ProverOptions options = cce.NonNull(CommandLineOptions.Clo.TheProverFactory).BlankProverOptions();
@@ -127,11 +117,10 @@ namespace Microsoft.Boogie {
if (timeout > 0) {
options.TimeLimit = timeout * 1000;
}
- options.BitVectors = this.bitvectors;
options.Parse(CommandLineOptions.Clo.ProverOptions);
- ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors);
+ ContextCacheKey key = new ContextCacheKey(prog);
ProverContext ctx;
ProverInterface prover;
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 08:46:08 +0000