solve some ram issues
This commit is contained in:
parent
9f6a0da017
commit
8ffa57c23d
|
@ -28,6 +28,7 @@
|
|||
use std::{
|
||||
collections::{HashMap, HashSet},
|
||||
marker::PhantomData,
|
||||
num::NonZeroUsize,
|
||||
};
|
||||
|
||||
use crate::literal::TheoryAtom;
|
||||
|
@ -42,6 +43,12 @@ mod theory;
|
|||
#[derive(Debug)]
|
||||
pub struct Theory(Num);
|
||||
|
||||
impl From<Theory> for (Num, Option<NonZeroUsize>) {
|
||||
fn from(value: Theory) -> Self {
|
||||
(value.0, None)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Num> for Theory {
|
||||
fn from(value: Num) -> Self {
|
||||
Self(value)
|
||||
|
@ -119,16 +126,22 @@ impl Aba {
|
|||
|
||||
#[derive(Debug)]
|
||||
struct TheoryHelper<T: TheoryAtom> {
|
||||
_idx: usize,
|
||||
_atom: Num,
|
||||
idx: usize,
|
||||
atom: Num,
|
||||
inner: PhantomData<T>,
|
||||
}
|
||||
|
||||
impl<T: TheoryAtom> From<TheoryHelper<T>> for (Num, Option<NonZeroUsize>) {
|
||||
fn from(value: TheoryHelper<T>) -> Self {
|
||||
(value.atom, NonZeroUsize::new(value.idx + 1))
|
||||
}
|
||||
}
|
||||
|
||||
impl<T: TheoryAtom> TheoryHelper<T> {
|
||||
fn new(idx: usize, atom: Num) -> Self {
|
||||
Self {
|
||||
_idx: idx,
|
||||
_atom: atom,
|
||||
idx,
|
||||
atom,
|
||||
inner: PhantomData,
|
||||
}
|
||||
}
|
||||
|
|
|
@ -123,7 +123,7 @@ fn calculate_loops_and_their_support(aba: &Aba) -> Vec<r#Loop> {
|
|||
loops.push(r#Loop { heads, support });
|
||||
if loops.len() >= universe.len() {
|
||||
if loops.len() == universe.len() {
|
||||
eprintln!("Too... many... cycles... Aborting cycle detection. Solver? You're on your own now");
|
||||
eprintln!("Too... many... cycles... Aborting cycle detection with {} cycles. Solver? You're on your own now", loops.len());
|
||||
}
|
||||
std::ops::ControlFlow::Break(())
|
||||
} else {
|
||||
|
|
|
@ -1,3 +1,5 @@
|
|||
use std::num::NonZeroUsize;
|
||||
|
||||
use cadical::Solver;
|
||||
|
||||
use crate::{
|
||||
|
@ -52,6 +54,12 @@ pub trait MultishotProblem {
|
|||
#[derive(Debug)]
|
||||
pub struct SetTheory(Num);
|
||||
|
||||
impl From<SetTheory> for (Num, Option<NonZeroUsize>) {
|
||||
fn from(value: SetTheory) -> Self {
|
||||
(value.0, None)
|
||||
}
|
||||
}
|
||||
|
||||
impl From<Num> for SetTheory {
|
||||
fn from(value: Num) -> Self {
|
||||
Self(value)
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
use std::{
|
||||
any::{Any, TypeId},
|
||||
fmt::Debug,
|
||||
num::NonZeroUsize,
|
||||
};
|
||||
|
||||
use crate::aba::Num;
|
||||
|
@ -13,8 +14,8 @@ pub enum Literal {
|
|||
}
|
||||
|
||||
/// New type to prevent creation of arbitrary SAT literals
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct RawLiteral(String);
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||
pub struct RawLiteral(TypeId, Num, Option<NonZeroUsize>);
|
||||
|
||||
/// Convert the type into it's literal
|
||||
#[doc(notable_trait)]
|
||||
|
@ -32,9 +33,10 @@ pub trait IntoLiteral: Sized {
|
|||
}
|
||||
|
||||
/// Implement [`IntoLiteral`] for all types that are 'static, sized and debuggable
|
||||
impl<T: Any + Debug + Sized> IntoLiteral for T {
|
||||
impl<T: Any + Into<(Num, Option<NonZeroUsize>)>> IntoLiteral for T {
|
||||
fn into_literal(self) -> RawLiteral {
|
||||
RawLiteral(format!("{:?}#{:?}", TypeId::of::<T>(), self))
|
||||
let (num, index) = self.into();
|
||||
RawLiteral(TypeId::of::<T>(), num, index)
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -69,7 +71,7 @@ impl Literal {
|
|||
}
|
||||
|
||||
impl std::ops::Deref for Literal {
|
||||
type Target = String;
|
||||
type Target = RawLiteral;
|
||||
|
||||
fn deref(&self) -> &Self::Target {
|
||||
match self {
|
||||
|
@ -81,22 +83,16 @@ impl std::ops::Deref for Literal {
|
|||
impl std::fmt::Debug for Literal {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
Literal::Pos(str) => write!(f, "+{str}"),
|
||||
Literal::Neg(str) => write!(f, "-{str}"),
|
||||
Literal::Pos(str) => write!(f, "+{str:?}"),
|
||||
Literal::Neg(str) => write!(f, "-{str:?}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::ops::Deref for RawLiteral {
|
||||
type Target = String;
|
||||
// impl std::ops::Deref for RawLiteral {
|
||||
// type Target = String;
|
||||
|
||||
fn deref(&self) -> &Self::Target {
|
||||
&self.0
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for RawLiteral {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
std::fmt::Display::fmt(&self.0, f)
|
||||
}
|
||||
}
|
||||
// fn deref(&self) -> &Self::Target {
|
||||
// &self.0
|
||||
// }
|
||||
// }
|
||||
|
|
|
@ -4,17 +4,17 @@ use cadical::Solver;
|
|||
|
||||
use crate::{
|
||||
clauses::{Clause, RawClause},
|
||||
literal::Literal,
|
||||
literal::{Literal, RawLiteral},
|
||||
};
|
||||
|
||||
#[derive(Debug, Default)]
|
||||
pub struct Mapper {
|
||||
map: HashMap<String, u32>,
|
||||
map: HashMap<RawLiteral, u32>,
|
||||
}
|
||||
|
||||
pub enum ReconstructedLiteral {
|
||||
Pos(String),
|
||||
Neg(String),
|
||||
Pos(RawLiteral),
|
||||
Neg(RawLiteral),
|
||||
}
|
||||
|
||||
impl Mapper {
|
||||
|
@ -34,10 +34,10 @@ impl Mapper {
|
|||
}
|
||||
|
||||
pub fn as_raw(&mut self, lit: &Literal) -> i32 {
|
||||
let key = self.map.get(lit.as_str()).copied().unwrap_or_else(|| {
|
||||
let key = self.map.get(lit).copied().unwrap_or_else(|| {
|
||||
debug_assert!(self.map.len() <= i32::MAX as usize, "Mapper overflowed");
|
||||
let new = self.map.len() as u32 + 1;
|
||||
self.map.insert(lit.to_string(), new);
|
||||
self.map.insert((**lit).clone(), new);
|
||||
new
|
||||
}) as i32;
|
||||
match lit {
|
||||
|
@ -51,24 +51,23 @@ impl Mapper {
|
|||
sat: &'s Solver,
|
||||
) -> impl Iterator<Item = ReconstructedLiteral> + 's {
|
||||
self.map.iter().flat_map(|(lit, raw)| {
|
||||
let (_, lit) = lit.split_once('#').expect("All literals must contain a #");
|
||||
sat.value(*raw as i32).map(|result| match result {
|
||||
true => ReconstructedLiteral::Pos(lit.to_owned()),
|
||||
false => ReconstructedLiteral::Neg(lit.to_owned()),
|
||||
true => ReconstructedLiteral::Pos(lit.clone()),
|
||||
false => ReconstructedLiteral::Neg(lit.clone()),
|
||||
})
|
||||
})
|
||||
}
|
||||
|
||||
pub fn get_raw(&self, lit: &Literal) -> Option<i32> {
|
||||
self.map.get(lit.as_str()).map(|&raw| raw as i32)
|
||||
self.map.get(lit).map(|&raw| raw as i32)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for ReconstructedLiteral {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
ReconstructedLiteral::Pos(str) => write!(f, "+{str}"),
|
||||
ReconstructedLiteral::Neg(str) => write!(f, "-{str}"),
|
||||
ReconstructedLiteral::Pos(str) => write!(f, "+{str:?}"),
|
||||
ReconstructedLiteral::Neg(str) => write!(f, "-{str:?}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue