# Defining constraints -- datasorts and stacst

194 views

### M88

Apr 7, 2018, 12:25:05 AM4/7/18
to ats-lang-users

I was looking into the rock-paper-scissors example (here and here) 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
| cA_2
| 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,cB_1)) &&
isCA1(sA_1(cA_1,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.

### gmhwxi

Apr 7, 2018, 9:16:45 AM4/7/18
to ats-lang-users

It seems that isCA1_praxi should be declared
as follows:

praxi
isCA1_praxi{cb:catB} (): [isCA1(sA_1(cA_1,cb))] void

### M88

Apr 7, 2018, 9:09:48 PM4/7/18
to ats-lang-users

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.

### Hongwei Xi

Apr 8, 2018, 7:47:12 AM4/8/18
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.`

--
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+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

### M88

Apr 17, 2018, 4:12:12 PM4/17/18
to ats-lang-users
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).
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

### Hongwei Xi

Apr 17, 2018, 8:29:57 PM4/17/18
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

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

### M88

Apr 21, 2018, 9:13:25 AM4/21/18
to ats-lang-users
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.

### Hongwei Xi

Apr 21, 2018, 10:39:14 AM4/21/18
The built-in constraint-solver cannot handle constants
introduced via 'stacst' very well. It was meant to only handle
integer constraints. I did a bit of hacking to allow very limited
handling of constants. If you need serious constraint-solving,