You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
49 lines
1.5 KiB
49 lines
1.5 KiB
open Resolution |
|
open Circuits |
|
open StellarCircuits |
|
|
|
(* ======================================== |
|
Tests |
|
======================================== *) |
|
|
|
(* _________ Tests on Resolution _________ *) |
|
let y = Var("y") |
|
let x = Var("x") |
|
let z = Var("z") |
|
let r = Var("r") |
|
let zero = make_const "0" |
|
let s x = Func("s", Npol, [x]) |
|
let add p x y z = Func("add", p, [x;y;z]) |
|
|
|
(* Convert int to term *) |
|
let rec enat i = |
|
if i = 0 then zero else s (enat (i-1)) |
|
|
|
(* makes the constellation corresponding to an addition *) |
|
let make_const_add n m = |
|
[[add Pos zero y y]; [add Neg x y z; add Pos (s x) y (s z)]; [add Neg (enat n) (enat m) r; r]] |
|
|
|
let constellation = make_const_add 1 3 ;; |
|
|
|
print_dgraph (dgraph constellation) ;; |
|
|
|
(* simple determinist constellation test*) |
|
let test = [ [Func("e", Neg, [x]); x] ; [Func("e", Pos, [Func("d", Npol, [y])]) ; Func("e", Npol, [x]) ] ] ;; |
|
print_dgraph (dgraph test);; |
|
exec test ;; |
|
|
|
(* _________ Tests on exec using Stellar Circuits _________ *) |
|
|
|
(* Constellation of excluded middle without boolean doors *) |
|
let excl_mid_no_prop = (const_of_circuit (make_em_circ 1));; |
|
|
|
(* Constellation of excluded middle with boolean doors *) |
|
let excl_mid_prop = ((const_of_circuit (make_em_circ 1))@[[Func("or", Pos, [Func("0", Npol, []); Func("1", Npol, []); Func("1", Npol, [])])];[Func("neg",Pos, [Func("1", Npol, []); Func("0", Npol, [])])]]);; |
|
|
|
let exec_exmid_noprop = exec excl_mid_no_prop [0];; |
|
(* should return 1*) |
|
let exec_exmid_prop = exec excl_mid_prop [0];; |
|
|
|
print_const exec_exmid_prop;; |
|
|
|
let test_fam = excl_mid_prop@test |