mirror of
https://github.com/circify/circ.git
synced 2026-01-11 14:47:59 -05:00
8140b1369e
Previously, the traversal stack held (node, children queued) pairs. When visiting a node without it's children queued, we would queue them all. They take a lot of memory! Now, the stack holds children iterators. Also: this patch fixes many bugs introduced by the prior one.
33 lines
1.3 KiB
Bash
Executable File
33 lines
1.3 KiB
Bash
Executable File
#!/usr/bin/env zsh
|
|
|
|
set -ex
|
|
|
|
disable -r time
|
|
|
|
BIN=./target/debug/examples/circ
|
|
|
|
$BIN --language datalog ./examples/datalog/inv.pl r1cs --action count || true
|
|
$BIN --language datalog ./examples/datalog/call.pl r1cs --action count || true
|
|
$BIN --language datalog ./examples/datalog/arr.pl r1cs --action count || true
|
|
|
|
function getconstraints {
|
|
grep -E "Final r1cs: .* constraints" -o | grep -E -o "\\b[0-9]+"
|
|
}
|
|
|
|
# Small R1cs b/c too little recursion.
|
|
size=$(($BIN --language datalog ./examples/datalog/dumb_hash.pl --datalog-rec-limit 4 r1cs --action count || true) | getconstraints)
|
|
[ "$size" -lt 10 ]
|
|
|
|
# Big R1cs b/c enough recursion
|
|
size=$(($BIN --language datalog ./examples/datalog/dumb_hash.pl --datalog-rec-limit 5 r1cs --action count || true) | getconstraints)
|
|
[ "$size" -gt 250 ]
|
|
size=$(($BIN --language datalog ./examples/datalog/dumb_hash.pl --datalog-rec-limit 10 r1cs --action count || true) | getconstraints)
|
|
[ "$size" -gt 250 ]
|
|
size=$(($BIN --language datalog ./examples/datalog/dec.pl --datalog-rec-limit 2 r1cs --action count || true) | getconstraints)
|
|
[ "$size" -gt 250 ]
|
|
|
|
# Test prim-rec test
|
|
$BIN --language datalog ./examples/datalog/dec.pl --datalog-lint-prim-rec true smt
|
|
|
|
($BIN --language datalog ./examples/datalog/not_dec.pl --datalog-lint-prim-rec true smt || true) | grep -E 'Not prim'
|