|
| 1 | +mod bindings { |
| 2 | + #![allow( |
| 3 | + unused, |
| 4 | + non_upper_case_globals, |
| 5 | + non_camel_case_types, |
| 6 | + non_snake_case, |
| 7 | + )] |
| 8 | + include!("./bindings.rs"); |
| 9 | +} |
| 10 | + |
| 11 | +use crate::{ |
| 12 | + cnf::{ |
| 13 | + CNF, |
| 14 | + Lit, |
| 15 | + Var, |
| 16 | + }, |
| 17 | + solver::{ |
| 18 | + Solver, |
| 19 | + Model, |
| 20 | + }, |
| 21 | +}; |
| 22 | +use std::collections::HashMap; |
| 23 | +use super::config::Config; |
| 24 | + |
| 25 | +/// The Maplesat solver |
| 26 | +pub struct Maplesat { |
| 27 | + n_threads: u32, |
| 28 | + clause_limit: u32, |
| 29 | +} |
| 30 | + |
| 31 | +impl Maplesat { |
| 32 | + pub fn new() -> Self { |
| 33 | + Self { |
| 34 | + n_threads: 4, |
| 35 | + clause_limit: 10, |
| 36 | + } |
| 37 | + } |
| 38 | + pub fn set_n_threads(&mut self, n_threads: u32) { |
| 39 | + self.n_threads = n_threads; |
| 40 | + } |
| 41 | + pub fn set_clause_limit(&mut self, clause_limit: u32) { |
| 42 | + self.clause_limit = clause_limit; |
| 43 | + } |
| 44 | +} |
| 45 | + |
| 46 | +impl Solver for Maplesat { |
| 47 | + fn solve_with_config( |
| 48 | + &self, |
| 49 | + cnf: &CNF, |
| 50 | + config: &Config, |
| 51 | + ) -> Option<Model> { |
| 52 | + // Uses the C bindings to create a maplesat solver, |
| 53 | + // fill it with the CNF, and solve the CNF |
| 54 | + unsafe { |
| 55 | + let ptr = bindings::maplesat_new(); |
| 56 | + let mut m_vars: HashMap<Var, i32> = HashMap::new(); |
| 57 | + for clause in cnf.get_clauses() { |
| 58 | + if config.get_kill() { break; } |
| 59 | + bindings::maplesat_add_clause_begin(ptr); |
| 60 | + for lit in clause.get_lits() { |
| 61 | + let m_var = match m_vars.get(&lit.get_var()) { |
| 62 | + Some(m_var) => *m_var, |
| 63 | + None => { |
| 64 | + let m_lit = bindings::maplesat_new_lit(ptr); |
| 65 | + let m_var = bindings::maplesat_lit_to_var(m_lit); |
| 66 | + m_vars.insert(lit.get_var(), m_var); |
| 67 | + m_var |
| 68 | + }, |
| 69 | + }; |
| 70 | + let mut m_lit = bindings::maplesat_make_lit(m_var); |
| 71 | + if !lit.get_sign() { |
| 72 | + m_lit = bindings::maplesat_negate_lit(m_lit); |
| 73 | + } |
| 74 | + bindings::maplesat_add_clause_add_lit(ptr, m_lit); |
| 75 | + } |
| 76 | + if bindings::maplesat_add_clause_commit(ptr) == 0 { |
| 77 | + return None; |
| 78 | + } |
| 79 | + } |
| 80 | + let sat = if config.get_kill() { |
| 81 | + false |
| 82 | + } else { |
| 83 | + bindings::maplesat_solve(ptr) != 0 |
| 84 | + }; |
| 85 | + let model = if sat { |
| 86 | + let mut model = Model::new(); |
| 87 | + for (var, m_var) in m_vars { |
| 88 | + let lbool = bindings::maplesat_model_value_var( |
| 89 | + ptr, |
| 90 | + m_var, |
| 91 | + ); |
| 92 | + if lbool == bindings::maplesat_ltrue { |
| 93 | + model.add(Lit::pos(var)); |
| 94 | + } else if lbool == bindings::maplesat_lfalse { |
| 95 | + model.add(Lit::neg(var)); |
| 96 | + } else { |
| 97 | + unreachable!() |
| 98 | + } |
| 99 | + } |
| 100 | + Some(model) |
| 101 | + } else { |
| 102 | + None |
| 103 | + }; |
| 104 | + bindings::maplesat_delete(ptr); |
| 105 | + model |
| 106 | + } |
| 107 | + } |
| 108 | +} |
0 commit comments