github/Picus
1
1
Fork 0
mirror of https://github.com/Veridise/Picus.git synced 2026-05-11 03:00:06 -04:00
Code Issues Packages Projects Releases Wiki Activity

fix: speed up variable extractions (#32)

Browse Source 
Prior this commit, the variables are repeatedly appended at the back of
a list, causing quadratic running time. Since ordering doesn't matter,
this commit makes it appends to the front instead.

Note that the algorithm overall is still potentially quadratic.
A proper fix needs to changes the interface significantly to introduce
an additional accumulator. This commit simply makes a minimal fix for
the immediate issue that we are having,
which causes CompConstant to get stuck.
This commit is contained in:
sorawee
2023-09-07 16:46:05 -07:00
committed by GitHub
parent 2b28e47055
commit f696a052a2
1 changed files with 21 additions and 84 deletions
Download Patch File Download Diff File Expand all files Collapse all files

105
picus/r1cs/r1cs-grammar.rkt
View File

@@ -125,12 +125,7 @@
; define internal function
(define (do obj0)
(match obj0
[(rcmds vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rcmds vs) (append* (for/list ([v vs]) (do v)))]
[(rraw v) (list )]
[(rlogic v) (list )]
[(rdef v t) (list )]
@@ -143,19 +138,9 @@
[(rlt lhs rhs) (append (do lhs) (do rhs))]
[(rgeq lhs rhs) (append (do lhs) (do rhs))]
[(rgt lhs rhs) (append (do lhs) (do rhs))]
[(rand vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rand vs) (append* (for/list ([v vs]) (do v)))]
[(rimp lhs rhs) (append (do lhs) (do rhs))]
[(ror vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(ror vs) (append* (for/list ([v vs]) (do v)))]
[(rint v) (list )]
[(rvar v)
; (fixme) we here assume prefix is either "x" or "y"
@@ -173,26 +158,11 @@
)
]
[(rtype v) (list )]
[(radd vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rsub vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rmul vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(radd vs) (append* (for/list ([v vs]) (do v)))]
[(rsub vs) (append* (for/list ([v vs]) (do v)))]
[(rmul vs) (append* (for/list ([v vs]) (do v)))]
[(rmod v mod) (append (do v) (do mod))]
[else (tokamak:exit "not supported: ~a" obj0)]
[_ (tokamak:exit "not supported: ~a" obj0)]
)
)
; then call it and remove duplicates, and return
@@ -214,12 +184,7 @@
; define internal function
(define (do obj0)
(match obj0
[(rcmds vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rcmds vs) (append* (for/list ([v vs]) (do v)))]
[(rraw v) (list )]
[(rlogic v) (list )]
[(rdef v t) (list )]
@@ -246,18 +211,8 @@
)
]
[(rtype v) (list )]
[(radd vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(rsub vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v))))
res
)
]
[(radd vs) (append* (for/list ([v vs]) (do v)))]
[(rsub vs) (append* (for/list ([v vs]) (do v)))]
; (assumed optimized version)
; - 1*x will be x, which will not be captured by rmul
; - (fixme) this could be wrong, a*x is treated as linear,
@@ -275,7 +230,7 @@
)
]
[(rmod v mod) (append (do v) (do mod))]
[else (tokamak:exit "not supported: ~a" obj0)]
[_ (tokamak:exit "not supported: ~a" obj0)]
)
)
; then call it and remove duplicates, and return
@@ -286,12 +241,7 @@
; define internal function
(define (do obj0 [include? #f])
(match obj0
[(rcmds vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v include?))))
res
)
]
[(rcmds vs) (append* (for/list ([v vs]) (do v include?)))]
[(rraw v) (list )]
[(rlogic v) (list )]
[(rdef v t) (list )]
@@ -323,30 +273,17 @@
]
[(rtype v) (list )]
[(radd vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v include?))))
res
)
]
[(rsub vs)
(let ([res (list )])
(for ([v vs]) (set! res (append res (do v include?))))
res
)
]
(append* (for/list ([v vs]) (do v include?)))]
[(rsub vs) (append* (for/list ([v vs]) (do v include?)))]
[(rmul vs)
(let ([res (list )][vv (filter (lambda (x) (rvar? x)) vs)])
(if (<= (length vv) 1)
; less than 1 var, this is just linear
(set! res (list ))
; more than 1 var, all involved vars are non-linear
(for ([v vv]) (set! res (append res (do v #t))))
)
res
)
]
(define vv (filter (lambda (x) (rvar? x)) vs))
(if (<= (length vv) 1)
; less than 1 var, this is just linear
'()
; more than 1 var, all involved vars are non-linear
(append* (for/list ([v vs]) (do v #t))))]
[(rmod v mod) (append (do v include?) (do mod include?))]
[else (tokamak:exit "not supported: ~a" obj0)]
[_ (tokamak:exit "not supported: ~a" obj0)]
)
)
; then call it and remove duplicates, and return