Defining constraints -- datasorts and stacst

194 views
Skip to first unread message

M88

unread,
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

unread,
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

unread,
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

unread,
Apr 8, 2018, 7:47:12 AM4/8/18
to ats-lan...@googlegroups.com
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.
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.

M88

unread,
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

unread,
Apr 17, 2018, 8:29:57 PM4/17/18
to ats-lan...@googlegroups.com
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

unread,
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

unread,
Apr 21, 2018, 10:39:14 AM4/21/18
to ats-lan...@googlegroups.com
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,
please use Z3 instead.

The built-in constraint solver uses so-called Fourier-Motzkin variable
elimination method, which is exponential time (worst-cast) and polynomial
time (probability). A variable is introduced for each non-variable expression.
If you explicitly introduce variables for expressions, the solver should work
more efficiently.

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.
Reply all
Reply to author
Forward
0 new messages