search

jonnybest / Alloy2RelSMT

This is Alloy2RelSMT, a converter. It translates Alloy models into SMT files with a specific relational theory.
1 stars 0 forks source link

handle ordering functions efficiently #26

Closed jonnybest closed 11 years ago

jonnybest commented 12 years ago

as mentioned in 21dfe563b13063511a6a3439156c765165bba0a6 some functions and constants could be expensive. I should evaluate the need for having those functions and efficiently include or exclude them from a given model.

jonnybest commented 11 years ago

I have a number of commits trying to improve performance of ordering and cardinality. Probably the most significant is a5248e962c0deafec75f3c130da42fe47891b521, the lemma about cardX being the ord of lastX.

It looks like this:

(assert
(! 
; lemma about cardinality being the ord of lastMutex
(forall ((x Atom)) (=> (in_1 x lastMutex) (= (card_1 Mutex) (ord Mutex x)))) 
:named l6 
) 
)