I have this following case modified from tests/lib.rs
fn test_pb() {
let cfg = Config::new();
let ctx = Context::new(&cfg);
let x = ast::Bool::new_const(&ctx, "x");
let y = ast::Bool::new_const(&ctx, "y");
let a = ast::Bool::new_const(&ctx, "a");
let b = ast::Bool::new_const(&ctx, "b");
let c = ast::Bool::new_const(&ctx, "c");
let d = ast::Bool::new_const(&ctx, "d");
let solver = Solver::new(&ctx);
solver.push();
// this line
solver.assert(&ast::Bool::pb_eq(
&ctx,
&[(&a, 1), (&b, 1), (&c, 1), (&d, 1)],
2,
));
solver.push();
solver.assert(&ast::Bool::pb_eq(&ctx, &[(&x, 1), (&y, 1)], 1));
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();
let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
info!("x: {}", xv);
info!("y: {}", yv);
assert!((xv && !yv) || (!xv && yv));
info!("{:?}", solver.get_statistics());
solver.pop(1);
solver.push();
solver.assert(&ast::Bool::pb_ge(&ctx, &[(&x, 1), (&y, 1)], 2));
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();
let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
info!("x: {}", xv);
info!("y: {}", yv);
assert!(xv && yv);
info!("{:?}", solver.get_statistics());
solver.pop(1);
solver.assert(&ast::Bool::pb_le(&ctx, &[(&x, 1), (&y, 1)], 0));
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();
let xv = model.eval(&x, true).unwrap().as_bool().unwrap();
let yv = model.eval(&y, true).unwrap().as_bool().unwrap();
info!("x: {}", xv);
info!("y: {}", yv);
assert!(!xv && !yv);
info!("{:?}", solver.get_statistics());
let res = solver.check();
info!("{res:?}");
info!("{:?}", solver.get_statistics());
}
Basically I want to see that the assertion (a+b+c+d==2) has only one-time affect on the number of decisions, since it is pushed to the bottom of the assertion stack and have no affect on other assertions.
However, without that assertion, the final number of decisions is 1 while with that assertion, the final number of decision becomes 11.
I have this following case modified from
tests/lib.rs
Basically I want to see that the assertion (a+b+c+d==2) has only one-time affect on the number of decisions, since it is pushed to the bottom of the assertion stack and have no affect on other assertions.
However, without that assertion, the final number of decisions is 1 while with that assertion, the final number of decision becomes 11.
Is there something that I've missed?