search

vale1410 / bule

The SAT and QBF Programming Language Bule
Other
21 stars 3 forks source link

Incorrect behavior when enumerating models #60

Closed vale1410 closed 1 year ago

vale1410 commented 1 year ago

Call the following program with --solve --models 0 does not iterate through all models, but stops with the first one and does not continue: 

#ground dim[1..4]. 
#ground ex[x], ex[y]. 
ex[E],  dim[I] :: #exists[0] v(E,I).   
dim[I] :: ~v(x,I) | ~v(y,I).
AbdallahS commented 1 year ago

Yeah, it's the usual issue with the embedded qbf solver that is buggy. Duplicate of issue #38 . You can run with '--solve --models 0 --solver minisat' or with '--solve --models 0 --solver "depqbf --no-dynamic-nenofex --qdo"' and it should work.