Adding fixedpoint engine backend

1 files changed, 15 insertions, 9 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index da73dea1..1f4b6a7f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -23,7 +23,8 @@ namespace Microsoft.Boogie.SMTLib
   // Options for the linearisation

   public class LineariserOptions

   {

-    public static readonly LineariserOptions Default = new LineariserOptions();

+    public static LineariserOptions Default = new LineariserOptions();

+    public bool LabelsBelowQuantifiers = false;

   }

 

 

@@ -518,23 +519,28 @@ namespace Microsoft.Boogie.SMTLib
 

       public bool VisitLabelOp(VCExprNAry node, LineariserOptions options)

       {

-        if (ExprLineariser.UnderQuantifier > 0) {

+        if (ExprLineariser.UnderQuantifier > 0 && !options.LabelsBelowQuantifiers) {

           ExprLineariser.Linearise(node[0], options);

           return true;

         }

 

         var op = (VCExprLabelOp)node.Op;

-        if (CommandLineOptions.Clo.UseLabels) {

-          // Z3 extension

-          //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

-          wr.Write("(! ");

+

+        if (CommandLineOptions.Clo.UseLabels)

+        {

+            // Z3 extension

+            //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

+            wr.Write("(! ");

         }

 

-        wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

-            

+        if(!options.LabelsBelowQuantifiers)

+            wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

+

         ExprLineariser.Linearise(node[0], options);

 

-        wr.Write(")");

+

+        if (!options.LabelsBelowQuantifiers) 

+            wr.Write(")");

 

         if (CommandLineOptions.Clo.UseLabels)

           wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));