vale1410/bule

The SAT and QBF Programming Language Bule

bule's Issues

Grounding of arithmetic involving negative integers

Consider the following program.

test[-1].
test[X] :: do(1+X).

I would expect it to ground to do(0), instead, I get a syntax error about invalid token '+-'

Line number in error message is wrong when there are multiple files.

Consider the command bule solve file1.bul file2.bul . If there is an error in file2.bul, the line reported will off by the number of lines in file1

performance test 2

> bule ipc_2000_blocks_10_11.bul

grounds successful whereas:

> bule ipc_2000_blocks_10_12.bul
Warning. Grounding predicate type used in a rule without being defined anywhere.
Fatal error: exception Stack overflow

ipc_2000_blocks_10_11.bul.txt
ipc_2000_blocks_10_12.bul.txt

More information in Error for debugging : line numbers

For certain errors Bule does not output info needed for tracing the problem like line number and file name.

Example:

File:

#ground a[12]. 

a[Y] :: #ground b[X]. 

running Bule outputs:

Fatal error: exception Bule2.Circuit.UnboundVar("X")

missing line number and more.

Running bule2 with introduction examples creates infinite loop.

when running bule2 --solve --models 0 graph_colouring_basic.bul wtih unchanged graph_colouring_basic.bul
output is

Instance ground. Starts solving
SAT
Model 1: ~set_a_blue ~set_a_green ~set_a_red ~set_e_blue ~set_e_green ~set_e_red

If running bule2 --solve --models 0 graph_colouring_basic.bul --solver minisat, the output is as expected

Instance ground. Starts solving
SAT
Model 1: ~set_a_blue ~set_a_green  set_a_red ~set_e_blue  set_e_green ~set_e_red
Model 2: ~set_a_blue ~set_a_green  set_a_red  set_e_blue ~set_e_green ~set_e_red
Model 3: ~set_a_blue  set_a_green ~set_a_red ~set_e_blue ~set_e_green  set_e_red
Model 4: ~set_a_blue  set_a_green ~set_a_red  set_e_blue ~set_e_green ~set_e_red
Model 5:  set_a_blue ~set_a_green ~set_a_red ~set_e_blue  set_e_green ~set_e_red
Model 6:  set_a_blue ~set_a_green ~set_a_red ~set_e_blue ~set_e_green  set_e_red
No more models. Total: 6 displayed models out of 6 models.

Distinguish `bule dimacs` and `bule ground`

Distinguish correctly:

• bule dimacs (to be piped to a SAT or QBF Solver)
• bule ground (for debugging with textual output)

@AbdallahS

Fix std Err and Output of Bule regarding pipe from Solvers

Currently the std.output of the solvers is piped to stderr from bule. Fix.

Alternative notation for quantifiers

I'd like to be able to write #E[T] :: var[T] as an alternative to #exists[T] :: var[T], same with #A[T] instead of #forall[T]. This is shorter and no less readable because we are used to $\exists$ and $\forall$ in mathematics.

bule dimacs doesn't seem to work

bule dimacs sample.bul returns

c dimacs grounding called.
prepare with args
p cnf 10 2
e 5 8 9 2 3 4 6 7 10 11 0 
dom[c]. | .
#exists | [0] |  | all[X] |  | all[Y] |  | dom[Z] | :: | q(X | Y | Z)?.

the sample.bul file contains:

  dom[a].
  dom[b].
  dom[c]. 
  mom[d].
  mom[e].
  dom[X] :: all[X].
  mom[X] :: all[X].
  #exists [0], all[X], all[Y], dom[Z] :: q(X,Y,Z)?
  dom[X], mom[Y] :: dom[Z] : q(X,Y,Z).
  dom[X], dom[Y] :: q(X,Y,c) | q(Y,X,b).

prefix standard library predicates with std_

do it

Display more information from the original unground program

Problem: Given a ground clause it can be hard to find out from which Bule rule it came from. I start to comment out Rules and see how the ground program changes.

Easy and very useful information:
Before every set of ground clauses display the original Bule Rule in a comment

For example, this program:

#ground dom[1], dom[2], dom[3].

dom[X] :: #forall[X] varA(X). 
dom[X] :: #exists[X] varE(X). 

dom[A] :: varA(A) | dom[E] : varE(E). 
dom[E],dom[A] :: ~varE(E) | varA(A). 

The result from bule test.bul --origin would be:

%% dom[X] :: #forall[X] varA(X). 
%% generates 3 universal variables
%% dom[X] :: #exists[X] varE(X). 
%% generates 3 existential variables 
#forall[0] varA(1).
#exists[1] varE(1).
#forall[2] varA(2).
#exists[3] varE(2).
#forall[4] varA(3).
#exists[5] varE(3).

%% dom[A] :: varA(A) | dom[E] : varE(E). 
%% grounds to 3 clauses: 
 varA(1) |  varE(1) |  varE(2) |  varE(3).
 varA(2) |  varE(1) |  varE(2) |  varE(3).
 varA(3) |  varE(1) |  varE(2) |  varE(3).

%%  dom[E],dom[A] :: ~varE(E) | varA(A). 
%% grounds to 9 clauses: 
~varE(1) |  varA(1).
~varE(1) |  varA(2).
~varE(1) |  varA(3).
~varE(2) |  varA(1).
~varE(2) |  varA(2).
~varE(2) |  varA(3).
~varE(3) |  varA(1).
~varE(3) |  varA(2).
~varE(3) |  varA(3).

Bule command not working

Hello!

So in the instructions for set up, commands such as bule list and bule add is not working. Specifically, the error message is:

---

Command 'bule' not found, did you mean:

command 'buble' from deb node-buble (0.19.8-8)

Try: sudo apt install

---

I know that the commands are stored in cmd directory but how can I install bule to make it source these files?

Code with a variable occuring in different quantifier blocks isn't rejected.

The following code grounds fine, but it shouldn't.

#exists[0] :: a?
#forall[1] :: a?
#exists[2] :: c?

a | c.

Same story with

#exists[0] :: a?
#forall[1] :: c?
#exists[2] :: a?

a | c.

Dont allow free variables

Flag to remove solver output

Hello!

Just wondering if there is an optional flag to suppress the output as shown below. If not, is there any possibility that this can be created soon?

Negation in Generator and Free Variables

%% %% %%% Problem with negation and _ :
%% val[X], ~map[_,X] :: debug[X].

Ship a QBF solver with Bule2.

Minisiat is provided for pure SAT formulas, but Bule2 can only generate DIMACS for QBF formulas and cannot drive a solver. It is desirable to have a solver embedded to be able to nicely print the models.

Preserve literal order in grounding

This will facilitate debugging.

Let bule read from stdin

Many unix commands can read their input from the standard input channel. It would be nice for bule to allow that too.

For example cat file1.bul file2.bul | bule file3.bul or, alternatively use - as a signal for stdin reading cat file1.bul file2.bul | bule file3.bul -.

(this is not so useful with piping from cat as bule can take many files as input already, but it can be useful with grep or bule2 input).

Introduce error detection mechanism in the grounding

Something similar to assertions in other languages, for instance running bule2 on the following code

:: dom[X], bad[X] :: #fail.
dom[1..3].
bad[3..5].

should produce an error message (because of X=3) and stop grounding. This makes it possible to detect errors in the grounding process or in parameters files.

Similarly, we could introduce a dual keyword for grounding that needs to take place.

:: dom[X], need[X] :: #required.
dom[1..3].
need[1..4].

should produce an error message because of X=4 missing.

bule solve doesn't display propagated literals.

literals eliminated during unit propagation are not presenit in the bule solve model.

Introdiuce Bule solve option to avoid printing variable assigned false

Running bule2 --solve --models 0 test.bule2 on file containing:

#exists[0] x.
#exists[0] y.
#exists[0] z.
x | y.
~z.

Returns the following output:

Model 1: ~x  y ~z
Model 2:  x ~y ~z
Model 3:  x  y ~z

I would like bule2 option so that the output is:

Model 1:  y 
Model 2:  x  
Model 3:  x  y 

Using wrong brackets: better error message

Currently, following program

#ground v(1).

results in this error message:

Fatal error: exception Invalid_argument("Parser error. In file error.bul, at line 6, column 9: syntax error. <YOUR SYNTAX ERROR MESSAGE HERE>\n (error 56)")

Better error message:

Line 1, wrong usage of parenthesis for extensional atom. Please use brackets.

Introduce syntax "#forall" without specifying the level

Dual to issue #34 , but it's not clear to me in the universal case whether the variables should be going outermost or second innermost before the existential one.

Variables introduced several times in the same block should be fine

The following snippet is converted to incorrect qdimacs (with variable v appearing twice in the block) and causes issues in the solver.

#ground p[x], p[y].
p[A] :: #exists v.
v.
~v.

Single literals giving unexpected results

dom[a].
dom[b].
dom[c]. 
mom[d].
mom[e].
dom[X] :: all[X].
mom[X] :: all[X].
#exists [0], all[X], all[Y], dom[Z] :: q(X,Y,Z)?
q(c,e,c).
dom[X], mom[Y] :: dom[Z] : q(X,Y,Z).
dom[X], dom[Y] :: q(X,Y,c) | q(Y,X,b).

In this code block, I have explicitly mentioned q(c,e,c) to be true but it comes out to be false. This isn't just the case here, it happens every time. Single literals are not getting implemented correctly.

bule solve sample.bul return :

C program grounded in 32.605973ms.
This is a QBF problem
Using a QBF solver instance 'depqbf --no-dynamic-nenofex --qdo'
Solving. . .

-------- Solver output ----- 
2021/06/12 12:04:01 solver>>  s cnf 1 75 15
-------- Solver output end ----- 
s SAT
--------
~q(c,e,c).
q(c,d,c).
q(c,c,c).
q(c,b,c).
~q(a,d,a).
~q(a,e,a).
q(c,a,c).
q(b,e,c).
q(b,d,c).
~q(b,d,a).
~q(b,e,a).
q(b,c,c).
q(b,b,c).
q(b,a,c).
~q(c,d,a).
~q(c,e,a).
q(a,e,c).
q(a,d,c).
q(a,c,c).
q(a,b,c).
q(a,a,c).
q(c,e,b).
~q(c,d,b).
~q(c,c,b).
~q(c,b,b).
~q(c,a,b).
~q(a,a,b).
~q(a,b,b).
~q(a,c,b).
~q(a,d,b).
~q(a,e,b).
~q(b,a,b).
~q(b,b,b).
~q(b,c,b).
~q(b,d,b).
~q(b,e,b).
--------

BUG: Comments not properly handled

Comments for solvers are improperly handled.

Modified bule2/lib/Solve.ml to fix the issue:

Below is the code from line 24:
let input_lines inp =
let l = ref [] in
(try
while true do l := input_line inp :: !l done
with End_of_file -> ());
List.rev !l

let isnt_comment line =
String.length line > 0 && line.[0] <> 'c'

let run_process cmd dimacs =
let inp, out = Unix.open_process cmd in
fprintf out "%s%!" (Dimacs.Print.qbf_file dimacs);
close_out out;
let lines = input_lines inp in
close_in inp;
let lines = List.filter isnt_comment lines in
parse_output lines

Bule doesnt solve equations with `2*X==4`

n[1].
n[2].
n[2*X] :: m[X].

should ground to n[1].n[2].m[1].

There is a way around it by just adding a domain predicate for the variables to be solved:

Grouding: Avoid generating identical clauses from unnamed variables.

Consider the following program.

bar[a]. bar[b].
bar[X], bar[Y] :: foo[X,Y].

foo[X,_] :: var(X).

Bule grounds it to

var(a). var(a). var(b). var(b).

Whereas

var(a). var(b).

would be preferable.

Variables in domains not matching

This issue is similar to #26 (comment)

#ground d_t[a, f(a)].
#ground d_t[b, f(b)].

d_t[X, f(X)] :: m(X).

produces no grounding result. By changing the clause to:

d_t[X, f(X_1)], X == X_1 :: m(X).

We get the grounding result

m(a).
m(b).

performance test 1

This program generate 360000 facts, but gets a stackoverflow error when called with --facts

#ground p[1..600].  
p[X], p[Y] :: #ground q[X,Y,X+Y].

with p[1..500] it manages to ground and print the facts.

Bule2 syntax is not used in the README

For example dom[1..3]. should be #ground dom[1..3]. Not sure if this is intentional or not.

Happy to make a PR to update syntax in the syntax section to bule2 if needed.

order of arithemtic expression matter

following program gives an error message: Fatal error: exception Failure("Error: variable X is unbound in an arithmetical expression when grounding p[X \\+ 1].")

#ground p[1], t[2].                                                                                                                       
p[X+1], p[X] :: #ground q[X]. 

it works correctly if order in the generator is swapped:

#ground p[1], t[2].                                                                                                                       
p[X], p[X+1]  :: #ground q[X]. 

Allow multiple search variable declaration sentences per line.

The following snippet creates a panic error in bule.

#exists[0] :: assign(1,1,1,2)? #exists[0] :: assign(1,1,1,1)?
~assign(1,1,1,2) | ~assign(1,1,1,1).
assign(1,1,1,2) | assign(1,1,1,1).

#exists with no [I] puts variables per default on innermost level.

similar for #forall second to innermost level of #exists

Allow for Implication `->` in the Clauses

Allow for simple Implications => in the Clause. Left part of implication is separated by & , and right party by | .
Iterators ground straight forward generate & on the left, and | on the right. Only one level term rewriting.

rule :: <generator> <RuleSep>  <iterator> ( <AND> <iterator> ) *  <Implication>  <iterator> ( <OR> <iterator> )* <EndRule> 

<generator> :: <factOrConstraint> ( , <factOrConstraint>)  
<iterator> :: <factOrConstraint> ( , <factOrConstraint>)  : <literal>

literal :: (~  | <atom>) 

Example:

dom[1].dom[2].
dom[X], dom[Y], X==Y ::
        ~q(X) &
        dom[X], dom[Y], X > Y : vale(X)  
        ->
        q(Y) |
        dom[Z] : r(Y,Z).

Thanks to
@AbdallahS

Don't show negative literals by default

Introduce more show command-line options, like show positive, show all, show none.

Introduce "bule2 --blame"

For given grounding files, and a given model not satisfying the corresponding formula, identify which clauses are not satisfied by the model. Ideally, we would also identify the lifted clauses.

fix output syntax

this is old:

#exists[0] :: set(e,red)?
#exists[0] :: set(e,green)?

should be :

#exists[0] set(e,red).
#exists[0] set(e,green).

and with issue ... it could be:

#exists set(e,red).
#exists set(e,green).

Variables within functions not matching in Bule2

Given the following Bule2 example:

d_colored[va].
d_colored[vb].
d_colored1[color(va, red)].
d_colored1[color(vb, red)].
:: d_colored[Vv] :: colored(Vv) -> : d_colored1[color(Vv, Vc)] : colored1(color(Vv, Vc)).

It produces the grounding result:

colored(va) -> .
colored(vb) -> .

The expected grounding would be:

colored(va) -> colored1(color(va, red)).
colored(vb) -> colored1(color(vb, red)).

By changing the Bule2 rule to:

:: d_colored[Vv] :: colored(Vv) -> : d_colored1[color(V1, Vc)], V1 == Vv : colored1(color(V1, Vc)).

The grounding produces the expected result. This problem appears to only happen with variables within functions. e.g.

Generate clauses of which

The following program should not generate any unit clauses:

#ground f[1],f[2],f[3]. 
f[X] :: var(X). 

Bule grounds this to:

Warning. Undeclared variables: var(1) var(2) var(3)

 var(1).
 var(2).
 var(3).

It's good that it notifies that clauses are generated of which no variables are introduced.
In my opinion it should not generate the clauses at all.

For example:

#ground f[1],f[2].     
f[X] :: #exists[0] foo(X).  
f[X] :: bar(X) | foo(X). 

In my opinion it should not generate the clauses.

Alternative option: it generates the clauses with the atoms that have been introduced.

Bule DIMACS output file could be more readable

It would be great if there could be a mapping from strings to integer in the comments of the dimacs file in order to make it more readable.

Bule doesnt complain about wrong , and : in iterators.

Examples;

fact[B], literal(B).

instead of

fact[B] : literal(B).

bule version

bule --version or bule version should provide the current version.

introduce ranges in definitions

we would like something like

Q:=1..4 :: #ground dom[Q].

Syntax in bule ground for variable declaration

The bule syntax for version 4 does not have ? anymore.

following bule program

#exists[0] v(1).

with running bule on it gives:

#exists[0] :: v(1)?

should not return with question mark.

Infinite loop for multiple models (QBF mode with custom solver)

bule version check

bule --version has no output

Unfinished last statement is not detected and no error is raised

The following code shouldn't solve/ground at all because there is no final full stop after a[0].

a[1].
#exists[0], a[X] :: var(X)?
a[X]:: var(X).
a[0]

Introduce a #show command

Currently there is just a #hide command which stops search variables front being show in stdout when solving / grounding.

It would be helpful to have a #show command where only variables with #show in front of them are shown.