thread 'main' panicked after cargo bool

[DanieleMarchei]

After executing cargo bool I get the following error:

thread 'main' panicked at 'Either iters or workload is required.', /home/mypath/ruler/src/lib.rs:823:18
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I am not fluent in Rust so I do not understand the error above. What could be causing it?

Here are the steps I followed during installation:

• installed libz3 (sudo apt install libz3-dev)
• cargo build --release (this took a few seconds instead of a few minutes)

My os is Pop!_OS 22.04 LTS.

[bksaiki]

Hi @DanieleMarchei , you need to provide --iters <n> as an argument on the command line. Or --workload <file> where <file> is just a text file containing boolean expressions, say

(-> true ?a) ==> ?a
?a ==> (or ?a ?a)
(or ?a ?a) ==> ?a
?a ==> (and ?a ?a)
(and ?a ?a) ==> ?a
(~ ?a) ==> (^ true ?a)
(^ true ?a) ==> (~ ?a)
(~ ?a) ==> (-> ?a false)
(-> ?a false) ==> (~ ?a)
(xor ?a ?a) ==> 0
?a ==> (or ?a 0)
(or ?a 0) ==> ?a
?a ==> (xor ?a 0)
(xor ?a 0) ==> ?a

We definitely need to write more documentation. I hope this helps!

[amyjzhu]

It's worth mentioning that if you want to run the version of Ruler described in the OOPSLA 2021 paper, you should use the oopsla21-aec branch. The tool is currently under active development.

[DanieleMarchei]

Thank you, I managed to run the bool example. I will close the issue.

About what @amyjzhu said, should I be using Ruler on the oopsla21-aec branch or is it ok to just work on the master branch? Also, is there an example somewhere on how to saturate conditional rewriting rules?

[chandrakananandi]

Thank you, I managed to run the bool example. I will close the issue.

About what @amyjzhu said, should I be using Ruler on the oopsla21-aec branch or is it ok to just work on the master branch? Also, is there an example somewhere on how to saturate conditional rewriting rules?

If you want a stable version, you should use the oopsla21-aec branch.

What do you mean by saturate conditional rewriting rules? Ruler currently does not infer that many conditional rules. It is something we are working on though and are very excited about!

[DanieleMarchei]

What do you mean by saturate conditional rewriting rules?

I am trying to find a terminating confluent TRS for a particular monoid that has conditional axioms. Since the Knuth Bendix procedure cannot deal with conditional equations I was wondering if Ruler could work with them. From issue #3 I got the sense that it might but I don't know how.

[chandrakananandi]

What do you mean by saturate conditional rewriting rules?

I am trying to find a terminating confluent TRS for a particular monoid that has conditional axioms. Since the Knuth Bendix procedure cannot deal with conditional equations I was wondering if Ruler could work with them. From issue #3 I got the sense that it might but I don't know how.

So if you are interesting in applying conditional rewrites, you should look into the egg equality saturation engine which has support for conditional appliers. Ruler uses egg as the equality saturation engine.

Ruler at the moment infers mainly axioms over total functions with some basic support for operators like division. We are working on extending that though!

If you want to apply conditional axioms, I think egg's conditional applier is what you want.