I've been experimenting with Z3 and it's proven to be very useful. I would
like to keep using the built-in constraint solver for various reasons.
Perhaps this is a novice question, but how does one establish equality
within a datasort?
For example, given datasort
datasort item
| a
| b
| c
How can I establish that a == a ?
I can use scase, but that is only optimal for a small number of branches.
It would be nice to use sif.
I can declare a static function like
stacst item_id : (item) -> int
stacst item_eq : (item,item) -> bool
extern praxi item_uniq : [
item_id(a) == 1;
item_id(b) == 2;
item_id(c) == 3
] void
extern praxi item_eq_praxi{a,b:item} : [
item_eq(a,b) == (item_id(a) == item_id(b))
] void
But the constraint solver still gives me errors, because either
item_eq(a,b) == (a == b) does not resolve (eg, in a sif branch), or
vice-versa (eg, in nested scase).
On Sunday, April 8, 2018 at 7:47:12 AM UTC-4, gmhwxi wrote:
>
>
> There are two styles of theorem-proving in ATS:
>
>
> http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/index.html
>
> To avoid explicit quantifier elimination performed by the following code,
>
> prval () = isCA1_praxi{cB_1}()
> prval () = isCA1_praxi{cB_2}()
> prval () = isCA1_praxi{cB_3}()
>
> you can try:
>
> prval() = $solver_assert(isCA1_praxi)
>
> and then use Z3 to solve the generated constraints. Doing so means that you
> are at the mercy
>
> of Z3's quantifier elimination heuristics or (black) magic.
>
>
>
> On Sat, Apr 7, 2018 at 9:09 PM, M88 <abys...@gmail.com <javascript:>>
> wrote:
>
>>
>> It seems that isCA1_praxi should be declared
>>> as follows:
>>>
>>> praxi
>>> isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void
>>>
>>
>> Yes, this makes sense -- I am looking for universal quantification.
>>
>> I suppose the issue here is how it would be invoked. Would I
>> still need to invoke the proof as follows?
>>
>> prval () = isCA1_praxi{cB_1}()
>> prval () = isCA1_praxi{cB_2}()
>> prval () = isCA1_praxi{cB_3}()
>>
>> ********
>>
>> After giving this some thought, I realized I could invoke the proof
>> within a constructor, omitting the need to explicitly specify each
>> "catB."
>>
>> fun makeCA1 {cb:catB}() : [sa:sortA | isCA1(sa) ] typeA(sa)
>>
>> What tripped me up at first is that the return value of each constructor
>> should specify the constraint "isCA1" if I use this approach, whereas
>> the former let me invoke the proofs globally.
>>
>>
>> On Saturday, April 7, 2018 at 12:25:05 AM UTC-4, M88 wrote:
>>>>
>>>>
>>>> I was looking into the rock-paper-scissors example (here
>>>> <https://groups.google.com/forum/#!topic/ats-lang-users/YcdEzhJdJzs>
>>>> and here
>>>> <https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST20/test25.dats>)
>>>>
>>>> and I found it very useful for learning how to define predicates in the
>>>> statics.
>>>>
>>>> I had made an attempt something similar, but using independent
>>>> datasorts as parameters.
>>>>
>>>> For example:
>>>>
>>>> datasort catA =
>>>> | cA_1
>>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>>> | cA_2
>>>> <https://maps.google.com/?q=cA_1+%C2%A0%C2%A0+%7C+cA_2&entry=gmail&source=g>
>>>> | cA_3
>>>>
>>>> datasort catB =
>>>> | cB_1
>>>> | cB_2
>>>> | cB_3
>>>>
>>>> datasort sortA =
>>>> | sA_1 of (catA, catB)
>>>> | sA_2
>>>> | sA_3
>>>>
>>>> // only sortA is used to define types. Eg,
>>>> abst@ype typeA(sortA)
>>>>
>>>> I ran into a few issues. I arrived at a solution, but I thought it
>>>> could be cleaner.
>>>>
>>>> First, I discovered that I wasn't able to define equalities with
>>>> datasorts. Eg, {sa:sortA | sa == sA_2}. It would typecheck, but the
>>>> constraints could not be solved. I suppose this makes sense, considering
>>>> the definition of ==. Does ATS supply a way to determine equalities on
>>>> datasorts? Is there another feature that would make this unnecessary?
>>>>
>>>> As an alternative, I decided to declare a static predicate, as in the
>>>> rock-paper-scissors example:
>>>>
>>>> stacst isCA1 : sortA -> bool
>>>>
>>>> // This works, but becomes quite verbose.
>>>> praxi isCA1_praxi ():
>>>> [
>>>> isCA1(sA_1(cA_1
>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_1)) &&
>>>> isCA1(sA_1(cA_1
>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,cB_2)) &&
>>>> isCA1(sA_1(cA_1,cB_3))
>>>> ] void
>>>>
>>>> The verbosity isn't an issue in this example, but becomes pretty
>>>> unmanageable as the relationships get more complex. I would like to say,
>>>> "for any catB". I tried using universal and existential quantification,
>>>> but the constraints would not solve. I would like to avoid passing catB
>>>> explicitly.
>>>>
>>>> Is there a way to reduce it to something like this:
>>>>
>>>> // The constraints will not solve:
>>>> praxi isCA1_praxi ():
>>>> [ cb: catB |
>>>> isCA1(sA_1(cA_1,cb))
>>>> ] void
>>>>
>>>> Perhaps I am abusing datasorts -- suggestions for other approaches are
>>>> welcome.
>>>>
>>>>
>>>> --
>> You received this message because you are subscribed to the Google Groups
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to ats-lang-user...@googlegroups.com <javascript:>.
>> To post to this group, send email to ats-lan...@googlegroups.com
>> <javascript:>.
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/68469c62-1ab0-4d0c-936b-e8775877b5f3%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%40googlegroups.com.
