Thanks for the response -- it helped me resolve a few issues. I could
encode a few properties in the item ids, which let me replace several
constraints with stadef. I managed to get the same code working for both
the native constraint solver and Z3.
It did make my error messages less pretty, but I suppose that's not much of
an issue.
I did find that many problems (with the native solver) stemmed from writing
code in this pattern:
// not good
sortdef sortA = int
sortdef sortB = int
stacst const1 : (sortA) -> bool
stacst const2 : (sortB,sortA) -> bool
extern praxi const1_praxi {s:sortA} () : [
const1(s) == ( s >= 1024 && s < 2048 )
] void
extern praxi const2_praxi {b:sortB}{a:sortA} () : [
const2(b,a) == const1(a)
] void
The following typechecks much faster:
// ok
sortdef sortA = int
sortdef sortB = int
stadef const1 ( s:sortA) : bool = ( s >= 1024 && s < 2048 )
stacst const2 : (sortB,sortA) -> bool
// no const2_praxi needed
// const2 might be much more complex in a real example, so I left this one
extern praxi const2_praxi {b:sortB}{a:sortA} () : [
const2(b,a) == const1(a)
] void
I did notice that native constraint solving seems to go 2-3x faster when
values are reused (eg, assigned to a variable). Do constraints need to be
solved for each variable, even if they are the same type? I'm a bit
curious as to how this works.
On Tuesday, April 17, 2018 at 8:29:57 PM UTC-4, gmhwxi wrote:
>
> The built-in solver in ATS is very limited in its handling of datasorts
> like the following one:
>
> datasort item =
> | a
> | b
> | c
>
> In practice, I try to use integers instead:
>
> sortdef item = int
> #define item_a 0
> #define item_b 1
> #define item_c 2
>
>
>
>
>
> On Tue, Apr 17, 2018 at 4:12 PM, M88 <[email protected] <javascript:>>
> wrote:
>
>> 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 <[email protected]> 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
>>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,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
>>>>>> <https://maps.google.com/?q=1(cA_1&entry=gmail&source=g>,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 [email protected].
>>>> To post to this group, send email to [email protected].
>>>> 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 [email protected] <javascript:>.
>> To post to this group, send email to [email protected]
>> <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/82adac20-edf8-4974-ad88-32455de26f16%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%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 [email protected].
To post to this group, send email to [email protected].
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/71209c8a-4a6c-4152-9b3e-826d747a7fe2%40googlegroups.com.
