diff options
| author |  MichalMoskal <unknown> | 2011-02-15 21:38:02 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-15 21:38:02 +0000 |
| commit | cc665557287b709705414c637298cc3097fe1136 (patch) | |
| tree | c36fc6d99269801ac3f5b36c9784dcf180ae66a5 | |
| parent | b6df5bd0a3b71ae1eb2b4912384be6a0dbe39db9 (diff) | |
Print terms in SMT2 syntax (drop term/formula distinction)
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 723 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 2 |
3 files changed, 240 insertions, 487 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index d7251f09..cf392277 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -24,6 +24,8 @@ namespace Microsoft.Boogie.SMTLib {
public string Output = "boogie-vc-@PROC@.smt";
public bool UsePredicates = false;
+ public bool UseWeights = true;
+ public bool UseLabels = false;
protected override bool Parse(string opt)
{
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index d7b6bb7f..a7283a60 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -21,47 +21,27 @@ namespace Microsoft.Boogie.SMTLib {
// Options for the linearisation
- public class LineariserOptions {
-
- public readonly bool AsTerm;
- public LineariserOptions SetAsTerm(bool newVal) {
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- if (newVal)
- return DefaultTerm;
- else
- return Default;
- }
-
- internal LineariserOptions(bool asTerm) {
- this.AsTerm = asTerm;
- }
-
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Default!=null);
- Contract.Invariant(DefaultTerm!=null);
-}
-
- public static readonly LineariserOptions Default = new LineariserOptions (false);
- internal static readonly LineariserOptions DefaultTerm = new LineariserOptions (true);
+ public class LineariserOptions
+ {
+ public static readonly LineariserOptions Default = new LineariserOptions();
}
////////////////////////////////////////////////////////////////////////////////////////
// Lineariser for expressions. The result (bool) is currently not used for anything
- public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
+ public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
+ {
- public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) {
- Contract.Requires(e != null);
- Contract.Requires(namer != null);
- Contract.Ensures(Contract.Result<string>() != null);
+ public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts)
+ {
+ Contract.Requires(e != null);
+ Contract.Requires(namer != null);
+ Contract.Ensures(Contract.Result<string>() != null);
StringWriter sw = new StringWriter();
- SMTLibExprLineariser lin = new SMTLibExprLineariser (sw, namer, opts);
- Contract.Assert(lin!=null);
+ SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts);
+ Contract.Assert(lin != null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
}
@@ -70,46 +50,47 @@ void ObjectInvariant() private readonly TextWriter wr;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
+ void ObjectInvariant()
+ {
+ Contract.Invariant(wr != null);
Contract.Invariant(Namer != null);
-}
+ }
private SMTLibOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser { get {
- Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool,LineariserOptions>>() !=null);
+ private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
- if (OpLinObject == null)
- OpLinObject = new SMTLibOpLineariser(this, wr);
- return OpLinObject;
- } }
+ if (OpLinObject == null)
+ OpLinObject = new SMTLibOpLineariser(this, wr);
+ return OpLinObject;
+ }
+ }
internal readonly UniqueNamer Namer;
internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) {
- Contract.Requires(wr != null);Contract.Requires(namer != null);
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts)
+ {
+ Contract.Requires(wr != null); Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
this.ProverOptions = opts;
}
- public void Linearise(VCExpr expr, LineariserOptions options) {
+ public void Linearise(VCExpr expr, LineariserOptions options)
+ {
Contract.Requires(expr != null);
Contract.Requires(options != null);
expr.Accept<bool, LineariserOptions>(this, options);
}
- public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {
- Contract.Requires(expr != null);
- Contract.Requires(options != null);
- Linearise(expr, options.SetAsTerm(true));
- }
-
/////////////////////////////////////////////////////////////////////////////////////
- internal static string TypeToString(Type t) {
+ internal static string TypeToString(Type t)
+ {
Contract.Requires(t != null);
Contract.Ensures(Contract.Result<string>() != null);
@@ -122,7 +103,7 @@ void ObjectInvariant() throw new cce.UnreachableException();
} // bitvectors are currently not handled for SMT-Lib solvers
else {
- // at this point, only the types U, T should be left
+ // at this point, only the types U, T should be left (except when /typeEncoding:m is used)
System.IO.StringWriter buffer = new System.IO.StringWriter();
using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
t.Emit(stream);
@@ -132,99 +113,24 @@ void ObjectInvariant() }
/////////////////////////////////////////////////////////////////////////////////////
- /////////////////////////////////////////////////////////////////////////////////////
-
- /// <summary>
- /// The name for logical conjunction in Simplify
- /// </summary>
- internal const string andName = "and"; // conjunction
- internal const string orName = "or"; // disjunction
- internal const string notName = "not"; // negation
- internal const string impliesName = "implies"; // implication
- internal const string iteName = "ite"; // if-then-else
- internal const string iffName = "iff"; // logical equivalence
- internal const string eqName = "="; // equality
- internal const string lessName = "<";
- internal const string greaterName = ">";
- internal const string atmostName = "<=";
- internal const string atleastName = ">=";
- internal const string TRUEName = "true"; // nullary predicate that is always true
- internal const string FALSEName = "false"; // nullary predicate that is always false
- internal const string subtypeName = "UOrdering2";
- internal const string subtypeArgsName = "UOrdering3";
-
- internal const string distinctName = "distinct";
-
- internal const string boolTrueName = "boolTrue";
- internal const string boolFalseName = "boolFalse";
- internal const string boolAndName = "boolAnd";
- internal const string boolOrName = "boolOr";
- internal const string boolNotName = "boolNot";
- internal const string boolIffName = "boolIff";
- internal const string boolImpliesName = "boolImplies";
- internal const string boolIteName = "ite";
- internal const string termUEqual = "UEqual";
- internal const string termTEqual = "TEqual";
- internal const string termIntEqual = "IntEqual";
- internal const string termLessName = "intLess";
- internal const string termGreaterName = "intGreater";
- internal const string termAtmostName = "intAtMost";
- internal const string termAtleastName = "intAtLeast";
- internal const string intAddName = "+";
- internal const string intSubName = "-";
- internal const string intMulName = "*";
- internal const string intDivName = "boogieIntDiv";
- internal const string intModName = "boogieIntMod";
-
- internal void AssertAsTerm(string x, LineariserOptions options) {
- Contract.Requires(x != null);
- Contract.Requires(options != null);
- if (!options.AsTerm)
- System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
- }
-
- internal void AssertAsFormula(string x, LineariserOptions options) {
- Contract.Requires(x != null);
- Contract.Requires(options != null);
- if (options.AsTerm)
- System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprLiteral node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- if (options.AsTerm) {
-
- if (node == VCExpressionGenerator.True)
- wr.Write("{0}", boolTrueName);
- else if (node == VCExpressionGenerator.False)
- wr.Write("{0}", boolFalseName);
- else if (node is VCExprIntLit) {
- // some SMT-solvers do not understand negative literals
- // (e.g., yices)
- BigNum lit = ((VCExprIntLit)node).Val;
- if (lit.IsNegative)
- wr.Write("({0} 0 {1})", intSubName, lit.Abs);
- else
- wr.Write(lit);
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
+ public bool Visit(VCExprLiteral node, LineariserOptions options)
+ {
+ if (node == VCExpressionGenerator.True)
+ wr.Write("true");
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("false");
+ else if (node is VCExprIntLit) {
+ // some SMT-solvers do not understand negative literals
+ // (e.g., yices)
+ BigNum lit = ((VCExprIntLit)node).Val;
+ if (lit.IsNegative)
+ wr.Write("(- 0 {0})", lit.Abs);
+ else
+ wr.Write(lit);
} else {
-
- if (node == VCExpressionGenerator.True)
- wr.Write("{0}", TRUEName);
- else if (node == VCExpressionGenerator.False)
- wr.Write("{0}", FALSEName);
- else if (node is VCExprIntLit) {
- System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
- } else
- {Contract.Assert(false); throw new cce.UnreachableException();}
-
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
return true;
@@ -232,22 +138,21 @@ void ObjectInvariant() /////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprNAry node, LineariserOptions options) {
+ public bool Visit(VCExprNAry node, LineariserOptions options)
+ {
//Contract.Requires(node != null);
//Contract.Requires(options != null);
-
+
VCExprOp op = node.Op;
- Contract.Assert(op!=null);
+ Contract.Assert(op != null);
- if (!options.AsTerm &&
- (op.Equals(VCExpressionGenerator.AndOp) ||
- op.Equals(VCExpressionGenerator.OrOp))) {
+ if (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp)) {
// handle these operators without recursion
wr.Write("({0}",
- op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
- Contract.Assert(enumerator!=null);
+ op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");
+ IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
while (enumerator.MoveNext()) {
VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
if (naryExpr == null || !naryExpr.Op.Equals(op)) {
@@ -266,79 +171,73 @@ void ObjectInvariant() /////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprVar node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- string printedName = Namer.GetQuotedName(node, node.Name);
- Contract.Assert(printedName!=null);
-
- if (options.AsTerm ||
- // formula variables are easy to identify in SMT-Lib
- printedName[0] == '$')
- wr.Write("{0}", printedName);
- else
- wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName);
-
+ public bool Visit(VCExprVar node, LineariserOptions options)
+ {
+ wr.Write(Namer.GetQuotedName(node, node.Name));
return true;
}
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprQuantifier node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- AssertAsFormula(node.Quan.ToString(), options);
- Contract.Assert(node.TypeParameters.Count == 0);
+ public bool Visit(VCExprQuantifier node, LineariserOptions options)
+ {
+ Contract.Assert(node.TypeParameters.Count == 0);
Namer.PushScope(); try {
- string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
- wr.Write("({0} ", kind);
+ string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
+ wr.Write("\n({0} (", kind);
- for (int i = 0; i < node.BoundVars.Count; i++)
- {
+ for (int i = 0; i < node.BoundVars.Count; i++) {
VCExprVar var = node.BoundVars[i];
- Contract.Assert(var!=null);
+ Contract.Assert(var != null);
string printedName = Namer.GetLocalName(var, var.Name);
- Contract.Assert(printedName!=null);
+ Contract.Assert(printedName != null);
wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));
}
-
- /* if (options.QuantifierIds) {
- // only needed for Z3
- VCQuantifierInfos! infos = node.Infos;
- if (infos.qid != null) {
- wr.Write("(QID ");
- wr.Write(infos.qid);
- wr.Write(") ");
- }
- if (0 <= infos.uniqueId) {
- wr.Write("(SKOLEMID ");
- wr.Write(infos.uniqueId);
- wr.Write(") ");
- }
- } */
- Linearise(node.Body, options);
+ wr.Write(")");
- WriteTriggers(node.Triggers, options);
- wr.Write(")");
+ VCQuantifierInfos infos = node.Infos;
+ var weight = QKeyValue.FindIntAttribute(infos.attributes, "weight", 1);
+ if (!ProverOptions.UseWeights)
+ weight = 1;
+ var hasAttrs = node.Triggers.Count > 0 || infos.qid != null || weight != 1;
+
+ if (hasAttrs)
+ wr.Write("(! ");
+
+ Linearise(node.Body, options);
+
+ if (hasAttrs) {
+ wr.Write("\n");
+ if (infos.qid != null)
+ wr.Write(" :named {0}\n", SMTLibNamer.QuoteId(infos.qid));
+ if (weight != 1)
+ wr.Write(" :weight {0}\n", weight);
+ WriteTriggers(node.Triggers, options);
+
+ wr.Write(")");
+ }
+
+ wr.Write(")\n");
- return true;
+ return true;
} finally {
Namer.PopScope();
}
}
- private void WriteTriggers(List<VCTrigger/*!>!*/> triggers, LineariserOptions options) {
+ private void WriteTriggers(List<VCTrigger/*!>!*/> triggers, LineariserOptions options)
+ {
Contract.Requires(options != null);
Contract.Requires(triggers != null);
// first, count how many neg/pos triggers there are
int negTriggers = 0;
int posTriggers = 0;
foreach (VCTrigger vcTrig in triggers) {
- Contract.Assert(vcTrig!=null);
+ Contract.Assert(vcTrig != null);
if (vcTrig.Pos) {
posTriggers++;
} else {
@@ -348,15 +247,15 @@ void ObjectInvariant() if (posTriggers > 0) {
foreach (VCTrigger vcTrig in triggers) {
- Contract.Assert(vcTrig!=null);
+ Contract.Assert(vcTrig != null);
if (vcTrig.Pos) {
- wr.Write(" :pat {");
+ wr.Write(" :pattern (");
foreach (VCExpr e in vcTrig.Exprs) {
- Contract.Assert(e!=null);
+ Contract.Assert(e != null);
wr.Write(" ");
- LineariseAsTerm(e, options);
+ Linearise(e, options);
}
- wr.Write(" } ");
+ wr.Write(")\n");
}
}
} else if (negTriggers > 0) {
@@ -364,13 +263,12 @@ void ObjectInvariant() // will ignore the negative patterns and output a warning. Therefore
// we never specify both negative and positive triggers
foreach (VCTrigger vcTrig in triggers) {
- Contract.Assert(vcTrig!=null);
+ Contract.Assert(vcTrig != null);
if (!vcTrig.Pos) {
- wr.Write(" :nopat { ");
- Contract.Assert(vcTrig.Exprs.Count == 1);
- wr.Write(" ");
- LineariseAsTerm(vcTrig.Exprs[0], options);
- wr.Write(" } ");
+ wr.Write(" :no-pattern (");
+ Contract.Assert(vcTrig.Exprs.Count == 1);
+ Linearise(vcTrig.Exprs[0], options);
+ wr.Write(")\n");
}
}
}
@@ -378,29 +276,21 @@ void ObjectInvariant() /////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprLet node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- Namer.PushScope(); try {
-
- foreach (VCExprLetBinding b in node) {
- Contract.Assert(b != null);
- bool formula = b.V.Type.IsBool;
-
- wr.Write("({0} (let");
- string printedName = Namer.GetQuotedName(b.V, b.V.Name);
-
- wr.Write("{0} ", printedName);
- Linearise(b.E, options.SetAsTerm(!formula));
+ public bool Visit(VCExprLet node, LineariserOptions options)
+ {
+ Namer.PushScope();
+ try {
+ wr.Write("(let (");
+ foreach (VCExprLetBinding b in node) {
+ Contract.Assert(b != null);
+ wr.Write("({0} ", Namer.GetQuotedName(b.V, b.V.Name));
+ Linearise(b.E, options);
+ wr.Write(")\n");
+ }
wr.Write(") ");
- }
- Linearise(node.Body, options);
-
- for (int i = 0; i < node.Length; ++i)
+ Linearise(node.Body, options);
wr.Write(")");
-
- return true;
-
+ return true;
} finally {
Namer.PopScope();
}
@@ -409,18 +299,20 @@ void ObjectInvariant() /////////////////////////////////////////////////////////////////////////////////////
// Lineariser for operator terms. The result (bool) is currently not used for anything
- internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {
+ internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/>
+ {
private readonly SMTLibExprLineariser ExprLineariser;
private readonly TextWriter wr;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
- Contract.Invariant(ExprLineariser!=null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(wr != null);
+ Contract.Invariant(ExprLineariser != null);
+ }
- public SMTLibOpLineariser(SMTLibExprLineariser ExprLineariser, TextWriter wr) {
+ public SMTLibOpLineariser(SMTLibExprLineariser ExprLineariser, TextWriter wr)
+ {
Contract.Requires(ExprLineariser != null);
Contract.Requires(wr != null);
this.ExprLineariser = ExprLineariser;
@@ -428,196 +320,103 @@ void ObjectInvariant() }
///////////////////////////////////////////////////////////////////////////////////
-
- private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
- LineariserOptions options,
- bool argsAsTerms) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- WriteApplication(op, op, args, options, argsAsTerms);
- }
-
- private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
- LineariserOptions options) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- WriteApplication(op, op, args, options, options.AsTerm);
- }
-
- private void WriteTermApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
- LineariserOptions options) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- ExprLineariser.AssertAsTerm(op, options);
- WriteApplication(op, op, args, options, options.AsTerm);
- }
-
- private void WriteApplication(string termOp, string predOp,
- IEnumerable<VCExpr/*!>!*/> args, LineariserOptions options) {
- Contract.Requires(predOp != null);
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- WriteApplication(termOp, predOp, args, options, options.AsTerm);
- }
-
- private void WriteApplication(string termOp, string predOp,
- IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
- // change the AsTerm option for the arguments?
- bool argsAsTerms) {
- Contract.Requires(predOp != null);
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- string opName = options.AsTerm ? termOp : predOp;
- Contract.Assert(opName!=null);
- LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
- Contract.Assert(newOptions!=null);
+ private void WriteApplication(string opName, IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options)
+ {
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Requires(options != null);
+ Contract.Assert(opName != null);
bool hasArgs = false;
foreach (VCExpr e in args) {
- Contract.Assert(e!=null);
+ Contract.Assert(e != null);
if (!hasArgs)
wr.Write("({0}", opName);
wr.Write(" ");
- ExprLineariser.Linearise(e, newOptions);
+ ExprLineariser.Linearise(e, options);
hasArgs = true;
}
-
+
if (hasArgs)
wr.Write(")");
else
wr.Write("{0}", opName);
}
- // write an application that can only be a term.
- // if the expression is supposed to be printed as a formula,
- // it is turned into an equation (EQ (f args) |@true|)
- private void WriteApplicationTermOnly(string termOp,
- IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options) {
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args));
- Contract.Requires(options != null);
- if (!options.AsTerm)
- // Write: (EQ (f args) |@true|)
- // where "args" are written as terms
- wr.Write("({0} ", eqName);
-
- WriteApplication(termOp, args, options, true);
-
- if (!options.AsTerm)
- wr.Write(" {0})", boolTrueName);
- }
-
///////////////////////////////////////////////////////////////////////////////////
-
- public bool VisitNotOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas
+
+ public bool VisitNotOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("not", node, options); // arguments can be both terms and formulas
return true;
}
- private bool PrintEq(VCExprNAry node, LineariserOptions options) {
+ private bool PrintEq(VCExprNAry node, LineariserOptions options)
+ {
Contract.Requires(node != null);
Contract.Requires(options != null);
- if (options.AsTerm) {
- // use equality on terms, also if the arguments have type bool
- Contract.Assert(node[0].Type.Equals(node[1].Type));
- if (node[0].Type.IsBool) {
- WriteApplication(boolIffName, node, options);
- } else if (node[0].Type.IsInt) {
- WriteApplication(termIntEqual, node, options);
- } else {
- // TODO: make this less hackish
- CtorType t = node[0].Type as CtorType;
- if (t != null && t.Decl.Name.Equals("U")) {
- WriteApplication(termUEqual, node, options);
- } else if (t != null && t.Decl.Name.Equals("T")) {
- WriteApplication(termTEqual, node, options);
- } else {
- {Contract.Assert(false); throw new cce.UnreachableException();} // unknown type
- }
- }
+
+ // not sure if this is needed
+ if (node[0].Type.IsBool) {
+ Contract.Assert(node[1].Type.IsBool);
+ // use equivalence
+ WriteApplication("iff", node, options);
} else {
- if (node[0].Type.IsBool) {
- Contract.Assert(node[1].Type.IsBool);
- // use equivalence
- WriteApplication(iffName, node, options);
- } else {
- // use equality and write the arguments as terms
- WriteApplication(eqName, node, options, true);
- }
+ WriteApplication("=", node, options);
}
return true;
}
- public bool VisitEqOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
+ public bool VisitEqOp(VCExprNAry node, LineariserOptions options)
+ {
return PrintEq(node, options);
}
- public bool VisitNeqOp (VCExprNAry node, LineariserOptions options) {
+ public bool VisitNeqOp(VCExprNAry node, LineariserOptions options)
+ {
//Contract.Requires(node != null);
//Contract.Requires(options != null);
- wr.Write("({0} ", options.AsTerm ? boolNotName : notName);
+ wr.Write("(not ");
PrintEq(node, options);
wr.Write(")");
return true;
}
- public bool VisitAndOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- Contract.Assert(options.AsTerm);
- WriteApplication(boolAndName, andName, node, options);
+ public bool VisitAndOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("and", node, options);
return true;
}
- public bool VisitOrOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- Contract.Assert(options.AsTerm);
- WriteApplication(boolOrName, orName, node, options);
+ public bool VisitOrOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("or", node, options);
return true;
}
- public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(boolImpliesName, impliesName, node, options);
+ public bool VisitImpliesOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("=>", node, options);
return true;
}
- public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(boolIteName, iteName, node, options);
+ public bool VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("ite", node, options);
return true;
}
- public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
+ public bool VisitCustomOp(VCExprNAry node, LineariserOptions options)
+ {
VCExprCustomOp op = (VCExprCustomOp)node.Op;
- WriteApplicationTermOnly(op.Name, node, options);
+ WriteApplication(op.Name, node, options);
return true;
}
- public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {
+ public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options)
+ {
//Contract.Requires(node != null);
//Contract.Requires(options != null);
-
- ExprLineariser.AssertAsFormula(distinctName, options);
if (node.Length < 2) {
ExprLineariser.Linearise(VCExpressionGenerator.True, options);
@@ -628,196 +427,146 @@ void ObjectInvariant() wr.Write("(and ");
foreach (var g in groupings) {
- wr.Write("({0}", distinctName);
+ wr.Write("(distinct");
foreach (VCExpr e in g) {
Contract.Assert(e != null);
wr.Write(" ");
- ExprLineariser.LineariseAsTerm(e, options);
+ ExprLineariser.Linearise(e, options);
}
wr.Write(")");
}
if (groupings.Length > 1)
wr.Write(")");
+ wr.Write("\n");
}
return true;
}
- public bool VisitLabelOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- //Contract.Requires(node.Length>=1);
- // VCExprLabelOp! op = (VCExprLabelOp)node.Op;
- // TODO
- // wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
- ExprLineariser.Linearise(node[0], options);
- // wr.Write(")");
+ public bool VisitLabelOp(VCExprNAry node, LineariserOptions options)
+ {
+ var op = (VCExprLabelOp)node.Op;
+ if (ExprLineariser.ProverOptions.UseLabels) {
+ // Z3 extension
+ wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(")");
+ } else {
+ ExprLineariser.Linearise(node[0], options);
+ }
return true;
}
public bool VisitSelectOp(VCExprNAry node, LineariserOptions options)
{
- //Contract.Requires(options != null);
- //Contract.Requires(node != null);
var name = SimplifyLikeExprLineariser.SelectOpName(node);
name = ExprLineariser.Namer.GetQuotedName(name, name);
-
- wr.Write("(" + name);
- foreach (VCExpr/*!*/ e in node) {
- Contract.Assert(e != null);
- wr.Write(" ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
+ WriteApplication(name, node, options);
return true;
}
public bool VisitStoreOp(VCExprNAry node, LineariserOptions options)
{
- //Contract.Requires(options != null);
- //Contract.Requires(node != null);
var name = SimplifyLikeExprLineariser.StoreOpName(node);
name = ExprLineariser.Namer.GetQuotedName(name, name);
-
- wr.Write("(" + name);
- foreach (VCExpr e in node) {
- Contract.Assert(e != null);
- wr.Write(" ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
+ WriteApplication(name, node, options);
return true;
}
- public bool VisitBvOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ public bool VisitBvOp(VCExprNAry node, LineariserOptions options)
+ {
+ { Contract.Assert(false); throw new NotImplementedException(); } // TODO
}
- public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options)
+ {
+ { Contract.Assert(false); throw new NotImplementedException(); } // TODO
}
- public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ public bool VisitBvConcatOp(VCExprNAry node, LineariserOptions options)
+ {
+ { Contract.Assert(false); throw new NotImplementedException(); } // TODO
}
- public bool VisitAddOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intAddName, node, options);
+ public bool VisitAddOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("+", node, options);
return true;
}
- public bool VisitSubOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intSubName, node, options);
+ public bool VisitSubOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("-", node, options);
return true;
}
- public bool VisitMulOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intMulName, node, options);
+ public bool VisitMulOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("*", node, options);
return true;
}
- public bool VisitDivOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intDivName, node, options);
+ public bool VisitDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("int_div", node, options);
return true;
}
- public bool VisitModOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intModName, node, options);
+ public bool VisitModOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("int_mod", node, options);
return true;
}
- public bool VisitLtOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms
+ public bool VisitLtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("<", node, options);
return true;
}
- public bool VisitLeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms
+ public bool VisitLeOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("<=", node, options);
return true;
}
- public bool VisitGtOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms
+ public bool VisitGtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication(">", node, options);
return true;
}
- public bool VisitGeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms
+ public bool VisitGeOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication(">=", node, options);
return true;
}
- public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(subtypeName, node, options, true); // arguments are always terms
+ public bool VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("UOrdering2", node, options);
return true;
}
- public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
+ public bool VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("UOrdering3", node, options);
return true;
}
- public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
+ public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
+ {
VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
- Contract.Assert(op!=null);
+ Contract.Assert(op != null);
string printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
- Contract.Assert(printedName!=null);
+ Contract.Assert(printedName != null);
- if (ExprLineariser.ProverOptions.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool) {
- WriteApplication(printedName, node, options, true);
- } else {
- // arguments are always terms
- WriteApplicationTermOnly(printedName, node, options);
- }
+ WriteApplication(printedName, node, options);
return true;
}
-
+
}
}
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index a3528362..91e4b92b 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -28,6 +28,8 @@ namespace Microsoft.Boogie.SMTLib // Z3 extensions
"lblneg", "lblpos", "lbl-lit",
"if", "&&", "||", "equals", "equiv", "bool",
+ // Boogie-defined
+ "int_mod", "int_div", "UOrdering2", "UOrdering3",
};
static Dictionary<string, bool> reservedSmtWords;
|