SMT-LIB 2.6 conformance, support for cvc5, and generalization for alternative SMT-solvers

README.md

@@ -134,6 +134,7 @@ method main() {
 * You need recent installations of
   1. the [sbt build tool](https://www.scala-sbt.org/)
   2. the [Z3 SMT solver](https://github.com/Z3Prover/z3/releases)
+  3. the [cvc5 SMT solver](https://github.com/cvc5/cvc5/releases)
 * Clone this repository *recursively* by running:  
 `git clone --recursive https://github.com/viperproject/silicon`
 

src/main/resources/cvc5config.smt2

@@ -0,0 +1,20 @@
+; 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/.
+
+; Requires CVC5 >= 1.0.0
+(set-option :print-success true)
+
+(set-logic ALL)
+(set-option :seed 0)
+(set-option :sat-random-seed 0)
+
+; default options as used by boogie
+(set-option :incremental true) ; required for push and pop
+(set-option :condense-function-values false)
+(set-option :strict-parsing false)
+(set-option :produce-models true) ; enabled to support proverStdIO. retrieveAndSaveModel
+
+; Translated from z3config
+(set-option :global-declarations true)
+(set-option :type-checking true)

src/main/resources/field_value_functions_axioms.smt2

@@ -12,11 +12,11 @@
 ; been emitted.
 
 (assert (forall ((vs $FVF<$T$>) (ws $FVF<$T$>)) (!
-    (implies
+    (=>
       (and
         (Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
         (forall ((x $Ref)) (!
-          (implies
+          (=>
             (Set_in x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
           ; :pattern ((Set_in x ($FVF.domain_$FLD$ vs)))
@@ -33,8 +33,8 @@
 
 (assert (forall ((r $Ref) (pm $FPM)) (!
     ($Perm.isValidVar ($FVF.perm_$FLD$ pm r))
-    :pattern ($FVF.perm_$FLD$ pm r))))
+    :pattern (($FVF.perm_$FLD$ pm r))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.
 
 (assert (forall ((r $Ref) (f $S$)) (!
     (= ($FVF.loc_$FLD$ f r) true)
-    :pattern ($FVF.loc_$FLD$ f r))))
+    :pattern (($FVF.loc_$FLD$ f r))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.

src/main/resources/field_value_functions_axioms_no_triggers.smt2

@@ -12,11 +12,11 @@
 ; been emitted.
 
 (assert (forall ((vs $FVF<$T$>) (ws $FVF<$T$>)) (!
-    (implies
+    (=>
       (and
         (Set_equal ($FVF.domain_$FLD$ vs) ($FVF.domain_$FLD$ ws))
         (forall ((x $Ref)) (!
-          (implies
+          (=>
             (Set_in x ($FVF.domain_$FLD$ vs))
             (= ($FVF.lookup_$FLD$ vs x) ($FVF.lookup_$FLD$ ws x)))
           :qid |qp.$FVF<$T$>-eq-inner|

src/main/resources/preamble.smt2

@@ -10,8 +10,8 @@
 
 ; --- Snapshots ---
 
-(declare-datatypes () ((
-    $Snap ($Snap.unit)
+(declare-datatypes (($Snap 0)) ((
+    ($Snap.unit)
     ($Snap.combine ($Snap.first $Snap) ($Snap.second $Snap)))))
 
 ; --- References ---
@@ -21,8 +21,8 @@
 
 ; --- Permissions ---
 
-(declare-sort $FPM)
-(declare-sort $PPM)
+(declare-sort $FPM 0)
+(declare-sort $PPM 0)
 (define-sort $Perm () Real)
 
 (define-const $Perm.Write $Perm 1.0)

src/main/resources/predicate_snap_functions_axioms.smt2

@@ -11,11 +11,11 @@
 ; been emitted.
 
 (assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
-    (implies
+    (=>
       (and
         (Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
         (forall ((x $Snap)) (!
-          (implies
+          (=>
             (Set_in x ($PSF.domain_$PRD$ vs))
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
           ; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
@@ -32,8 +32,8 @@
 
 (assert (forall ((s $Snap) (pm $PPM)) (!
     ($Perm.isValidVar ($PSF.perm_$PRD$ pm s))
-    :pattern ($PSF.perm_$PRD$ pm s))))
+    :pattern (($PSF.perm_$PRD$ pm s))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.
 
 (assert (forall ((s $Snap) (f $S$)) (!
     (= ($PSF.loc_$PRD$ f s) true)
-    :pattern ($PSF.loc_$PRD$ f s))))
+    :pattern (($PSF.loc_$PRD$ f s))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.

src/main/resources/predicate_snap_functions_axioms_no_triggers.smt2

@@ -11,11 +11,11 @@
 ; been emitted.
 
 (assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
-    (implies
+    (=>
       (and
         (Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
         (forall ((x $Snap)) (!
-          (implies
+          (=>
             (Set_in x ($PSF.domain_$FRD$ vs))
             (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
           :qid |qp.$PSF<$S$>-eq-inner|