Add mapToSet and mapPrj#624
Conversation
|
I've added some fq files and run the new tests by hand. When I try to run all the tests with: I get a |
|
I've got one more weird one to throw in here. Don't merge this yet. |
| -- to False, and all positive elements are mapped to True. In practice, | ||
| -- negative elements should not exist because Map is intended to be used | ||
| -- as a bag, so the element is a non-negative number representing | ||
| -- the occurrences of its corresponding key. |
There was a problem hiding this comment.
There seems to be some assumptions implicit here that I don't have. For instance: How is the value of the integers in the map relevant to the conversion function?
I'm discovering that I can't find where the sorts Set and Map or their operations are defined.
There was a problem hiding this comment.
Map is Array Int Int, and Set is Array Int Bool. There's a big prelude at the top of many of the smt files generated by liquid-fixpoint that looks like this:
(define-sort Elt () Int)
(define-sort LSet () (Array Elt Bool))
(define-fun smt_set_emp () LSet ((as const LSet) false))
(define-fun smt_set_sng ((x Elt)) LSet (store ((as const LSet) false) x true))
(define-fun smt_set_mem ((x Elt) (s LSet)) Bool (select s x))
(define-fun smt_set_add ((s LSet) (x Elt)) LSet (store s x true))
(define-fun smt_set_cup ((s1 LSet) (s2 LSet)) LSet ((_ map or) s1 s2))
(define-fun smt_set_cap ((s1 LSet) (s2 LSet)) LSet ((_ map and) s1 s2))
(define-fun smt_set_com ((s LSet)) LSet ((_ map not) s))
(define-fun smt_set_dif ((s1 LSet) (s2 LSet)) LSet (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 LSet) (s2 LSet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(define-fun smt_map_cup ((m1 Map) (m2 Map)) Map ((_ map (+ (Elt Elt) Elt)) m1 m2))
(define-fun smt_map_prj ((s LSet) (m Map)) Map ((_ map (ite (Bool Elt Elt) Elt)) s m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_to_set ((m Map)) LSet ((_ map (> (Elt Elt) Bool)) m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_max ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_min ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_shift ((n Int) (m Map)) Map (lambda ((i Int)) (select m (- i n))))
(define-fun smt_map_def ((v Elt)) Map ((as const (Map)) v))
All of those are defined in z3Preamble.
How is the value of the integers in the map relevant to the conversion function?
If the conversion function exists at all, then the values must be relevant. The Array type from smtlib maps all keys to a value, so there are no positions at which a value is absent. I chose to interpret Map more specifically to mean Bag for this function because that seems to be its only use in liquid haskell's standard library.
|
I've add three more, with tests, in the latest commit. One unions maps, combining elements with Also, I can just remove |
|
Hey @andrewthad do you really need the Or ideally have it user-defined in some way instead of build it. |
|
I don't need any of these anymore. I had been trying to see how far I could get with having Liquid Haskell enforce that contexts (for a lambda calculus implementation) were well formed. It actually worked pretty well, but I've stopped pursuing this approach. So if you need to get rid of any of these to make cvc5 work, get rid of them. |
|
Thanks!!! |
Adds
mapToSetandmapPrj, defined like this:The intent is to make it possible (in the liquidhaskell repo) to write a function that unions two bags (in
Language.Haskell.Liquid.Bag) by choosing the first non-zero element rather than by summing the elements.The implementations in this PR bake in zero as a special value, further committing the
Maptype in liquid-fixpoint to bag interpretation.