summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs42
-rw-r--r--Source/Core/VCExp.cs2
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs12
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs3
-rw-r--r--Source/Provers/SMTLib/SMTLibProverOptions.cs3
-rw-r--r--Source/Provers/SMTLib/Z3.cs4
-rw-r--r--Source/Provers/Z3/Prover.cs4
7 files changed, 21 insertions, 49 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7f5642f3..3a80a2ea 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -697,52 +697,14 @@ namespace Microsoft.Boogie {
}
return g;
}
-
- // Delete unreachable Blocks of an Impl. This helps avoid a bug inside
- // NewComputeDominators
-
- public void pruneUnreachableBlocks(Implementation impl)
- {
- // Do a BFS to find all reachable blocks
- List<Block> reachableBlocks = new List<Block>();
- HashSet<string> visited = new HashSet<string>();
- List<Block> worklist = new List<Block>();
-
- visited.Add(impl.Blocks[0].Label);
- worklist.Add(impl.Blocks[0]);
-
- while (worklist.Count != 0)
- {
- var block = worklist[0];
- worklist.RemoveAt(0);
-
- reachableBlocks.Add(block);
- GotoCmd gc = block.TransferCmd as GotoCmd;
- if(gc == null) continue;
-
- foreach (Block succ in gc.labelTargets)
- {
- if (visited.Contains(succ.Label)) continue;
- visited.Add(succ.Label);
- worklist.Add(succ);
- }
- }
-
- // Delete unreachable blocks
-
- // Make sure that the start block hasn't changed.
- Contract.Assert(reachableBlocks[0] == impl.Blocks[0]);
-
- impl.Blocks = reachableBlocks;
- }
-
+
public Dictionary<string, Dictionary<string, Block>> ExtractLoops() {
List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
- pruneUnreachableBlocks(impl);
+ impl.PruneUnreachableBlocks();
Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
g.ComputeLoops();
if (!g.Reducible) {
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index be6695e8..5b7fc946 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -113,7 +113,7 @@ The generic options may or may not be used by the prover plugin.
if (opt.Length == name.Length) {
field = "";
return true;
- } else if (opt[name.Length] == '=') {
+ } else if (opt[name.Length] == '=' || opt[name.Length] == ':') {
field = opt.Substring(name.Length + 1);
return true;
}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 42cf89ab..bc137492 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -152,10 +152,8 @@ namespace Microsoft.Boogie.SMTLib
SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");
}
- if (CommandLineOptions.Clo.UseArrayTheory) {
- SendCommon("; skipping logic setting (using arrays)");
- } else {
- SendCommon("(set-logic UFNIA)");
+ if (!string.IsNullOrEmpty(options.Logic)) {
+ SendCommon("(set-logic " + options.Logic + ")");
}
SendCommon("; done setting options\n");
@@ -348,8 +346,10 @@ namespace Microsoft.Boogie.SMTLib
posLabels = Enumerable.Empty<string>();
var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();
var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");
- SendThisVC("(assert " + expr + ")");
- SendThisVC("(check-sat)");
+ if (errorsLeft > 0) {
+ SendThisVC("(assert " + expr + ")");
+ SendThisVC("(check-sat)");
+ }
}
SendThisVC("(pop 1)");
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 0793c614..a874c6c5 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -27,6 +27,9 @@ namespace Microsoft.Boogie.SMTLib
// Bitvectors
"extract", "concat",
"bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
+ // arrays
+ "store", "select", "const", "default", "map", "union", "intersect", "difference", "complement",
+ "subset", "array-ext", "as-array", "Array",
// Z3 (and not only?) extensions to bitvectors
"bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0",
"bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 44f91cc2..653b2c15 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -34,6 +34,7 @@ namespace Microsoft.Boogie.SMTLib
public List<OptionValue> SmtOptions = new List<OptionValue>();
public List<string> SolverArguments = new List<string>();
public bool MultiTraces = false;
+ public string Logic = "";
// Z3 specific (at the moment; some of them make sense also for other provers)
public bool UseZ3 = true;
@@ -92,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib
ParseBool(opt, "USE_Z3", ref UseZ3) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+ ParseString(opt, "LOGIC", ref Logic) ||
base.Parse(opt);
}
@@ -114,6 +116,7 @@ USE_WEIGHTS=<bool> Pass :weight annotations on quantified formulas (defau
VERBOSITY=<int> 1 - print prover output (default: 0)
O:<name>=<value> Pass (set-option :<name> <value>) to the SMT solver.
C:<string> Pass <string> to the SMT on the command line.
+LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty)
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 54742802..da9e8faa 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -157,8 +157,10 @@ namespace Microsoft.Boogie.SMTLib
options.AddWeakSmtOption("WARNING", "false");
}
- if (options.TimeLimit > 0)
+ if (options.TimeLimit > 0) {
options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());
+ options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);
+ }
// legacy option handling
if (!CommandLineOptions.Clo.z3AtFlag)
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs
index 83294381..640f98ae 100644
--- a/Source/Provers/Z3/Prover.cs
+++ b/Source/Provers/Z3/Prover.cs
@@ -4,7 +4,7 @@
//
//-----------------------------------------------------------------------------
-//#define RECENT_Z3 // 2.20 or newer
+// #define RECENT_Z3 // 2.20 or newer
using System;
using System.IO;
@@ -135,7 +135,9 @@ namespace Microsoft.Boogie.Z3
AddOption(result, "ARITH_RANDOM_INITIAL_VALUE", "true");
// The left-to-right structural case-splitting strategy.
+#if !RECENT_Z3
AddOption(result, "SORT_AND_OR", "false");
+#endif
AddOption(result, "CASE_SPLIT", "3");
// In addition delay adding unit conflicts.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 18:19:33 +0000