Kodkod translation fails
Description
Environment
Gliffy Diagrams
Activity
Michael Leuschel August 19, 2015 at 7:05 AM
The warning message only appears in the very latest version of probcli.
You actually managed to reproduce the problem: Kodkod translation fails and ProB falls back to its own kernel and hence the enumeration warning (which I am also investigating btw )
Sebastian Krings August 19, 2015 at 7:02 AM
can not reproduce the problem:
krings@Sebastian-Macbook-Uni prolog (develop) $ sicstus -l src/prob_cli.pl --goal "go_cli." – -p KODKOD TRUE -repl
% compiling /Users/krings/repositories/prolog/src/prob_cli.pl...
not_removing_in_meta_predicate(~~0)
64-bit platform
SICStus 4.3.2 (x86_64-darwin-14.0.0): Fri May 8 10:06:06 CEST 2015
Licensed to studentSP4.3phil-fak.uni-duesseldorf.de
ProB Interactive Expression and Predicate Evaluator
Type ":help" for more information.
>>> f={(7|>8),(8|>9),(9|>10),(10|>8)} & x <: f[x] & x /= {}
kodkod ok: (f = {(7|>8),(8|>9),(9|>10),(10|>8)} & x <: f[... ints: none, intatoms: irange(0,10)
Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).
Warning: enumerating x : INTEGER : 1:sup ---> 1:3
Warning: enumerating x : INTEGER : inf: -1 ---> -1: -1
Existentially Quantified Predicate over f,x is POSSIBLY FALSE [** ENUMERATION WARNING **]
>>>
Details
Details
Assignee
Michael LeuschelReporter
Michael LeuschelPriority
Major
For the following predicate the Kodkod translation predicate fails:
>>> f = {(7|>8),(8|>9),(9|>10),(10|>8)} & x <: f[x] & x /= {}
kodkod ok: (f = {(7|>8),(8|>9),(9|>10),(10|>8)} & x <: f[... ints: none, intatoms: irange(0,10)
! Kodkod Transformation Failed[b(identifier(f),set(couple(integer,integer)),[analysis([elem(right(interval)):irange(8,10),elem(left(interval)):irange(7,10),card:irange(4,4)])]),b(identifier,set(integer),[analysis([elem(interval):irange(8,10),card:irange(0,4)])])]
Warning: enumerating x : INTEGER : 1:sup ---> 1:3
Warning: enumerating x : INTEGER : inf: -1 ---> -1: -1
Existentially Quantified Predicate over f,x is POSSIBLY FALSE [** ENUMERATION WARNING **]
It seems the predicate register_problem from kodkod_process.pl called by apply_transformation2 in kodkod.pl fails.
The problem seems to lie in:
extract_int_types2([],[]) :- !.
extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax,IntsetName,Min,Max)]) :-
selectchk(relation(IntsetName,_,intsetrel(_Id,RMin,Max)),IntRelations,Rest),!,
Min is min(RMin,0),
extract_int_types2(Rest,[inttype(PowName,PowMin,PowMax)]). % What if Rest is [] ??
extract_int_types2(IntRelations,[inttype(PowName,PowMin,PowMax)]) :-
memberchk(relation(PowName,_,pow2rel(_Id,RPowMin,PowMax)),IntRelations),!,
PowMin is min(RPowMin,0).
which I don't understand yet.
The debug trace is:
17 5 Call: kodkod_process:extract_int_types2([relation(is,11,intsetrel(is,0,10))],_3177333) ? s
17 5 Fail: kodkod_process:extract_int_types2([relation(is,11,intsetrel(is,0,10))],_3177333) ? r
17 5 Call: kodkod_process:extract_int_types2([relation(is,11,intsetrel(is,0,10))],_3177333) ?
18 6 Call: selectchk(relation(_3180329,_3180339,intsetrel(_3180345,_3180347,_3180333)),[relation(is,11,intsetrel(is,0,10))],_3180357) ? s
18 6 Exit: selectchk(relation(is,11,intsetrel(is,0,10)),[relation(is,11,intsetrel(is,0,10))],[]) ?
19 6 Call: kodkod_process:extract_int_types2([],[inttype(_3180323,_3180325,_3180327)]) ?
20 7 Call: memberchk(relation(_3180323,_3182597,pow2rel(_3182603,_3182605,_3180327)),[]) ?
20 7 Fail: memberchk(relation(_3180323,_3182597,pow2rel(_3182603,_3182605,_3180327)),[]) ?
19 6 Fail: kodkod_process:extract_int_types2([],[inttype(_3180323,_3180325,_3180327)]) ?
17 5 Fail: kodkod_process:extract_int_types2([relation(is,11,intsetrel(is,0,10))],_3177333)