1pub mod craig;
2pub mod itp;
3pub mod tracer;
4
5use giputils::hash::GHashMap;
6use logicrs::{Lit, LitVec, Var, satif::Satif};
7use std::ffi::{c_int, c_void};
8
9unsafe extern "C" {
10 fn cadical_solver_new() -> *mut c_void;
11 fn cadical_solver_free(s: *mut c_void);
12 fn cadical_solver_add_clause(s: *mut c_void, clause: *mut c_int, len: c_int);
13 fn cadical_solver_solve(s: *mut c_void, assumps: *mut c_int, len: c_int) -> c_int;
14 fn cadical_solver_constrain(s: *mut c_void, constrain: *mut c_int, len: c_int);
15 fn cadical_solver_simplify(s: *mut c_void) -> c_int;
16 fn cadical_solver_freeze(s: *mut c_void, lit: c_int);
17 fn cadical_set_polarity(s: *mut c_void, lit: c_int);
18 fn cadical_unset_polarity(s: *mut c_void, lit: c_int);
19 fn cadical_solver_model_value(s: *mut c_void, lit: c_int) -> c_int;
20 fn cadical_solver_conflict_has(s: *mut c_void, lit: c_int) -> bool;
21 fn cadical_solver_clauses(s: *mut c_void, len: *mut c_int) -> *mut c_void;
22 fn cadical_set_seed(s: *mut c_void, seed: c_int);
23}
24
25fn lit_to_cadical_lit(lit: &Lit) -> i32 {
26 let mut res = Into::<usize>::into(lit.var()) as i32 + 1;
27 if !lit.polarity() {
28 res = -res;
29 }
30 res
31}
32
33fn cadical_lit_to_lit(lit: i32) -> Lit {
34 let p = lit > 0;
35 let v = Var::new(lit.unsigned_abs() as usize - 1);
36 Lit::new(v, p)
37}
38
39pub struct Solver {
40 solver: *mut c_void,
41 num_var: usize,
42 tracer_map: GHashMap<*const c_void, *const c_void>,
43}
44
45impl Solver {
46 pub fn new() -> Self {
47 Self {
48 solver: unsafe { cadical_solver_new() },
49 num_var: 0,
50 tracer_map: GHashMap::default(),
51 }
52 }
53}
54
55impl Satif for Solver {
56 #[inline]
57 fn new_var(&mut self) -> Var {
58 self.num_var += 1;
59 Var::new(self.num_var - 1)
60 }
61
62 #[inline]
63 fn num_var(&self) -> usize {
64 self.num_var
65 }
66
67 #[inline]
68 fn add_clause(&mut self, clause: &[Lit]) {
69 let clause: Vec<i32> = clause.iter().map(lit_to_cadical_lit).collect();
70 unsafe { cadical_solver_add_clause(self.solver, clause.as_ptr() as _, clause.len() as _) }
71 }
72
73 fn solve(&mut self, assumps: &[Lit]) -> bool {
74 let assumps: Vec<i32> = assumps.iter().map(lit_to_cadical_lit).collect();
75 match unsafe {
76 cadical_solver_solve(self.solver, assumps.as_ptr() as _, assumps.len() as _)
77 } {
78 10 => true,
79 20 => false,
80 _ => todo!(),
81 }
82 }
83
84 fn sat_value(&self, lit: Lit) -> Option<bool> {
85 let lit = lit_to_cadical_lit(&lit);
86 let res = unsafe { cadical_solver_model_value(self.solver, lit) };
87 if res == lit {
88 Some(true)
89 } else if res == -lit {
90 Some(false)
91 } else {
92 None
93 }
94 }
95
96 fn unsat_has(&self, lit: Lit) -> bool {
97 let lit = lit_to_cadical_lit(&lit);
98 unsafe { cadical_solver_conflict_has(self.solver, lit) }
99 }
100
101 fn simplify(&mut self) -> Option<bool> {
102 match unsafe { cadical_solver_simplify(self.solver) } {
103 10 => Some(true),
104 20 => Some(false),
105 _ => None,
106 }
107 }
108
109 fn set_frozen(&mut self, var: Var, frozen: bool) {
110 assert!(frozen);
111 unsafe { cadical_solver_freeze(self.solver, lit_to_cadical_lit(&var.lit())) }
112 }
113
114 fn clauses(&self) -> Vec<LitVec> {
115 let mut cnf = Vec::new();
116 unsafe {
117 let mut len = 0;
118 let clauses: *mut usize = cadical_solver_clauses(self.solver, &mut len as *mut _) as _;
119 if len > 0 {
120 let clauses = Vec::from_raw_parts(clauses, len as _, len as _);
121 for i in (0..clauses.len()).step_by(2) {
122 let data = clauses[i] as *mut i32;
123 let len = clauses[i + 1];
124 let cls: Vec<_> = (0..len).map(|i| *data.add(i)).collect();
125 cnf.push(LitVec::from_iter(cls.into_iter().map(cadical_lit_to_lit)));
126 }
127 }
128 }
129 cnf
130 }
131
132 fn set_seed(&mut self, seed: u64) {
133 unsafe { cadical_set_seed(self.solver, seed as _) }
134 }
135}
136
137impl Solver {
138 pub fn solve_with_constrain(&mut self, assumps: &[Lit], constrain: &[Lit]) -> bool {
139 let constrain: Vec<i32> = constrain.iter().map(lit_to_cadical_lit).collect();
140 unsafe {
141 cadical_solver_constrain(self.solver, constrain.as_ptr() as _, constrain.len() as _)
142 };
143 self.solve(assumps)
144 }
145
146 pub fn set_polarity(&mut self, var: Var, pol: Option<bool>) {
147 match pol {
148 Some(p) => {
149 let p = var.lit().not_if(!p);
150 unsafe { cadical_set_polarity(self.solver, lit_to_cadical_lit(&p)) }
151 }
152 None => unsafe { cadical_unset_polarity(self.solver, lit_to_cadical_lit(&var.lit())) },
153 };
154 }
155}
156
157impl Drop for Solver {
158 fn drop(&mut self) {
159 unsafe { cadical_solver_free(self.solver) };
160 }
161}
162
163impl Default for Solver {
164 fn default() -> Self {
165 Self::new()
166 }
167}
168
169#[test]
170fn test() {
171 use logicrs::LitVec;
172 let mut solver = Solver::new();
173 let lit0: Lit = solver.new_var().into();
174 let lit1: Lit = solver.new_var().into();
175 let lit2: Lit = solver.new_var().into();
176 solver.add_clause(&LitVec::from([lit0, !lit2]));
177 solver.add_clause(&LitVec::from([lit1, !lit2]));
178 solver.add_clause(&LitVec::from([!lit0, !lit1, lit2]));
179 if solver.solve(&[lit2]) {
180 assert!(solver.sat_value(lit0).unwrap());
181 assert!(solver.sat_value(lit1).unwrap());
182 assert!(solver.sat_value(lit2).unwrap());
183 } else {
184 panic!()
185 }
186 }