maxpre/
sat.rs

1//! # Interface for Preprocessing [`rustsat::instances::SatInstance`] types
2
3use rustsat::{
4    encodings::{card, pb},
5    instances::{Cnf, ManageVars, SatInstance},
6    types::{
7        constraints::{CardConstraint, PbConstraint},
8        Clause,
9    },
10};
11
12use crate::PreproClauses;
13
14pub trait PreproSat: PreproClauses {
15    /// Initializes a new preprocessor from a [`SatInstance`] where the instance
16    /// is converted to [`CNF`] with the given encoders.
17    fn new_with_encoders<VM, CardEnc, PBEnc>(
18        inst: SatInstance<VM>,
19        card_encoder: CardEnc,
20        pb_encoder: PBEnc,
21        inprocessing: bool,
22    ) -> Self
23    where
24        VM: ManageVars,
25        CardEnc: FnMut(CardConstraint, &mut Cnf, &mut dyn ManageVars),
26        PBEnc: FnMut(PbConstraint, &mut Cnf, &mut dyn ManageVars),
27        Self: Sized,
28    {
29        let (cnf, _) = inst.into_cnf_with_encoders(card_encoder, pb_encoder);
30        <Self as PreproClauses>::new::<Vec<(Clause, usize)>>(cnf, vec![], inprocessing)
31    }
32    /// Initializes a new preprocessor from a [`SatInstance`]
33    fn new<VM>(inst: SatInstance<VM>, inprocessing: bool) -> Self
34    where
35        VM: ManageVars,
36        Self: Sized,
37    {
38        Self::new_with_encoders(
39            inst,
40            |constr, cnf, vm| {
41                card::default_encode_cardinality_constraint(constr, cnf, vm)
42                    .expect("cardinality encoding ran out of memory")
43            },
44            |constr, cnf, vm| {
45                pb::default_encode_pb_constraint(constr, cnf, vm)
46                    .expect("pb encoding ran out of memory")
47            },
48            inprocessing,
49        )
50    }
51    /// Gets the preprocessed instance as a [`SatInstance`]
52    fn prepro_instance(&mut self) -> SatInstance {
53        let (cnf, objs) = <Self as PreproClauses>::prepro_instance(self);
54        debug_assert!(objs.is_empty());
55        SatInstance::from(cnf)
56    }
57}
58
59impl<PP: PreproClauses> PreproSat for PP {}
maxpre/sat.rs

maxpre/
sat.rs
