From af98a9dec9410930553c3c2f86ca10b26c7e559e Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 31 Aug 2016 15:19:12 -0400
Subject: [PATCH] add solve

---
 turnstile/examples/rosette/rosette2.rkt       | 25 +++++++++++++++--
 .../tests/rosette/rosette-guide-tests.rkt     | 28 +++++++++++++++++++
 2 files changed, 50 insertions(+), 3 deletions(-)

diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 2379bef..f13e556 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -459,7 +459,18 @@
 (define-rosette-primop <= : (Ccase-> (C→ CInt CInt CBool)
                                      (C→ Int Int Bool)))
 (define-rosette-primop >= : (Ccase-> (C→ CInt CInt CBool)
-                                    (C→ Int Int Bool)))
+                                     (C→ Int Int Bool)))
+
+(define-rosette-primop abs : (Ccase-> (C→ CPosInt CPosInt)
+                                      (C→ PosInt PosInt)
+                                      (C→ CZero CZero)
+                                      (C→ Zero Zero)
+                                      (C→ CNegInt CPosInt)
+                                      (C→ NegInt PosInt)
+                                      (C→ CInt CInt)
+                                      (C→ Int Int)
+                                      (C→ CNum CNum)
+                                      (C→ Num Num)))
 
 (define-rosette-primop not : (C→ Any Bool))
 (define-rosette-primop false? : (C→ Any Bool))
@@ -552,6 +563,10 @@
 
 (define-base-types CSolution CPict)
 
+(define-rosette-primop core : (C→ Any Any))
+(define-rosette-primop sat? : (C→ Any Bool))
+(define-rosette-primop unsat? : (C→ Any Bool))
+
 (define-typed-syntax verify
   [(_ e) ≫
    [⊢ [e ≫ e- ⇒ : _]]
@@ -570,8 +585,6 @@
    --------
    [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
 
-(define-rosette-primop core : (C→ Any Any))
-(define-rosette-primop sat? : (C→ Any Bool))
 
 (define-typed-syntax synthesize
   [(_ #:forall ie #:guarantee ge) ≫
@@ -586,6 +599,12 @@
    --------
    [⊢ [_ ≫ (ro:synthesize #:forall ie- #:assume ae- #:guarantee ge-) ⇒ : CSolution]]])
 
+(define-typed-syntax solve
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇒ : _]]
+   --------
+   [⊢ [_ ≫ (ro:solve e-) ⇒ : CSolution]]])
+
 ;; ---------------------------------
 ;; Subtyping
 
diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt
index 593d4ae..294ffb8 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt
@@ -82,12 +82,19 @@
 (check-type+asserts (same poly factored -1) : Unit -> (void) (list))
 (check-type+asserts (same poly factored -2) : Unit -> (void) (list))
 
+;; 2.3.1 Verification
+
 (define-symbolic i integer? : Int)
 (define cex (verify (same poly factored i)))
+(check-type cex : CSolution)
+(check-type (sat? cex) : Bool -> #t)
+(check-type (unsat? cex) : Bool -> #f)
 (check-type (evaluate i cex) : Int -> 12)
 (check-runtime-exn (same poly factored 12))
 (clear-asserts!)
 
+;; 2.3.2 Debugging
+
 (require "../../rosette/query/debug.rkt"
          "../../rosette/lib/render.rkt")
 (define/debug (factored/d [x : Int] -> Int)
@@ -98,6 +105,8 @@
 ;; TESTING TODO: requires visual inspection (in DrRacket)
 (check-type (render ucore) : CPict)
 
+;; 2.3.3 Synthesis
+
 (require "../../rosette/lib/synthax.rkt")
 (define (factored/?? [x : Int] -> Int)
  (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
@@ -107,9 +116,28 @@
               #:guarantee (same poly factored/?? i)))
 (check-type binding : CSolution)
 (check-type (sat? binding) : Bool -> #t)
+(check-type (unsat? binding) : Bool -> #f)
 ;; TESTING TODO: requires visual inspection of stdout
 (check-type (print-forms binding) : Unit -> (void))
 ;; typed/rosette should print: 
 ;;  '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
 ;; (untyped) rosette should print: 
 ;;  '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
+
+;; 2.3.4 Angelic Execution
+
+(define-symbolic x y integer? : Int)
+(define sol
+  (solve (begin (assert (not (= x y)))
+                (assert (< (abs x) 10))
+                (assert (< (abs y) 10))
+                (assert (not (= (poly x) 0)))
+                (assert (= (poly x) (poly y))))))
+(check-type sol : CSolution)
+(check-type (sat? sol) : Bool -> #t)
+(check-type (unsat? sol) : Bool -> #f)
+(check-type (evaluate x sol) : Int -> -5)
+(check-type (evaluate y sol) : Int -> 2)
+(check-type (evaluate (poly x) sol) : Int -> 120)
+(check-type (evaluate (poly y) sol) : Int -> 120)
+