From 952fcb88797a1771eb018e63e8446055e944e035 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 17 Jan 2018 18:51:42 +0000
Subject: Modified unification so Type_check.instantiation_of works after
 sizeof rewriting

This change allows the AST to be type-checked after sizeof
re-writing. It modifies the unification algorithm to better support
checking multiplication in constraints, by using division and modulus
SMT operators if they are defined.

Also made sure the typechecker doesn't re-introduce E_constraint
nodes, otherwise re-checking after sizeof-rewriting will re-introduce
constraint nodes.
---
 aarch64/prelude.sail | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'aarch64')

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index e81dddcb..ca7e872d 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -5,6 +5,14 @@ type bits ('n : Int) = vector('n, dec, bit)
 
 infix 4 ==
 
+val div = {
+  smt : "div"
+} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm))
+
+val mod = {
+  smt : "mod"
+} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
+
 val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool
 val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
 val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-- 
cgit v1.2.3