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. On Sat, Apr 21, 2018 at 9:13 AM, M88 <[email protected]> wrote: > 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]> 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-boo >>>> l-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-1a >>>>> b0-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]. >>> 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/ms >>> gid/ats-lang-users/82adac20-edf8-4974-ad88-32455de26f16%40go >>> oglegroups.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 > <https://groups.google.com/d/msgid/ats-lang-users/71209c8a-4a6c-4152-9b3e-826d747a7fe2%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/CAPPSPLr6PmO1tWDTqJv9A69zzLrxciYJO72Ogb9EC41_PLG-fA%40mail.gmail.com.
