Moved axioms derived from Dafny into dedicated directory and added Ms-PL

LICENSE.txt

@@ -1,13 +1,18 @@
 Silicon and all files of its source code are licensed under the Mozilla Public
-License Version 2.0 (see below or http://www.mozilla.org/MPL/2.0/), *except*
-files found in the following directories (and their sub-directories), which
-are licensed under Public Domain
-(see http://creativecommons.org/publicdomain/zero/1.0/):
-
-   docs/licenses
-   project
-   src/test/resources
-   utils
+License Version 2.0 (see below or http://www.mozilla.org/MPL/2.0/), with the
+following *exceptions*:
+
+- Files found in the following directories (and their sub-directories), which
+  are licensed under Public Domain
+  (see http://creativecommons.org/publicdomain/zero/1.0/):
+
+    docs/licenses
+    project
+    src/test/resources
+    utils
+
+- Files found in src/main/resources/dafny_axioms (and its sub-directories),
+  which are licensed under Microsoft Public License (Ms-PL)
 
 
 

src/main/resources/dafny_axioms/LICENSE.TXT

@@ -0,0 +1,61 @@
+Microsoft Public License (Ms-PL) 
+
+This license governs use of the accompanying software. If you use the 
+software, you accept this license. If you do not accept the license, do 
+not use the software. 
+
+1. Definitions 
+
+The terms "reproduce," "reproduction," "derivative works," and 
+"distribution" have the same meaning here as under U.S. copyright law. 
+
+A "contribution" is the original software, or any additions or changes 
+to the software. 
+
+A "contributor" is any person that distributes its contribution under 
+this license. 
+
+"Licensed patents" are a contributor's patent claims that read directly 
+on its contribution. 
+
+2. Grant of Rights 
+
+(A) Copyright Grant- Subject to the terms of this license, including the 
+license conditions and limitations in section 3, each contributor grants 
+you a non-exclusive, worldwide, royalty-free copyright license to 
+reproduce its contribution, prepare derivative works of its 
+contribution, and distribute its contribution or any derivative works 
+that you create. 
+
+(B) Patent Grant- Subject to the terms of this license, including the 
+license conditions and limitations in section 3, each contributor grants 
+you a non-exclusive, worldwide, royalty-free license under its licensed 
+patents to make, have made, use, sell, offer for sale, import, and/or 
+otherwise dispose of its contribution in the software or derivative 
+works of the contribution in the software. 
+
+3. Conditions and Limitations 
+
+(A) No Trademark License- This license does not grant you rights to use 
+any contributors' name, logo, or trademarks. 
+
+(B) If you bring a patent claim against any contributor over patents 
+that you claim are infringed by the software, your patent license from 
+such contributor to the software ends automatically. 
+
+(C) If you distribute any portion of the software, you must retain all 
+copyright, patent, trademark, and attribution notices that are present 
+in the software. 
+
+(D) If you distribute any portion of the software in source code form, 
+you may do so only under this license by including a complete copy of 
+this license with your distribution. If you distribute any portion of 
+the software in compiled or object code form, you may only do so under a 
+license that complies with this license. 
+
+(E) The software is licensed "as-is." You bear the risk of using it. The 
+contributors give no express warranties, guarantees or conditions. You 
+may have additional consumer rights under your local laws which this 
+license cannot change. To the extent permitted under your local laws, 
+the contributors exclude the implied warranties of merchantability, 
+fitness for a particular purpose and non-infringement.

src/main/resources/multisets_axioms_dafny.smt2 → src/main/resources/dafny_axioms/multisets_axioms_dafny.smt2

@@ -1,23 +1,24 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
 
-; These axioms correspond to Dafny's multiset axiomatisation from 2013-06-27.
-; They depend on the set axiomatisation due to the fromSet-function.
 
 ;
 ; Multiset axioms
 ;
 
 ;type MultiSet T = [T]int;
 
-
 ; 2013-07-24 Malte: Ignored for now. Not sure when it should be used.
 ;// ints are non-negative, used after havocing, and for conversion from sequences to multisets.
 ;axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) }
 ;  $IsGoodMultiSet(ms) <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx]));
 
-
 ;axiom (forall<T> s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s));
 (assert (forall ((xs $Multiset<$S$>)) (!
   (< 0 ($Multiset.card xs))

src/main/resources/multisets_declarations_dafny.smt2 → src/main/resources/dafny_axioms/multisets_declarations_dafny.smt2

@@ -1,9 +1,10 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
-
-; These declarations correspond to Dafny's multiset axiomatisation from 2013-06-27.
-; They depend on the set axiomatisation due to the fromSet-function.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
 
 
 

src/main/resources/sequences_axioms_dafny.smt2 → src/main/resources/dafny_axioms/sequences_axioms_dafny.smt2

@@ -1,6 +1,12 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
+
 
 ; General sequence axioms
 

src/main/resources/sequences_declarations_dafny.smt2 → src/main/resources/dafny_axioms/sequences_declarations_dafny.smt2

@@ -1,6 +1,12 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
+
 
 ; General sequence declarations
 

src/main/resources/sequences_int_axioms_dafny.smt2 → src/main/resources/dafny_axioms/sequences_int_axioms_dafny.smt2

@@ -1,6 +1,12 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
+
 
 ; Axioms specific to integer sequences
 

src/main/resources/dafny_axioms/sequences_int_declarations_dafny.smt2

@@ -0,0 +1,13 @@
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
+
+
+; Declarations specific to integer sequences
+
+(declare-fun $Seq.rng (Int Int) $Seq<Int>)

src/main/resources/sets_axioms_dafny.smt2 → src/main/resources/dafny_axioms/sets_axioms_dafny.smt2

@@ -1,8 +1,12 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
 
-; These axioms correspond to Dafny's set axiomatisation from 2013-06-27.
 
 ; type Set T = [T]bool;
 

src/main/resources/sets_declarations_dafny.smt2 → src/main/resources/dafny_axioms/sets_declarations_dafny.smt2

@@ -1,8 +1,12 @@
-; This Source Code Form is subject to the terms of the Mozilla Public
-; License, v. 2.0. If a copy of the MPL was not distributed with this
-; file, You can obtain one at http://mozilla.org/MPL/2.0/.
+; These axioms are derived from the corresponding axioms of the prelude of
+; Microsoft's Dafny tool by translating them from Boogie to SMT-LIB. Visit
+; http://dafny.codeplex.com for more information about the Dafny verifier.
+;
+; This file is subject to the terms of the Microsoft Public License
+; (Ms-PL). A copy of the Ms-PL can be found in the same directory in which
+; this file is located.
+
 
-; These declarations correspond to Dafny's set axiomatisation from 2013-06-27.
 
 (declare-fun $Set.in ($S$ $Set<$S$>) Bool)
 

src/main/scala/theories/Multisets.scala

@@ -71,14 +71,14 @@ class DefaultMultisetsEmitter(prover: Prover,
   def declareSymbols() {
     collectedSorts foreach {s =>
       prover.logComment(s"/multisets_declarations_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/multisets_declarations_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/multisets_declarations_dafny.smt2", s.elementsSort)
     }
   }
 
   def emitAxioms() {
     collectedSorts foreach {s =>
       prover.logComment(s"/multisets_axioms_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/multisets_axioms_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/multisets_axioms_dafny.smt2", s.elementsSort)
     }
   }
 }

src/main/scala/theories/Sequences.scala

@@ -69,24 +69,24 @@ class DefaultSequencesEmitter(prover: Prover,
   def declareSymbols() {
     collectedSorts foreach {s =>
       prover.logComment(s"/sequences_declarations_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/sequences_declarations_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sequences_declarations_dafny.smt2", s.elementsSort)
     }
 
     if (collectedSorts contains terms.sorts.Seq(terms.sorts.Int)) {
-      prover.logComment("/sequences_int_declarations_dafny.smt2")
-      preambleFileEmitter.emitSortParametricAssertions("/sequences_int_declarations_dafny.smt2", terms.sorts.Int)
+      prover.logComment("/dafny_axioms/sequences_int_declarations_dafny.smt2")
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sequences_int_declarations_dafny.smt2", terms.sorts.Int)
     }
   }
 
   def emitAxioms() {
     collectedSorts foreach {s =>
       prover.logComment(s"/sequences_axioms_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/sequences_axioms_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sequences_axioms_dafny.smt2", s.elementsSort)
     }
 
     if (collectedSorts contains terms.sorts.Seq(terms.sorts.Int)) {
-      prover.logComment("/sequences_int_axioms_dafny.smt2")
-      preambleFileEmitter.emitSortParametricAssertions("/sequences_int_axioms_dafny.smt2", terms.sorts.Int)
+      prover.logComment("/dafny_axioms/sequences_int_axioms_dafny.smt2")
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sequences_int_axioms_dafny.smt2", terms.sorts.Int)
     }
   }
 }

src/main/scala/theories/Sets.scala

@@ -74,14 +74,14 @@ class DefaultSetsEmitter(prover: Prover,
   def declareSymbols() {
     collectedSorts foreach {s =>
       prover.logComment(s"/sets_declarations_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/sets_declarations_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sets_declarations_dafny.smt2", s.elementsSort)
     }
   }
 
   def emitAxioms() {
     collectedSorts foreach {s =>
       prover.logComment(s"/sets_axioms_dafny.smt2 [${s.elementsSort}]")
-      preambleFileEmitter.emitSortParametricAssertions("/sets_axioms_dafny.smt2", s.elementsSort)
+      preambleFileEmitter.emitSortParametricAssertions("/dafny_axioms/sets_axioms_dafny.smt2", s.elementsSort)
     }
   }
 }