From d1a0d24c1f2b0debe988cc2023ffc274fe7ca852 Mon Sep 17 00:00:00 2001 From: Felix Date: Mon, 1 Jan 2024 21:07:45 -0500 Subject: [PATCH 1/5] de/serialize expressions and add type helper methods --- antwort_core/Cargo.toml | 1 + antwort_core/src/ast.rs | 74 ++++++++++++++++++++++++++++++++++++++++- 2 files changed, 74 insertions(+), 1 deletion(-) diff --git a/antwort_core/Cargo.toml b/antwort_core/Cargo.toml index 3439ba1..c29f52d 100644 --- a/antwort_core/Cargo.toml +++ b/antwort_core/Cargo.toml @@ -4,3 +4,4 @@ version = "0.1.0" edition = "2021" [dependencies] +serde = { version = "1.0.193", features = ["derive"] } diff --git a/antwort_core/src/ast.rs b/antwort_core/src/ast.rs index aa33575..78a6907 100644 --- a/antwort_core/src/ast.rs +++ b/antwort_core/src/ast.rs @@ -1,4 +1,6 @@ -#[derive(Debug, PartialEq, Clone)] +use serde::{Deserialize, Serialize}; + +#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)] pub enum Expr { Variable(String), Negation(Box), @@ -36,4 +38,74 @@ impl Expr { } } } + + pub fn is_variable(&self) -> bool { + match self { + Expr::Variable(_) => true, + _ => false, + } + } + + pub fn is_negation(&self) -> bool { + match self { + Expr::Negation(_) => true, + _ => false, + } + } + + pub fn is_disjunction(&self) -> bool { + match self { + Expr::Disjunction(_) => true, + _ => false, + } + } + + pub fn is_conjunction(&self) -> bool { + match self { + Expr::Conjunction(_) => true, + _ => false, + } + } + + pub fn is_implication(&self) -> bool { + match self { + Expr::Implication(_, _) => true, + _ => false, + } + } + + pub fn is_equivalence(&self) -> bool { + match self { + Expr::Equivalence(_, _) => true, + _ => false, + } + } + + /// Returns true if the expression is a literal. + /// A literal is either a variable or a negated variable. + pub fn is_literal(&self) -> bool { + match self { + Expr::Variable(_) => true, + Expr::Negation(a) => a.as_ref().is_variable(), + _ => false, + } + } + + /// Returns true if the expression is a clause. + /// A clause is a disjunction of literals. + pub fn is_clause(&self) -> bool { + match self { + Expr::Disjunction(a) => a.iter().all(|e| e.is_literal()), + _ => false, + } + } + + /// Returns true if the expression is in conjunctive normal form. + /// An expression is in conjunctive normal form if it is a conjunction of clauses. + pub fn is_cnf(&self) -> bool { + match self { + Expr::Conjunction(a) => a.iter().all(|e| e.is_clause()), + _ => false, + } + } } From 2daee19b339b8e0992f05b71a1bde11b064f2b95 Mon Sep 17 00:00:00 2001 From: Felix Date: Mon, 1 Jan 2024 21:11:44 -0500 Subject: [PATCH 2/5] add integration tests directory --- .../tests/integration/demorgans/1/input.cnf.json | 14 ++++++++++++++ antwort/tests/integration/demorgans/1/input.json | 12 ++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 antwort/tests/integration/demorgans/1/input.cnf.json create mode 100644 antwort/tests/integration/demorgans/1/input.json diff --git a/antwort/tests/integration/demorgans/1/input.cnf.json b/antwort/tests/integration/demorgans/1/input.cnf.json new file mode 100644 index 0000000..3bcd784 --- /dev/null +++ b/antwort/tests/integration/demorgans/1/input.cnf.json @@ -0,0 +1,14 @@ +{ + "Conjunction": [ + { + "Negation": { + "Variable": "a" + } + }, + { + "Negation": { + "Variable": "b" + } + } + ] +} \ No newline at end of file diff --git a/antwort/tests/integration/demorgans/1/input.json b/antwort/tests/integration/demorgans/1/input.json new file mode 100644 index 0000000..0863386 --- /dev/null +++ b/antwort/tests/integration/demorgans/1/input.json @@ -0,0 +1,12 @@ +{ + "Negation": { + "Disjunction": [ + { + "Variable": "a" + }, + { + "Variable": "b" + } + ] + } +} \ No newline at end of file From 85a6582acca3e499b5e5547e4de9b00662e62c56 Mon Sep 17 00:00:00 2001 From: Felix Date: Mon, 1 Jan 2024 22:09:19 -0500 Subject: [PATCH 3/5] add integration test directory --- .../integration/demorgans/{1/input.cnf.json => 1.input.cnf.json} | 0 .../tests/integration/demorgans/{1/input.json => 1.input.json} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename antwort/tests/integration/demorgans/{1/input.cnf.json => 1.input.cnf.json} (100%) rename antwort/tests/integration/demorgans/{1/input.json => 1.input.json} (100%) diff --git a/antwort/tests/integration/demorgans/1/input.cnf.json b/antwort/tests/integration/demorgans/1.input.cnf.json similarity index 100% rename from antwort/tests/integration/demorgans/1/input.cnf.json rename to antwort/tests/integration/demorgans/1.input.cnf.json diff --git a/antwort/tests/integration/demorgans/1/input.json b/antwort/tests/integration/demorgans/1.input.json similarity index 100% rename from antwort/tests/integration/demorgans/1/input.json rename to antwort/tests/integration/demorgans/1.input.json From 55ceaae4848f6b765b70e59524dae11c663e49bf Mon Sep 17 00:00:00 2001 From: Felix Date: Mon, 1 Jan 2024 23:31:08 -0500 Subject: [PATCH 4/5] integration testing infrastructure (FAILING) --- .vscode/settings.json | 4 +++ antwort/Cargo.toml | 5 +++ antwort/build.rs | 57 ++++++++++++++++++++++++++++++++ antwort/src/main.rs | 10 +++--- antwort/tests/gen_test_template | 4 +++ antwort/tests/generated_tests.rs | 31 +++++++++++++++++ 6 files changed, 106 insertions(+), 5 deletions(-) create mode 100644 antwort/build.rs create mode 100644 antwort/tests/gen_test_template create mode 100644 antwort/tests/generated_tests.rs diff --git a/.vscode/settings.json b/.vscode/settings.json index 29cc142..773f995 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -3,4 +3,8 @@ "editor.defaultFormatter": "rust-lang.rust-analyzer", "editor.formatOnSave": true, "rust-analyzer.showUnlinkedFileNotification": false, + "workbench.iconTheme": "vs-seti", + "[json]": { + "editor.defaultFormatter": "vscode.json-language-features" + }, } diff --git a/antwort/Cargo.toml b/antwort/Cargo.toml index 095065c..efa12a3 100644 --- a/antwort/Cargo.toml +++ b/antwort/Cargo.toml @@ -8,3 +8,8 @@ antwort_core = {path = "../antwort_core" } antwort_solver = {path = "../antwort_solver" } antwort_macros = {path = "../antwort_macros" } linkme = "0.3.20" +serde_json = "1.0.109" + +[build-dependencies] +convert_case = "0.6.0" +walkdir = "2.4.0" diff --git a/antwort/build.rs b/antwort/build.rs new file mode 100644 index 0000000..b76a794 --- /dev/null +++ b/antwort/build.rs @@ -0,0 +1,57 @@ +use convert_case::{Case, Casing}; +use std::{env::var, error::Error, fs::read_dir, fs::write, fs::File, io::Write}; +use walkdir::WalkDir; + +fn main() -> Result<(), Box> { + let out_dir = var("OUT_DIR")?; + let dest_path = format!("{}/gen_tests.rs", out_dir); + let mut file = File::create(&dest_path)?; + + let test_dir = "tests/integration"; + + for entry in WalkDir::new(test_dir) { + let entry = entry?; + if entry.file_type().is_dir() { + let input_bases = read_dir(entry.path())? + .filter_map(Result::ok) + .filter(|ent| { + ent.file_name() + .into_string() + .unwrap() + .ends_with(".input.json") + }) + .filter_map(|ent| { + ent.path() + .file_name() + .and_then(|stem| stem.to_str()) + .map(|s| s.to_owned().split('.').next().unwrap().to_owned()) + }) + .collect(); + write_tests(&mut file, entry.path().to_str().unwrap(), input_bases); + } + } + + Ok(()) +} + +fn write_tests(file: &mut File, dir_path: &str, input_bases: Vec) { + for base in input_bases { + let test_name = format!("{}_{}", dir_path, base); + let test_name = string_to_fn_name(&test_name); + write!( + file, + include_str!("./tests/gen_test_template"), + test_name = test_name, + dir_path = dir_path, + input_base = base + ) + .unwrap(); + } +} + +fn string_to_fn_name(s: &str) -> String { + s.to_case(Case::Snake) + .chars() + .map(|c| if c.is_alphanumeric() { c } else { '_' }) + .collect() +} diff --git a/antwort/src/main.rs b/antwort/src/main.rs index 4804f0d..bb7e0d1 100644 --- a/antwort/src/main.rs +++ b/antwort/src/main.rs @@ -41,15 +41,15 @@ fn de_morgans2(expr: &Expr) -> Result { fn main() { let rules = get_rules(); - println!("{:?}", rules); - let res = rules[0].apply(&Expr::Variable("a".to_string())); - println!("{:?}", res); + println!("Rules: {:?}", rules); - let expr = Expr::Negation(Box::new(Expr::Conjunction(vec![ + let expr = Expr::Negation(Box::new(Expr::Disjunction(vec![ Expr::Variable("a".to_string()), Expr::Variable("b".to_string()), ]))); - rewrite(&expr); + println!("Original: {}", serde_json::to_string_pretty(&expr).unwrap()); + let res = rewrite(&expr); + println!("Rewritten: {}", serde_json::to_string_pretty(&res).unwrap()); let mut f = Formula::new(); let mut c1 = Clause::new(); diff --git a/antwort/tests/gen_test_template b/antwort/tests/gen_test_template new file mode 100644 index 0000000..5c33ee0 --- /dev/null +++ b/antwort/tests/gen_test_template @@ -0,0 +1,4 @@ +#[test] +fn {test_name}() -> Result<(), Box> {{ + integration_test("{dir_path}", "{input_base}") +}} \ No newline at end of file diff --git a/antwort/tests/generated_tests.rs b/antwort/tests/generated_tests.rs new file mode 100644 index 0000000..7b68534 --- /dev/null +++ b/antwort/tests/generated_tests.rs @@ -0,0 +1,31 @@ +use antwort::rule_engine::rewrite; +use antwort::Expr; +use serde_json::from_str; +use std::error::Error; +use std::fs::read_to_string; + +fn integration_test(dir_path: &str, input_base: &str) -> Result<(), Box> { + let input_json_path = format!("{}/{}.input.json", dir_path, input_base); + let input_str = read_to_string(&input_json_path)?; + let input_expr: Expr = from_str(&input_str)?; + + let input_cnf_path = format!("{}/{}.input.cnf.json", dir_path, input_base); + let input_cnf_str = read_to_string(input_cnf_path)?; + let input_cnf_expr: Expr = from_str(&input_cnf_str)?; + assert!( + input_cnf_expr.is_cnf(), + "The expected expression is not in CNF: {}", + input_cnf_str + ); + + assert_eq!( + rewrite(&input_expr), + input_cnf_expr, + "The input expression does not reduce to CNF: {}", + input_json_path + ); + + Ok(()) +} + +include!(concat!(env!("OUT_DIR"), "/gen_tests.rs")); From 031faaa0508fa47d543beca75a776042235c1fc3 Mon Sep 17 00:00:00 2001 From: Felix Date: Tue, 2 Jan 2024 11:49:27 -0500 Subject: [PATCH 5/5] fix rule registry and correct CNF check method --- antwort/src/_rules/index.rs | 36 +++++++++++++++ antwort/src/main.rs | 44 ++----------------- antwort/src/rule_engine.rs | 3 +- antwort/tests/generated_tests.rs | 19 +++----- .../integration/demorgans/1.input.cnf.json | 14 ------ antwort_core/src/ast.rs | 8 ++-- 6 files changed, 52 insertions(+), 72 deletions(-) create mode 100644 antwort/src/_rules/index.rs delete mode 100644 antwort/tests/integration/demorgans/1.input.cnf.json diff --git a/antwort/src/_rules/index.rs b/antwort/src/_rules/index.rs new file mode 100644 index 0000000..1b03bff --- /dev/null +++ b/antwort/src/_rules/index.rs @@ -0,0 +1,36 @@ +use antwort::{macros::register_rule, rule::RuleApplicationError, Expr}; + +#[register_rule] +fn example_rule(_expr: &Expr) -> Result { + Err(RuleApplicationError::RuleNotApplicable) +} + +#[register_rule] +fn de_morgans1(expr: &Expr) -> Result { + if let Expr::Negation(b) = expr { + if let Expr::Disjunction(exprs) = b.as_ref() { + return Ok(Expr::Conjunction( + exprs + .iter() + .map(|e| Expr::Negation(Box::new(e.clone()))) + .collect(), + )); + } + } + Err(RuleApplicationError::RuleNotApplicable) +} + +#[register_rule] +fn de_morgans2(expr: &Expr) -> Result { + if let Expr::Negation(b) = expr { + if let Expr::Conjunction(exprs) = b.as_ref() { + return Ok(Expr::Disjunction( + exprs + .iter() + .map(|e| Expr::Negation(Box::new(e.clone()))) + .collect(), + )); + } + } + Err(RuleApplicationError::RuleNotApplicable) +} diff --git a/antwort/src/main.rs b/antwort/src/main.rs index bb7e0d1..702d4bc 100644 --- a/antwort/src/main.rs +++ b/antwort/src/main.rs @@ -1,47 +1,11 @@ -use antwort::macros::register_rule; -use antwort::rule::RuleApplicationError; -use antwort::rule_engine::{get_rules, rewrite}; +use antwort::rule_engine::rewrite; use antwort::solver::{solve, Clause, Formula}; -use antwort::Expr; -#[register_rule] -fn example_rule(_expr: &Expr) -> Result { - Err(RuleApplicationError::RuleNotApplicable) -} - -#[register_rule] -fn de_morgans1(expr: &Expr) -> Result { - if let Expr::Negation(b) = expr { - if let Expr::Disjunction(exprs) = b.as_ref() { - return Ok(Expr::Conjunction( - exprs - .iter() - .map(|e| Expr::Negation(Box::new(e.clone()))) - .collect(), - )); - } - } - Err(RuleApplicationError::RuleNotApplicable) -} - -#[register_rule] -fn de_morgans2(expr: &Expr) -> Result { - if let Expr::Negation(b) = expr { - if let Expr::Conjunction(exprs) = b.as_ref() { - return Ok(Expr::Disjunction( - exprs - .iter() - .map(|e| Expr::Negation(Box::new(e.clone()))) - .collect(), - )); - } - } - Err(RuleApplicationError::RuleNotApplicable) -} +// TODO: This should be done via imports, not includes +include!("./_rules/index.rs"); fn main() { - let rules = get_rules(); - println!("Rules: {:?}", rules); + use antwort::Expr; let expr = Expr::Negation(Box::new(Expr::Disjunction(vec![ Expr::Variable("a".to_string()), diff --git a/antwort/src/rule_engine.rs b/antwort/src/rule_engine.rs index 64eb868..90769e1 100644 --- a/antwort/src/rule_engine.rs +++ b/antwort/src/rule_engine.rs @@ -43,8 +43,9 @@ fn rewrite_iteration(expr: &Expr, rules: &Vec) -> Option { /// Rewrites the expression using the rules in the registry. /// Continues until no more rules are applicable to the expression or any sub-expression. pub fn rewrite(expr: &Expr) -> Expr { - println!("REWRITE: {:?}", expr); let rules = get_rules(); + println!("RULES: {:?}", rules); + println!("REWRITE: {:?}", expr); let mut new = expr.clone(); while let Some(step) = rewrite_iteration(&new, &rules) { new = step; diff --git a/antwort/tests/generated_tests.rs b/antwort/tests/generated_tests.rs index 7b68534..33a8257 100644 --- a/antwort/tests/generated_tests.rs +++ b/antwort/tests/generated_tests.rs @@ -1,28 +1,21 @@ use antwort::rule_engine::rewrite; -use antwort::Expr; use serde_json::from_str; use std::error::Error; use std::fs::read_to_string; +include!("../src/_rules/index.rs"); + fn integration_test(dir_path: &str, input_base: &str) -> Result<(), Box> { + use antwort::Expr; + let input_json_path = format!("{}/{}.input.json", dir_path, input_base); let input_str = read_to_string(&input_json_path)?; let input_expr: Expr = from_str(&input_str)?; - let input_cnf_path = format!("{}/{}.input.cnf.json", dir_path, input_base); - let input_cnf_str = read_to_string(input_cnf_path)?; - let input_cnf_expr: Expr = from_str(&input_cnf_str)?; assert!( - input_cnf_expr.is_cnf(), - "The expected expression is not in CNF: {}", - input_cnf_str - ); - - assert_eq!( - rewrite(&input_expr), - input_cnf_expr, + rewrite(&input_expr).is_cnf(), "The input expression does not reduce to CNF: {}", - input_json_path + input_json_path, ); Ok(()) diff --git a/antwort/tests/integration/demorgans/1.input.cnf.json b/antwort/tests/integration/demorgans/1.input.cnf.json deleted file mode 100644 index 3bcd784..0000000 --- a/antwort/tests/integration/demorgans/1.input.cnf.json +++ /dev/null @@ -1,14 +0,0 @@ -{ - "Conjunction": [ - { - "Negation": { - "Variable": "a" - } - }, - { - "Negation": { - "Variable": "b" - } - } - ] -} \ No newline at end of file diff --git a/antwort_core/src/ast.rs b/antwort_core/src/ast.rs index 78a6907..6efb02e 100644 --- a/antwort_core/src/ast.rs +++ b/antwort_core/src/ast.rs @@ -92,20 +92,20 @@ impl Expr { } /// Returns true if the expression is a clause. - /// A clause is a disjunction of literals. + /// A clause is a single literal or a disjunction of literals. pub fn is_clause(&self) -> bool { match self { Expr::Disjunction(a) => a.iter().all(|e| e.is_literal()), - _ => false, + expr => expr.is_literal(), } } /// Returns true if the expression is in conjunctive normal form. - /// An expression is in conjunctive normal form if it is a conjunction of clauses. + /// An expression is in conjunctive normal form if it is a single clause or a conjunction of clauses. pub fn is_cnf(&self) -> bool { match self { Expr::Conjunction(a) => a.iter().all(|e| e.is_clause()), - _ => false, + expr => expr.is_clause(), } } }