File tree Expand file tree Collapse file tree 4 files changed +13
-16
lines changed Expand file tree Collapse file tree 4 files changed +13
-16
lines changed Original file line number Diff line number Diff line change 3030 (IS_TOPIC :binary@prove )
3131 (IS_DATA :binary@prove )
3232 (LOG_ENTRY_SIZE :i32 )
33- (LOCAL_SIZE :i32 ))
34- ; ; (PHASE_ID :i16) defcomputedcolumn
33+ (LOCAL_SIZE :i32 )
34+ (PHASE_ID :i16 ))
3535
3636; ; aliases
3737(defalias
Original file line number Diff line number Diff line change 7171 (phase-constancy [PHASE 1] TXRCPT_SIZE))
7272
7373; ; 4.1.2 Global Phase Constraints ;;
74- (defcomputedcolumn (PHASE_ID :i16 )
75- (+
76- (* 1 [PHASE 1])
77- (* 2 [PHASE 2])
78- (* 3 [PHASE 3])
79- (* 4 [PHASE 4])
80- (* 5 [PHASE 5])
74+ (defconstraint impose-phase-id ()
75+ (eq! PHASE_ID
76+ (+ (reduce +
77+ (for k [1 : 5] (* k [PHASE k])))
8178 (* SUBPHASE_ID_WEIGHT_IS_PREFIX IS_PREFIX)
8279 (* SUBPHASE_ID_WEIGHT_IS_OT IS_TOPIC)
8380 (* SUBPHASE_ID_WEIGHT_IS_OD IS_DATA)
8481 (* SUBPHASE_ID_WEIGHT_DEPTH DEPTH_1)
85- (* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL)))
82+ (* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL))))
8683
8784(defconstraint initial-stamp (:domain {0})
8885 (begin (vanishes! ABS_TX_NUM)
Original file line number Diff line number Diff line change 3333 (IS_TOPIC :binary@prove )
3434 (IS_DATA :binary@prove )
3535 (LOG_ENTRY_SIZE :i32 )
36- (LOCAL_SIZE :i32 ))
37- ; ; (PHASE_ID :i16) defcomputedcolumn
36+ (LOCAL_SIZE :i32 )
37+ (PHASE_ID :i16 ))
3838
3939; ; aliases
4040(defalias
Original file line number Diff line number Diff line change 6868 (phase-constancy PHASE_1 TXRCPT_SIZE))
6969
7070; ; 4.1.2 Global Phase Constraints ;;
71- (defcomputedcolumn (PHASE_ID :i16 )
72- ( +
73- (* 1 PHASE_1)
71+ (defconstraint impose-phase-id ( )
72+ (eq! PHASE_ID
73+ ( + (* 1 PHASE_1)
7474 (* 2 PHASE_2)
7575 (* 3 PHASE_3)
7676 (* 5 PHASE_5)
7777 (* SUBPHASE_ID_WEIGHT_IS_PREFIX IS_PREFIX)
7878 (* SUBPHASE_ID_WEIGHT_IS_OT IS_TOPIC)
7979 (* SUBPHASE_ID_WEIGHT_IS_OD IS_DATA)
8080 (* SUBPHASE_ID_WEIGHT_DEPTH DEPTH_1)
81- (* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL)))
81+ (* SUBPHASE_ID_WEIGHT_INDEX_LOCAL IS_TOPIC INDEX_LOCAL))))
8282
8383(defconstraint initial-stamp (:domain {0})
8484 (begin (vanishes! ABS_TX_NUM)
You can’t perform that action at this time.
0 commit comments