pub use crate::{
assign::AssignReason,
cdb::{Clause, ClauseIF, ClauseId, ClauseIdIF, Watch},
config::Config,
};
use {
crate::solver::SolverEvent,
std::{
cmp::Ordering,
convert::TryFrom,
fmt,
fs::File,
io::{BufRead, BufReader},
ops::{Index, IndexMut, Neg, Not},
path::{Path, PathBuf},
},
};
pub trait PropertyReference<I, O> {
fn refer(&self, key: I) -> &O;
}
pub trait PropertyDereference<I, O: Sized> {
fn derefer(&self, key: I) -> O;
}
pub trait LitIF {
fn as_bool(&self) -> bool;
fn from_assign(vi: VarId, p: bool) -> Self;
fn vi(self) -> VarId;
fn is_none(&self) -> bool;
}
pub trait ActivityIF<Ix> {
fn activity(&mut self, ix: Ix) -> f64;
fn average_activity(&self) -> f64;
fn set_activity(&mut self, ix: Ix, val: f64);
fn reward_at_analysis(&mut self, _ix: Ix) {
#[cfg(debug)]
todo!()
}
fn reward_at_assign(&mut self, _ix: Ix) {
#[cfg(debug)]
todo!()
}
fn reward_at_propagation(&mut self, _ix: Ix) {
#[cfg(debug)]
todo!()
}
fn reward_at_unassign(&mut self, _ix: Ix) {
#[cfg(debug)]
todo!()
}
fn update_rewards(&mut self);
fn update_activity_decay(&mut self, _index: Option<usize>) {
#[cfg(debug)]
todo!()
}
}
pub trait Instantiate {
fn instantiate(conf: &Config, cnf: &CNFDescription) -> Self;
fn handle(&mut self, _e: SolverEvent) {}
}
pub trait Delete<T> {
fn delete_unstable<F>(&mut self, filter: F)
where
F: FnMut(&T) -> bool;
}
pub type VarId = usize;
pub type DecisionLevel = u32;
#[derive(Clone, Copy, Debug, Default, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Lit {
ordinal: u32,
}
pub const NULL_LIT: Lit = Lit { ordinal: 0 };
impl fmt::Display for Lit {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}L", i32::from(self))
}
}
pub fn i32s(v: &[Lit]) -> Vec<i32> {
v.iter().map(|l| i32::from(*l)).collect::<Vec<_>>()
}
impl From<(VarId, bool)> for Lit {
#[inline]
fn from((vi, b): (VarId, bool)) -> Self {
Lit {
ordinal: ((vi as u32) * 2) + (b as u32),
}
}
}
impl From<(VarId, Option<bool>)> for Lit {
#[inline]
fn from((vi, ob): (VarId, Option<bool>)) -> Self {
match ob {
None => NULL_LIT,
Some(b) => Lit::from((vi, b)),
}
}
}
impl From<usize> for Lit {
#[inline]
fn from(l: usize) -> Self {
Lit { ordinal: l as u32 }
}
}
impl From<i32> for Lit {
#[inline]
fn from(x: i32) -> Self {
Lit {
ordinal: (if x < 0 { -2 * x } else { 2 * x + 1 }) as u32,
}
}
}
impl From<ClauseId> for Lit {
#[inline]
fn from(cid: ClauseId) -> Self {
Lit {
ordinal: cid.ordinal & 0x7FFF_FFFF,
}
}
}
impl From<Lit> for bool {
#[inline]
fn from(l: Lit) -> bool {
(l.ordinal & 1) != 0
}
}
impl From<Lit> for ClauseId {
#[inline]
fn from(l: Lit) -> ClauseId {
ClauseId {
ordinal: l.ordinal | 0x8000_0000,
}
}
}
impl From<Lit> for usize {
#[inline]
fn from(l: Lit) -> usize {
l.ordinal as usize
}
}
impl From<Lit> for i32 {
#[inline]
fn from(l: Lit) -> i32 {
if l.ordinal % 2 == 0 {
((l.ordinal >> 1) as i32).neg()
} else {
(l.ordinal >> 1) as i32
}
}
}
impl From<&Lit> for i32 {
#[inline]
fn from(l: &Lit) -> i32 {
if l.ordinal % 2 == 0 {
((l.ordinal >> 1) as i32).neg()
} else {
(l.ordinal >> 1) as i32
}
}
}
impl Not for Lit {
type Output = Lit;
#[inline]
fn not(self) -> Self {
Lit {
ordinal: self.ordinal ^ 1,
}
}
}
impl Index<Lit> for [bool] {
type Output = bool;
#[inline]
fn index(&self, l: Lit) -> &Self::Output {
unsafe { self.get_unchecked(usize::from(l)) }
}
}
impl IndexMut<Lit> for [bool] {
#[inline]
fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
unsafe { self.get_unchecked_mut(usize::from(l)) }
}
}
impl Index<Lit> for Vec<bool> {
type Output = bool;
#[inline]
fn index(&self, l: Lit) -> &Self::Output {
unsafe { self.get_unchecked(usize::from(l)) }
}
}
impl IndexMut<Lit> for Vec<bool> {
#[inline]
fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
unsafe { self.get_unchecked_mut(usize::from(l)) }
}
}
impl Index<Lit> for Vec<Vec<Watch>> {
type Output = Vec<Watch>;
#[inline]
fn index(&self, l: Lit) -> &Self::Output {
unsafe { self.get_unchecked(usize::from(l)) }
}
}
impl IndexMut<Lit> for Vec<Vec<Watch>> {
#[inline]
fn index_mut(&mut self, l: Lit) -> &mut Self::Output {
unsafe { self.get_unchecked_mut(usize::from(l)) }
}
}
impl LitIF for Lit {
#[inline]
fn as_bool(&self) -> bool {
self.ordinal & 1 == 1
}
#[inline]
fn from_assign(vi: VarId, p: bool) -> Lit {
Lit {
ordinal: (vi as u32) << 1 | (p as u32),
}
}
#[inline]
fn vi(self) -> VarId {
(self.ordinal >> 1) as VarId
}
#[inline]
fn is_none(&self) -> bool {
self.ordinal == 0
}
}
pub trait EmaIF {
type Input;
fn get(&self) -> f64;
fn reset(&mut self) {}
fn update(&mut self, x: Self::Input);
fn trend(&self) -> f64 {
unimplemented!()
}
}
#[derive(Clone, Debug)]
pub struct Ema {
val: f64,
#[cfg(feature = "ema_calibration")]
cal: f64,
sca: f64,
}
impl EmaIF for Ema {
type Input = f64;
#[cfg(not(feature = "ema_calibration"))]
fn update(&mut self, x: Self::Input) {
self.val = self.sca * x + (1.0 - self.sca) * self.val;
}
#[cfg(feature = "ema_calibration")]
fn update(&mut self, x: Self::Input) {
self.val = self.sca * x + (1.0 - self.sca) * self.val;
self.cal = self.sca + (1.0 - self.sca) * self.cal;
}
#[cfg(feature = "ema_calibration")]
fn get(&self) -> f64 {
self.val / self.cal
}
#[cfg(not(feature = "ema_calibration"))]
fn get(&self) -> f64 {
self.val
}
}
impl Ema {
pub fn new(s: usize) -> Ema {
Ema {
val: 0.0,
#[cfg(feature = "ema_calibration")]
cal: 0.0,
sca: 1.0 / (s as f64),
}
}
}
#[derive(Clone, Debug)]
pub struct Ema2 {
fast: f64,
slow: f64,
#[cfg(feature = "ema_calibration")]
calf: f64,
#[cfg(feature = "ema_calibration")]
cals: f64,
fe: f64,
se: f64,
}
impl EmaIF for Ema2 {
type Input = f64;
fn get(&self) -> f64 {
self.fast
}
#[cfg(not(feature = "ema_calibration"))]
fn update(&mut self, x: Self::Input) {
self.fast = self.fe * x + (1.0 - self.fe) * self.fast;
self.slow = self.se * x + (1.0 - self.se) * self.slow;
}
#[cfg(feature = "ema_calibration")]
fn update(&mut self, x: Self::Input) {
self.fast = self.fe * x + (1.0 - self.fe) * self.fast;
self.slow = self.se * x + (1.0 - self.se) * self.slow;
self.calf = self.fe + (1.0 - self.fe) * self.calf;
self.cals = self.se + (1.0 - self.se) * self.cals;
}
#[cfg(not(feature = "ema_calibration"))]
fn reset(&mut self) {
self.slow = self.fast;
}
#[cfg(feature = "ema_calibration")]
fn reset(&mut self) {
self.slow = self.fast;
self.cals = self.calf;
}
#[cfg(not(feature = "ema_calibration"))]
fn trend(&self) -> f64 {
self.fast / self.slow
}
#[cfg(feature = "ema_calibration")]
fn trend(&self) -> f64 {
self.fast / self.slow * (self.cals / self.calf)
}
}
impl Ema2 {
pub fn new(f: usize) -> Ema2 {
Ema2 {
fast: 0.0,
slow: 0.0,
#[cfg(feature = "ema_calibration")]
calf: 0.0,
#[cfg(feature = "ema_calibration")]
cals: 0.0,
fe: 1.0 / (f as f64),
se: 1.0 / (f as f64),
}
}
pub fn with_slow(mut self, s: usize) -> Ema2 {
self.se = 1.0 / (s as f64);
self
}
pub fn get_slow(&self) -> f64 {
self.slow
}
}
#[derive(Clone, Debug)]
pub struct EmaSU {
last: f64,
ema: Ema,
}
impl EmaIF for EmaSU {
type Input = usize;
fn update(&mut self, x: Self::Input) {
let diff: f64 = x as f64 - self.last;
self.ema.update(diff);
self.last = x as f64;
}
fn get(&self) -> f64 {
self.ema.get()
}
}
impl EmaSU {
pub fn new(s: usize) -> Self {
EmaSU {
last: 0.0,
ema: Ema::new(s),
}
}
pub fn get_ema(&self) -> &Ema {
&self.ema
}
}
#[derive(Debug, Eq, PartialEq)]
pub enum SolverError {
IOError,
Inconsistent,
NullLearnt,
OutOfMemory,
OutOfRange,
TimeOut,
SolverBug,
UndescribedError,
}
impl fmt::Display for SolverError {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{:?}", self)
}
}
pub type MaybeInconsistent = Result<(), SolverError>;
#[derive(Clone, Debug)]
pub enum CNFIndicator {
Void,
File(String),
LitVec(usize),
}
impl Default for CNFIndicator {
fn default() -> Self {
CNFIndicator::Void
}
}
impl fmt::Display for CNFIndicator {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
CNFIndicator::Void => write!(f, "No CNF specified)"),
CNFIndicator::File(file) => write!(f, "CNF file({})", file),
CNFIndicator::LitVec(n) => write!(f, "A vec({} clauses)", n),
}
}
}
#[derive(Clone, Debug)]
pub struct CNFDescription {
pub num_of_variables: usize,
pub num_of_clauses: usize,
pub pathname: CNFIndicator,
}
impl Default for CNFDescription {
fn default() -> CNFDescription {
CNFDescription {
num_of_variables: 0,
num_of_clauses: 0,
pathname: CNFIndicator::Void,
}
}
}
impl fmt::Display for CNFDescription {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
let CNFDescription {
num_of_variables: nv,
num_of_clauses: nc,
pathname: path,
} = &self;
write!(f, "CNF({}, {}, {})", nv, nc, path)
}
}
impl<V> From<&[V]> for CNFDescription
where
V: AsRef<[i32]>,
{
fn from(vec: &[V]) -> Self {
let num_of_variables = vec
.iter()
.map(|clause| clause.as_ref().iter().map(|l| l.abs()).max().unwrap_or(0))
.max()
.unwrap_or(0) as usize;
CNFDescription {
num_of_variables,
num_of_clauses: vec.len(),
pathname: CNFIndicator::LitVec(vec.len()),
}
}
}
#[derive(Debug)]
pub struct CNFReader {
pub cnf: CNFDescription,
pub reader: BufReader<File>,
}
impl TryFrom<&str> for CNFReader {
type Error = SolverError;
fn try_from(s: &str) -> Result<Self, Self::Error> {
CNFReader::try_from(&PathBuf::from(s))
}
}
impl TryFrom<&PathBuf> for CNFReader {
type Error = SolverError;
fn try_from(path: &PathBuf) -> Result<Self, Self::Error> {
let pathname = if path.to_string_lossy().is_empty() {
"--".to_string()
} else {
Path::new(&path.to_string_lossy().into_owned())
.file_name()
.map_or("aStrangeNamed".to_string(), |f| {
f.to_string_lossy().into_owned()
})
};
let fs = File::open(path).map_or(Err(SolverError::IOError), Ok)?;
let mut reader = BufReader::new(fs);
let mut buf = String::new();
let mut nv: usize = 0;
let mut nc: usize = 0;
let mut found_valid_header = false;
loop {
buf.clear();
match reader.read_line(&mut buf) {
Ok(0) => break,
Ok(_k) => {
let mut iter = buf.split_whitespace();
if iter.next() == Some("p") && iter.next() == Some("cnf") {
if let Some(v) = iter.next().map(|s| s.parse::<usize>().ok().unwrap()) {
if let Some(c) = iter.next().map(|s| s.parse::<usize>().ok().unwrap()) {
nv = v;
nc = c;
found_valid_header = true;
break;
}
}
}
continue;
}
Err(e) => {
println!("{}", e);
return Err(SolverError::IOError);
}
}
}
if !found_valid_header {
return Err(SolverError::IOError);
}
let cnf = CNFDescription {
num_of_variables: nv,
num_of_clauses: nc,
pathname: CNFIndicator::File(pathname),
};
Ok(CNFReader { cnf, reader })
}
}
impl<T> Delete<T> for Vec<T> {
fn delete_unstable<F>(&mut self, mut filter: F)
where
F: FnMut(&T) -> bool,
{
let mut i = 0;
while i != self.len() {
if filter(&mut self[i]) {
self.swap_remove(i);
break;
} else {
i += 1;
}
}
}
}
pub trait FlagIF {
fn is(&self, flag: Flag) -> bool;
fn set(&mut self, f: Flag, b: bool);
fn turn_off(&mut self, flag: Flag);
fn turn_on(&mut self, flag: Flag);
}
bitflags! {
pub struct Flag: u16 {
const DEAD = 0b0000_0000_0000_0001;
const LEARNT = 0b0000_0000_0000_0010;
const OCCUR_LINKED = 0b0000_0000_0000_0100;
const ENQUEUED = 0b0000_0000_0000_1000;
const TOUCHED = 0b0000_0000_0001_0000;
const VIVIFIED = 0b0000_0000_0010_0000;
const VIVIFIED2 = 0b0000_0000_0100_0000;
const DERIVE20 = 0b0000_0000_1000_0000;
const VIV_ASSUMED = 0b0000_0001_0000_0000;
const ELIMINATED = 0b0000_0010_0000_0000;
const CA_SEEN = 0b0000_0100_0000_0000;
const PHASE = 0b0000_1000_0000_0000;
const STAGED = 0b0001_0000_0000_0000;
#[cfg(feature = "just_used")]
const JUST_USED = 0b0010_0000_0000_0000;
}
}
#[derive(Debug)]
pub struct Logger {
dest: Option<File>,
}
impl Default for Logger {
fn default() -> Self {
Logger { dest: None }
}
}
impl fmt::Display for Logger {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "Dump({:?})", self.dest)
}
}
impl Logger {
pub fn new<T: AsRef<str>>(fname: T) -> Self {
Logger {
dest: File::create(fname.as_ref()).ok(),
}
}
pub fn dump(&mut self, mes: String) {
use std::io::Write;
if let Some(f) = &mut self.dest {
f.write_all(&mes.into_bytes())
.unwrap_or_else(|_| panic!("fail to dump {:?}", f));
} else {
println!("{}", mes);
}
}
}
#[derive(Clone, Debug)]
pub struct OrderedProxy<T: Clone + Default + Sized> {
index: f64,
body: T,
}
impl<T: Clone + Default + Sized> Default for OrderedProxy<T> {
fn default() -> Self {
OrderedProxy {
index: 0.0,
body: T::default(),
}
}
}
impl<T: Clone + Default + Sized> PartialEq for OrderedProxy<T> {
fn eq(&self, other: &OrderedProxy<T>) -> bool {
self.index == other.index
}
}
impl<T: Clone + Default + Sized> Eq for OrderedProxy<T> {}
impl<T: Clone + Default + PartialEq> PartialOrd for OrderedProxy<T> {
fn partial_cmp(&self, other: &OrderedProxy<T>) -> Option<Ordering> {
if (self.index - other.index).abs() < f64::EPSILON {
Some(Ordering::Equal)
} else if self.index < other.index {
Some(Ordering::Less)
} else {
Some(Ordering::Greater)
}
}
}
impl<T: Clone + Default + PartialEq> Ord for OrderedProxy<T> {
fn cmp(&self, other: &OrderedProxy<T>) -> Ordering {
if (self.index - other.index).abs() < f64::EPSILON {
Ordering::Equal
} else if self.index < other.index {
Ordering::Less
} else {
Ordering::Greater
}
}
}
impl<T: Clone + Default + Sized> OrderedProxy<T> {
pub fn new(body: T, index: f64) -> Self {
OrderedProxy { index, body }
}
pub fn new_invert(body: T, rindex: f64) -> Self {
OrderedProxy {
index: -rindex,
body,
}
}
pub fn to(&self) -> T {
self.body.clone()
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_cnf() {
if let Ok(reader) = CNFReader::try_from("tests/sample.cnf") {
assert_eq!(reader.cnf.num_of_variables, 250);
assert_eq!(reader.cnf.num_of_clauses, 1065);
} else {
panic!("failed to load tests/sample.cnf");
}
}
}