Browse Source

Generalized variables beyond booleans

karmarkar
Thomas Johnson 3 years ago
parent
commit
dbe84af033
  1. 1
      Cargo.toml
  2. 134
      src/clause.rs
  3. 9
      src/main.rs
  4. 155
      src/variable.rs

1
Cargo.toml

@ -8,3 +8,4 @@ edition = "2018"
[dependencies]
colored = "1.9.3"
nalgebra = "0.21.0"

134
src/clause.rs

@ -2,135 +2,10 @@
use colored::{control::ShouldColorize, Colorize};
use core::fmt::{Display, Formatter};
use core::hash::{Hash, Hasher};
use std::cell::RefCell;
use std::collections::hash_map::HashMap;
use std::collections::hash_set::HashSet;
use std::rc::Rc;
#[derive(Debug, Clone)]
struct VariableInner {
name: String,
assignment: RefCell<Option<bool>>,
}
/// 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(Rc<VariableInner>);
impl Variable {
/// Creates a new variable with no assignment.
pub fn from_name(name: String) -> Variable {
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: bool) {
*self.0.assignment.borrow_mut() = Some(v);
}
/// Removes the assignment from the variable.
pub fn unassign(&self) {
*self.0.assignment.borrow_mut() = None;
}
/// Returns the variable's assignment, or `None` if there isn't one.
pub fn get_assignment(&self) -> Option<bool> {
self.0.assignment.borrow().clone()
}
/// Creates a literal from this variable. It is a negative literal iff `neg` is `true`.
pub fn get_literal(&self, neg: bool) -> Literal {
Literal {
neg,
var: self.clone(),
}
}
/// 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)
}
/// 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 {
Variable(Rc::new((*self.0).clone()))
}
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 PartialEq for Variable {
fn eq(&self, other: &Self) -> bool {
Rc::ptr_eq(&self.0, &other.0)
}
}
impl Eq for Variable {}
/// Note that hashes will be equal for two variables when one is a clone of the other.
impl Hash for Variable {
fn hash<H: Hasher>(&self, state: &mut H) {
(&*self.0 as *const _ as *const ()).hash(state);
}
}
impl Display for Variable {
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),
}
}
}
impl core::fmt::Debug for Variable {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
<Self as core::fmt::Display>::fmt(self, fmt)
}
}
pub type Variable = crate::variable::Variable<bool>;
/// A literal -- that is, an expression which is either a variable or the negation of a variable.
#[derive(Clone, Debug)]
@ -140,6 +15,11 @@ pub struct Literal {
}
impl Literal {
/// Constructs a literal from a variable.
pub fn from_var(var: Variable, neg: bool) -> Literal {
Literal { neg, var }
}
/// Assign a value to the literal. Note that if the literal is negated, the assignment to the
/// underlying variable is also negated.
pub fn assign(&self, v: bool) {
@ -346,7 +226,7 @@ impl Clone for ClauseList {
for clause in self.iter() {
let mut newclause = Clause::new();
for lit in clause.iter() {
let key = &*lit.get_variable().0 as *const _ as *const ();
let key = lit.get_variable().get_ptr();
if map.contains_key(&key) {
newclause.push(map.get(&key).unwrap().get_literal(lit.is_neg()));
} else {

9
src/main.rs

@ -1,8 +1,15 @@
// vim: ts=4 sw=4 et
#![feature(specialization)]
#![feature(non_ascii_idents)]
#[macro_use]
/// Useful for disjunctive clauses and variables.
/// Useful for disjunctive clauses.
pub mod clause;
/// Variables -- both boolean, and otherwise.
pub mod variable;
/// Affine scaling, linear systems and inequalities, etc.
pub mod affine_scaling;
/// I made this before I knew I didn't need it. :/
pub mod hash_wrapper;
mod messy_minsat;

155
src/variable.rs

@ -0,0 +1,155 @@
// vim: ts=4 sw=4 et
use crate::clause::Literal;
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::fmt::Debug for Variable<bool> {
// fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
// <Self as core::fmt::Display>::fmt(self, fmt)
// }
//}
Loading…
Cancel
Save