sat_interface/
multisolver.rs

1// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2// SPDX-License-Identifier: Apache-2.0
3
4//! This module union multiple solvers as one solver by using these solvers in a round-robin manner.
5
6use crate::{AddConstraints, Model, SatSolver};
7
8/// treats multiple [SatSolver]s as one [SatSolver]
9pub struct MultiSolver<T> {
10    solvers: Vec<T>,
11    idx: usize,
12}
13
14impl<T> MultiSolver<T> {
15    /// rotate to the next solver
16    pub fn next(&mut self) {
17        self.idx += 1;
18        if self.idx >= self.solvers.len() {
19            self.idx = 0;
20        }
21    }
22
23    /// return a mutable slice of [SatSolver]s
24    pub fn as_mut_slice(&mut self) -> &mut [T] {
25        self.solvers.as_mut_slice()
26    }
27}
28
29impl<T> MultiSolver<T>
30where
31    T: SatSolver,
32{
33    /// n > 0
34    pub fn new_by_size(n: usize) -> Self {
35        let mut solvers = vec![];
36        for _ in 0..n {
37            solvers.push(T::new());
38        }
39        Self { solvers, idx: 0 }
40    }
41}
42
43impl<T, C> AddConstraints<C> for MultiSolver<T>
44where
45    T: AddConstraints<C>,
46{
47    fn insert(&mut self, constraints: &C) {
48        self.as_mut_slice().insert(constraints)
49    }
50}
51
52impl<T> SatSolver for MultiSolver<T>
53where
54    T: SatSolver,
55{
56    type Status = T::Status;
57
58    fn new() -> Self {
59        Self::new_by_size(1)
60    }
61
62    fn solve(&mut self) -> Self::Status {
63        self.solvers[self.idx].solve()
64    }
65
66    fn val(&mut self, lit: i32) -> bool {
67        SatSolver::val(&mut self.solvers[self.idx], lit)
68    }
69
70    fn load_model(&mut self) -> Model {
71        self.solvers[self.idx].load_model()
72    }
73
74    fn block_model(&mut self) {
75        let model = self.load_model();
76        let negated = model.negate();
77        for s in self.solvers.iter_mut() {
78            s.insert(&negated);
79        }
80    }
81}
sat_interface/multisolver.rs

sat_interface/
multisolver.rs
