add forms and tests for guide sec49 solver and sols

turnstile/examples/rosette/rosette-notes.txt

@@ -69,6 +69,7 @@ Rosette TODO:
 
 Rosette use case questions:
 - does the predicate in define-symbolic need to be an arbitrary expression?
+- should z3 be part of #lang rosette?
 
 2016-08-31 --------------------
 

turnstile/examples/rosette/rosette2.rkt

@@ -1333,16 +1333,19 @@
 ;; ---------------------------------
 ;; solver forms
 
-(define-base-types CSolution CPict)
+(define-base-types CSolution CSolver CPict)
 
-(provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
-                            [model : (C→ CSolution (CHashTable Any Any))]
+(provide (rosette-typed-out [sat? : (C→ Any Bool)]
+                            [unsat? : (C→ Any Bool)]
+                            [solution? : CPred]
+                            [unknown? : CPred]
                             [sat : (Ccase-> (C→ CSolution)
                                             (C→ (CHashTable Any Any) CSolution))]
-                            [sat? : (C→ Any Bool)]
-                            [unsat? : (C→ Any Bool)]
                             [unsat : (Ccase-> (C→ CSolution)
-                                              (C→ (CListof Bool) CSolution))]))
+                                              (C→ (CListof Bool) CSolution))]
+                            [unknown : (C→ CSolution)]
+                            [model : (C→ CSolution (CHashTable Any Any))]
+                            [core : (C→ CSolution (U (Listof Any) CFalse))]))
 
 ;(define-rosette-primop forall : (C→ (CListof Any) Bool Bool))
 ;(define-rosette-primop exists : (C→ (CListof Any) Bool Bool))
@@ -1454,6 +1457,33 @@
    --------
    [⊢ [_ ≫ (ro:optimize #:maximize maxe- #:minimize mine- #:guarantee ge-) ⇒ : CSolution]]])
 
+;; this must be a macro in order to support Racket's overloaded set/get
+;; parameter patterns
+(define-typed-syntax current-solver
+  [_:id ≫
+   --------
+   [⊢ [_ ≫ ro:current-solver ⇒ : (CParamof CSolver)]]]
+  [(_) ≫
+   --------
+   [⊢ [_ ≫ (ro:current-solver) ⇒ : CSolver]]]
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇐ : CSolver]]
+   --------
+   [⊢ [_ ≫ (ro:current-solver e-) ⇒ : CUnit]]])
+
+;(define-rosette-primop gen:solver : CSolver)
+(define-rosette-primop solver? : CPred)
+(define-rosette-primop solver-assert : (C→ CSolver (CListof Bool) CUnit))
+(define-rosette-primop solver-clear : (C→ CSolver CUnit))
+(define-rosette-primop solver-minimize : (C→ CSolver (CListof (U Int Num BV)) CUnit))
+(define-rosette-primop solver-maximize : (C→ CSolver (CListof (U Int Num BV)) CUnit))
+(define-rosette-primop solver-check : (C→ CSolver CSolution))
+(define-rosette-primop solver-debug : (C→ CSolver CSolution))
+(define-rosette-primop solver-shutdown : (C→ CSolver CUnit))
+;; this is in rosette/solver/smt/z3 (is not in #lang rosette)
+;; make this part of base typed/rosette or separate lib?
+;(define-rosette-primop z3 : (C→ CSolver))
+
 ;; ---------------------------------
 ;; Symbolic reflection
 

turnstile/examples/tests/rosette/rosette-guide-sec49-tests.rkt

@@ -0,0 +1,32 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; Examples from the Rosette Guide, Section 4.9 Solvers and Solutions
+
+;; 4.9.1 The Solver Interface
+
+(check-type (current-solver) : CSolver -> (current-solver))
+;; TODO
+;(check-type gen:solver : CSolver)
+
+;; 4.9.2 Solutions
+(define-symbolic a b boolean?)
+(define-symbolic x y integer?)
+(define sol
+  (solve (begin (assert a)
+                (assert (= x 1))
+                (assert (= y 2)))))
+(check-type sol : CSolution)
+(check-type (sat? sol) : Bool -> #t)
+(check-type (evaluate (list 4 5 x) sol) : (Listof Int) -> '(4 5 1))
+(check-type (evaluate (list 4 5 x) sol) : (CListof Int)) ; concrete list ok
+(check-not-type (evaluate (list 4 5 x) sol) : (Listof Nat))
+(define vec (vector a))
+(check-type (evaluate vec sol) : (CMVectorof Bool))
+;'#(#t)
+; evaluation produces a new vector
+(check-type (eq? vec (evaluate vec sol)) : Bool -> #f)
+(check-type (evaluate (+ x y) sol) : Int -> 3)
+(check-not-type (evaluate (+ x y) sol) : CInt) ; not concrete
+(check-type (evaluate (and a b) sol) : Bool -> b)
+(check-not-type (evaluate (and a b) sol) : CBool) ; not concrete

turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt

@@ -9,7 +9,8 @@
           "rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3 BVs"
           "rosette-guide-sec44-tests.rkt" "Rosette Guide, Section 4.4 Uninterp Fns"
           "rosette-guide-sec45-tests.rkt" "Rosette Guide, Section 4.5 Procedures"
-          "rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8")
+          "rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8"
+          "rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9")
 
 (do-tests "bv-tests.rkt" "BV SDSL - General"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")