Merge pull request #5 from lixitrixi/integration-tests

Here I create an integration testing framework to allow testing the full application workflow against various example problems. This will highlight issues like insufficient reduction rules.

.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"
+    },
 }

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"

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<dyn Error>> {
+    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<String>) {
+    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()
+}

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<Expr, RuleApplicationError> {
+    Err(RuleApplicationError::RuleNotApplicable)
+}
+
+#[register_rule]
+fn de_morgans1(expr: &Expr) -> Result<Expr, RuleApplicationError> {
+    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<Expr, RuleApplicationError> {
+    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)
+}

antwort/src/main.rs

@@ -1,55 +1,19 @@
-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<Expr, RuleApplicationError> {
-    Err(RuleApplicationError::RuleNotApplicable)
-}
-
-#[register_rule]
-fn de_morgans1(expr: &Expr) -> Result<Expr, RuleApplicationError> {
-    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<Expr, RuleApplicationError> {
-    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);
-    let res = rules[0].apply(&Expr::Variable("a".to_string()));
-    println!("{:?}", res);
+    use antwort::Expr;
 
-    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();

antwort/src/rule_engine.rs

@@ -43,8 +43,9 @@ fn rewrite_iteration(expr: &Expr, rules: &Vec<Rule>) -> Option<Expr> {
 /// 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;

antwort/tests/gen_test_template

@@ -0,0 +1,4 @@
+#[test]
+fn {test_name}() -> Result<(), Box<dyn Error>> {{
+    integration_test("{dir_path}", "{input_base}")
+}}

antwort/tests/generated_tests.rs

@@ -0,0 +1,24 @@
+use antwort::rule_engine::rewrite;
+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<dyn Error>> {
+    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)?;
+
+    assert!(
+        rewrite(&input_expr).is_cnf(),
+        "The input expression does not reduce to CNF: {}",
+        input_json_path,
+    );
+
+    Ok(())
+}
+
+include!(concat!(env!("OUT_DIR"), "/gen_tests.rs"));

antwort/tests/integration/demorgans/1.input.json

@@ -0,0 +1,12 @@
+{
+    "Negation": {
+        "Disjunction": [
+            {
+                "Variable": "a"
+            },
+            {
+                "Variable": "b"
+            }
+        ]
+    }
+}

antwort_core/Cargo.toml

@@ -4,3 +4,4 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
+serde = { version = "1.0.193", features = ["derive"] }

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<Expr>),
@@ -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 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()),
+            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 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()),
+            expr => expr.is_clause(),
+        }
+    }
 }