Browse Source

Merge remote-tracking branch 'origin' into bfs

clause_generator
Cameron Weinfurt 3 years ago
parent
commit
dd27e5c6dc
  1. 48
      src/clause.rs
  2. 2
      src/main.rs
  3. 7
      src/messy_minsat.rs

48
src/clause.rs

@ -14,10 +14,13 @@ struct VariableInner {
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,
@ -25,22 +28,27 @@ impl Variable {
}))
}
/// 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,
@ -48,14 +56,18 @@ impl Variable {
}
}
/// 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()))
}
@ -87,6 +99,7 @@ impl PartialEq for Variable {
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);
@ -119,6 +132,7 @@ impl core::fmt::Debug for Variable {
}
}
/// A literal -- that is, an expression which is either a variable or the negation of a variable.
#[derive(Clone, Debug)]
pub struct Literal {
neg: bool,
@ -126,22 +140,29 @@ pub struct Literal {
}
impl Literal {
/// 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) {
self.var.assign(v ^ self.neg);
}
/// Removes the assignment from the underlying variable.
pub fn unassign(&self) {
self.var.unassign();
}
/// Gets the assignment of the literal. This evaluates the literal based on the assignment to
/// the underlying variable.
pub fn get_assignment(&self) -> Option<bool> {
self.var.get_assignment().map(|x| x ^ self.neg)
}
/// Returns a clone of the underlying variable.
pub fn get_variable(&self) -> Variable {
self.var.clone()
}
/// Returns `true` iff the literal is a negation of the underlying variable.
pub fn is_neg(&self) -> bool {
self.neg
}
@ -178,38 +199,47 @@ impl Display for Literal {
}
}
/// A disjunctive clause of literals.
#[derive(Clone, Debug)]
pub struct Clause {
literals: Vec<Literal>,
}
impl Clause {
/// Creates a new empty clause.
pub fn new() -> Clause {
Clause {
literals: Vec::new(),
}
}
/// Disjoins (ORs) a literal with the clause.
pub fn push(&mut self, l: Literal) {
self.literals.push(l);
}
/// Returns the number of literals in the clause.
pub fn len(&self) -> usize {
self.literals.len()
}
/// Returns an iterator through all the literals in the clause.
pub fn iter(&self) -> impl Iterator<Item = &Literal> {
self.literals.iter()
}
/// Returns a mutable iterator through all the literals in the clause.
pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Literal> {
self.literals.iter_mut()
}
/// Swaps the literals at two indicies.
pub fn swap(&mut self, i: usize, j: usize) {
self.literals.swap(i, j);
}
/// If all the literals in the clause are assigned, return the truth value of the clause.
/// Otherwise, return `None`.
pub fn eval(&self) -> Option<bool> {
self.literals.iter().fold(Some(false), |r, o| {
r.and_then(|b| o.get_assignment().map(|v| v | b))
@ -246,40 +276,50 @@ impl Display for Clause {
}
}
/// Represents a list of clauses.
#[derive(Debug)]
pub struct ClauseList {
clauses: Vec<Clause>,
}
impl ClauseList {
/// Creates a new, empty list of clauses.
pub fn new() -> ClauseList {
ClauseList {
clauses: Vec::new(),
}
}
/// Creates a copy of the clause list. Note that the underlying variables still share a
/// reference.
pub fn copy(&self) -> ClauseList {
ClauseList {
clauses: self.clauses.clone(),
}
}
/// Adds a clause to the list.
pub fn push(&mut self, clause: Clause) {
self.clauses.push(clause);
}
/// Returns the number of clauses in the list.
pub fn len(&self) -> usize {
self.clauses.len()
}
/// Returns an iterator over all the clauses in the list.
pub fn iter(&self) -> impl Iterator<Item = &Clause> {
self.clauses.iter()
}
/// Returns a mutable iterator over all the clauses in the list.
pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Clause> {
self.clauses.iter_mut()
}
/// Returns a `HashSet` over all the variables referenced in the clauses in the list. Note that
/// the returned variables share a reference with the ones in the clause list.
pub fn get_vars(&self) -> HashSet<Variable> {
let mut set = HashSet::new();
for clause in self.iter() {
@ -290,12 +330,15 @@ impl ClauseList {
set
}
/// Returns a vector containing all the clauses in the list.
pub fn into_vec(self) -> Vec<Clause> {
self.clauses
}
}
// Properly creates new variables that don't share assignments with the old ones
/// Note that cloning a clause list gives a new list whose variables do not share references with
/// the ones from the old list. Use `copy` if you don't want this.
impl Clone for ClauseList {
fn clone(&self) -> Self {
let mut map = HashMap::<_, Variable>::new();
@ -332,6 +375,8 @@ impl core::ops::IndexMut<usize> for ClauseList {
}
}
/// Defines a DSL which allows for the declaration of many variables at once. See the unit tests
/// for examples.
#[macro_export]
macro_rules! vars {
[] => {};
@ -344,6 +389,7 @@ macro_rules! vars {
};
}
/// Defines a DSL for assigning many variables at once. See the unit tests for examples.
#[macro_export]
macro_rules! assign_vars {
{ } => {};
@ -377,6 +423,8 @@ macro_rules! add_terms {
};
}
/// Defines a DSL for constructing clauses using a convenient syntax. See the unit tests for
/// examples.
#[macro_export]
macro_rules! make_clause {
{ } => { Clause::new() };

2
src/main.rs

@ -1,7 +1,7 @@
// vim: ts=4 sw=4 et
#[macro_use]
/// TODO: document this
/// Useful for disjunctive clauses and variables.
pub mod clause;
/// I made this before I knew I didn't need it. :/
pub mod hash_wrapper;

7
src/messy_minsat.rs

@ -5,6 +5,13 @@ use std::collections::hash_map::HashMap;
use std::collections::hash_set::HashSet;
use std::rc::Rc;
/*****************************
* *
* Every oven has a vent. *
* Graham Northup *
* *
*****************************/
/// Represents a clause with a nonnegative weight. Not to be confused with [crate::clause::Clause].
struct ClauseInner {
weight: usize,

Loading…
Cancel
Save