#lang racket

(require "../interpreter.rkt" "../stack.rkt" "../state.rkt" "../greensyn.rkt")

(define (syn-lookup)
  (define comm (make-vector 1))
  ;; set up the program
  (greensyn-reset 8 1 (constraint t))

  ;; set pair
  (greensyn-input (progstate a b p i r s 1 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 0 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 2 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 1 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 4 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 2 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 8 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 3 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 16 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 4 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 32 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 5 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 64 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 6 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  ;; set pair
  (greensyn-input (progstate a b p i r s 128 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-output (progstate a b p i r s 7 (copy-stack data) (copy-stack return) (vector-copy memory 0 64)))
  (greensyn-send-recv (default-commstate))
  (greensyn-commit)

  (greensyn-check-sat #:file "syn.smt2" "dup dup or nop a! @p !+ @p !+ @p !+ @p !+ @p !+ @p !+ @p !+ @p !+ @p a! 0 +* +* +* +* +* +* +* +* +* +* +* +* +* +* +* +* +* +* a nop 2/ 2/ 2/ nop 2/ 2/ 7 nop and a! @ nop" #:time-limit 100000))
s
(syn-lookup)

;; (define (verify)
;;   (greensyn-reset 4 1 (constraint t))
;;   (greensyn-spec "dup - 1 nop + and")
;;   (greensyn-verify "verify.smt2" "1 over - nop + and"))
;;   ;(greensyn-verify "verify.smt2" "dup - 180065 nop + and"))

;; (verify)