Solving MAXSAT and saying a few words about it.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

172 lines
5.0 KiB

// vim: ts=4 sw=4 et
use crate::clause::Literal;
use crate::karmarkar;
use colored::{control::ShouldColorize, Colorize};
use core::fmt::{Display, Formatter};
use core::hash::{Hash, Hasher};
use std::cell::RefCell;
use std::rc::Rc;
#[derive(Debug, Clone)]
struct VariableInner<T> {
name: String,
assignment: RefCell<Option<T>>,
}
/// A variable, with a name and an assignment. Cloning a variable preserves a reference to its
/// assignment, so changing the assignment on one instance changes it in theh others.
#[derive(Clone)]
pub struct Variable<T>(Rc<VariableInner<T>>);
impl<T> Variable<T> {
/// Creates a new variable with no assignment.
pub fn from_name(name: String) -> Variable<T> {
Variable(Rc::new(VariableInner {
name,
assignment: RefCell::new(None),
}))
}
/// Returns the name of a variable.
pub fn get_name(&self) -> &String {
&self.0.name
}
/// Sets the assignment of a variable to the value given.
pub fn assign(&self, v: T) {
*self.0.assignment.borrow_mut() = Some(v);
}
/// Removes the assignment from the variable.
pub fn unassign(&self) {
*self.0.assignment.borrow_mut() = None;
}
/// Returns a raw pointer pointing to the inner struct. This should only be used for
/// comparison.
pub fn get_ptr(&self) -> *const () {
&*self.0 as *const _ as *const ()
}
}
impl<T> Variable<T>
where
T: Clone,
{
/// Returns the variable's assignment, or `None` if there isn't one.
pub fn get_assignment(&self) -> Option<T> {
self.0.assignment.borrow().clone()
}
/// Duplicates this variable. This is like `clone()`, but the assignment of the new variable no
/// longer shares a reference with this one.
pub fn duplicate(&self) -> Variable<T> {
Variable(Rc::new((*self.0).clone()))
}
}
/// The specific case for Boolean variables.
impl Variable<bool> {
/// Creates a literal from this variable. It is a negative literal iff `neg` is `true`.
pub fn get_literal(&self, neg: bool) -> Literal {
Literal::from_var(self.clone(), neg)
}
/// Creates a positive literal from this variable.
pub fn get_pos_literal(&self) -> Literal {
self.get_literal(false)
}
/// Creates a negative literal from this variable.
pub fn get_neg_literal(&self) -> Literal {
self.get_literal(true)
}
/// Utility function for getting a string representing the variable without colorizing it.
pub fn get_uncolored_string(&self) -> String {
let should_color = ShouldColorize::from_env().should_colorize();
macro_rules! cd {
($($s:literal)?) => {
if should_color {
format!("{}", self.0.name)
} else {
format!(concat!($($s, )?"{}"), self.0.name)
}
}
}
match self.get_assignment() {
None => cd!(),
Some(true) => cd!("¹"),
Some(false) => cd!("⁰"),
}
}
}
impl<T> PartialEq for Variable<T> {
fn eq(&self, other: &Self) -> bool {
Rc::ptr_eq(&self.0, &other.0)
}
}
impl<T> Eq for Variable<T> {}
/// Note that hashes will be equal for two variables when one is a clone of the other.
impl<T> Hash for Variable<T> {
fn hash<H: Hasher>(&self, state: &mut H) {
(&*self.0 as *const _ as *const ()).hash(state);
}
}
impl Display for Variable<bool> {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
let should_color = ShouldColorize::from_env().should_colorize();
macro_rules! cd {
($($s:literal)?$(, $col:ident)?) => {
if should_color {
write!(fmt, "{}", self.0.name$(.$col())?)
} else {
write!(fmt, concat!($($s, )?"{}"), self.0.name)
}
}
}
match self.get_assignment() {
None => cd!(),
Some(true) => cd!("¹", bright_blue),
Some(false) => cd!("⁰", bright_red),
}
}
}
// RIP specialized debug info, it ICEs in 1.42.0-nightly
/*default*/
impl<T: core::fmt::Debug + Clone> core::fmt::Debug for Variable<T> {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
match self.get_assignment() {
Some(val) => write!(fmt, "{}<{:?}>", self.0.name, val),
None => write!(fmt, "{}", self.0.name),
}
}
}
impl core::ops::Mul<karmarkar::Fl> for &Variable<karmarkar::Fl> {
type Output = karmarkar::Term;
fn mul(self, coeff: karmarkar::Fl) -> Self::Output {
karmarkar::Term::from_var(self.clone(), coeff)
}
}
impl core::ops::Neg for &Variable<karmarkar::Fl> {
type Output = karmarkar::Term;
fn neg(self) -> Self::Output {
karmarkar::Term::from_var(self.clone(), -1.0)
}
}
//impl core::fmt::Debug for Variable<bool> {
// fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
// <Self as core::fmt::Display>::fmt(self, fmt)
// }
//}