solver panics when called twice

[mmaroti]

Using this test program

extern crate batsat;
use batsat::callbacks::Basic;
use batsat::clause::{lbool, Lit, Var};
use batsat::core::Solver;
use batsat::SolverInterface;

pub fn main() {
    let mut solver: Solver<Basic> = Solver::new(Default::default(), Default::default());

    let a = Lit::new(solver.new_var_default(), false);
    let b = Lit::new(solver.new_var_default(), false);
    assert!(solver.add_clause_reuse(&mut vec![a, b]));
    assert_eq!(solver.solve_limited(&[!b]), lbool::TRUE);
    assert!(solver.add_clause_reuse(&mut vec![!a, b]));
    assert!(solver.add_clause_reuse(&mut vec![!a, !b]));
    solver.solve_limited(&[]);
}

I am seeing a panic in the last line with the error thread 'main' panicked at 'attempt to subtract with overflow'. I think this should not happen as you can add clauses between calling the solver in the original minisat and in all other sat solvers that I have tried (varisat, cryptominisat, minisat crate).

[c-cube]

Can you retry using master, actually? I can reproduce that on 3.1 but not on master.

[mmaroti]

I have used 3.1, sorry for not testing the master branch. I will do a test now.

[c-cube]

No worries! :slightly_smiling_face:

[mmaroti]

The same code panics for me on the master branch! I have used the debug build.

[c-cube]

yep, same for me, I was testing in release. CI catches it now at least. Thanks for trying!

[mmaroti]

Downloaded your latest master branch in a pristine directory and run cargo test and it fails within the new interface::test::test_reg7.

[mmaroti]

Excellent, at least you can reproduce it. Thanks for looking into this.

[mmaroti]

Thanks for the fix, it works for my real problems as well, and it is fast!

[c-cube]

glad to hear that! What are you using the solver for? :slightly_smiling_face:

[mmaroti]

Universal algebraic (pure math) research, porting an old code base from java to rust: https://github.com/mmaroti/uasat-rs

[c-cube]

0.4 was just released btw, you may want to update your cargo file :)

[mmaroti]

Excellent, thanks, I will do that. Miklos

On Thu, May 7, 2020 at 9:56 PM Simon Cruanes notifications@github.com wrote:

0.4 was just released btw, you may want to update your cargo file :)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/c-cube/batsat/issues/7#issuecomment-625464744, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAHK7NZ4QNK4AAKTTTHAQQTRQMG7LANCNFSM4MQLQFVA .