From bb71924ca935e8faf2f564007b567a9dd0c7163f Mon Sep 17 00:00:00 2001 From: hal8174 Date: Thu, 10 Oct 2024 00:23:33 +0200 Subject: [PATCH] Add parsing and fix bugs --- Cargo.lock | 422 ++++++++++++++++++++++++++++++++++++++++++++++++++++ Cargo.toml | 1 + src/expr.rs | 274 +++++++++++++++++++++++++++++----- src/main.rs | 58 +++++--- 4 files changed, 700 insertions(+), 55 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 362bf7f..47f545d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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" diff --git a/Cargo.toml b/Cargo.toml index 4608f86..ae37162 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,3 +4,4 @@ version = "0.1.0" edition = "2021" [dependencies] +miette = { version = "7.2.0", features = ["fancy"] } diff --git a/src/expr.rs b/src/expr.rs index 36202b4..f8c4edd 100644 --- a/src/expr.rs +++ b/src/expr.rs @@ -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), } +#[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>; + + fn next(&mut self) -> Option { + 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 { + 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 { + 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); } diff --git a/src/main.rs b/src/main.rs index 4cf4759..9ea66c3 100644 --- a/src/main.rs +++ b/src/main.rs @@ -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();