Skip to content

Commit

Permalink
fix: balanced vtree, literal initialization, dimacs parsing
Browse files Browse the repository at this point in the history
  • Loading branch information
@jsfpdn
jsfpdn committed Nov 25, 2024
1 parent 86d62be commit 9d34d4f
Show file tree
Hide file tree
Showing 6 changed files with 276 additions and 316 deletions.
132 changes: 31 additions & 101 deletions sdd-rs-lib/literal/manager.rs
View file
Original file line number Diff line number Diff line change
@@ -1,43 +1,22 @@
use std::cell::RefCell;
use std::collections::{BTreeSet, HashMap};

use crate::literal::{Literal, Polarity, Variable, VariableIdx};
use crate::sdd::{Sdd, SddId, SddRef, SddType};
use crate::vtree::{VTreeManager, VTreeRef};
use crate::literal::{Polarity, Variable, VariableIdx};
use crate::sdd::SddRef;

#[derive(Clone, Debug)]
struct LiteralVariants {
positive_literal: Option<SddRef>,
negative_literal: Option<SddRef>,
pub(crate) struct LiteralVariants {
positive_literal: SddRef,
negative_literal: SddRef,
}

impl LiteralVariants {
fn get(&self, polarity: Polarity) -> Option<SddRef> {
pub(crate) fn get(&self, polarity: Polarity) -> SddRef {
match polarity {
Polarity::Positive => self.positive_literal.clone(),
Polarity::Negative => self.negative_literal.clone(),
}
}

fn insert(&mut self, sdd: SddRef) {
let polarity = {
match sdd.0.borrow().sdd_type {
SddType::Literal(ref literal) => literal.polarity(),
_ => unreachable!(),
}
};

match polarity {
Polarity::Positive => {
assert!(self.positive_literal.is_none());
self.positive_literal = Some(sdd);
}
Polarity::Negative => {
assert!(self.negative_literal.is_none());
self.negative_literal = Some(sdd);
}
}
}
}

#[derive(Debug)]
Expand All @@ -52,55 +31,19 @@ impl LiteralManager {
}
}

pub(crate) fn new_literal(
&self,
label: &str,
polarity: Polarity,
next_sdd_idx: SddId,
vtree_manager: &mut VTreeManager,
) -> (SddRef, bool) {
// TODO: Do not create a new literal but retrieve it only instead.
unimplemented!();
// let variable = match self.find_by_label(label) {
// None => {
// let variable = Variable::new(label, self.literals.borrow().len() as u32);
// vtree_manager.add_variable(&variable);
// variable
// }
// Some((variable, variants)) => {
// // Either positive or negative literal has been already constructed,
// // if it was, return it.
// if let Some(sdd) = variants.get(polarity) {
// return (sdd, false);
// }
// variable
// }
// };

// // SddRef has not been constructed yet, we need to create it now and add it to the HashMap.
// let literal = Literal::new_with_label(polarity, variable.clone());
// let vtree = vtree_manager.get_variable_vtree(&variable).unwrap();

// (self.create_sdd_ref(literal, next_sdd_idx, vtree), true)
}

pub(crate) fn new_literal_from_idx(
pub(crate) fn add_variable(
&self,
variable_idx: VariableIdx,
next_sdd_idx: SddId,
polarity: Polarity,
vtree_manager: &mut VTreeManager,
) -> (SddRef, bool) {
let variable = self
.literals
.borrow()
.iter()
.find(|(variable, _)| variable.index() == variable_idx)
.map(|(variable, _)| variable)
.cloned()
.unwrap();

self.new_literal(&variable.label(), polarity, next_sdd_idx, vtree_manager)
variable: &Variable,
positive_literal: SddRef,
negative_literal: SddRef,
) {
self.literals.borrow_mut().insert(
variable.clone(),
LiteralVariants {
positive_literal,
negative_literal,
},
);
}

pub(crate) fn len(&self) -> usize {
Expand All @@ -120,49 +63,36 @@ impl LiteralManager {
self.literals.borrow().contains_key(variable)
}

fn find_by_label(&self, label: &str) -> Option<(Variable, LiteralVariants)> {
pub(crate) fn find_by_index(&self, index: VariableIdx) -> Option<(Variable, LiteralVariants)> {
self.literals
.borrow()
.iter()
.find(|(variable, _)| variable.label() == label)
.find(|(variable, _)| variable.index() == index)
.map(|(variable, variants)| (variable.clone(), variants.clone()))
}

fn create_sdd_ref(&self, literal: Literal, sdd_idx: SddId, vtree: VTreeRef) -> SddRef {
let sdd = SddRef::new(Sdd::new(
SddType::Literal(literal.clone()),
sdd_idx,
vtree,
None,
));

let variants = match self.find_by_label(&literal.var_label().label()) {
Some((_, variants)) => variants,
_ => LiteralVariants {
positive_literal: None,
negative_literal: None,
},
};

let mut variants = variants.clone();
variants.insert(sdd.clone());

pub(crate) fn find_by_label(&self, label: &str) -> Option<(Variable, LiteralVariants)> {
self.literals
.borrow_mut()
.insert(literal.var_label(), variants);

sdd
.borrow()
.iter()
.find(|(variable, _)| variable.label() == label)
.map(|(variable, variants)| (variable.clone(), variants.clone()))
}
}

#[cfg(test)]
mod test {
use crate::literal::Polarity;
use crate::manager::options::vars;
use crate::manager::{options::SddOptions, SddManager};

#[test]
fn create_literals() {
let manager = SddManager::new(SddOptions::default());
let options = SddOptions::builder()
.variables(vars(vec!["a", "b"]))
.build();
let manager = SddManager::new(options);

manager.literal("a", Polarity::Negative);
manager.literal("a", Polarity::Positive);

Expand Down
45 changes: 17 additions & 28 deletions sdd-rs-lib/manager/dimacs.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ impl Clause {
.zip(self.var_label_polarities.iter())
{
// DIMACS variables are indexed from 1 but our variables start at 0.
let lit = manager.literal_from_idx(VariableIdx((*idx - 1) as u32), *polarity);
let lit = manager.literal_from_idx(&VariableIdx(*idx as u32 - 1), *polarity);
sdd = manager.disjoin(&sdd, &lit);
}

Expand Down Expand Up @@ -86,15 +86,26 @@ impl<'a> DimacsReader<'a> {
return Ok(None);
}

let mut clause = vec![];
match self.reader.read_until(b'0', &mut clause) {
let mut clause = String::new();
match self.reader.read_line(&mut clause) {
Ok(read) => {
if read == 0 {
self.state = DimacsReaderState::Finished;
Ok(None)
} else {
self.state = DimacsReaderState::ParsingClauses;
self.parse_clause_line(&clause)
let mut clause = clause.trim().to_owned();
if clause == "%" {
let _ = self.reader.read_line(&mut clause);
if clause == "0" {
return Ok(None);
}
return Err(format!(
"expected '0' after '%' but found '{clause}' instead"
));
}

self.parse_clause_line(clause)
}
}
Err(err) => Err(format!("could not parse clause: {err}")),
Expand Down Expand Up @@ -134,33 +145,11 @@ impl<'a> DimacsReader<'a> {
Ok(Preamble { clauses, variables })
}

fn parse_clause_line(&mut self, line: &[u8]) -> Result<Option<Clause>, String> {
let tokens: Vec<_> = line
.split(|num| *num == b' ' || *num == b'\n')
.filter(|variable| !variable.is_empty())
.map(String::from_utf8_lossy)
.collect();

// Check whether this is the special (and optional) syntax for EOF.
if tokens.len() == 2 {
let fst_token = tokens.first().unwrap();
let snd_token = tokens.get(1).unwrap();

if fst_token == "%" {
if snd_token == "0" {
self.state = DimacsReaderState::Finished;
return Ok(None);
}

return Err(format!(
"found '%' and next symbol should be '0' instead of '{snd_token}'"
));
}
}
fn parse_clause_line(&mut self, line: String) -> Result<Option<Clause>, String> {
let tokens: Vec<_> = line.split(" ").filter(|token| *token != "0").collect();

let literals: Vec<_> = tokens
.iter()
.filter(|token| *token != "0")
.map(|variable_idx| match variable_idx.trim().parse::<i64>() {
Err(err) => Err(format!("literal '{variable_idx}' is invalid: {err}")),
Ok(idx) => Ok((Polarity::from(!variable_idx.starts_with("-")), idx)),
Expand Down
Loading

0 comments on commit 9d34d4f

Please sign in to comment.