summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs50
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs15
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs73
3 files changed, 46 insertions, 92 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index cf392277..6e99252c 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -63,7 +63,6 @@ void ObjectInvariant()
Contract.Invariant(AxBuilder != null);
Contract.Invariant(Namer != null);
Contract.Invariant(DeclCollector != null);
- Contract.Invariant(BadBenchmarkWords != null);
Contract.Invariant(cce.NonNullElements(Axioms));
Contract.Invariant(cce.NonNullElements(TypeDecls));
Contract.Invariant(_backgroundPredicates != null);
@@ -78,7 +77,7 @@ void ObjectInvariant()
Contract.Requires(options != null);
Contract.Requires(gen != null);
Contract.Requires(ctx != null);
- InitializeGlobalInformation("UnivBackPred2.smt");
+ InitializeGlobalInformation("UnivBackPred2.smt2");
this.ctx = ctx;
@@ -98,10 +97,8 @@ void ObjectInvariant()
}
AxBuilder = axBuilder;
- UniqueNamer namer = new UniqueNamer ();
- Namer = namer;
- Namer.Spacer = "__";
- this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, namer);
+ Namer = new SMTLibNamer();
+ this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, Namer);
}
@@ -129,18 +126,22 @@ void ObjectInvariant()
TextWriter output = OpenOutputFile(descriptiveName);
Contract.Assert(output!=null);
- string name =
- MakeBenchmarkNameSafe(SMTLibNamer.QuoteId(descriptiveName));
- Contract.Assert(name!=null);
- WriteLineAndLog(output, "(benchmark " + name);
WriteLineAndLog(output, _backgroundPredicates);
+ string name = SMTLibNamer.QuoteId(descriptiveName);
+ WriteLineAndLog(output, "(set-info :boogie-vc-id " + name + ")");
if (!AxiomsAreSetup) {
- AddAxiom(VCExpr2String(ctx.Axioms, -1));
+ var axioms = ctx.Axioms;
+ var nary = axioms as VCExprNAry;
+ if (nary != null && nary.Op == VCExpressionGenerator.AndOp)
+ foreach(var expr in nary.UniformArguments)
+ AddAxiom(VCExpr2String(expr, -1));
+ else
+ AddAxiom(VCExpr2String(axioms, -1));
AxiomsAreSetup = true;
}
- string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";
+ string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
string prelude = ctx.GetProverCommands(true);
Contract.Assert(prelude!=null);
WriteLineAndLog(output, prelude);
@@ -151,32 +152,15 @@ void ObjectInvariant()
}
foreach (string s in Axioms) {
Contract.Assert(s!=null);
- WriteLineAndLog(output, ":assumption");
- WriteLineAndLog(output, s);
+ WriteLineAndLog(output, "(assert " + s + ")");
}
WriteLineAndLog(output, vcString);
- WriteLineAndLog(output, ")");
+ WriteLineAndLog(output, "(check-sat)");
output.Close();
}
- // certain words that should not occur in the name of a benchmark
- // because some solvers don't like them
- private readonly static List<string/*!>!*/> BadBenchmarkWords = new List<string/*!*/> ();
- static SMTLibProcessTheoremProver() {
- BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");
- }
-
- private string MakeBenchmarkNameSafe(string name) {
- Contract.Requires(name != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2)
- name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i+1]);
- return name;
- }
-
private TextWriter OpenOutputFile(string descriptiveName) {
Contract.Requires(descriptiveName != null);
Contract.Ensures(Contract.Result<TextWriter>() != null);
@@ -189,6 +173,10 @@ void ObjectInvariant()
private void WriteLineAndLog(TextWriter output, string msg) {
Contract.Requires(output != null);
Contract.Requires(msg != null);
+ var idx = msg.IndexOf('\n');
+ if (idx > 0) {
+ msg = msg.Replace("\r", "").Replace("\n", "\r\n");
+ }
LogActivity(msg);
output.WriteLine(msg);
}
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 91e4b92b..e57d8deb 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -11,6 +11,7 @@ namespace Microsoft.Boogie.SMTLib
// The following Boogie ID characters are not SMT ID characters: `'\#
const string idCharacters = "~!@$%^&*_-+=<>.?/";
+
static string[] reservedSmtWordsList =
{ // Basic symbols:
"", "!", "_", "as", "DECIMAL", "exists", "forall", "let", "NUMERAL", "par", "STRING",
@@ -38,10 +39,8 @@ namespace Microsoft.Boogie.SMTLib
static void InitSymbolLists()
{
- if (symbolListsInitilized)
- return;
-
lock (reservedSmtWordsList) {
+ // don't move out, c.f. http://en.wikipedia.org/wiki/Double-checked_locking
if (symbolListsInitilized)
return;
reservedSmtWords = new Dictionary<string, bool>();
@@ -50,15 +49,12 @@ namespace Microsoft.Boogie.SMTLib
validIdChar = new bool[255];
for (int i = 0; i < validIdChar.Length; ++i)
validIdChar[i] = char.IsLetterOrDigit((char)i) || idCharacters.IndexOf((char)i) >= 0;
- System.Threading.Thread.MemoryBarrier(); // c.f. http://en.wikipedia.org/wiki/Double-checked_locking
symbolListsInitilized = true;
}
}
static string AddQuotes(string s)
{
- InitSymbolLists();
-
var allGood = true;
foreach (char ch in s) {
@@ -77,17 +73,15 @@ namespace Microsoft.Boogie.SMTLib
static string NonKeyword(string s)
{
- InitSymbolLists();
-
if (reservedSmtWords.ContainsKey(s) || char.IsDigit(s[0]))
s = "q@" + s;
// | and \ are illegal even in quoted identifiers
if (s.IndexOf('|') >= 0)
- s = s.Replace("|", "");
+ s = s.Replace("|", "_");
if (s.IndexOf('\\') >= 0)
- s = s.Replace("\\", "");
+ s = s.Replace("\\", "_");
return s;
}
@@ -110,6 +104,7 @@ namespace Microsoft.Boogie.SMTLib
public SMTLibNamer()
{
this.Spacer = "@@";
+ InitSymbolLists();
}
}
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index b4728ff7..f9e517ba 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -6,6 +6,7 @@
using System;
using System.Collections;
using System.Collections.Generic;
+using System.Linq;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using Microsoft.Boogie.VCExprAST;
@@ -93,6 +94,12 @@ void ObjectInvariant()
return SMTLibExprLineariser.TypeToString(t);
}
+ private string TypeToStringReg(Type t)
+ {
+ RegisterType(t);
+ return TypeToString(t);
+ }
+
public override bool Visit(VCExprNAry node, bool arg) {
Contract.Requires(node != null);
@@ -106,26 +113,9 @@ void ObjectInvariant()
string printedName = Namer.GetQuotedName(f, f.Name);
Contract.Assert(printedName != null);
- bool isPred = Options.UsePredicates && f.OutParams[0].TypedIdent.Type.IsBool;
- string decl = (isPred ? ":extrapreds" : ":extrafuns") + " ((" + printedName;
-
- foreach (Variable v in f.InParams) {
- Contract.Assert(v != null);
- RegisterType(v.TypedIdent.Type);
- decl += " " + TypeToString(v.TypedIdent.Type);
- }
-
-
Contract.Assert(f.OutParams.Length == 1);
- if (!isPred)
- foreach (Variable v in f.OutParams) {
- Contract.Assert(v != null);
- RegisterType(v.TypedIdent.Type);
- decl += " " + TypeToString(v.TypedIdent.Type);
- }
-
- decl += "))";
-
+ var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");
+ string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";
AddDeclaration(decl);
KnownFunctions.Add(f, true);
}
@@ -141,7 +131,7 @@ void ObjectInvariant()
Contract.Assert(printedName!=null);
RegisterType(node.Type);
string decl =
- ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";
+ "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
KnownVariables.Add(node, true);
}
@@ -179,7 +169,7 @@ void ObjectInvariant()
}
RegisterType(mapType.Result);
- declString += ":extrasorts ( " + TypeToString(type);
+ declString += "(declare-sort " + TypeToString(type) + " 0";
/*
if (CommandLineOptions.Clo.UseArrayTheory) {
@@ -201,7 +191,7 @@ void ObjectInvariant()
return;
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {
- AddDeclaration(":extrasorts ( " + TypeToString(type) + " )");
+ AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");
KnownTypes.Add(type, true);
return;
}
@@ -214,14 +204,7 @@ void ObjectInvariant()
name = Namer.GetQuotedName(name, name);
if (!KnownSelectFunctions.ContainsKey(name)) {
- string decl = ":extrafuns (( " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- decl += " ))";
+ string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
KnownSelectFunctions.Add(name, true);
}
@@ -234,14 +217,7 @@ void ObjectInvariant()
name = Namer.GetQuotedName(name, name);
if (!KnownStoreFunctions.ContainsKey(name)) {
- string decl = ":extrafuns (( " + name;
-
- foreach (VCExpr ch in node) {
- decl += " " + TypeToString(ch.Type);
- }
- decl += " " + TypeToString(node.Type);
-
- decl += "))";
+ string decl = "(declare-fun " + name + " (" + node.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(node.Type) + ")";
AddDeclaration(decl);
if (CommandLineOptions.Clo.MonomorphicArrays && !CommandLineOptions.Clo.UseArrayTheory) {
@@ -250,20 +226,15 @@ void ObjectInvariant()
if (!KnownSelectFunctions.ContainsKey(sel)) {
// need to declare it before reference
- string seldecl = ":extrafuns (( " + sel;
- foreach (VCExpr ch in node) {
- seldecl += " " + TypeToString(ch.Type);
- }
- AddDeclaration(seldecl + "))");
+ var args = node.SkipEnd(1);
+ var ret = node.Last();
+ string seldecl = "(declare-fun " + sel + " (" + args.MapConcat(n => TypeToString(n.Type), " ") + ") " + TypeToString(ret.Type) + ")";
+ AddDeclaration(seldecl);
KnownSelectFunctions.Add(sel, true);
}
- var eq = "=";
- if (node[node.Arity - 1].Type.IsBool)
- eq = "iff";
-
- string ax1 = ":assumption (forall ";
- string ax2 = ":assumption (forall ";
+ string ax1 = "(assert (forall ";
+ string ax2 = "(assert (forall ";
string argX = "", argY = "";
string dist = "";
@@ -281,10 +252,10 @@ void ObjectInvariant()
}
}
string v = " ?x" + (node.Arity - 1);
- ax1 += "(" + eq + " (" + sel + " (" + name + " ?x0" + argX + v + ")" + argX + ") " + v + ")";
+ ax1 += "(= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argX + ") " + v + ")";
ax1 += ")";
- ax2 += "(implies (or " + dist + ") (" + eq + " (" + sel + " (" + name + " ?x0" + argX + v + ")" + argY + ") (" + sel + " ?x0" + argY + ")))";
+ ax2 += "(=> (or " + dist + ") (= (" + sel + " (" + name + " ?x0" + argX + v + ")" + argY + ") (" + sel + " ?x0" + argY + ")))";
ax2 += ")";
AddDeclaration(ax1);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 00:25:26 +0000