hal8174/simple-sat-solver
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add parsing and fix bugs

Browse source
This commit is contained in:
hal8174 2024-10-10 00:23:33 +02:00
parent 34ad3315b3
commit bb71924ca9
4 changed files with 700 additions and 55 deletions
Download patch file Download diff file Expand all files Collapse all files

422
Cargo.lock generated
View file

@ -2,6 +2,428 @@
# It is not intended for manual editing.
version = 3
[[package]]
name = "addr2line"
version = "0.24.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1"
dependencies = [
"gimli",
]
[[package]]
name = "adler2"
version = "2.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627"
[[package]]
name = "backtrace"
version = "0.3.74"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8d82cb332cdfaed17ae235a638438ac4d4839913cc2af585c3c6746e8f8bee1a"
dependencies = [
"addr2line",
"cfg-if",
"libc",
"miniz_oxide",
"object",
"rustc-demangle",
"windows-targets 0.52.6",
]
[[package]]
name = "backtrace-ext"
version = "0.2.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "537beee3be4a18fb023b570f80e3ae28003db9167a751266b259926e25539d50"
dependencies = [
"backtrace",
]
[[package]]
name = "bitflags"
version = "2.6.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
[[package]]
name = "cfg-if"
version = "1.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
[[package]]
name = "errno"
version = "0.3.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba"
dependencies = [
"libc",
"windows-sys 0.52.0",
]
[[package]]
name = "gimli"
version = "0.31.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f"
[[package]]
name = "is_ci"
version = "1.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7655c9839580ee829dfacba1d1278c2b7883e50a277ff7541299489d6bdfdc45"
[[package]]
name = "libc"
version = "0.2.159"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5"
[[package]]
name = "linux-raw-sys"
version = "0.4.14"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "78b3ae25bc7c8c38cec158d1f2757ee79e9b3740fbc7ccf0e59e4b08d793fa89"
[[package]]
name = "memchr"
version = "2.7.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
[[package]]
name = "miette"
version = "7.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4edc8853320c2a0dab800fbda86253c8938f6ea88510dc92c5f1ed20e794afc1"
dependencies = [
"backtrace",
"backtrace-ext",
"cfg-if",
"miette-derive",
"owo-colors",
"supports-color",
"supports-hyperlinks",
"supports-unicode",
"terminal_size",
"textwrap",
"thiserror",
"unicode-width",
]
[[package]]
name = "miette-derive"
version = "7.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dcf09caffaac8068c346b6df2a7fc27a177fd20b39421a39ce0a211bde679a6c"
dependencies = [
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "miniz_oxide"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1"
dependencies = [
"adler2",
]
[[package]]
name = "object"
version = "0.36.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e"
dependencies = [
"memchr",
]
[[package]]
name = "owo-colors"
version = "4.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "fb37767f6569cd834a413442455e0f066d0d522de8630436e2a1761d9726ba56"
[[package]]
name = "proc-macro2"
version = "1.0.87"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b3e4daa0dcf6feba26f985457cdf104d4b4256fc5a09547140f3631bb076b19a"
dependencies = [
"unicode-ident",
]
[[package]]
name = "quote"
version = "1.0.37"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
dependencies = [
"proc-macro2",
]
[[package]]
name = "rustc-demangle"
version = "0.1.24"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
[[package]]
name = "rustix"
version = "0.38.37"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811"
dependencies = [
"bitflags",
"errno",
"libc",
"linux-raw-sys",
"windows-sys 0.52.0",
]
[[package]]
name = "simple-sat-solver"
version = "0.1.0"
dependencies = [
"miette",
]
[[package]]
name = "smawk"
version = "0.3.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b7c388c1b5e93756d0c740965c41e8822f866621d41acbdf6336a6a168f8840c"
[[package]]
name = "supports-color"
version = "3.0.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8775305acf21c96926c900ad056abeef436701108518cf890020387236ac5a77"
dependencies = [
"is_ci",
]
[[package]]
name = "supports-hyperlinks"
version = "3.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2c0a1e5168041f5f3ff68ff7d95dcb9c8749df29f6e7e89ada40dd4c9de404ee"
[[package]]
name = "supports-unicode"
version = "3.0.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b7401a30af6cb5818bb64852270bb722533397edcfc7344954a38f420819ece2"
[[package]]
name = "syn"
version = "2.0.79"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
]
[[package]]
name = "terminal_size"
version = "0.3.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "21bebf2b7c9e0a515f6e0f8c51dc0f8e4696391e6f1ff30379559f8365fb0df7"
dependencies = [
"rustix",
"windows-sys 0.48.0",
]
[[package]]
name = "textwrap"
version = "0.16.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "23d434d3f8967a09480fb04132ebe0a3e088c173e6d0ee7897abbdf4eab0f8b9"
dependencies = [
"smawk",
"unicode-linebreak",
"unicode-width",
]
[[package]]
name = "thiserror"
version = "1.0.64"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "d50af8abc119fb8bb6dbabcfa89656f46f84aa0ac7688088608076ad2b459a84"
dependencies = [
"thiserror-impl",
]
[[package]]
name = "thiserror-impl"
version = "1.0.64"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3"
dependencies = [
"proc-macro2",
"quote",
"syn",
]
[[package]]
name = "unicode-ident"
version = "1.0.13"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe"
[[package]]
name = "unicode-linebreak"
version = "0.1.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3b09c83c3c29d37506a3e260c08c03743a6bb66a9cd432c6934ab501a190571f"
[[package]]
name = "unicode-width"
version = "0.1.14"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
[[package]]
name = "windows-sys"
version = "0.48.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
dependencies = [
"windows-targets 0.48.5",
]
[[package]]
name = "windows-sys"
version = "0.52.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d"
dependencies = [
"windows-targets 0.52.6",
]
[[package]]
name = "windows-targets"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c"
dependencies = [
"windows_aarch64_gnullvm 0.48.5",
"windows_aarch64_msvc 0.48.5",
"windows_i686_gnu 0.48.5",
"windows_i686_msvc 0.48.5",
"windows_x86_64_gnu 0.48.5",
"windows_x86_64_gnullvm 0.48.5",
"windows_x86_64_msvc 0.48.5",
]
[[package]]
name = "windows-targets"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
dependencies = [
"windows_aarch64_gnullvm 0.52.6",
"windows_aarch64_msvc 0.52.6",
"windows_i686_gnu 0.52.6",
"windows_i686_gnullvm",
"windows_i686_msvc 0.52.6",
"windows_x86_64_gnu 0.52.6",
"windows_x86_64_gnullvm 0.52.6",
"windows_x86_64_msvc 0.52.6",
]
[[package]]
name = "windows_aarch64_gnullvm"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8"
[[package]]
name = "windows_aarch64_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
[[package]]
name = "windows_aarch64_msvc"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc"
[[package]]
name = "windows_aarch64_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
[[package]]
name = "windows_i686_gnu"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e"
[[package]]
name = "windows_i686_gnu"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
[[package]]
name = "windows_i686_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
[[package]]
name = "windows_i686_msvc"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406"
[[package]]
name = "windows_i686_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
[[package]]
name = "windows_x86_64_gnu"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e"
[[package]]
name = "windows_x86_64_gnu"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
[[package]]
name = "windows_x86_64_gnullvm"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc"
[[package]]
name = "windows_x86_64_gnullvm"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
[[package]]
name = "windows_x86_64_msvc"
version = "0.48.5"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
[[package]]
name = "windows_x86_64_msvc"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"

1
Cargo.toml
View file

@ -4,3 +4,4 @@ version = "0.1.0"
edition = "2021"
[dependencies]
miette = { version = "7.2.0", features = ["fancy"] }

274
src/expr.rs
View file

@ -1,6 +1,6 @@
use std::collections::HashMap;
use crate::dpll::Index;
use miette::{miette, Context, Result};
use std::collections::HashMap;
#[derive(Debug, Clone)]
pub enum Expr {
@ -10,17 +10,186 @@ pub enum Expr {
Or(Vec<Expr>),
}
#[derive(Debug)]
pub enum Token<'s> {
Literal(&'s str),
Not,
And,
Or,
ParenOpen,
ParenClose,
}
pub struct Tokanizer<'s> {
s: &'s str,
start_brace: bool,
end_brace: bool,
}
impl<'s> Tokanizer<'s> {
pub fn new(s: &'s str) -> Self {
Self {
s: s.trim(),
start_brace: false,
end_brace: false,
}
}
}
impl<'s> Iterator for Tokanizer<'s> {
type Item = Result<Token<'s>>;
fn next(&mut self) -> Option<Self::Item> {
if !self.start_brace {
self.start_brace = true;
Some(Ok(Token::ParenOpen))
} else if !self.s.is_empty() {
self.s = self.s.trim_start();
if self.s.starts_with('(') {
let (_, r) = self.s.split_at(1);
self.s = r;
Some(Ok(Token::ParenOpen))
} else if self.s.starts_with(')') {
let (_, r) = self.s.split_at(1);
self.s = r;
Some(Ok(Token::ParenClose))
} else if self.s.starts_with('!') {
let (_, r) = self.s.split_at(1);
self.s = r;
Some(Ok(Token::Not))
} else if self.s.starts_with('&') {
let (_, r) = self.s.split_at(1);
self.s = r;
Some(Ok(Token::And))
} else if self.s.starts_with('|') {
let (_, r) = self.s.split_at(1);
self.s = r;
Some(Ok(Token::Or))
} else if self.s.starts_with(|c: char| c.is_alphanumeric()) {
if let Some(f) = self.s.find(|c: char| !c.is_alphanumeric()) {
let (l, r) = self.s.split_at(f);
self.s = r;
Some(Ok(Token::Literal(l)))
} else {
let s = self.s;
self.s = "";
Some(Ok(Token::Literal(s)))
}
} else {
Some(Err(miette!("Unexpected character.")))
}
} else if !self.end_brace {
self.end_brace = true;
Some(Ok(Token::ParenClose))
} else {
None
}
}
}
impl Expr {
fn parse_expr(tokanizer: &mut Tokanizer) -> Result<Expr> {
if let Some(token) = tokanizer.next().transpose()? {
match token {
Token::Literal(l) => Ok(Expr::Literal(l.to_string())),
Token::Not => Ok(Expr::Not(Box::new(Self::parse_expr(tokanizer)?))),
Token::ParenOpen => {
let first_expr = Self::parse_expr(tokanizer)?;
if let Some(next_token) = tokanizer.next().transpose()? {
match next_token {
Token::And => {
let mut v = vec![first_expr];
loop {
v.push(Self::parse_expr(tokanizer)?);
if let Some(next_token) = tokanizer.next().transpose()? {
match next_token {
Token::And => (),
Token::ParenClose => break,
_ => {
return Err(miette!(
"Unexpected toekn {:?}",
next_token
))
}
}
} else {
return Err(miette!("Unexpected end of line"));
}
}
Ok(Expr::And(v))
}
Token::Or => {
let mut v = vec![first_expr];
loop {
v.push(Self::parse_expr(tokanizer)?);
if let Some(next_token) = tokanizer.next().transpose()? {
match next_token {
Token::Or => (),
Token::ParenClose => break,
_ => {
return Err(miette!(
"Unexpected toekn {:?}",
next_token
))
}
}
} else {
return Err(miette!("Unexpected end of line"));
}
}
Ok(Expr::Or(v))
}
Token::ParenClose => Ok(first_expr),
_ => Err(miette!("Unexpected toekn {:?}", next_token)),
}
} else {
Err(miette!("Unexpected end of line"))
}
}
_ => Err(miette!("Unexpected token {:?}", token)),
}
} else {
Err(miette!("Unexpected end of line"))
}
}
pub fn parse(input: &str) -> Result<Self> {
let mut v = Vec::new();
for (i, line) in input.lines().enumerate() {
let mut tokanizer = Tokanizer::new(line);
let e = Self::parse_expr(&mut tokanizer).with_context(|| format!("In line {i}"))?;
v.push(e);
}
if v.len() == 1 {
Ok(v.into_iter().next().unwrap())
} else {
Ok(Expr::And(v))
}
}
pub fn disjunctiveNormalForm(self) -> Self {
// dbg!(&self);
match self {
Expr::Literal(_) => self,
Expr::Not(n) => match *n {
Expr::Literal(_) => Expr::Not(n),
Expr::Not(i) => i.disjunctiveNormalForm(),
Expr::And(v) => Expr::Or(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
.disjunctiveNormalForm(),
Expr::Or(v) => Expr::And(v.into_iter().map(|e| Expr::Not(Box::new(e))).collect())
.disjunctiveNormalForm(),
Expr::And(v) => Expr::Or(
v.into_iter()
.map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm())
.collect(),
)
.disjunctiveNormalForm(),
Expr::Or(v) => Expr::And(
v.into_iter()
.map(|e| Expr::Not(Box::new(e)).disjunctiveNormalForm())
.collect(),
)
.disjunctiveNormalForm(),
},
Expr::And(v) => {
let v = v
@ -78,21 +247,26 @@ impl Expr {
if let Expr::Or(v) = Expr::Not(Box::new(self)).disjunctiveNormalForm() {
Expr::And(
v.into_iter()
.map(|e| {
if let Expr::And(v) = e {
Expr::Or(
v.into_iter()
.map(|e| match e {
Expr::Literal(s) => Expr::Not(Box::new(Expr::Literal(s))),
Expr::Not(n) => *n,
Expr::And(_) => unreachable!(),
Expr::Or(_) => unreachable!(),
})
.collect(),
)
} else {
unreachable!()
.map(|e| match e {
Expr::And(v) => Expr::Or(
v.into_iter()
.map(|e| match e {
Expr::Literal(s) => Expr::Not(Box::new(Expr::Literal(s))),
Expr::Not(n) => *n,
Expr::And(_) => unreachable!(),
Expr::Or(_) => unreachable!(),
})
.collect(),
),
Expr::Literal(s) => Expr::Literal(s),
Expr::Not(n) => {
if let Expr::Literal(s) = *n {
Expr::Not(Box::new(Expr::Literal(s)))
} else {
unreachable!()
}
}
_ => unreachable!(),
})
.collect(),
)
@ -115,39 +289,63 @@ impl Expr {
let mut nextfree = 1;
for e in v {
let mut s = Vec::new();
let v = if let Expr::Or(v) = e {
v
} else {
unreachable!()
};
for l in v {
if let Expr::Literal(l) = l {
let s = match e {
Expr::Or(v) => {
let mut s = Vec::new();
for l in v {
if let Expr::Literal(l) = l {
if let Some(&i) = map.get(&l) {
s.push(i);
} else {
map.insert(l, nextfree);
s.push(nextfree);
nextfree += 1;
}
} else if let Expr::Not(n) = l {
if let Expr::Literal(l) = *n {
if let Some(&i) = map.get(&l) {
s.push(-i);
} else {
map.insert(l, nextfree);
s.push(-nextfree);
nextfree += 1;
}
} else {
unreachable!()
}
} else {
unreachable!()
}
}
s.sort();
s
}
Expr::Literal(l) => {
if let Some(&i) = map.get(&l) {
s.push(i);
vec![i]
} else {
map.insert(l, nextfree);
s.push(nextfree);
let i = nextfree;
nextfree += 1;
vec![i]
}
} else if let Expr::Not(n) = l {
}
Expr::Not(n) => {
if let Expr::Literal(l) = *n {
if let Some(&i) = map.get(&l) {
s.push(-i);
vec![-i]
} else {
map.insert(l, nextfree);
s.push(-nextfree);
let i = nextfree;
nextfree += 1;
vec![-i]
}
} else {
unreachable!()
}
} else {
unreachable!()
}
}
_ => unreachable!(),
};
cnf.push(s);
}

58
src/main.rs
View file

@ -1,35 +1,59 @@
use dpll::dpll;
use expr::Expr;
use expr::{Expr, Tokanizer};
use miette::Result;
mod dpll;
mod expr;
fn main() {
let v = Expr::Not(Box::new(Expr::And(vec![
Expr::Or(vec![
Expr::Literal(String::from("a")),
Expr::Literal(String::from("b")),
]),
Expr::Or(vec![
Expr::Literal(String::from("c")),
Expr::Literal(String::from("d")),
]),
])));
fn main() -> Result<()> {
let s = "dfjsk&(dfjsk| !fjdsk| ((djask& ffadsfj)|fjskd))";
// let s = "!!(!!fjdsk & fjds)";
dbg!(&v);
let e = Expr::parse(s)?;
dbg!(v.clone().disjunctiveNormalForm());
dbg!(v.clone().conjunctiveNormalForm());
dbg!(&e);
dbg!(Expr::Not(Box::new(e.clone())).disjunctiveNormalForm());
dbg!(e.clone().conjunctiveNormalForm());
let (cnf, _) = dbg!(v.clone().to_dpll_cnf());
let (cnf, map) = e.to_dpll_cnf();
dbg!(&cnf, &map);
let mut solution = Vec::new();
dbg!(dpll(&cnf, &mut solution));
dpll(&cnf, &mut solution);
dbg!(solution);
Ok(())
}
// fn main() {
// let v = Expr::Not(Box::new(Expr::And(vec![
// Expr::Or(vec![
// Expr::Literal(String::from("a")),
// Expr::Literal(String::from("b")),
// ]),
// Expr::Or(vec![
// Expr::Literal(String::from("c")),
// Expr::Literal(String::from("d")),
// ]),
// ])));
// dbg!(&v);
// dbg!(v.clone().disjunctiveNormalForm());
// dbg!(v.clone().conjunctiveNormalForm());
// let (cnf, _) = dbg!(v.clone().to_dpll_cnf());
// let mut solution = Vec::new();
// dbg!(dpll(&cnf, &mut solution));
// dbg!(solution);
// }
// fn main() {
// let mut solution = Vec::new();