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

small triggers

Browse Source
This commit is contained in:
chyanju
2022-04-22 17:44:57 -07:00
parent a81c551aae
commit de473e500c
2 changed files with 11 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
test-push-button-equivalence.rkt
View File

@@ -1,6 +1,8 @@
#lang rosette
(require rosette/solver/smt/boolector)
(when (boolector-available?)
(define use-boolector #t) ; use boolector or not?
(when (and use-boolector (boolector-available?))
; (current-solver (boolector #:logic 'QF_BV))
(current-solver (boolector))
)
(printf "# using solver: ~a\n" (current-solver))
@@ -17,9 +19,9 @@
; set the example
; (define json-path "./examples/test1a.json") ; not equivalent
(define json-path "./examples/test1.json") ; equivalent
(define r1cs-path "./examples/test1.r1cs")
(define sym-path "./examples/test1.sym")
(define json-path "./examples/test2.json") ; equivalent
(define r1cs-path "./examples/test2.r1cs")
(define sym-path "./examples/test2.sym")
; =======================
; load and interpret r1cs

8
test-uniqueness.rkt
View File

@@ -1,6 +1,8 @@
#lang rosette
(require rosette/solver/smt/boolector)
(when (boolector-available?)
(define use-boolector #f) ; use boolector or not?
(when (and use-boolector (boolector-available?))
; (current-solver (boolector #:logic 'QF_BV))
(current-solver (boolector))
)
(printf "# using solver: ~a\n" (current-solver))
@@ -12,8 +14,8 @@
(require "./picus/r1cs.rkt")
(require "./picus/r1cs-interpreter.rkt")
;(define r0 (read-r1cs "./examples/test0.r1cs"))
(define r0 (read-r1cs "./examples/test2.r1cs"))
(define r0 (read-r1cs "./examples/test0.r1cs"))
;(define r0 (read-r1cs "./examples/test2.r1cs"))
;(define r0 (read-r1cs "./examples/bigmod_5_2.r1cs"))
;(define r0 (read-r1cs "./examples/bigmod_10_2.r1cs"))
;(define r0 (read-r1cs "./examples/bigmod_86_3.r1cs"))