From f36bf3a8deb021414e751d87f5b4927f566eaf98 Mon Sep 17 00:00:00 2001 From: Andrei Date: Sun, 14 Jan 2024 05:25:05 +0000 Subject: [PATCH 1/2] Support pair equality in rewriter. --- saw-core/src/Verifier/SAW/Rewriter.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index aa51f2638d..e1de79c3df 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -325,6 +325,9 @@ boolEqIdent = mkIdent (mkModuleName ["Prelude"]) "boolEq" vecEqIdent :: Ident vecEqIdent = mkIdent (mkModuleName ["Prelude"]) "vecEq" +pairEqIdent :: Ident +pairEqIdent = mkIdent (mkModuleName ["Prelude"]) "pairEq" + arrayEqIdent :: Ident arrayEqIdent = mkIdent (mkModuleName ["Prelude"]) "arrayEq" @@ -393,6 +396,7 @@ ruleOfProp sc term ann = (R.asApplyAll -> (R.isGlobalDef equalNatIdent -> Just (), [x, y])) -> eqRule x y (R.asApplyAll -> (R.isGlobalDef boolEqIdent -> Just (), [x, y])) -> eqRule x y (R.asApplyAll -> (R.isGlobalDef vecEqIdent -> Just (), [_, _, _, x, y])) -> eqRule x y + (R.asApplyAll -> (R.isGlobalDef pairEqIdent -> Just (), [_, _, _, _, x, y])) -> eqRule x y (R.asApplyAll -> (R.isGlobalDef arrayEqIdent -> Just (), [_, _, x, y])) -> eqRule x y (R.asApplyAll -> (R.isGlobalDef intEqIdent -> Just (), [x, y])) -> eqRule x y (R.asApplyAll -> (R.isGlobalDef intModEqIdent -> Just (), [_, x, y])) -> eqRule x y From 61738e9355900e5b63c8892b378931be96ea582a Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 03:37:28 +0000 Subject: [PATCH 2/2] Address comments. --- intTests/test2009/test.saw | 4 ++++ intTests/test2009/test.sh | 4 ++++ 2 files changed, 8 insertions(+) create mode 100644 intTests/test2009/test.saw create mode 100644 intTests/test2009/test.sh diff --git a/intTests/test2009/test.saw b/intTests/test2009/test.saw new file mode 100644 index 0000000000..f4c5adc448 --- /dev/null +++ b/intTests/test2009/test.saw @@ -0,0 +1,4 @@ +let pairEq = parse_core "pairEq (Vec 32 Bool) (Vec 32 Bool) (bvEq 32) (bvEq 32)"; +t <- prove_print w4 {{ \x -> pairEq (x, x + 1) (x, 1 + x) }}; +print_term (rewrite (addsimp t empty_ss) {{ (0 : [32], 0 + 1 : [32]) }}); + diff --git a/intTests/test2009/test.sh b/intTests/test2009/test.sh new file mode 100644 index 0000000000..d0c501894a --- /dev/null +++ b/intTests/test2009/test.sh @@ -0,0 +1,4 @@ +set -e + +$SAW test.saw +