Shuffle and Scramble QBF Files

Bule offers to scramble QBF/SAT Dimacs files:

>>> cat  test.cnf | bule shuffle --polarity --seed 123

Fixed bugs

• Many smaller bugs
• Sequence of facts in the same line are handled. e.g. f[1]. f[2]. now correct parsing.
• Range in Equivalence is correctly handled: e.g. F==1..4::p(X),q(X+1).

Variable declaration modified. Change in Syntax of #exists and #forall

• exist -> exists
• From now on variable declarations are done as follows:

#exists[Level], .... :: variable(...)?
#forall[Level], .... :: variable(...)?

Example from the Connect4 encoding:

#exists[T], domC[C], domR0[R], domT0[T] :: occupied(C,R,T)? 
#exists[d], dom[C,R]                              :: board(C,R)?
#exists[d], dom[C,R], C+(q-1)<=c, R<=r            :: winO(C,R,1)?
#exists[d], dom[C,R], C<=c , R+(q-1)<=r           :: winO(C,R,0)?
#exists[d], dom[C,R], dir[Z], C+q-1<=c,R+q-1<=r   :: winD(C,R,Z)?

add, remove and list available SAT and QBF solvers

• Command add, rm, list to handle SAT and QBF solvers
• Call SAT solver on SAT formula, and QBF on QBF formulas.
• Proper output parsing and replacing integers by bule literals.

Syntax adapted to :: and -> to make it clear between clause and fact generation

Now => is replaced by :: and -> depending if it's a clause generation or a fact generation.

Facts are generated like this now:

a[X] -> b[X].

but for clauses :

a[X] :: ~c(X), c(X+1).

The rest stays the same !

Small bugfixes

As v2.5.

Bule calls DEPQBF solver

Now bule can solve QBF formulas and replace ids with meaningful identifiers.

Example:

$ cat test-input/w03.bul:
q(1), q(2).
q(4), q(5).
Y == X+1 => ~q(X), ~q(Y).

$ bule solve test-input/w03.bul
TRUE
q(5) ~q(1) q(2) ~q(4)