From 5e8691afd402d0bd0e29f0ec340c19f77e379fa8 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 27 Dec 2024 14:15:57 -0800 Subject: [PATCH] make sure registration variables are internal also update golds --- Data/SBV/Core/Model.hs | 10 +- SBVTestSuite/GoldFiles/query_uisatex1.gold | 133 +++++++++--------- SBVTestSuite/GoldFiles/query_uisatex2.gold | 132 ++++++++--------- SBVTestSuite/GoldFiles/uiSat_test1.gold | 3 +- SBVTestSuite/GoldFiles/uiSat_test2.gold | 4 +- SBVTestSuite/GoldFiles/uiSat_test3.gold | 7 +- .../GoldFiles/unint-axioms-empty.gold | 15 +- SBVTestSuite/TestSuite/Basics/UISat.hs | 9 +- SBVTestSuite/TestSuite/Queries/UISatEx.hs | 7 +- .../TestSuite/Uninterpreted/Axioms.hs | 2 +- 10 files changed, 169 insertions(+), 153 deletions(-) diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs index 7e60bcfb3..419bbb60d 100644 --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -59,7 +59,7 @@ module Data.SBV.Core.Model ( import Control.Applicative (ZipList(ZipList)) import Control.Monad (when, unless, mplus) -import Control.Monad.IO.Class (MonadIO) +import Control.Monad.IO.Class (MonadIO, liftIO) import GHC.Generics (M1(..), U1(..), (:*:)(..), K1(..)) import qualified GHC.Generics as G @@ -2492,8 +2492,12 @@ class SMTDefinable a where cgUninterpret nm code v = sbvDefineValue nm Nothing $ UICodeC (v, code) sym = uninterpret - default registerSMTFunction :: (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic () - registerSMTFunction f = free_ >>= registerSMTFunction . f + default registerSMTFunction :: forall b c. (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic () + registerSMTFunction f = do let k = kindOf (Proxy @b) + st <- symbolicEnv + v <- liftIO $ internalVariable st k + let b = SBV $ SVal k $ Right $ cache (const (pure v)) + registerSMTFunction $ f b -- | Kind of uninterpretation data UIKind a = UIFree Bool -- ^ completely uninterpreted. If Bool is true, then this is curried. diff --git a/SBVTestSuite/GoldFiles/query_uisatex1.gold b/SBVTestSuite/GoldFiles/query_uisatex1.gold index 2bc9003b1..68fb0154b 100644 --- a/SBVTestSuite/GoldFiles/query_uisatex1.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex1.gold @@ -20,33 +20,34 @@ [GOOD] (define-fun s9 () Int (- 3)) [GOOD] (define-fun s11 () Int 9) [GOOD] (define-fun s14 () Int 1) -[GOOD] (define-fun s17 () Int 0) -[GOOD] (define-fun s20 () Int 5) -[GOOD] (define-fun s22 () Int 7) -[GOOD] (define-fun s24 () Int 6) -[GOOD] (define-fun s28 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0))) -[GOOD] (define-fun s31 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0))) -[GOOD] (define-fun s32 () Int 121) -[GOOD] (define-fun s37 () Int 8) -[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (_ +oo 8 24)) -[GOOD] (define-fun s41 () String (_ char #x63)) -[GOOD] (define-fun s42 () String "hey") -[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) -[GOOD] (define-fun s46 () String "tey") -[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0))) -[GOOD] (define-fun s50 () String (_ char #x72)) -[GOOD] (define-fun s51 () String "foo") -[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) -[GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) -[GOOD] (define-fun s56 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0))))) -[GOOD] (define-fun s59 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5))) -[GOOD] (define-fun s60 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))))) -[GOOD] (define-fun s62 () Int 21) -[GOOD] (define-fun s64 () (Seq Int) (seq.unit 5)) -[GOOD] (define-fun s65 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24)))) -[GOOD] (define-fun s67 () Int 210) +[GOOD] (define-fun s21 () Int 5) +[GOOD] (define-fun s23 () Int 7) +[GOOD] (define-fun s25 () Int 6) +[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0))) +[GOOD] (define-fun s32 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0))) +[GOOD] (define-fun s33 () Int 121) +[GOOD] (define-fun s38 () Int 8) +[GOOD] (define-fun s40 () (_ FloatingPoint 8 24) (_ +oo 8 24)) +[GOOD] (define-fun s42 () String (_ char #x63)) +[GOOD] (define-fun s43 () String "hey") +[GOOD] (define-fun s45 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) +[GOOD] (define-fun s47 () String "tey") +[GOOD] (define-fun s49 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0))) +[GOOD] (define-fun s51 () String (_ char #x72)) +[GOOD] (define-fun s52 () String "foo") +[GOOD] (define-fun s54 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) +[GOOD] (define-fun s56 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +[GOOD] (define-fun s57 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0))))) +[GOOD] (define-fun s60 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5))) +[GOOD] (define-fun s61 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))))) +[GOOD] (define-fun s63 () Int 21) +[GOOD] (define-fun s65 () (Seq Int) (seq.unit 5)) +[GOOD] (define-fun s66 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24)))) +[GOOD] (define-fun s68 () Int 210) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () Int) +[GOOD] (declare-fun s17 () Bool) ; tracks user variable "__internal_sbv_s17" +[GOOD] (declare-fun s18 () Int) ; tracks user variable "__internal_sbv_s18" [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- @@ -66,55 +67,59 @@ [GOOD] (define-fun s13 () Int (q1 s0)) [GOOD] (define-fun s15 () Int (+ s0 s14)) [GOOD] (define-fun s16 () Bool (= s13 s15)) -[GOOD] (define-fun s18 () Int (q2 false s17)) -[GOOD] (define-fun s19 () Int (q2 true s5)) -[GOOD] (define-fun s21 () Bool (= s19 s20)) -[GOOD] (define-fun s23 () Int (q2 false s22)) -[GOOD] (define-fun s25 () Bool (= s23 s24)) -[GOOD] (define-fun s26 () Int (q2 false s3)) -[GOOD] (define-fun s27 () Bool (= s5 s26)) -[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) (q3 s28 true s3)) -[GOOD] (define-fun s30 () Bool (fp.eq s28 s29)) -[GOOD] (define-fun s33 () (_ FloatingPoint 8 24) (q3 s31 true s32)) -[GOOD] (define-fun s34 () Bool (fp.isZero s33)) -[GOOD] (define-fun s35 () Bool (fp.isNegative s33)) -[GOOD] (define-fun s36 () Bool (and s34 s35)) -[GOOD] (define-fun s38 () (_ FloatingPoint 8 24) (q3 s31 false s37)) -[GOOD] (define-fun s40 () Bool (fp.eq s38 s39)) -[GOOD] (define-fun s43 () (_ FloatingPoint 8 24) (q4 s41 s42)) -[GOOD] (define-fun s45 () Bool (fp.eq s43 s44)) -[GOOD] (define-fun s47 () (_ FloatingPoint 8 24) (q4 s41 s46)) -[GOOD] (define-fun s49 () Bool (fp.eq s47 s48)) -[GOOD] (define-fun s52 () (_ FloatingPoint 8 24) (q4 s50 s51)) -[GOOD] (define-fun s54 () Bool (fp.eq s52 s53)) -[GOOD] (define-fun s57 () Int (q5 s55 s56)) -[GOOD] (define-fun s58 () Bool (= s22 s57)) -[GOOD] (define-fun s61 () Int (q5 s59 s60)) -[GOOD] (define-fun s63 () Bool (= s61 s62)) -[GOOD] (define-fun s66 () Int (q5 s64 s65)) -[GOOD] (define-fun s68 () Bool (= s66 s67)) +[GOOD] (define-fun s19 () Int (q2 s17 s18)) +[GOOD] (define-fun s20 () Int (q2 true s5)) +[GOOD] (define-fun s22 () Bool (= s20 s21)) +[GOOD] (define-fun s24 () Int (q2 false s23)) +[GOOD] (define-fun s26 () Bool (= s24 s25)) +[GOOD] (define-fun s27 () Int (q2 false s3)) +[GOOD] (define-fun s28 () Bool (= s5 s27)) +[GOOD] (define-fun s30 () (_ FloatingPoint 8 24) (q3 s29 true s3)) +[GOOD] (define-fun s31 () Bool (fp.eq s29 s30)) +[GOOD] (define-fun s34 () (_ FloatingPoint 8 24) (q3 s32 true s33)) +[GOOD] (define-fun s35 () Bool (fp.isZero s34)) +[GOOD] (define-fun s36 () Bool (fp.isNegative s34)) +[GOOD] (define-fun s37 () Bool (and s35 s36)) +[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (q3 s32 false s38)) +[GOOD] (define-fun s41 () Bool (fp.eq s39 s40)) +[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) (q4 s42 s43)) +[GOOD] (define-fun s46 () Bool (fp.eq s44 s45)) +[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) (q4 s42 s47)) +[GOOD] (define-fun s50 () Bool (fp.eq s48 s49)) +[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) (q4 s51 s52)) +[GOOD] (define-fun s55 () Bool (fp.eq s53 s54)) +[GOOD] (define-fun s58 () Int (q5 s56 s57)) +[GOOD] (define-fun s59 () Bool (= s23 s58)) +[GOOD] (define-fun s62 () Int (q5 s60 s61)) +[GOOD] (define-fun s64 () Bool (= s62 s63)) +[GOOD] (define-fun s67 () Int (q5 s65 s66)) +[GOOD] (define-fun s69 () Bool (= s67 s68)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s4) [GOOD] (assert s8) [GOOD] (assert s12) [GOOD] (assert s16) -[GOOD] (assert s21) -[GOOD] (assert s25) -[GOOD] (assert s27) -[GOOD] (assert s30) -[GOOD] (assert s36) -[GOOD] (assert s40) -[GOOD] (assert s45) -[GOOD] (assert s49) -[GOOD] (assert s54) -[GOOD] (assert s58) -[GOOD] (assert s63) -[GOOD] (assert s68) +[GOOD] (assert s22) +[GOOD] (assert s26) +[GOOD] (assert s28) +[GOOD] (assert s31) +[GOOD] (assert s37) +[GOOD] (assert s41) +[GOOD] (assert s46) +[GOOD] (assert s50) +[GOOD] (assert s55) +[GOOD] (assert s59) +[GOOD] (assert s64) +[GOOD] (assert s69) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 0)) +[SEND] (get-value (s17)) +[RECV] ((s17 false)) +[SEND] (get-value (s18)) +[RECV] ((s18 0)) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold index 449716bb3..ba8f25fbe 100644 --- a/SBVTestSuite/GoldFiles/query_uisatex2.gold +++ b/SBVTestSuite/GoldFiles/query_uisatex2.gold @@ -20,33 +20,35 @@ [GOOD] (define-fun s9 () Int (- 3)) [GOOD] (define-fun s11 () Int 9) [GOOD] (define-fun s14 () Int 1) -[GOOD] (define-fun s17 () Int 0) -[GOOD] (define-fun s20 () Int 5) -[GOOD] (define-fun s22 () Int 7) -[GOOD] (define-fun s24 () Int 6) -[GOOD] (define-fun s28 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0))) -[GOOD] (define-fun s31 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0))) -[GOOD] (define-fun s32 () Int 121) -[GOOD] (define-fun s37 () Int 8) -[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (_ +oo 8 24)) -[GOOD] (define-fun s41 () String (_ char #x63)) -[GOOD] (define-fun s42 () String "hey") -[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) -[GOOD] (define-fun s46 () String "tey") -[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0))) -[GOOD] (define-fun s50 () String (_ char #x72)) -[GOOD] (define-fun s51 () String "foo") -[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) -[GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) -[GOOD] (define-fun s56 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0))))) -[GOOD] (define-fun s59 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5))) -[GOOD] (define-fun s60 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))))) -[GOOD] (define-fun s62 () Int 21) -[GOOD] (define-fun s64 () (Seq Int) (seq.unit 5)) -[GOOD] (define-fun s65 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24)))) -[GOOD] (define-fun s67 () Int 210) +[GOOD] (define-fun s21 () Int 5) +[GOOD] (define-fun s23 () Int 7) +[GOOD] (define-fun s25 () Int 6) +[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0))) +[GOOD] (define-fun s32 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0))) +[GOOD] (define-fun s33 () Int 121) +[GOOD] (define-fun s38 () Int 8) +[GOOD] (define-fun s40 () (_ FloatingPoint 8 24) (_ +oo 8 24)) +[GOOD] (define-fun s42 () String (_ char #x63)) +[GOOD] (define-fun s43 () String "hey") +[GOOD] (define-fun s45 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0))) +[GOOD] (define-fun s47 () String "tey") +[GOOD] (define-fun s49 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0))) +[GOOD] (define-fun s51 () String (_ char #x72)) +[GOOD] (define-fun s52 () String "foo") +[GOOD] (define-fun s54 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0))) +[GOOD] (define-fun s56 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) +[GOOD] (define-fun s57 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0))))) +[GOOD] (define-fun s60 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5))) +[GOOD] (define-fun s61 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0))))) +[GOOD] (define-fun s63 () Int 21) +[GOOD] (define-fun s65 () (Seq Int) (seq.unit 5)) +[GOOD] (define-fun s66 () (Seq (_ FloatingPoint 8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24)))) +[GOOD] (define-fun s68 () Int 210) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () Int) +[GOOD] (declare-fun s17 () Bool) ; tracks user variable "__internal_sbv_s17" +[GOOD] (declare-fun s18 () Int) ; tracks user variable "__internal_sbv_s18" +[GOOD] (declare-fun s70 () Int) ; tracks user variable "__internal_sbv_s70" [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- @@ -67,52 +69,52 @@ [GOOD] (define-fun s13 () Int (q1 s0)) [GOOD] (define-fun s15 () Int (+ s0 s14)) [GOOD] (define-fun s16 () Bool (= s13 s15)) -[GOOD] (define-fun s18 () Int (q2 false s17)) -[GOOD] (define-fun s19 () Int (q2 true s5)) -[GOOD] (define-fun s21 () Bool (= s19 s20)) -[GOOD] (define-fun s23 () Int (q2 false s22)) -[GOOD] (define-fun s25 () Bool (= s23 s24)) -[GOOD] (define-fun s26 () Int (q2 false s3)) -[GOOD] (define-fun s27 () Bool (= s5 s26)) -[GOOD] (define-fun s29 () (_ FloatingPoint 8 24) (q3 s28 true s3)) -[GOOD] (define-fun s30 () Bool (fp.eq s28 s29)) -[GOOD] (define-fun s33 () (_ FloatingPoint 8 24) (q3 s31 true s32)) -[GOOD] (define-fun s34 () Bool (fp.isZero s33)) -[GOOD] (define-fun s35 () Bool (fp.isNegative s33)) -[GOOD] (define-fun s36 () Bool (and s34 s35)) -[GOOD] (define-fun s38 () (_ FloatingPoint 8 24) (q3 s31 false s37)) -[GOOD] (define-fun s40 () Bool (fp.eq s38 s39)) -[GOOD] (define-fun s43 () (_ FloatingPoint 8 24) (q4 s41 s42)) -[GOOD] (define-fun s45 () Bool (fp.eq s43 s44)) -[GOOD] (define-fun s47 () (_ FloatingPoint 8 24) (q4 s41 s46)) -[GOOD] (define-fun s49 () Bool (fp.eq s47 s48)) -[GOOD] (define-fun s52 () (_ FloatingPoint 8 24) (q4 s50 s51)) -[GOOD] (define-fun s54 () Bool (fp.eq s52 s53)) -[GOOD] (define-fun s57 () Int (q5 s55 s56)) -[GOOD] (define-fun s58 () Bool (= s22 s57)) -[GOOD] (define-fun s61 () Int (q5 s59 s60)) -[GOOD] (define-fun s63 () Bool (= s61 s62)) -[GOOD] (define-fun s66 () Int (q5 s64 s65)) -[GOOD] (define-fun s68 () Bool (= s66 s67)) -[GOOD] (define-fun s69 () Bool (q6 s17)) +[GOOD] (define-fun s19 () Int (q2 s17 s18)) +[GOOD] (define-fun s20 () Int (q2 true s5)) +[GOOD] (define-fun s22 () Bool (= s20 s21)) +[GOOD] (define-fun s24 () Int (q2 false s23)) +[GOOD] (define-fun s26 () Bool (= s24 s25)) +[GOOD] (define-fun s27 () Int (q2 false s3)) +[GOOD] (define-fun s28 () Bool (= s5 s27)) +[GOOD] (define-fun s30 () (_ FloatingPoint 8 24) (q3 s29 true s3)) +[GOOD] (define-fun s31 () Bool (fp.eq s29 s30)) +[GOOD] (define-fun s34 () (_ FloatingPoint 8 24) (q3 s32 true s33)) +[GOOD] (define-fun s35 () Bool (fp.isZero s34)) +[GOOD] (define-fun s36 () Bool (fp.isNegative s34)) +[GOOD] (define-fun s37 () Bool (and s35 s36)) +[GOOD] (define-fun s39 () (_ FloatingPoint 8 24) (q3 s32 false s38)) +[GOOD] (define-fun s41 () Bool (fp.eq s39 s40)) +[GOOD] (define-fun s44 () (_ FloatingPoint 8 24) (q4 s42 s43)) +[GOOD] (define-fun s46 () Bool (fp.eq s44 s45)) +[GOOD] (define-fun s48 () (_ FloatingPoint 8 24) (q4 s42 s47)) +[GOOD] (define-fun s50 () Bool (fp.eq s48 s49)) +[GOOD] (define-fun s53 () (_ FloatingPoint 8 24) (q4 s51 s52)) +[GOOD] (define-fun s55 () Bool (fp.eq s53 s54)) +[GOOD] (define-fun s58 () Int (q5 s56 s57)) +[GOOD] (define-fun s59 () Bool (= s23 s58)) +[GOOD] (define-fun s62 () Int (q5 s60 s61)) +[GOOD] (define-fun s64 () Bool (= s62 s63)) +[GOOD] (define-fun s67 () Int (q5 s65 s66)) +[GOOD] (define-fun s69 () Bool (= s67 s68)) +[GOOD] (define-fun s71 () Bool (q6 s70)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s4) [GOOD] (assert s8) [GOOD] (assert s12) [GOOD] (assert s16) -[GOOD] (assert s21) -[GOOD] (assert s25) -[GOOD] (assert s27) -[GOOD] (assert s30) -[GOOD] (assert s36) -[GOOD] (assert s40) -[GOOD] (assert s45) -[GOOD] (assert s49) -[GOOD] (assert s54) -[GOOD] (assert s58) -[GOOD] (assert s63) -[GOOD] (assert s68) +[GOOD] (assert s22) +[GOOD] (assert s26) +[GOOD] (assert s28) +[GOOD] (assert s31) +[GOOD] (assert s37) +[GOOD] (assert s41) +[GOOD] (assert s46) +[GOOD] (assert s50) +[GOOD] (assert s55) +[GOOD] (assert s59) +[GOOD] (assert s64) +[GOOD] (assert s69) [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) diff --git a/SBVTestSuite/GoldFiles/uiSat_test1.gold b/SBVTestSuite/GoldFiles/uiSat_test1.gold index 03054d216..d63fc605e 100644 --- a/SBVTestSuite/GoldFiles/uiSat_test1.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test1.gold @@ -11,13 +11,14 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0" [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- [GOOD] (declare-fun q1 (Bool) Bool) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s0 () Bool (q1 false)) +[GOOD] (define-fun s1 () Bool (q1 s0)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- *** Checking Satisfiability, all solutions.. diff --git a/SBVTestSuite/GoldFiles/uiSat_test2.gold b/SBVTestSuite/GoldFiles/uiSat_test2.gold index 8618fa0c4..b51f9d790 100644 --- a/SBVTestSuite/GoldFiles/uiSat_test2.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test2.gold @@ -11,13 +11,15 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0" +[GOOD] (declare-fun s1 () Bool) ; tracks user variable "__internal_sbv_s1" [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- [GOOD] (declare-fun q2 (Bool Bool) Bool) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s0 () Bool (q2 false false)) +[GOOD] (define-fun s2 () Bool (q2 s0 s1)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- *** Checking Satisfiability, all solutions.. diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold index 1bc153188..d6c660bd1 100644 --- a/SBVTestSuite/GoldFiles/uiSat_test3.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test3.gold @@ -11,6 +11,9 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0" +[GOOD] (declare-fun s2 () Bool) ; tracks user variable "__internal_sbv_s2" +[GOOD] (declare-fun s3 () Bool) ; tracks user variable "__internal_sbv_s3" [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- @@ -18,8 +21,8 @@ [GOOD] (declare-fun q2 (Bool Bool) Bool) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- -[GOOD] (define-fun s0 () Bool (q1 false)) -[GOOD] (define-fun s1 () Bool (q2 false false)) +[GOOD] (define-fun s1 () Bool (q1 s0)) +[GOOD] (define-fun s4 () Bool (q2 s2 s3)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- *** Checking Satisfiability, all solutions.. diff --git a/SBVTestSuite/GoldFiles/unint-axioms-empty.gold b/SBVTestSuite/GoldFiles/unint-axioms-empty.gold index b23803d75..01d692074 100644 --- a/SBVTestSuite/GoldFiles/unint-axioms-empty.gold +++ b/SBVTestSuite/GoldFiles/unint-axioms-empty.gold @@ -12,10 +12,11 @@ [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- -[GOOD] (define-fun s2 () Thing Thing_witness) [GOOD] ; --- top level inputs --- -[GOOD] (declare-fun s4 () Thing) +[GOOD] (declare-fun s2 () Thing) ; tracks user variable "__internal_sbv_s2" +[GOOD] (declare-fun s3 () Thing) ; tracks user variable "__internal_sbv_s3" [GOOD] (declare-fun s5 () Thing) +[GOOD] (declare-fun s6 () Thing) [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- @@ -29,15 +30,15 @@ (let ((l1_s2 (thingMerge l1_s0 l1_s1))) (let ((l1_s3 (distinct l1_s0 l1_s2))) l1_s3)))) -[GOOD] (define-fun s3 () Thing (thingMerge s2 s2)) -[GOOD] (define-fun s6 () Bool (= s4 s5)) -[GOOD] (define-fun s7 () Bool (thingCompare s4 s5)) -[GOOD] (define-fun s8 () Bool (=> s6 s7)) +[GOOD] (define-fun s4 () Thing (thingMerge s2 s3)) +[GOOD] (define-fun s7 () Bool (= s5 s6)) +[GOOD] (define-fun s8 () Bool (thingCompare s5 s6)) +[GOOD] (define-fun s9 () Bool (=> s7 s8)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s0) [GOOD] (assert s1) -[GOOD] (assert (not s8)) +[GOOD] (assert (not s9)) [SEND] (check-sat) [RECV] unsat *** Solver : Z3 diff --git a/SBVTestSuite/TestSuite/Basics/UISat.hs b/SBVTestSuite/TestSuite/Basics/UISat.hs index 03a053744..7f89cd2bc 100644 --- a/SBVTestSuite/TestSuite/Basics/UISat.hs +++ b/SBVTestSuite/TestSuite/Basics/UISat.hs @@ -14,7 +14,6 @@ module TestSuite.Basics.UISat(tests) where -import Data.SBV.Control import Utils.SBVTestFramework -- Test suite @@ -45,15 +44,15 @@ q2 = uninterpret "q2" test1 :: ConstraintSet test1 = do setLogic Logic_ALL - registerUISMTFunction q1 + registerSMTFunction q1 test2 :: ConstraintSet test2 = do setLogic Logic_ALL - registerUISMTFunction q2 + registerSMTFunction q2 test3 :: ConstraintSet test3 = do setLogic Logic_ALL - registerUISMTFunction q1 - registerUISMTFunction q2 + registerSMTFunction q1 + registerSMTFunction q2 {- HLint ignore module "Reduce duplication" -} diff --git a/SBVTestSuite/TestSuite/Queries/UISatEx.hs b/SBVTestSuite/TestSuite/Queries/UISatEx.hs index 12619bbe6..017e4820b 100644 --- a/SBVTestSuite/TestSuite/Queries/UISatEx.hs +++ b/SBVTestSuite/TestSuite/Queries/UISatEx.hs @@ -47,9 +47,8 @@ testQuery2 rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=J where qCore = do core let q6 :: SInteger -> SBool q6 = uninterpret "q6" - constrain $ q6 0 .=> q6 0 - query $ do registerUISMTFunction q6 -- Not really necessary, but testing it doesn't break anything - ensureSat + registerSMTFunction q6 + query $ do ensureSat qv1 <- getFunction q1 qv2 <- getFunction q2 qv3 <- getFunction q3 @@ -80,7 +79,7 @@ core = do x <- sInteger_ constrain $ q1 (-3) .== 9 constrain $ q1 x .== x+1 - registerUISMTFunction q2 -- Not really necessary, but testing it doesn't break anything + registerSMTFunction q2 -- Not really necessary, but testing it doesn't break anything constrain $ q2 sTrue 3 .== 5 constrain $ q2 sFalse 7 .== 6 constrain $ q2 sFalse 12 .== 3 diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs b/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs index b6b39a528..072b7ea0f 100644 --- a/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs +++ b/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs @@ -62,7 +62,7 @@ thingMerge = uninterpret "thingMerge" p1 :: Symbolic SBool p1 = do constrain $ \(Forall x) -> thingCompare x x constrain $ \(Forall k1) (Forall k2) -> k1 ./= thingMerge k1 k2 - registerUISMTFunction thingMerge + registerSMTFunction thingMerge k1 <- free_ k2 <- free_ return $ k1 .== k2 .=> thingCompare k1 k2