Skip to content

Commit

Permalink
Merge pull request #684 from octalsrc/fix-smtdefinable
Browse files Browse the repository at this point in the history 
Fix SMTDefinable instances for 8-arg through 12-arg uninterpreted functions
  • Loading branch information
@LeventErkok
LeventErkok authored Mar 22, 2024
2 parents 98464ad + 8910010 commit a7c022d
Show file tree
Hide file tree
Showing 2 changed files with 156 additions and 5 deletions.
10 changes: 5 additions & 5 deletions Data/SBV/Core/Model.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2611,7 +2611,7 @@ instance (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c,
result st = do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7)
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki]) =<< retrieveUICode nm st ka uiKind
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
sw0 <- sbvToSV st arg0
sw1 <- sbvToSV st arg1
sw2 <- sbvToSV st arg2
Expand Down Expand Up @@ -2647,7 +2647,7 @@ instance (SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d,
result st = do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8)
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj]) =<< retrieveUICode nm st ka uiKind
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
sw0 <- sbvToSV st arg0
sw1 <- sbvToSV st arg1
sw2 <- sbvToSV st arg2
Expand Down Expand Up @@ -2685,7 +2685,7 @@ instance (SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e,
result st = do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9)
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk]) =<< retrieveUICode nm st ka uiKind
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
sw0 <- sbvToSV st arg0
sw1 <- sbvToSV st arg1
sw2 <- sbvToSV st arg2
Expand Down Expand Up @@ -2725,7 +2725,7 @@ instance (SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f,
result st = do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10)
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl]) =<< retrieveUICode nm st ka uiKind
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
sw0 <- sbvToSV st arg0
sw1 <- sbvToSV st arg1
sw2 <- sbvToSV st arg2
Expand Down Expand Up @@ -2767,7 +2767,7 @@ instance (SymVal m, SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g,
result st = do isSMT <- inSMTMode st
case (isSMT, uiKind) of
(True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11)
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl, km]) =<< retrieveUICode nm st ka uiKind
_ -> do newUninterpreted st (nm, mbArgs) (SBVType [km, kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
sw0 <- sbvToSV st arg0
sw1 <- sbvToSV st arg1
sw2 <- sbvToSV st arg2
Expand Down
151 changes: 151 additions & 0 deletions SBVTestSuite/TestSuite/Uninterpreted/Function.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,12 @@
-- Testsuite for Documentation.SBV.Examples.Uninterpreted.Function
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module TestSuite.Uninterpreted.Function(tests) where
Expand All @@ -17,8 +23,153 @@ import Documentation.SBV.Examples.Uninterpreted.Function

import Utils.SBVTestFramework

data A1
mkUninterpretedSort ''A1

data A2
mkUninterpretedSort ''A2

data A3
mkUninterpretedSort ''A3

data A4
mkUninterpretedSort ''A4

data A5
mkUninterpretedSort ''A5

data A6
mkUninterpretedSort ''A6

data A7
mkUninterpretedSort ''A7

data A8
mkUninterpretedSort ''A8

data A9
mkUninterpretedSort ''A9

data A10
mkUninterpretedSort ''A10

data A11
mkUninterpretedSort ''A11

data A12
mkUninterpretedSort ''A12


f1 :: SA1 -> SBool
f1 = uninterpret "f1"

f2 :: SA1 -> SA2 -> SBool
f2 = uninterpret "f2"

f3 :: SA1 -> SA2 -> SA3 -> SBool
f3 = uninterpret "f3"

f4 :: SA1 -> SA2 -> SA3 -> SA4 -> SBool
f4 = uninterpret "f4"

f5 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
f5 = uninterpret "f5"

f6 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
f6 = uninterpret "f6"

f7 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
f7 = uninterpret "f7"

f8 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
f8 = uninterpret "f8"

f9 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
f9 = uninterpret "f9"

f10 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
f10 = uninterpret "f10"

f11 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
f11 = uninterpret "f11"

f12 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
f12 = uninterpret "f12"

thm1 :: SA1 -> SA1 -> SBool
thm1 x a1 =
x .== a1
.=> f1 x .== f1 a1

thm2 :: SA1 -> SA1 -> SA2 -> SBool
thm2 x a1 a2 =
x .== a1
.=> f2 x a2 .== f2 a1 a2

thm3 :: SA1 -> SA1 -> SA2 -> SA3 -> SBool
thm3 x a1 a2 a3 =
x .== a1
.=> f3 x a2 a3 .== f3 a1 a2 a3

thm4 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SBool
thm4 x a1 a2 a3 a4 =
x .== a1
.=> f4 x a2 a3 a4 .== f4 a1 a2 a3 a4

thm5 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
thm5 x a1 a2 a3 a4 a5 =
x .== a1
.=> f5 x a2 a3 a4 a5 .== f5 a1 a2 a3 a4 a5

thm6 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
thm6 x a1 a2 a3 a4 a5 a6 =
x .== a1
.=> f6 x a2 a3 a4 a5 a6 .== f6 a1 a2 a3 a4 a5 a6

thm7 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
thm7 x a1 a2 a3 a4 a5 a6 a7 =
x .== a1
.=> f7 x a2 a3 a4 a5 a6 a7 .== f7 a1 a2 a3 a4 a5 a6 a7

thm8 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
thm8 x a1 a2 a3 a4 a5 a6 a7 a8 =
x .== a1
.=> f8 x a2 a3 a4 a5 a6 a7 a8 .== f8 a1 a2 a3 a4 a5 a6 a7 a8

thm9 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
thm9 x a1 a2 a3 a4 a5 a6 a7 a8 a9 =
x .== a1
.=> f9 x a2 a3 a4 a5 a6 a7 a8 a9 .== f9 a1 a2 a3 a4 a5 a6 a7 a8 a9

thm10 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
thm10 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
x .== a1
.=> f10 x a2 a3 a4 a5 a6 a7 a8 a9 a10 .== f10 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10

thm11 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
thm11 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
x .== a1
.=> f11 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 .== f11 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11

thm12 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
thm12 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
x .== a1
.=> f12 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 .== f12 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12

tests :: TestTree
tests =
testGroup "Uninterpreted.Function"
[ testCase "aufunc-0" (assertIsThm thmGood)
, testCase "aufunc-1" (assertIsThm thm1)
, testCase "aufunc-2" (assertIsThm thm2)
, testCase "aufunc-3" (assertIsThm thm3)
, testCase "aufunc-4" (assertIsThm thm4)
, testCase "aufunc-5" (assertIsThm thm5)
, testCase "aufunc-6" (assertIsThm thm6)
, testCase "aufunc-7" (assertIsThm thm7)
, testCase "aufunc-8" (assertIsThm thm8)
, testCase "aufunc-9" (assertIsThm thm9)
, testCase "aufunc-10" (assertIsThm thm10)
, testCase "aufunc-11" (assertIsThm thm11)
, testCase "aufunc-12" (assertIsThm thm12)
]

0 comments on commit a7c022d

Please sign in to comment.