PasteRack.org
Paste # 583
2018-08-10 04:07:20

Fork as a new paste.

Paste viewed 171 times.


Embed:

Synthesis.rkt

#lang rosette
(require rosette/lib/synthax)


(define (polynomial x)
  (expt (+ 1 x) 5))


(define (poly-factor x)
  (+ (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))
     (* (??) (expt x (??)))))

(define (same p f x)
  (assert (= (p x) (f x))))

(define-symbolic i integer?)

(define binding
    (synthesize #:forall (list i) 
                #:guarantee (same polynomial poly-factor i)))


(print-forms binding)


sat-model: contract violation
  expected: sat?
  given: (unsat)