semitone 0.0.13

SeMiTONE is a Satisfiability Modulo TheOries NEtwork, allowing the creation of variables and constraints in different underlying theories.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

use crate::{rational::InfRational, sat_solver::Lit};
use std::collections::HashMap;

pub struct ProxyRegistry {
    pub proxy_to_constraint: HashMap<Lit, TheoryConstraint>,
    pub constraint_to_proxy: HashMap<TheoryConstraint, Lit>,
}

impl ProxyRegistry {
    pub fn new() -> Self {
        Self { proxy_to_constraint: HashMap::new(), constraint_to_proxy: HashMap::new() }
    }

    pub fn get_proxy(&self, constraint: &TheoryConstraint) -> Option<&Lit> {
        self.constraint_to_proxy.get(constraint)
    }

    pub fn get_constraint(&self, lit: Lit) -> Option<&TheoryConstraint> {
        self.proxy_to_constraint.get(&lit)
    }

    pub fn register(&mut self, constraint: TheoryConstraint, lit: Lit) {
        self.proxy_to_constraint.insert(lit, constraint.clone());
        self.constraint_to_proxy.insert(constraint, lit);
    }
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub(super) enum TheoryConstraint {
    LraLb(usize, InfRational),
    LraUb(usize, InfRational),
    EnumEq(usize, i32),
}