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

adding lema basis

Browse Source
This commit is contained in:
clararod9
2022-08-31 15:19:37 -07:00
parent b592ed70a6
commit 0be361708c
9 changed files with 69 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
picus/optimizers/r1cs-cvc5-simple-optimizer.rkt
View File

@@ -151,6 +151,8 @@
(r1cs:ror (for/list ([v vs]) v))
)
]
[(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))]
[(r1cs:rint v)
(cond

2
picus/optimizers/r1cs-cvc5-template-optimizer.rkt
View File

@@ -32,6 +32,8 @@
[(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))]
[(r1cs:rint v) (r1cs:rint v)]
[(r1cs:rstr v) (r1cs:rstr v)]
[(r1cs:rvar v) (r1cs:rvar v)]

3
picus/optimizers/r1cs-z3-AB0-optimizer.rkt
View File

@@ -79,6 +79,9 @@
[(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))]
[(r1cs:rint v) (r1cs:rint v)]
[(r1cs:rstr v) (r1cs:rstr v)]
[(r1cs:rvar v) (r1cs:rvar v)]

2
picus/optimizers/r1cs-z3-simple-optimizer.rkt
View File

@@ -130,6 +130,8 @@
(r1cs:rand (for/list ([v new-vs]) v))
)
]
[(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))]
[(r1cs:ror vs)
(define new-vs (for/list ([v vs]) (optimize-r1cs v)))
; if there's only one element, extract content directly

2
picus/optimizers/r1cs-z3-template-optimizer.rkt
View File

@@ -32,6 +32,8 @@
[(r1cs:rand vs) (r1cs:rand (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:ror vs) (r1cs:ror (for/list ([v vs]) (optimize-r1cs v)))]
[(r1cs:rimp lhs rhs) (r1cs:rimp (optimize-r1cs lhs) (optimize-r1cs rhs))]
[(r1cs:rint v) (r1cs:rint v)]
[(r1cs:rstr v) (r1cs:rstr v)]
[(r1cs:rvar v) (r1cs:rvar v)]

1
picus/r1cs-cvc5-interpreter.rkt
View File

@@ -47,6 +47,7 @@
[(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))]
[(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))]
[(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
[(r1cs:rint v) (format "#f~am~a" v config:p)]
[(r1cs:rstr v) v]

2
picus/r1cs-grammar.rkt
View File

@@ -35,6 +35,8 @@
; sub-command level
(struct rand (vs) #:mutable #:transparent #:reflection-name 'r1cs:rand) ; vs: a list of bools
(struct ror (vs) #:mutable #:transparent #:reflection-name 'r1cs:ror) ; vs: a list of bools
(struct rimp (lhs rhs) #:mutable #:transparent #:reflection-name 'r1cs:imp)
; no rnot here out of simplicity, use neq, or other unequalty instead
; sub-command level
(struct radd (vs) #:mutable #:transparent #:reflection-name 'r1cs:radd) ; vs: list

2
picus/r1cs-z3-interpreter.rkt
View File

@@ -47,6 +47,8 @@
[(r1cs:rand vs) (foldr (make-format-op "and") null (for/list ([v vs]) (interpret-r1cs v)))]
[(r1cs:ror vs) (foldr (make-format-op "or") null (for/list ([v vs]) (interpret-r1cs v)))]
[(r1cs:rimp lhs rhs) (format "(=> ~a ~a)" (interpret-r1cs lhs) (interpret-r1cs rhs))]
[(r1cs:rint v) (format "~a" v)]
[(r1cs:rstr v) v]

54
test-pp-uniqueness.rkt
View File

@@ -21,6 +21,7 @@
(prefix-in cvc5-rint: "./picus/r1cs-cvc5-interpreter.rkt")
(prefix-in cvc5-parser: "./picus/r1cs-cvc5-parser.rkt")
(prefix-in cvc5-osimp: "./picus/optimizers/r1cs-cvc5-simple-optimizer.rkt")
(prefix-in cvc5-brep: "./picus/optimizers/r1cs-cvc5-base-representation-optimizer.rkt")
; note: cvc5 doesn't have AB0 optimizer, use template instead
)
@@ -108,10 +109,31 @@
[(equal? "z3" arg-solver) (lambda (x) (
z3-oab0:optimize-r1cs (z3-osimp:optimize-r1cs x)
))]
[(equal? "cvc5" arg-solver) (lambda (x) (cvc5-osimp:optimize-r1cs x))]
[(equal? "cvc5" arg-solver) (lambda (x)
(cvc5-osimp:optimize-r1cs x)
)]
[else (tokamak:exit "you can't reach here")]
)
)
(define (optimizer:get-base-representation)
(cond
[(equal? "z3" arg-solver) '()]
[(equal? "cvc5" arg-solver) (lambda (x)
(cvc5-brep:get-base-representations x)
)]
[else (tokamak:exit "you can't reach here")]
)
)
(define (optimizer:generate-base-representations-constraints)
(cond
[(equal? "z3" arg-solver) '()]
[(equal? "cvc5" arg-solver) (lambda (x y)
(cvc5-brep:generate-base-representations-constraints x y)
)]
[else (tokamak:exit "you can't reach here")]
)
)
(define (rint:interpret-r1cs)
(cond
[(equal? "z3" arg-solver) z3-rint:interpret-r1cs]
@@ -158,6 +180,23 @@
(printf "# parsing alternative r1cs...\n")
(define-values (_ alternative-definitions alternative-cnsts) ((parser:parse-r1cs) r0 xlist0))
(define optimized-original-cnsts ((optimizer:optimize) original-cnsts))
(define optimized-alternative-cnsts ((optimizer:optimize) alternative-cnsts))
; to generate the constraints checking for base-representations
(define base-representations-original ((optimizer:get-base-representation) optimized-original-cnsts))
(define base-representations-alternative ((optimizer:get-base-representation) optimized-alternative-cnsts))
;(printf "# Base representations original: ~a.\n" base-representations-original)
;(printf "# Base representations alternative: ~a.\n" base-representations-alternative)
(define constraints-base-representations
((optimizer:generate-base-representations-constraints)
base-representations-original
base-representations-alternative
)
)
(printf "# New constraints: ~a.\n" constraints-base-representations)
(define partial-cmds (r1cs:append-rcmds
(r1cs:rcmds (list
(r1cs:rcmt (r1cs:rstr "================================"))
@@ -173,6 +212,13 @@
))
alternative-definitions
alternative-cnsts
(r1cs:rcmds (list
(r1cs:rcmt (r1cs:rstr "================================"))
(r1cs:rcmt (r1cs:rstr "========= Added lemmas ========="))
(r1cs:rcmt (r1cs:rstr "================================"))
))
constraints-base-representations
))
; keep track of index of xlist (not xlist0 since that's incomplete)
@@ -252,6 +298,12 @@
))
alternative-definitions
(r1cs:get-subset-cmds alternative-cnsts list-c)
(r1cs:rcmds (list
(r1cs:rcmt (r1cs:rstr "================================"))
(r1cs:rcmt (r1cs:rstr "========= Added lemmas ========="))
(r1cs:rcmt (r1cs:rstr "================================"))
))
constraints-base-representations
)
)