From 85a65323bda16d372a9e163dc4225e5d5535d14c Mon Sep 17 00:00:00 2001 From: Peter Collingbourne Date: Thu, 6 Sep 2012 20:33:21 +0100 Subject: Implement support for alternative SMT solvers -- CVC3 and CVC4 --- Source/Provers/SMTLib/SMTLibLineariser.cs | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs') diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 0a0e37a2..6a2cbb6a 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -416,14 +416,7 @@ namespace Microsoft.Boogie.SMTLib Contract.Requires(node != null); Contract.Requires(options != null); - // not sure if this is needed - if (node[0].Type.IsBool) { - Contract.Assert(node[1].Type.IsBool); - // use equivalence - WriteApplication("iff", node, options); - } else { - WriteApplication("=", node, options); - } + WriteApplication("=", node, options); return true; } @@ -470,7 +463,10 @@ namespace Microsoft.Boogie.SMTLib public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) { VCExprCustomOp op = (VCExprCustomOp)node.Op; - WriteApplication(op.Name, node, options); + if (!ExprLineariser.ProverOptions.UseTickleBool && op.Name == "tickleBool") + ExprLineariser.Linearise(VCExpressionGenerator.True, options); + else + WriteApplication(op.Name, node, options); return true; } @@ -517,7 +513,7 @@ namespace Microsoft.Boogie.SMTLib } var op = (VCExprLabelOp)node.Op; - if (ExprLineariser.ProverOptions.UseLabels) { + if (CommandLineOptions.Clo.UseLabels) { // Z3 extension //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); wr.Write("(! "); @@ -529,7 +525,7 @@ namespace Microsoft.Boogie.SMTLib wr.Write(")"); - if (ExprLineariser.ProverOptions.UseLabels) + if (CommandLineOptions.Clo.UseLabels) wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label)); return true; -- cgit v1.2.3