XSB does not handle ints very well
Issue #653
resolved
Bijgevoegde file werkt als ik type int door een eindig type "num" vervang
Geeft dan 8 facts in mouseclick, zoals gewenst.
Maar het gaat mis als ik daar int schrijf...
Comments (12)
-
-
is het mogelijk om de CP bounds te laten genereren en dan die bounds te gebruiken voor de generatie?
-
Geen idee.. Als die het type kunnen verkleinen van de variabele die nu als int gegenereerd wordt, zou dat moeten werken. Ik heb echter geen idee of CP de functionaliteit op de juiste plaats aanbiedt.
-
@broesdecat ? Ik zou gokken dat de CP die X kan zetten tussen X2 en X2+sqSize
-
reporter
Dit heeft niet echt met CP te maken.
Er zijn methodes om bounds voor termen af te leiden, maar die werken bottom-up, die zouden hier niet werken.
Wat je eigenlijk wil is bounds op een variabele afleiden -> approximatie/bdds doen dit
-
reporter
@ingdas wat zou je dan doen?
x vervangen door een constante en de solver laten propageren?
Wat doen we in het algemeen, bij een grote theorie, voor elke deelformule solver even oproepen?
Ik denk niet dat dat de oplossing zal zijn. Er zijn technieken om die bounds gemakkeljk en algemener af te leiden @PieterVH heeft hier zijn masterthesis over gemaakt => in principe zou je gewoon de bounds op x die toch al bestaan moeten kunnen gebruiken. De BDDs zouden slim genoeg moeten zijn om af te leiden welke waarden relevant zijn
-
Ja, ik dacht inderdaad aan zoiets. als je al die waardes onbekende constanten maakt kan je denk ik voor veel situaties makkelijk bounds afleiden die eindig zijn. Maar ik ben maar aan het fantaseren, ik heb weinig intuitie over feasibility van zulke dingen.
De BDDs gaan in de eerste plaats wel over het herordenen van de nodes gaan maar niet direct over het combineren ervan dacht ik. Dat zou dan een uitbreidingsstap zijn? -> geen enkele van X>X2 en X<X2+sqSize is op zijn eentje sterk genoeg voor een generator
-
reporter
Het werk dat Pieter nu aan het doen is gaat inderdaad over herordenen.
Maar die "uitbreidingsstap" is al uitgebreid bestudeerd in Pieter zijn thesis.
Het is duidelijk hoe we dit soort problemen willen oplossen, door integratie van een LP solver die meteen kan detecteren dat een verzameling ongelijkheden samen genereerbaar is...
-
All right, ik heb weer bijgeleerd :-)
-
- changed status to resolved
Added an exception in XSB when trying to generate an infinite data type.
The exception is initally thrown in XSB, but XSBInterface.cpp catches it and re-throws it as an InternalIdpException.
This fixes bug
#653.→ <<cset b455aa5a1c32>>
-
Als hier nog nieuwe ideeën voor te verwerken zijn, heropen de je best issue.
Voorlopig opgelost door een exception in de ongeldige gevallen te gooien (want anders krijg je foute modellen - dit was de reden voor de issue)
-
Added an exception in XSB when trying to generate an infinite data type.
The exception is initally thrown in XSB, but XSBInterface.cpp catches it and re-throws it as an InternalIdpException.
This fixes bug
#653.→ <<cset c45a65203d1c>>
- Log in to comment
Het probleem ligt aan het feit dat je int gaat nodig hebben als generator (op de manier waarop xsb het ziet toch) in: ! S[square] X Y: idpdh_mouseclick(S,X,Y) <- idpd_xpos(S,X2) & X>X2 & X<X2+sqSize() & idpd_ypos(S,Y2) & Y>=Y2 & Y<Y2+sqSize().
Hij gaat voor o.a. X>X2 & X<X2+sqSize() alle waardes van int proberen af te lopen (wat ik verhinder, ik geef gewoon 'false' terug. Daarom heeft idpdh_mouseclick geen enkele waarheidswaarde in de uitgerekende definitie.