|
353 | 353 |
|
354 | 354 | (egglog-program-add! `(ruleset lifting) curr-program) |
355 | 355 |
|
356 | | - ;;; Adding function unsound before rules |
| 356 | + ;;; Adding function unsound? before rules |
357 | 357 |
|
358 | | - ;; unsound functions |
359 | | - (egglog-program-add! `(function unsound () bool :merge (or old new)) curr-program) |
| 358 | + ;; unsound detection function |
| 359 | + (egglog-program-add! `(function unsound? () bool :merge (or old new)) curr-program) |
360 | 360 | (egglog-program-add! `(ruleset unsound-rule) curr-program) |
361 | | - (egglog-program-add! `(set (unsound) false) curr-program) |
| 361 | + (egglog-program-add! `(set (unsound?) false) curr-program) |
362 | 362 |
|
363 | 363 | (egglog-program-add! |
364 | | - `(rule ((= (Num c1) (Num c2)) (!= c1 c2)) ((set (unsound) true)) :ruleset unsound-rule) |
| 364 | + `(rule ((= (Num c1) (Num c2)) (!= c1 c2)) ((set (unsound?) true)) :ruleset unsound-rule) |
365 | 365 | curr-program) |
366 | 366 |
|
367 | 367 | (for ([curr-expr const-fold]) |
|
825 | 825 | ;; 1. Run (PUSH) to the save the above state of the egraph |
826 | 826 | ;; 2. Repeat rules based on their ruleset tag once |
827 | 827 | ;; 3. Run the unsound-rule function ruleset once |
828 | | - ;; 4. Extract the (unsound) function that returns a bool |
829 | | - ;; 5. If (unsound) function returns "true", we have unsoundless, so go to Step 10 for ROLLBACK |
| 828 | + ;; 4. Extract the (unsound?) function that returns a bool |
| 829 | + ;; 5. If (unsound?) function returns "true", we have unsoundless, so go to Step 10 for ROLLBACK |
830 | 830 | ;; 6. Run (print-size) to get nodes of the form "node_name : num_nodes" for all nodes in egraph |
831 | 831 | ;; 7. If the total number of nodes is more than node-limit, do NOT ROLLBACK and go to Step 11 |
832 | 832 | ;; 8. Repeat rules based on the const-fold tag once and repeat Steps 3-7 |
|
853 | 853 | `(run-schedule (repeat 1 ,tag)) |
854 | 854 | '(print-size) |
855 | 855 | '(run unsound-rule 1) |
856 | | - '(extract (unsound)))) |
| 856 | + '(extract (unsound?)))) |
857 | 857 |
|
858 | 858 | ;; Get egglog output |
859 | 859 | (define-values (math-unsound? math-node-limit? math-total-nodes) |
|
913 | 913 | `(run-schedule (repeat 1 const-fold)) |
914 | 914 | '(print-size) |
915 | 915 | '(run unsound-rule 1) |
916 | | - '(extract (unsound)))) |
| 916 | + '(extract (unsound?)))) |
917 | 917 |
|
918 | 918 | (define-values (const-unsound? const-node-limit? const-total-nodes) |
919 | 919 | (get-egglog-output const-schedule |
|
0 commit comments