Support pair equality in rewriter. (#2009)

* Support pair equality in rewriter. * Address comments.
GaloisInc · Jan 16, 2024 · 9af2e0e · 9af2e0e
1 parent db2b19a
commit 9af2e0e
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/intTests/test2009/test.saw 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
@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -326,6 +326,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"
 
@@ -394,6 +397,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