maxpre/
base.rs

1//! # Base MaxPre Interface
2//!
3//! The low-abstraction MaxPre interface working on hard and soft clauses.
4
5use core::ffi::{c_int, c_uint, CStr};
6use std::ffi::CString;
7
8use cpu_time::ProcessTime;
9use rustsat::{
10    instances::Cnf,
11    types::{Assignment, Clause, Lit, Var, WClsIter},
12};
13
14use crate::Error;
15
16use super::{ffi, Options, PreproClauses, Stats};
17
18/// The main low-abstraction preprocessor type
19pub struct MaxPre {
20    /// The handle for the C API
21    handle: *mut ffi::CMaxPre,
22    /// Offsets of the objectives
23    offsets: Vec<isize>,
24    /// Statistics of the preprocessor
25    stats: Stats,
26}
27
28impl PreproClauses for MaxPre {
29    fn signature() -> &'static str {
30        let c_chars = unsafe { ffi::cmaxpre_signature() };
31        let c_str = unsafe { CStr::from_ptr(c_chars) };
32        c_str
33            .to_str()
34            .expect("MaxPre signature returned invalid UTF-8")
35    }
36
37    fn new<CI: WClsIter>(hards: Cnf, softs: Vec<(CI, isize)>, inprocessing: bool) -> Self {
38        let mut top = 1;
39        let softs: Vec<(Vec<(Clause, usize)>, isize)> = softs
40            .into_iter()
41            .map(|(cls, ofs)| (cls.into_iter().collect(), ofs))
42            .collect();
43        top = softs.iter().fold(top, |top, softs| {
44            softs.0.iter().fold(top, |top, (_, w)| top + w)
45        });
46        let mut stats = Stats {
47            n_objs: softs.len(),
48            n_orig_hard_clauses: hards.len(),
49            ..Default::default()
50        };
51        let handle = unsafe { ffi::cmaxpre_init_start(top as u64, ffi::map_bool(inprocessing)) };
52        hards.into_iter().for_each(|cl| {
53            cl.into_iter().for_each(|l| {
54                stats.max_orig_var = Self::track_max_var(stats.max_orig_var, l.var());
55                unsafe { ffi::cmaxpre_init_add_lit(handle, l.to_ipasir()) }
56            });
57            unsafe { ffi::cmaxpre_init_add_lit(handle, 0) };
58        });
59        let mut offsets = Vec::new();
60        softs.into_iter().enumerate().for_each(|(idx, softs)| {
61            offsets.push(softs.1);
62            stats.n_orig_soft_clauses.push(softs.0.len());
63            softs.0.into_iter().for_each(|(cl, w)| {
64                // Add zero weight for all previous objectives
65                (0..idx).for_each(|_| unsafe { ffi::cmaxpre_init_add_weight(handle, 0) });
66                // Add weight for the objective with index
67                unsafe { ffi::cmaxpre_init_add_weight(handle, w as u64) };
68                // Add literals
69                cl.into_iter().for_each(|l| {
70                    stats.max_orig_var = Self::track_max_var(stats.max_orig_var, l.var());
71                    unsafe { ffi::cmaxpre_init_add_lit(handle, l.to_ipasir()) }
72                });
73                unsafe { ffi::cmaxpre_init_add_lit(handle, 0) };
74            })
75        });
76        unsafe { ffi::cmaxpre_init_finalize(handle) };
77        Self {
78            handle,
79            offsets,
80            stats,
81        }
82    }
83
84    fn preprocess(&mut self, techniques: &str, log_level: c_int, time_limit: f64) {
85        let start = ProcessTime::now();
86        let techniques = CString::new(techniques).unwrap();
87        unsafe {
88            ffi::cmaxpre_preprocess(
89                self.handle,
90                techniques.as_ptr(),
91                log_level,
92                time_limit,
93                ffi::FALSE,
94                ffi::FALSE,
95            )
96        };
97        self.stats.prepro_time += start.elapsed();
98    }
99
100    fn top_weight(&self) -> u64 {
101        unsafe { ffi::cmaxpre_get_top_weight(self.handle) }
102    }
103
104    fn n_prepro_clauses(&self) -> c_uint {
105        unsafe { ffi::cmaxpre_get_n_prepro_clauses(self.handle) }
106    }
107
108    fn n_prepro_labels(&self) -> c_uint {
109        unsafe { ffi::cmaxpre_get_n_prepro_labels(self.handle) }
110    }
111
112    fn n_prepro_fixed_lits(&self) -> c_uint {
113        unsafe { ffi::cmaxpre_get_n_prepro_fixed(self.handle) }
114    }
115
116    fn prepro_instance(&mut self) -> (Cnf, Vec<(Vec<(Clause, usize)>, isize)>) {
117        let n_cls = self.n_prepro_clauses();
118        let top = self.top_weight();
119        let mut hards = Cnf::new();
120        let mut softs: Vec<Vec<(Clause, usize)>> = vec![Default::default(); self.stats.n_objs];
121        for cl_idx in 0..n_cls {
122            // Get clause
123            let mut clause = Clause::new();
124            let mut lit_idx = 0;
125            loop {
126                let lit = unsafe { ffi::cmaxpre_get_prepro_lit(self.handle, cl_idx, lit_idx) };
127                if lit == 0 {
128                    break;
129                }
130                let lit = Lit::from_ipasir(lit).unwrap();
131                self.stats.max_prepro_var =
132                    Self::track_max_var(self.stats.max_prepro_var, lit.var());
133                clause.add(lit);
134                lit_idx += 1;
135            }
136            // Get weights
137            let mut is_hard = true;
138            for obj_idx in 0..self.stats.n_objs {
139                let w = unsafe {
140                    ffi::cmaxpre_get_prepro_weight(self.handle, cl_idx, obj_idx as c_uint)
141                };
142                if w == 0 {
143                    continue;
144                }
145                if w != top {
146                    // Soft clause
147                    if softs.len() < obj_idx + 1 {
148                        softs.resize(obj_idx + 1, Default::default());
149                    }
150                    softs[obj_idx].push((clause.clone(), w as usize));
151                    is_hard = false;
152                }
153            }
154            if is_hard {
155                // Hard clause
156                hards.add_clause(clause);
157            }
158        }
159        self.stats.n_prepro_hard_clauses = hards.len();
160        self.stats.n_prepro_soft_clauses = softs.iter().map(|s| s.len()).collect();
161        self.stats.removed_weight.clear();
162        let softs = softs
163            .into_iter()
164            .enumerate()
165            .map(|(idx, s)| {
166                let rem_weight =
167                    unsafe { ffi::cmaxpre_get_removed_weight(self.handle, idx as c_uint) } as usize;
168                self.stats.removed_weight.push(rem_weight);
169                let offset = rem_weight as isize + self.offsets[idx];
170                (s, offset)
171            })
172            .collect();
173        (hards, softs)
174    }
175
176    fn prepro_labels(&self) -> Vec<Lit> {
177        let n_lbls = self.n_prepro_labels();
178        let mut lbls = Vec::new();
179        for lbl_idx in 0..n_lbls {
180            lbls.push(
181                Lit::from_ipasir(unsafe { ffi::cmaxpre_get_prepro_label(self.handle, lbl_idx) })
182                    .unwrap(),
183            );
184        }
185        lbls
186    }
187
188    fn prepro_fixed_lits(&self) -> Vec<Lit> {
189        let n_fixed = self.n_prepro_fixed_lits();
190        let mut fixed = Vec::new();
191        for fixed_idx in 0..n_fixed {
192            fixed.push(
193                Lit::from_ipasir(unsafe {
194                    ffi::cmaxpre_get_prepro_fixed_lit(self.handle, fixed_idx)
195                })
196                .unwrap(),
197            );
198        }
199        fixed
200    }
201
202    fn max_orig_var(&self) -> Var {
203        Lit::from_ipasir(unsafe { ffi::cmaxpre_get_original_variables(self.handle) })
204            .unwrap()
205            .var()
206    }
207
208    fn upper_bound(&self) -> u64 {
209        unsafe { ffi::cmaxpre_get_upper_bound(self.handle) }
210    }
211
212    fn reconstruct(&mut self, sol: Assignment) -> Assignment {
213        let start = ProcessTime::now();
214        sol.into_iter()
215            .for_each(|l| unsafe { ffi::cmaxpre_assignment_add(self.handle, l.to_ipasir()) });
216        unsafe { ffi::cmaxpre_reconstruct(self.handle) };
217        let max_var = self.max_orig_var();
218        let rec = (1..max_var.pos_lit().to_ipasir() + 1)
219            .map(|l| {
220                if unsafe { ffi::cmaxpre_reconstructed_val(self.handle, l) } > 0 {
221                    Lit::from_ipasir(l).unwrap()
222                } else {
223                    Lit::from_ipasir(-l).unwrap()
224                }
225            })
226            .collect();
227        self.stats.reconst_time += start.elapsed();
228        rec
229    }
230
231    fn add_var(&mut self) -> Result<Var, Error> {
232        let v = unsafe { ffi::cmaxpre_add_var(self.handle, 0) };
233        if v == 0 {
234            return Err(Error::Generic);
235        }
236        Ok(Lit::from_ipasir(v).unwrap().var())
237    }
238
239    fn add_clause(&mut self, clause: Clause) -> Result<(), Error> {
240        clause.into_iter().for_each(|l| unsafe {
241            ffi::cmaxpre_add_lit(self.handle, l.to_ipasir());
242        });
243        if unsafe { ffi::cmaxpre_add_lit(self.handle, 0) } == ffi::FALSE {
244            return Err(Error::Generic);
245        }
246        Ok(())
247    }
248
249    fn add_label(&mut self, label: Lit, weight: usize) -> Result<Lit, Error> {
250        let l = unsafe { ffi::cmaxpre_add_label(self.handle, label.to_ipasir(), weight as u64) };
251        if l == 0 {
252            return Err(Error::Generic);
253        }
254        Ok(Lit::from_ipasir(l).unwrap())
255    }
256
257    fn alter_weight(&mut self, label: Lit, weight: usize) -> Result<(), Error> {
258        if unsafe { ffi::cmaxpre_alter_weight(self.handle, label.to_ipasir(), weight as u64) }
259            == ffi::FALSE
260        {
261            return Err(Error::Generic);
262        }
263        Ok(())
264    }
265
266    fn label_to_var(&mut self, label: Lit) -> Result<(), Error> {
267        if unsafe { ffi::cmaxpre_label_to_var(self.handle, label.to_ipasir()) } == ffi::FALSE {
268            return Err(Error::Generic);
269        }
270        Ok(())
271    }
272
273    fn reset_removed_weight(&mut self) -> Result<(), Error> {
274        if unsafe { ffi::cmaxpre_reset_removed_weight(self.handle) } == ffi::FALSE {
275            return Err(Error::Generic);
276        }
277        Ok(())
278    }
279
280    fn removed_weight(&mut self) -> Vec<usize> {
281        self.stats.removed_weight = (0..self.stats.n_objs)
282            .map(|obj_idx| unsafe {
283                ffi::cmaxpre_get_removed_weight(self.handle, obj_idx as c_uint)
284            } as usize)
285            .collect();
286        self.stats.removed_weight.clone()
287    }
288
289    fn set_options(&mut self, opts: Options) {
290        if let Some(val) = opts.bve_sort_max_first {
291            unsafe { ffi::cmaxpre_set_bve_gate_extraction(self.handle, ffi::map_bool(val)) };
292        }
293        if let Some(val) = opts.label_matching {
294            unsafe { ffi::cmaxpre_set_label_matching(self.handle, ffi::map_bool(val)) };
295        }
296        if let Some(val) = opts.skip_technique {
297            unsafe { ffi::cmaxpre_set_skip_technique(self.handle, val) };
298        }
299        if let Some(val) = opts.bve_sort_max_first {
300            unsafe { ffi::cmaxpre_set_bve_sort_max_first(self.handle, ffi::map_bool(val)) };
301        }
302        if let Some(val) = opts.bve_local_grow_limit {
303            unsafe { ffi::cmaxpre_set_bve_local_grow_limit(self.handle, val) };
304        }
305        if let Some(val) = opts.bve_global_grow_limit {
306            unsafe { ffi::cmaxpre_set_bve_global_grow_limit(self.handle, val) };
307        }
308        if let Some(val) = opts.max_bbtms_vars {
309            unsafe { ffi::cmaxpre_set_max_bbtms_vars(self.handle, val) };
310        }
311        if let Some(val) = opts.harden_in_model_search {
312            unsafe { ffi::cmaxpre_set_harden_in_model_search(self.handle, ffi::map_bool(val)) };
313        }
314        if let Some(val) = opts.model_search_iter_limits {
315            unsafe { ffi::cmaxpre_set_model_search_iter_limit(self.handle, val) };
316        }
317    }
318
319    fn print_instance(&self) {
320        unsafe { ffi::cmaxpre_print_instance_stdout(self.handle) }
321    }
322
323    fn print_solution(&self, sol: Assignment, weight: usize) {
324        sol.into_iter()
325            .for_each(|l| unsafe { ffi::cmaxpre_assignment_add(self.handle, l.to_ipasir()) });
326        unsafe { ffi::cmaxpre_print_solution_stdout(self.handle, weight as u64) }
327    }
328
329    fn print_map(&self) {
330        unsafe { ffi::cmaxpre_print_map_stdout(self.handle) }
331    }
332
333    fn print_technique_log(&self) {
334        unsafe { ffi::cmaxpre_print_technique_log_stdout(self.handle) }
335    }
336
337    fn print_info_log(&self) {
338        unsafe { ffi::cmaxpre_print_info_log_stdout(self.handle) }
339    }
340
341    fn print_stats(&self) {
342        unsafe { ffi::cmaxpre_print_preprocessor_stats_stdout(self.handle) }
343    }
344
345    fn stats(&self) -> Stats {
346        self.stats.clone()
347    }
348}
349
350impl MaxPre {
351    /// Tracks a maximum variable
352    fn track_max_var(max_var: Option<Var>, new_var: Var) -> Option<Var> {
353        match max_var {
354            Some(max_var) => {
355                if new_var > max_var {
356                    Some(new_var)
357                } else {
358                    Some(max_var)
359                }
360            }
361            None => Some(new_var),
362        }
363    }
364}
365
366impl Drop for MaxPre {
367    fn drop(&mut self) {
368        unsafe { ffi::cmaxpre_release(self.handle) }
369    }
370}
371
372#[cfg(test)]
373mod tests {
374    use rustsat::{instances::Cnf, lit, types::Clause};
375
376    use crate::PreproClauses;
377
378    use super::MaxPre;
379
380    #[test]
381    fn construct() {
382        let mut cnf = Cnf::new();
383        cnf.add_binary(lit![0], lit![2]);
384        MaxPre::new::<Vec<(Clause, usize)>>(cnf, vec![], true);
385    }
386}
maxpre/base.rs

maxpre/
base.rs
