From fb625b965a2fd433406db741d38ab9d1239304e2 Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Thu, 4 Apr 2024 11:43:09 +0300 Subject: [PATCH] refactor: factor out solver integration tests --- Cargo.toml | 1 + cadical/Cargo.toml | 3 + cadical/tests/incremental.rs | 87 +---------- cadical/tests/phasing.rs | 39 +---- cadical/tests/small.rs | 112 ++------------ glucose/Cargo.toml | 3 + glucose/tests/incremental.rs | 88 +---------- glucose/tests/phasing.rs | 39 +---- glucose/tests/small.rs | 71 +-------- kissat/Cargo.toml | 3 + kissat/tests/small.rs | 112 ++------------ minisat/Cargo.toml | 3 + minisat/tests/incremental.rs | 87 +---------- minisat/tests/phasing.rs | 39 +---- minisat/tests/small.rs | 72 +-------- release-plz.toml | 5 + solvertests/Cargo.toml | 16 ++ solvertests/src/lib.rs | 275 +++++++++++++++++++++++++++++++++++ 18 files changed, 367 insertions(+), 688 deletions(-) create mode 100644 solvertests/Cargo.toml create mode 100644 solvertests/src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index cc31a465..468b0e15 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,7 @@ members = [ "glucose", "minisat", "ipasir", + "solvertests", ] resolver = "2" diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml index 8079e9e9..9afb53af 100644 --- a/cadical/Cargo.toml +++ b/cadical/Cargo.toml @@ -50,3 +50,6 @@ cc = { version = "1.0.83", features = ["parallel"] } git2 = "0.18.1" glob = "0.3.1" chrono = "0.4.31" + +[dev-dependencies] +rustsat-solvertests = { path = "../solvertests" } diff --git a/cadical/tests/incremental.rs b/cadical/tests/incremental.rs index 0f0df4e3..aed0e6f7 100644 --- a/cadical/tests/incremental.rs +++ b/cadical/tests/incremental.rs @@ -1,86 +1 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{SolveIncremental, SolverResult}, -}; -use rustsat_cadical::CaDiCaL; - -fn test_assumption_sequence(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -#[test] -fn assumption_sequence() { - let solver = CaDiCaL::default(); - test_assumption_sequence(solver); -} +rustsat_solvertests::incremental_tests!(rustsat_cadical::CaDiCaL); diff --git a/cadical/tests/phasing.rs b/cadical/tests/phasing.rs index 492faf6e..2f1c9370 100644 --- a/cadical/tests/phasing.rs +++ b/cadical/tests/phasing.rs @@ -1,34 +1,5 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{PhaseLit, Solve, SolverResult}, - types::TernaryVal, - var, -}; -use rustsat_cadical::CaDiCaL; - -fn test_phase_saving(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - solver.phase_lit(lit![0]).unwrap(); - solver.phase_lit(!lit![1]).unwrap(); - solver.phase_lit(lit![2]).unwrap(); - solver.phase_lit(!lit![3]).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let sol = solver.solution(var![3]).unwrap(); - assert_eq!(sol.lit_value(lit![0]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![1]), TernaryVal::False); - assert_eq!(sol.lit_value(lit![2]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![3]), TernaryVal::False); - solver.unphase_var(var![1]).unwrap(); - solver.unphase_var(var![0]).unwrap(); -} - -#[test] -fn phase_saving() { - let mut solver = CaDiCaL::default(); - solver.set_option("lucky", 0).unwrap(); - test_phase_saving(solver); -} +rustsat_solvertests::phasing_tests!({ + let mut slv = rustsat_cadical::CaDiCaL::default(); + slv.set_option("lucky", 0).unwrap(); + slv +}); diff --git a/cadical/tests/small.rs b/cadical/tests/small.rs index 5bd5d74c..b2e59e52 100644 --- a/cadical/tests/small.rs +++ b/cadical/tests/small.rs @@ -1,102 +1,20 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - solvers::{Solve, SolverResult}, -}; -use rustsat_cadical::CaDiCaL; - -fn small_sat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); -} - -fn small_unsat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf") - .unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -fn ms_segfault_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); +mod base { + rustsat_solvertests::base_tests!(rustsat_cadical::CaDiCaL); } -#[test] -fn small_sat() { - let solver = CaDiCaL::default(); - small_sat_instance(solver); +mod sat { + rustsat_solvertests::base_tests!({ + let mut slv = rustsat_cadical::CaDiCaL::default(); + slv.set_configuration(rustsat_cadical::Config::SAT).unwrap(); + slv + }); } -#[test] -fn small_unsat() { - let solver = CaDiCaL::default(); - small_unsat_instance(solver); -} - -#[test] -fn ms_segfault() { - let solver = CaDiCaL::default(); - ms_segfault_instance(solver); -} - -#[test] -fn sat_small_sat() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::SAT) - .unwrap(); - small_sat_instance(solver); -} - -#[test] -fn sat_small_unsat() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::SAT) - .unwrap(); - small_unsat_instance(solver); -} - -#[test] -fn sat_ms_segfault() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::SAT) - .unwrap(); - ms_segfault_instance(solver); -} - -#[test] -fn unsat_small_sat() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::UNSAT) - .unwrap(); - small_sat_instance(solver); -} - -#[test] -fn unsat_small_unsat() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::UNSAT) - .unwrap(); - small_unsat_instance(solver); -} - -#[test] -fn unsat_ms_segfault() { - let mut solver = CaDiCaL::default(); - solver - .set_configuration(rustsat_cadical::Config::UNSAT) - .unwrap(); - ms_segfault_instance(solver); +mod unsat { + rustsat_solvertests::base_tests!({ + let mut slv = rustsat_cadical::CaDiCaL::default(); + slv.set_configuration(rustsat_cadical::Config::UNSAT) + .unwrap(); + slv + }); } diff --git a/glucose/Cargo.toml b/glucose/Cargo.toml index 62879b18..8481d335 100644 --- a/glucose/Cargo.toml +++ b/glucose/Cargo.toml @@ -30,3 +30,6 @@ git2 = "0.18.1" glob = "0.3.1" chrono = "0.4.31" cmake = "0.1.50" + +[dev-dependencies] +rustsat-solvertests = { path = "../solvertests" } diff --git a/glucose/tests/incremental.rs b/glucose/tests/incremental.rs index 55bbf818..b8ed4aee 100644 --- a/glucose/tests/incremental.rs +++ b/glucose/tests/incremental.rs @@ -1,86 +1,6 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{SolveIncremental, SolverResult}, -}; -use rustsat_glucose::core::Glucose; - -fn test_assumption_sequence(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); +mod core { + rustsat_solvertests::incremental_tests!(rustsat_glucose::core::Glucose); } -#[test] -fn assumption_sequence() { - let solver = Glucose::default(); - test_assumption_sequence(solver); -} +// Note: Cannot test prepro version of glucose with this small example because +// the variable are eliminated by preprocessing diff --git a/glucose/tests/phasing.rs b/glucose/tests/phasing.rs index 4791dc44..20f886bb 100644 --- a/glucose/tests/phasing.rs +++ b/glucose/tests/phasing.rs @@ -1,38 +1,7 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{PhaseLit, Solve, SolverResult}, - types::TernaryVal, - var, -}; -use rustsat_glucose::{core, simp}; - -fn test_phase_saving(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - solver.phase_lit(lit![0]).unwrap(); - solver.phase_lit(!lit![1]).unwrap(); - solver.phase_lit(lit![2]).unwrap(); - solver.phase_lit(!lit![3]).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let sol = solver.solution(var![3]).unwrap(); - assert_eq!(sol.lit_value(lit![0]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![1]), TernaryVal::False); - assert_eq!(sol.lit_value(lit![2]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![3]), TernaryVal::False); - solver.unphase_var(var![1]).unwrap(); - solver.unphase_var(var![0]).unwrap(); -} -#[test] -fn core_phase_saving() { - let solver = core::Glucose::default(); - test_phase_saving(solver); +mod core { + rustsat_solvertests::phasing_tests!(rustsat_glucose::core::Glucose); } -#[test] -fn simp_phase_saving() { - let solver = simp::Glucose::default(); - test_phase_saving(solver); +mod simp { + rustsat_solvertests::phasing_tests!(rustsat_glucose::simp::Glucose); } diff --git a/glucose/tests/small.rs b/glucose/tests/small.rs index 35c29c93..c1780d5e 100644 --- a/glucose/tests/small.rs +++ b/glucose/tests/small.rs @@ -1,70 +1,7 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - solvers::{Solve, SolverResult}, -}; -use rustsat_glucose::{core, simp}; - -fn small_sat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); -} - -fn small_unsat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf") - .unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -fn ms_segfault_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -#[test] -fn core_small_sat() { - let solver = core::Glucose::default(); - small_sat_instance(solver); -} - -// Note: this instance seems too hard for glucose to solve -#[test] -#[ignore] -fn core_small_unsat() { - let solver = core::Glucose::default(); - small_unsat_instance(solver); -} - -#[test] -fn core_ms_segfault() { - let solver = core::Glucose::default(); - ms_segfault_instance(solver); -} - -#[test] -fn simp_small_sat() { - let solver = simp::Glucose::default(); - small_sat_instance(solver); -} - -// Note: this instance seems too hard for glucose to solve -#[test] -#[ignore] -fn simp_small_unsat() { - let solver = simp::Glucose::default(); - small_unsat_instance(solver); +mod core { + rustsat_solvertests::base_tests!(rustsat_glucose::core::Glucose, false, true); } -#[test] -fn simp_ms_segfault() { - let solver = simp::Glucose::default(); - ms_segfault_instance(solver); +mod simp { + rustsat_solvertests::base_tests!(rustsat_glucose::simp::Glucose, false, true); } diff --git a/kissat/Cargo.toml b/kissat/Cargo.toml index cf0817c4..b40c0074 100644 --- a/kissat/Cargo.toml +++ b/kissat/Cargo.toml @@ -35,3 +35,6 @@ cc = { version = "1.0.83", features = ["parallel"] } git2 = "0.18.1" glob = "0.3.1" chrono = "0.4.31" + +[dev-dependencies] +rustsat-solvertests = { path = "../solvertests" } diff --git a/kissat/tests/small.rs b/kissat/tests/small.rs index f7ddd67c..fb3371a0 100644 --- a/kissat/tests/small.rs +++ b/kissat/tests/small.rs @@ -1,102 +1,20 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - solvers::{Solve, SolverResult}, -}; -use rustsat_kissat::Kissat; - -fn small_sat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); -} - -fn small_unsat_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf") - .unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -fn ms_segfault_instance(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); +mod base { + rustsat_solvertests::base_tests!(rustsat_kissat::Kissat); } -#[test] -fn small_sat() { - let solver = Kissat::default(); - small_sat_instance(solver); +mod sat { + rustsat_solvertests::base_tests!({ + let mut slv = rustsat_kissat::Kissat::default(); + slv.set_configuration(rustsat_kissat::Config::SAT).unwrap(); + slv + }); } -#[test] -fn small_unsat() { - let solver = Kissat::default(); - small_unsat_instance(solver); -} - -#[test] -fn ms_segfault() { - let solver = Kissat::default(); - ms_segfault_instance(solver); -} - -#[test] -fn sat_small_sat() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::SAT) - .unwrap(); - small_sat_instance(solver); -} - -#[test] -fn sat_small_unsat() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::SAT) - .unwrap(); - small_unsat_instance(solver); -} - -#[test] -fn sat_ms_segfault() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::SAT) - .unwrap(); - ms_segfault_instance(solver); -} - -#[test] -fn unsat_small_sat() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::UNSAT) - .unwrap(); - small_sat_instance(solver); -} - -#[test] -fn unsat_small_unsat() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::UNSAT) - .unwrap(); - small_unsat_instance(solver); -} - -#[test] -fn unsat_ms_segfault() { - let mut solver = Kissat::default(); - solver - .set_configuration(rustsat_kissat::Config::UNSAT) - .unwrap(); - ms_segfault_instance(solver); +mod unsat { + rustsat_solvertests::base_tests!({ + let mut slv = rustsat_kissat::Kissat::default(); + slv.set_configuration(rustsat_kissat::Config::UNSAT) + .unwrap(); + slv + }); } diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml index ace5a5b1..ebae177f 100644 --- a/minisat/Cargo.toml +++ b/minisat/Cargo.toml @@ -30,3 +30,6 @@ git2 = "0.18.1" glob = "0.3.1" chrono = "0.4.31" cmake = "0.1.50" + +[dev-dependencies] +rustsat-solvertests = { path = "../solvertests" } diff --git a/minisat/tests/incremental.rs b/minisat/tests/incremental.rs index a29a9259..75a1f694 100644 --- a/minisat/tests/incremental.rs +++ b/minisat/tests/incremental.rs @@ -1,88 +1,5 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{SolveIncremental, SolverResult}, -}; -use rustsat_minisat::core::Minisat; - -fn test_assumption_sequence(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Sat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); - let res = solver - .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]]) - .unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -#[test] -fn assumption_sequence() { - let solver = Minisat::default(); - test_assumption_sequence(solver); +mod core { + rustsat_solvertests::incremental_tests!(rustsat_minisat::core::Minisat); } // Note: Cannot test prepro version of minisat with this small example because diff --git a/minisat/tests/phasing.rs b/minisat/tests/phasing.rs index a58eda45..ec89d6b5 100644 --- a/minisat/tests/phasing.rs +++ b/minisat/tests/phasing.rs @@ -1,38 +1,7 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - lit, - solvers::{PhaseLit, Solve, SolverResult}, - types::TernaryVal, - var, -}; -use rustsat_minisat::{core, simp}; - -fn test_phase_saving(mut solver: S) { - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - solver.phase_lit(lit![0]).unwrap(); - solver.phase_lit(!lit![1]).unwrap(); - solver.phase_lit(lit![2]).unwrap(); - solver.phase_lit(!lit![3]).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); - let sol = solver.solution(var![3]).unwrap(); - assert_eq!(sol.lit_value(lit![0]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![1]), TernaryVal::False); - assert_eq!(sol.lit_value(lit![2]), TernaryVal::True); - assert_eq!(sol.lit_value(lit![3]), TernaryVal::False); - solver.unphase_var(var![1]).unwrap(); - solver.unphase_var(var![0]).unwrap(); -} -#[test] -fn core_phase_saving() { - let solver = core::Minisat::default(); - test_phase_saving(solver); +mod core { + rustsat_solvertests::phasing_tests!(rustsat_minisat::core::Minisat); } -#[test] -fn simp_phase_saving() { - let solver = simp::Minisat::default(); - test_phase_saving(solver); +mod simp { + rustsat_solvertests::phasing_tests!(rustsat_minisat::simp::Minisat); } diff --git a/minisat/tests/small.rs b/minisat/tests/small.rs index 154c2c09..fd7e83c7 100644 --- a/minisat/tests/small.rs +++ b/minisat/tests/small.rs @@ -1,71 +1,7 @@ -use rustsat::{ - instances::{BasicVarManager, SatInstance}, - solvers::{Solve, SolverResult}, -}; -use rustsat_minisat::{core, simp}; - -#[test] -fn core_small_sat() { - let mut solver = core::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); -} - -// Note: this instance seems too hard for minisat to solve -#[test] -#[ignore] -fn core_small_unsat() { - let mut solver = core::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf") - .unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -#[test] -fn core_ms_segfault() { - let mut solver = core::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); -} - -#[test] -fn simp_small_sat() { - let mut solver = simp::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Sat); -} - -// Note: this instance seems too hard for minisat to solve -#[test] -#[ignore] -fn simp_small_unsat() { - let mut solver = simp::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf") - .unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); +mod core { + rustsat_solvertests::base_tests!(rustsat_minisat::core::Minisat, false, true); } -#[test] -fn simp_ms_segfault() { - let mut solver = simp::Minisat::default(); - let inst: SatInstance = - SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); - solver.add_cnf(inst.as_cnf().0).unwrap(); - let res = solver.solve().unwrap(); - assert_eq!(res, SolverResult::Unsat); +mod simp { + rustsat_solvertests::base_tests!(rustsat_minisat::simp::Minisat, false, true); } diff --git a/release-plz.toml b/release-plz.toml index 8d4d53b1..5a6295d1 100644 --- a/release-plz.toml +++ b/release-plz.toml @@ -30,3 +30,8 @@ semver_check = true name = "rustsat-ipasir" release = false git_release_enable = false + +[[package]] +name = "rustsat-solvertests" +release = false +git_release_enable = false diff --git a/solvertests/Cargo.toml b/solvertests/Cargo.toml new file mode 100644 index 00000000..757cc950 --- /dev/null +++ b/solvertests/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "rustsat-solvertests" +description = "Test code shared between sat solver crates" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[lib] +proc-macro = true + +[dependencies] +syn = "2.0" +quote = "1.0" +rustsat = { version = "0.4.3", path = "../rustsat", default-features = false } +proc-macro2 = "1.0" diff --git a/solvertests/src/lib.rs b/solvertests/src/lib.rs new file mode 100644 index 00000000..e20b8afd --- /dev/null +++ b/solvertests/src/lib.rs @@ -0,0 +1,275 @@ +extern crate proc_macro; + +use proc_macro::TokenStream; +use quote::{quote, ToTokens}; +use syn::{ + parse::Parse, parse_macro_input, parse_quote, punctuated::Punctuated, Attribute, Expr, LitBool, + Token, Type, +}; + +enum InitBy { + Default(Type), + Expr(Expr), +} + +impl Parse for InitBy { + fn parse(input: syn::parse::ParseStream) -> syn::Result { + let typr: syn::Result = input.parse(); + Ok(if let Ok(typ) = typr { + Self::Default(typ) + } else { + Self::Expr(input.parse()?) + }) + } +} + +impl ToTokens for InitBy { + fn to_tokens(&self, tokens: &mut proc_macro2::TokenStream) { + match self { + InitBy::Default(typ) => typ.to_tokens(tokens), + InitBy::Expr(expr) => expr.to_tokens(tokens), + } + } +} + +struct MacroInput { + slv: InitBy, + bools: Vec, +} + +impl Parse for MacroInput { + fn parse(input: syn::parse::ParseStream) -> syn::Result { + let slv: InitBy = input.parse()?; + if input.is_empty() { + return Ok(Self { slv, bools: vec![] }); + } + let _: Token![,] = input.parse()?; + let bools = Punctuated::::parse_terminated(input)?; + let bools: Vec<_> = bools.into_iter().map(|lit| lit.value).collect(); + Ok(Self { slv, bools }) + } +} + +#[proc_macro] +pub fn base_tests(tokens: TokenStream) -> TokenStream { + let input = parse_macro_input!(tokens as MacroInput); + let slv = input.slv; + let ignoretok = |idx: usize| -> Option { + if input.bools.len() > idx && input.bools[idx] { + Some(parse_quote! {#[ignore]}) + } else { + None + } + }; + let mut ts = quote! { + macro_rules! test_inst { + ($slv:ty, $inst:expr, $res:expr) => {{ + let mut solver = <$slv>::default(); + let inst = rustsat::instances::SatInstance::::from_dimacs_path($inst) + .expect("failed to parse instance"); + rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0) + .expect("failed to add cnf to solver"); + let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving"); + assert_eq!(res, $res); + }}; + ($init:expr, $inst:expr, $res:expr) => {{ + let mut solver = $init; + let inst = rustsat::instances::SatInstance::::from_dimacs_path($inst) + .expect("failed to parse instance"); + rustsat::solvers::Solve::add_cnf(&mut solver, inst.as_cnf().0) + .expect("failed to add cnf to solver"); + let res = rustsat::solvers::Solve::solve(&mut solver).expect("failed solving"); + assert_eq!(res, $res); + }}; + } + }; + let ignore = ignoretok(0); + ts.extend(quote! { + #[test] + #ignore + fn small_sat() { + test_inst!(#slv, "./data/AProVE11-12.cnf", rustsat::solvers::SolverResult::Sat); + } + }); + let ignore = ignoretok(1); + ts.extend(quote! { + #[test] + #ignore + fn small_unsat() { + test_inst!(#slv, "./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf", rustsat::solvers::SolverResult::Unsat); + } + }); + let ignore = ignoretok(2); + ts.extend(quote! { + #[test] + #ignore + fn minisat_segfault() { + test_inst!(#slv, "./data/minisat-segfault.cnf", rustsat::solvers::SolverResult::Unsat); + } + }); + ts.into() +} + +#[proc_macro] +pub fn incremental_tests(tokens: TokenStream) -> TokenStream { + let input = parse_macro_input!(tokens as MacroInput); + let slv = input.slv; + let ignoretok = |idx: usize| -> Option { + if input.bools.len() > idx && input.bools[idx] { + Some(parse_quote! {#[ignore]}) + } else { + None + } + }; + let mut ts = quote! { + macro_rules! init_slv { + ($slv:ty) => { + <$slv>::default() + }; + ($init:expr) => { + $init + }; + } + }; + let ignore = ignoretok(0); + ts.extend(quote! { + #[test] + #ignore + fn assumption_sequence() { + use rustsat::{ + instances::{SatInstance}, + lit, + solvers::{Solve, SolveIncremental, SolverResult::{Sat, Unsat}}, + }; + + let mut solver = init_slv!(#slv); + let inst: SatInstance = + SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); + solver.add_cnf(inst.as_cnf().0).unwrap(); + let res = solver.solve().unwrap(); + assert_eq!(res, Sat); + let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Sat); + let res = solver + .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Sat); + let res = solver + .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Sat); + let res = solver + .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Sat); + let res = solver + .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + let res = solver + .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]]) + .unwrap(); + assert_eq!(res, Unsat); + } + }); + ts.into() +} + +#[proc_macro] +pub fn phasing_tests(tokens: TokenStream) -> TokenStream { + let input = parse_macro_input!(tokens as MacroInput); + let slv = input.slv; + let ignoretok = |idx: usize| -> Option { + if input.bools.len() > idx && input.bools[idx] { + Some(parse_quote! {#[ignore]}) + } else { + None + } + }; + let mut ts = quote! { + macro_rules! init_slv { + ($slv:ty) => { + <$slv>::default() + }; + ($init:expr) => { + $init + }; + } + }; + let ignore = ignoretok(0); + ts.extend(quote! { + #[test] + #ignore + fn assumption_sequence() { + use rustsat::{ + instances::{SatInstance}, + lit, + solvers::{PhaseLit, Solve, SolverResult::Sat}, + types::TernaryVal::{True, False}, + var, + }; + let mut solver = init_slv!(#slv); + let inst: SatInstance = + SatInstance::from_dimacs_path("./data/small.cnf").unwrap(); + solver.add_cnf(inst.as_cnf().0).unwrap(); + solver.phase_lit(lit![0]).unwrap(); + solver.phase_lit(!lit![1]).unwrap(); + solver.phase_lit(lit![2]).unwrap(); + solver.phase_lit(!lit![3]).unwrap(); + let res = solver.solve().unwrap(); + assert_eq!(res, Sat); + let sol = solver.solution(var![3]).unwrap(); + assert_eq!(sol.lit_value(lit![0]), True); + assert_eq!(sol.lit_value(lit![1]), False); + assert_eq!(sol.lit_value(lit![2]), True); + assert_eq!(sol.lit_value(lit![3]), False); + solver.unphase_var(var![1]).unwrap(); + solver.unphase_var(var![0]).unwrap(); + } + }); + ts.into() +}