owestphal / IOTasks-demo

0 stars 0 forks source link

make ValueSet API available? #8

Closed jvoigtlaender closed 1 year ago

jvoigtlaender commented 1 year ago

I wanted to try out how the "product overflow" example behaves when the SMT solver is forbidden to choose 0 as one of the factors.

But I couldn't do this:

      (readInput x (ints `Intersection` complement (Eq 0)) AssumeValid)

because of:

Main.hs:24:41: error:
    Variable not in scope:
      complement :: ValueSet Integer -> ValueSet Integer
   |
24 |       (readInput x (ints `Intersection` complement (Eq 0)) AssumeValid)
   |                                         ^^^^^^^^^^
jvoigtlaender commented 1 year ago

Side note: The line numbering from the compiler message seems off, given that the example code with line numbers was as follows.

image

jvoigtlaender commented 1 year ago

Also, maybe it is worth adding something like

(\\) :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer

or

delete :: Integer -> ValueSet Integer -> ValueSet Integer

to the API?

(Names above are from the list API, there might be better ones.)

owestphal commented 1 year ago

there are now functions

with :: ValuesSet Integer -> Integer -> ValueSet Integer
without :: ValuesSet Integer -> Integer -> ValueSet Integer
(\\) :: ValueSet Integer -> ValueSet Integer -> ValueSet Integer

as well as functions for the basic constructors. (constructors are now hidden)