Modulo in constraints

Brandon_Barker · February 2, 2015, 11:48pm

Hi,

I’ve been playing around with P2 from project euler. I have a long way to
go (for the proof; even a semi-shoddy proof at that), but think I’ve made
significant progress. I’m now getting “ye olde constraint error”:

$ patsopt.exe -tc -d P2-bbarker.dats
/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
857(line=55, offs=28) – 857(line=55, offs=28): error(3): unsolved
constraint: C3NSTRprop(main; S2Eapp(S2Ecst(==); S2Eapp(S2Ecst(mod);
S2Eapp(S2Ecst(+); S2EVar(4158->S2Evar(ln1(7667))),
S2EVar(4159->S2Evar(ln2(7666)))), S2Eintinf(2)), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2brand_000_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Here’s the version of code pertinent to the question:

github.com

bbarker/ATS-Postiats-test/blob/dc9fb2465d0c8a7cfdb9e693fdbfb657c5ff847a/contrib/bbarker/PEULER/P2/P2-bbarker.dats

(*
** Project Euler: P2
** See https://projecteuler.net
*)
(* ****** ****** *)
//
// Author: Brandon Barker
// Authoremail: brandonDOTbarkerATgmailDOTcom
// Start time: January 31, 2015
//
(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)
//
staload "P2-bbarker.sats"

This file has been truncated. show original

Of course, it is probably more likely I have a typo somewhere else … I’ve
found many already, but am stuck now.

gmhwxi · February 3, 2015, 12:06am

nmod does not give you a type that is accurate enough for this task.
Try to use n - 2*half(n) (instead of nmod(n,2)) for this case.

As a rule of thumb, it is always a good idea to introduce a function of
your own
in this kind of situation:

fun my_mod2 {n:nat} (int(n)): int(n%2)

Then move on. You can always come back to deal with these introduced
functions later.

When programming, a programmer so often follows whatever the library
provides.

IMO, a programmer should be “self-centered”

Try to introduce whatever functions you need (if you can quickly convince
yourself
that these functions can be readily implemented based on some kind library).On Monday, February 2, 2015 at 6:48:24 PM UTC-5, Brandon Barker wrote:

Hi,

I’ve been playing around with P2 from project euler. I have a long way to
go (for the proof; even a semi-shoddy proof at that), but think I’ve made
significant progress. I’m now getting “ye olde constraint error”:

$ patsopt.exe -tc -d P2-bbarker.dats
/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
857(line=55, offs=28) – 857(line=55, offs=28): error(3): unsolved
constraint: C3NSTRprop(main; S2Eapp(S2Ecst(==); S2Eapp(S2Ecst(mod);
S2Eapp(S2Ecst(+); S2EVar(4158->S2Evar(ln1(7667))),
S2EVar(4159->S2Evar(ln2(7666)))), S2Eintinf(2)), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2brand_000_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Here’s the version of code pertinent to the question:

https://github.com/bbarker/ATS-Postiats-test/blob/dc9fb2465d0c8a7cfdb9e693fdbfb657c5ff847a/contrib/bbarker/PEULER/P2/P2-bbarker.dats

Of course, it is probably more likely I have a typo somewhere else …
I’ve found many already, but am stuck now.

gmhwxi · February 3, 2015, 2:44am

The type for my_mod2 does not look right.On Mon, Feb 2, 2015 at 9:39 PM, Brandon Barker brandon...@gmail.com wrote:

Good advice, thanks! But I now seem to be getting an invalid constraint
popping up: ln1 + ln2 = ln1, i.e.:

/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
1019(line=62, offs=7) – 1064(line=62, offs=52): error(3): unsolved
constraint: C3NSTRprop(main; S2Eeqeq(S2Eapp(S2Ecst(add_int_int);
S2Evar(ln1(7703)), S2Evar(ln2(7702))); S2Evar(ln1(7703))))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2brand_000_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Of course it is clear to me that is an invalid constraint, I just don’t
know why I have it. It is suggestive that I have a typo somewhere that is
making the loop signature unhappy.

Here’s my update:
fixed a constraint issue · bbarker/ATS-Postiats-test@46f94f7 · GitHub

On Mon, Feb 2, 2015 at 7:06 PM, gmhwxi gmh...@gmail.com wrote:

nmod does not give you a type that is accurate enough for this task.
Try to use n - 2*half(n) (instead of nmod(n,2)) for this case.

As a rule of thumb, it is always a good idea to introduce a function of
your own
in this kind of situation:

fun my_mod2 {n:nat} (int(n)): int(n%2)

Then move on. You can always come back to deal with these introduced
functions later.

When programming, a programmer so often follows whatever the library
provides.

IMO, a programmer should be “self-centered”

Try to introduce whatever functions you need (if you can quickly convince
yourself
that these functions can be readily implemented based on some kind
library).

On Monday, February 2, 2015 at 6:48:24 PM UTC-5, Brandon Barker wrote:

Hi,

I’ve been playing around with P2 from project euler. I have a long way
to go (for the proof; even a semi-shoddy proof at that), but think I’ve
made significant progress. I’m now getting “ye olde constraint error”:

$ patsopt.exe -tc -d P2-bbarker.dats
/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
857(line=55, offs=28) – 857(line=55, offs=28): error(3): unsolved
constraint: C3NSTRprop(main; S2Eapp(S2Ecst(==); S2Eapp(S2Ecst(mod);
S2Eapp(S2Ecst(+); S2EVar(4158->S2Evar(ln1(7667))),
S2EVar(4159->S2Evar(ln2(7666)))), S2Eintinf(2)), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: 2home_2brand_000_2ATS
2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Here’s the version of code pertinent to the question:
https://github.com/bbarker/ATS-Postiats-test/blob/
dc9fb2465d0c8a7cfdb9e693fdbfb657c5ff847a/contrib/bbarker/
PEULER/P2/P2-bbarker.dats

Of course, it is probably more likely I have a typo somewhere else …
I’ve found many already, but am stuck now.

–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/09491914-f512-4716-a091-e072541c1e0d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/09491914-f512-4716-a091-e072541c1e0d%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
Brandon Barker
brandon...@gmail.com

–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAORbNRoEFUjMdTrpiyij0ZzOYuMi6D%3DOtojPCVKWoecBFZpQxA%40mail.gmail.com
https://groups.google.com/d/msgid/ats-lang-users/CAORbNRoEFUjMdTrpiyij0ZzOYuMi6D%3DOtojPCVKWoecBFZpQxA%40mail.gmail.com?utm_medium=email&utm_source=footer
.

Brandon_Barker · February 3, 2015, 2:39am

Good advice, thanks! But I now seem to be getting an invalid constraint
popping up: ln1 + ln2 = ln1, i.e.:

/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
1019(line=62, offs=7) – 1064(line=62, offs=52): error(3): unsolved
constraint: C3NSTRprop(main; S2Eeqeq(S2Eapp(S2Ecst(add_int_int);
S2Evar(ln1(7703)), S2Evar(ln2(7702))); S2Evar(ln1(7703))))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2brand_000_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Of course it is clear to me that is an invalid constraint, I just don’t
know why I have it. It is suggestive that I have a typo somewhere that is
making the loop signature unhappy.

Here’s my update:
https://github.com/bbarker/ATS-Postiats-test/commit/46f94f770641b7916004a4fc550ff4e3f07c7b8aOn Mon, Feb 2, 2015 at 7:06 PM, gmhwxi gmh...@gmail.com wrote:

nmod does not give you a type that is accurate enough for this task.
Try to use n - 2*half(n) (instead of nmod(n,2)) for this case.

As a rule of thumb, it is always a good idea to introduce a function of
your own
in this kind of situation:

fun my_mod2 {n:nat} (int(n)): int(n%2)

Then move on. You can always come back to deal with these introduced
functions later.

When programming, a programmer so often follows whatever the library
provides.

IMO, a programmer should be “self-centered”

Try to introduce whatever functions you need (if you can quickly convince
yourself
that these functions can be readily implemented based on some kind
library).

On Monday, February 2, 2015 at 6:48:24 PM UTC-5, Brandon Barker wrote:

Hi,

I’ve been playing around with P2 from project euler. I have a long way to
go (for the proof; even a semi-shoddy proof at that), but think I’ve made
significant progress. I’m now getting “ye olde constraint error”:

$ patsopt.exe -tc -d P2-bbarker.dats
/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats:
857(line=55, offs=28) – 857(line=55, offs=28): error(3): unsolved
constraint: C3NSTRprop(main; S2Eapp(S2Ecst(==); S2Eapp(S2Ecst(mod);
S2Eapp(S2Ecst(+); S2EVar(4158->S2Evar(ln1(7667))),
S2EVar(4159->S2Evar(ln2(7666)))), S2Eintinf(2)), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: 2home_2brand_000_2ATS
2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

Here’s the version of code pertinent to the question:
https://github.com/bbarker/ATS-Postiats-test/blob/
dc9fb2465d0c8a7cfdb9e693fdbfb657c5ff847a/contrib/bbarker/
PEULER/P2/P2-bbarker.dats

Of course, it is probably more likely I have a typo somewhere else …
I’ve found many already, but am stuck now.

–
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.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/09491914-f512-4716-a091-e072541c1e0d%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/09491914-f512-4716-a091-e072541c1e0d%40googlegroups.com?utm_medium=email&utm_source=footer
.

Brandon Barker
brandon...@gmail.com

Topic		Replies	Views
Understanding unsolved constraints Google Group	5	431	August 6, 2014
Constraint cannot be translated into a form accepted by the constraint solver? Google Group	3	383	April 16, 2015
Weird Lemma In ATS Filter Function.b Google Group	7	510	August 8, 2015
Existential constraint solving Google Group	1	317	March 30, 2014
Patsolve_smt2 Google Group	1	427	June 26, 2016

Modulo in constraints

Related Topics