Abdallah

Bug in prenex handling of Or.

1

See line https://github.com/touist/touist/blob/1bf1b5254fcbe8e4f368c7684a5d51b9a1852487/src/lib/qbf.ml#L64 . The And on the right-hand side needs to be Or. I'll fix it at some point, but it'd be nice to have some unit tests for...

Latex.ast_fun unexpected behaviour

1

In the file src/lib/latex.ml, the function ast_fun behaves differently on `x mod y` than on `x add y` and other binary operators. This sounds strange to me and looks like...

Inconsistent behaviour of `--qdo` on input with no clauses

1

Consider the following input: a formula with 4 variables and no clauses. p cnf 4 0 e 1 2 3 4 0 Running `depqbf` on it returns `SAT` as expected....

Enabling size 19x19

1

Is it possible to enable board size 19x19? I've tried adding the option `-DSUPPORT_19x19` to the CMAKE_CXX_FLAGS, based on the configure file of [benzene-1](https://github.com/cgao3/benzene-1) , but I run into the...

Refining/constraining predicates based on combination of fields

5

Is there a mechanism to impose constraints on the predicate sub-class based on combinations of fields? In the following example, I would like any predicate intance that unifies with the...

Gringo considers unnecessary instantiations of rule heads.

12

Consider the following program. query(add(x,y)). value(x,2). value(y,30). value(E,@computeAdd("value",N1,N2)) :- query(E), E=add(E1,E2), value(E1,N1), value(E2,N2). value1(add(E1,E2),@computeAdd("value1",N1,N2)) :- query(add(E1,E2)), value(E1,N1), value(E2,N2). value2(E,@computeAdd("value2",N1,N2)) :- query(E), E > never, E=add(E1,E2), value(E1,N1), value(E2,N2). #script (python) import...