The back pred files have been eliminated. The small backpred string is now directly included in ProverInterface.cs.

3 files changed, 9 insertions, 148 deletions

diff --git a/Binaries/UnivBackPred2.smt b/Binaries/UnivBackPred2.smt
deleted file mode 100644
index 76c77d60..00000000
--- a/Binaries/UnivBackPred2.smt
+++ /dev/null
@@ -1,131 +0,0 @@
-; -------------------------------------------------------------------------

-; Boogie universal background predicate

-; Copyright (c) 2004-2006, Microsoft Corp.

-  :logic AUFLIA

-  :category { industrial }

-

-:extrasorts ( boogieU )

-:extrasorts ( boogieT )

-:extrasorts ( TermBool )

-

-:extrafuns (( boolTrue TermBool ))

-:extrafuns (( boolFalse TermBool ))

-:extrafuns (( boolIff TermBool TermBool TermBool ))

-:extrafuns (( boolImplies TermBool TermBool TermBool ))

-:extrafuns (( boolAnd TermBool TermBool TermBool ))

-:extrafuns (( boolOr TermBool TermBool TermBool ))

-:extrafuns (( boolNot TermBool TermBool ))

-:extrafuns (( UEqual boogieU boogieU TermBool ))

-:extrafuns (( TEqual boogieT boogieT TermBool ))

-:extrafuns (( IntEqual Int Int TermBool ))

-:extrafuns (( intLess Int Int TermBool ))

-:extrafuns (( intAtMost Int Int TermBool ))

-:extrafuns (( intGreater Int Int TermBool ))

-:extrafuns (( intAtLeast Int Int TermBool ))

-:extrafuns (( boogieIntMod Int Int Int ))

-:extrafuns (( boogieIntDiv Int Int Int ))

-

-; used for translation with type premisses

-:extrapreds (( UOrdering2 boogieU boogieU ))

-; used for translation with type arguments

-:extrapreds (( UOrdering3 boogieT boogieU boogieU ))

-

-; used for translation with type premisses

-:extrafuns (( TermUOrdering2 boogieU boogieU TermBool ))

-; used for translation with type arguments

-:extrafuns (( TermUOrdering3 boogieT boogieU boogieU TermBool ))

-

-  ; formula/term axioms

-  :assumption

-  (forall (?x TermBool) (?y TermBool)

-    (iff

-      (= (boolIff ?x ?y) boolTrue)

-      (iff (= ?x boolTrue) (= ?y boolTrue))))

-

-  :assumption

-  (forall (?x TermBool) (?y TermBool)

-    (iff

-      (= (boolImplies ?x ?y) boolTrue)

-      (implies (= ?x boolTrue) (= ?y boolTrue))))

-

-  :assumption

-  (forall (?x TermBool) (?y TermBool)

-    (iff

-      (= (boolAnd ?x ?y) boolTrue)

-      (and (= ?x boolTrue) (= ?y boolTrue))))

-

-  :assumption

-  (forall (?x TermBool) (?y TermBool)

-    (iff

-      (= (boolOr ?x ?y) boolTrue)

-      (or (= ?x boolTrue) (= ?y boolTrue))))

-

-  :assumption

-  (forall (?x TermBool)

-    (iff

-      (= (boolNot ?x) boolTrue)

-      (not (= ?x boolTrue)))

-    :pat { (boolNot ?x) }

-  )

-

-  :assumption

-  (forall (?x boogieU) (?y boogieU)

-    (iff

-      (= (UEqual ?x ?y) boolTrue)

-      (= ?x ?y)))

-

-  :assumption

-  (forall (?x boogieT) (?y boogieT)

-    (iff

-      (= (TEqual ?x ?y) boolTrue)

-      (= ?x ?y)))

-

-  :assumption

-  (forall (?x Int) (?y Int)

-    (iff

-      (= (IntEqual ?x ?y) boolTrue)

-      (= ?x ?y)))

-

-  :assumption

-  (forall (?x Int) (?y Int)

-    (iff

-      (= (intLess ?x ?y) boolTrue)

-      (< ?x ?y)))

-

-  :assumption

-  (forall (?x Int) (?y Int)

-    (iff

-      (= (intAtMost ?x ?y) boolTrue)

-      (<= ?x ?y)))

-

-  :assumption

-  (forall (?x Int) (?y Int)

-    (iff

-      (= (intAtLeast ?x ?y) boolTrue)

-      (>= ?x ?y)))

-

-  :assumption

-  (forall (?x Int) (?y Int)

-    (iff

-      (= (intGreater ?x ?y) boolTrue)

-      (> ?x ?y)))

-

-  ; false is not true

-  :assumption

-  (distinct boolFalse boolTrue)

-

-  :assumption

-  (forall (?x boogieU) (?y boogieU)

-    (iff

-      (= (TermUOrdering2 ?x ?y) boolTrue)

-      (UOrdering2 ?x ?y)))

-

-  :assumption

-  (forall (?x boogieT) (?y boogieU) (?z boogieU)

-    (iff

-      (= (TermUOrdering3 ?x ?y ?z) boolTrue)

-      (UOrdering3 ?x ?y ?z)))

-

-; End Boogie universal background predicate

-; -------------------------------------------------------------------------

-

diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
deleted file mode 100644
index 9bb05bfb..00000000
--- a/Binaries/UnivBackPred2.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; Boogie universal background predicate

-; Copyright (c) 2004-2010, Microsoft Corp.

-(set-info :category "industrial")

-(declare-sort |T@U| 0)

-(declare-sort |T@T| 0)

-(declare-fun real_pow (Real Real) Real)

-(declare-fun UOrdering2 (|T@U| |T@U|) Bool)

-(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 6b4f8cb9..dd9df8d3 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -53,7 +53,7 @@ namespace Microsoft.Boogie.SMTLib
       Contract.Requires(gen != null);

       Contract.Requires(ctx != null);

       

-      InitializeGlobalInformation("UnivBackPred2.smt2");

+      InitializeGlobalInformation();

       

       this.options = (SMTLibProverOptions)options;

       this.ctx = ctx;

@@ -1183,9 +1183,8 @@ namespace Microsoft.Boogie.SMTLib
 

     private static string _backgroundPredicates;

 

-    static void InitializeGlobalInformation(string backgroundPred)

+    static void InitializeGlobalInformation()

     {

-      Contract.Requires(backgroundPred != null);

       Contract.Ensures(_backgroundPredicates != null);

       //throws ProverException, System.IO.FileNotFoundException;

       if (_backgroundPredicates == null) {

@@ -1195,12 +1194,13 @@ namespace Microsoft.Boogie.SMTLib
         }

         else

         {

-            string codebaseString = cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));

-            string univBackPredPath = Path.Combine(codebaseString, backgroundPred);

-            using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))

-            {

-                _backgroundPredicates = reader.ReadToEnd();

-            }

+            _backgroundPredicates = @"

+(set-info :category ""industrial"")

+(declare-sort |T@U| 0)

+(declare-sort |T@T| 0)

+(declare-fun real_pow (Real Real) Real)

+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)

+(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)";

         }

       }

     }