Browse Source

added a few helpful functions

clause_generator
Thomas Johnson 3 years ago
parent
commit
d1d2ec6e57
  1. 47
      src/clause.rs

47
src/clause.rs

@ -4,6 +4,8 @@ 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)]
@ -12,7 +14,7 @@ struct VariableInner {
assignment: RefCell<Option<bool>>,
}
#[derive(Clone, Debug)]
#[derive(Clone)]
pub struct Variable(Rc<VariableInner>);
impl Variable {
@ -111,6 +113,12 @@ impl Display for Variable {
}
}
impl core::fmt::Debug for Variable {
fn fmt(&self, fmt: &mut Formatter) -> core::fmt::Result {
<Self as core::fmt::Display>::fmt(self, fmt)
}
}
#[derive(Clone, Debug)]
pub struct Literal {
neg: bool,
@ -229,7 +237,7 @@ impl Display for Clause {
write!(fmt, "⊥")
} else {
let mut iter = self.literals.iter();
write!(fmt, "{} ", iter.next().unwrap())?;
write!(fmt, "{}", iter.next().unwrap())?;
for lit in iter {
write!(fmt, " ∨ {}", lit)?;
}
@ -250,6 +258,12 @@ impl ClauseList {
}
}
pub fn copy(&self) -> ClauseList {
ClauseList {
clauses: self.clauses.clone(),
}
}
pub fn push(&mut self, clause: Clause) {
self.clauses.push(clause);
}
@ -265,12 +279,25 @@ impl ClauseList {
pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Clause> {
self.clauses.iter_mut()
}
pub fn get_vars(&self) -> HashSet<Variable> {
let mut set = HashSet::new();
for clause in self.iter() {
for lit in clause.iter() {
set.insert(lit.get_variable().clone());
}
}
set
}
pub fn into_vec(self) -> Vec<Clause> {
self.clauses
}
}
// Properly creates new variables that don't share assignments with the old ones
impl Clone for ClauseList {
fn clone(&self) -> Self {
use std::collections::hash_map::HashMap;
let mut map = HashMap::<_, Variable>::new();
let mut clauselist = ClauseList::new();
for clause in self.iter() {
@ -309,10 +336,10 @@ impl core::ops::IndexMut<usize> for ClauseList {
macro_rules! vars {
[] => {};
[$varname:ident$(,)?] => {
let $varname = Variable::from_name(stringify!($varname).into());
let $varname = $crate::clause::Variable::from_name(stringify!($varname).into());
};
[$varname:ident, $($varnames:ident),+] => {
let $varname = Variable::from_name(stringify!($varname).into());
let $varname = $crate::clause::Variable::from_name(stringify!($varname).into());
vars![$($varnames),+]
};
}
@ -340,13 +367,13 @@ macro_rules! assign_vars {
#[allow(unused_macros)]
macro_rules! add_terms {
($varname:ident) => {};
($varname:ident - $literal:ident $(| $(-)?$rest:ident)* ) => {
($varname:ident - $literal:ident $(| $($rest:tt)*)? ) => {
$varname.push($literal.get_neg_literal());
add_terms!($varname $($rest)|*)
add_terms!($varname $($($rest)*)?)
};
($varname:ident $literal:ident $(| $(-)?$rest:ident)* ) => {
($varname:ident $literal:ident $(| $($rest:tt)*)? ) => {
$varname.push($literal.get_pos_literal());
add_terms!($varname $($rest)|*)
add_terms!($varname $($($rest)*)?)
};
}
@ -354,7 +381,7 @@ macro_rules! add_terms {
macro_rules! make_clause {
{ } => { Clause::new() };
( $($contents:tt)* ) => {{
let mut clause = Clause::new();
let mut clause = $crate::clause::Clause::new();
add_terms!(clause $($contents)*);
clause
}};

Loading…
Cancel
Save