 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Implicit Set Protocol ;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defprotocol ImplicitStateSet
+;; Protocol used to represent both state sets, and value sets.
+;; State sets are like states, where the values implement PSet.
+;; Should also implement proper equality
+(defprotocol PSet
   (empty?    [s] "Is this set empty")
-;  (singleton-val [s v] "Return single possible value for far, or nil if not singleton")
   (singleton [s] "Return the singleton element making up this set, or nil if cardinality != 1.")
   (some-element [s] "Return an arbitrary element of this set, or throw if empty. ")
   (explicit-set [s] "Return an explicit outcome set. ")
-  (constrain [ss constraint] "Apply a constraint."))
-
+  (constrain [ss constraint] "Apply a constraint.")
+  (as-constraint [ss] "Return a constraint view.")
+  (subset? [s1 s2] "Is this set a (possibly improper) subset of the other?"))
+
+;; Allow Clojure sets to be used as value sets.
+(extend-type clojure.lang.IPersistentSet
+  PSet
+  (empty? [s] (clojure.core/empty? s))
+  (singleton [s] (util/singleton s))
+  (some-element [s]
+    (assert (not (clojure.core/empty? s)))
+    (first s))
+  (explicit-set [s] s)
+  (constrain [s constraint]
+    (assert (set? constraint))
+    (clojure.set/intersection s constraint))
+  (as-constraint [s] s)
+  (subset? [s1 s2] (util/subset? s1 s2)))
+
+
+(defn assert-pset! [x]
+  nil #_ (assert (satisfies? PSet x)))
+
+(defn proper-subset? [s1 s2]
+  (and (subset? s1 s2) (not (= s1 s2))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;; Factored Implicit Sets ;;;;;;;;;;;;;;;;;;;;;;;;;;;;

   (meta [this] meta)
   (withMeta [this new-meta] (LoggingFactoredStateSet. init context puts ooc new-meta))

  ImplicitStateSet
   (empty? [ss] #_(println "AAA" init) (some clojure.core/empty? (vals init)))
   (singleton [ss] 
     (when (every? util/singleton? (vals init))
       (extract-logging-state ss (util/map-vals util/safe-singleton init))))
   (some-element [ss]
     (assert (not (empty? ss)))
     (extract-logging-state ss (util/map-vals first init)))
   (explicit-set [ss]
     (let [kvs (seq init)
           ks  (map key kvs)
           vss (map val kvs)]
       (set (for [vs (apply cartesian-product vss)] (extract-logging-state ss (zipmap ks vs))))))
   (constrain    [ss constraint] 
;    (util/assert-is (every? context (keys constraint)))     
     (state/set-vars ss
     (for [[var vals] constraint
           :let [cur-vals (state/get-var ss var)
                 isect    (clojure.set/intersection vals cur-vals)]
           :when (not (= (count isect) (count cur-vals)))]
       (do #_ (util/assert-is (contains? context var)) ;; TODO: can't actually assert this without stronger conditions on what must be reported in precondition contexts, unfortunately.  I.e., how to do it may not depend on initial value, but operation may still constrain it ?!
           [var isect]))))
   
  state/FactoredState
   (get-var [ss var]
     (let [x (state/get-var init var)]
       (util/assert-is (set? x) "%s" [var])
       x))
   
   (set-var [ss var val]
       (util/assert-is (set? val) "%s" [var])
       (LoggingFactoredStateSet. (state/set-var init var val) ; init
                              context
                              (assoc puts var val)
                              (if (.contains context var) ooc (assoc ooc var val))
                              {}))
   (set-vars [ss vv-pairs]
       (doseq [[var val] vv-pairs] (util/assert-is (set? val) "%s" [var]))
       (LoggingFactoredStateSet. (state/set-vars init vv-pairs)
                              context
                              (into puts vv-pairs)

;; for now, we can just require that these be unconditional.
;; If we add unions, etc later, worry about details.
;; TODO: constraint is not the same as set-vars ?  ???

(declare make-logging-factored-state-set)

