Additionally generate truth tables

.vscode/settings.json

@@ -8,6 +8,7 @@
         "IVEQ",
         "petgraph",
         "Ponens",
+        "repr",
         "syntree",
         "Tollens"
     ]

CHANGELOG.md

@@ -17,6 +17,12 @@ and this project adheres to [Semantic Versioning](http://semver.org/).
     ```shell
     raa_tt -h
     ```
+* The binary tool can now additionally generate truth tables. This is only for reference reasons
+since many available tools understand or generate truth tables. The limit for the number of
+variables for which a truth table can be generated is currently arbitrarily set to 16.
+    ```shell
+    raa_tt -s "(a & a -> b) -> b" -q -t
+    ```
 
 ## 0.3.0 - 2023-11-05
 

src/bin/raa_tt/arguments.rs

@@ -7,14 +7,18 @@ use clap::Parser;
 #[command(author, version, about)]
 pub(crate) struct CliArgs {
     /// Input file
-    #[arg(short = 'f', long = "file", group = "input", required = true)]
+    #[arg(short, long, group = "input", required = true)]
     pub file: Option<PathBuf>,
 
     /// Input string
     #[arg(short = 's', group = "input", required = true)]
     pub text: Option<String>,
 
-    /// Decreased verbosity
+    /// Generate truth table
+    #[arg(short, long)]
+    pub truth_table: bool,
+
+    /// Decrease verbosity
     #[arg(short, long)]
     pub quiet: bool,
 }

src/bin/raa_tt/main.rs

@@ -5,10 +5,10 @@ mod arguments;
 use anyhow::{Context, Result};
 use clap::Parser;
 use parol_runtime::{log::debug, Report};
-use raa_tt::proposition::Proposition;
 use raa_tt::prover::Prover;
 use raa_tt::raa_tt_grammar::RaaTtGrammar;
 use raa_tt::raa_tt_parser::parse;
+use raa_tt::{proposition::Proposition, table_generator::TableGenerator};
 use std::{fs, time::Instant};
 
 use crate::arguments::CliArgs;
@@ -43,23 +43,30 @@ fn main() -> Result<()> {
         Ok(_) => {
             let elapsed_time = now.elapsed();
             if !quiet {
+                println!("{}", "-".repeat(80));
                 println!("Parsing took {} milliseconds.", elapsed_time.as_millis());
+                println!();
             }
             for p in &raa_tt_grammar.raa_tt.as_ref().unwrap().raa_tt_list {
                 let proposition: Proposition = (&*p.biconditional).into();
                 if !quiet {
-                    println!("Parsed expression: {proposition}");
+                    println!("{}", "-".repeat(80));
                 }
 
                 let solver = Prover::new();
                 let solve_result = solver.prove(&proposition);
                 match solve_result {
                     Ok(r) => {
-                        println!("// {r}");
-                        println!("{proposition}\n");
+                        println!();
+                        println!("{proposition} is {r}");
                     }
                     Err(e) => println!("Error occurred: {e}"),
                 }
+
+                if args.truth_table {
+                    let table_generator = TableGenerator::new();
+                    table_generator.generate_truth_table(&proposition)?;
+                }
             }
             Ok(())
         }

src/errors.rs

@@ -6,4 +6,10 @@ pub type Result<T> = std::result::Result<T, RaaError>;
 pub enum RaaError {
     #[error("Tried to use a void expression (internal error)")]
     VoidExpression,
+    #[error("Too many variables for truth table generation")]
+    TooManyVariables,
+    #[error("Variable {name} not defined")]
+    UndefinedVariable { name: String },
+    #[error(transparent)]
+    FormatError { source: std::fmt::Error },
 }

src/lib.rs

@@ -9,3 +9,4 @@ pub mod prover;
 pub mod raa_tt_grammar;
 mod raa_tt_grammar_trait;
 pub mod raa_tt_parser;
+pub mod table_generator;

src/proposition.rs

@@ -1,4 +1,7 @@
-use std::fmt::{Debug, Display, Error, Formatter};
+use std::{
+    collections::BTreeSet,
+    fmt::{Debug, Display, Error, Formatter},
+};
 
 use crate::{
     bi_implication::BiImplication, conjunction::Conjunction, disjunction::Disjunction,
@@ -16,6 +19,39 @@ pub enum Proposition {
     Disjunction(Disjunction),
     Conjunction(Conjunction),
 }
+impl Proposition {
+    pub(crate) fn get_variables(&self) -> BTreeSet<String> {
+        let mut vars = BTreeSet::new();
+        self.inner_get_variables(&mut vars);
+        vars
+    }
+
+    fn inner_get_variables(&self, vars: &mut BTreeSet<String>) {
+        match self {
+            Proposition::Void => (),
+            Proposition::Atom(v) => {
+                vars.insert(v.clone());
+            }
+            Proposition::Negation(Negation { inner }) => inner.inner_get_variables(vars),
+            Proposition::Implication(Implication { left, right }) => {
+                left.inner_get_variables(vars);
+                right.inner_get_variables(vars);
+            }
+            Proposition::BiImplication(BiImplication { left, right }) => {
+                left.inner_get_variables(vars);
+                right.inner_get_variables(vars);
+            }
+            Proposition::Disjunction(Disjunction { left, right }) => {
+                left.inner_get_variables(vars);
+                right.inner_get_variables(vars);
+            }
+            Proposition::Conjunction(Conjunction { left, right }) => {
+                left.inner_get_variables(vars);
+                right.inner_get_variables(vars);
+            }
+        }
+    }
+}
 
 impl Display for Proposition {
     fn fmt(&self, f: &mut Formatter<'_>) -> std::result::Result<(), Error> {

src/table_generator.rs

@@ -0,0 +1,98 @@
+use std::{cell::RefCell, collections::BTreeMap, fmt::Write};
+
+use crate::{
+    bi_implication::BiImplication,
+    conjunction::Conjunction,
+    disjunction::Disjunction,
+    errors::{RaaError, Result},
+    implication::Implication,
+    negation::Negation,
+    proposition::Proposition,
+};
+
+impl Proposition {
+    fn calculate_value(&self, vars: &BTreeMap<String, bool>) -> Result<bool> {
+        let result = match self {
+            Proposition::Void => Err(RaaError::VoidExpression)?,
+            Proposition::Atom(a) => vars
+                .get(a)
+                .ok_or(RaaError::UndefinedVariable { name: a.to_owned() })
+                .map(|b| *b)?,
+            Proposition::Negation(Negation { inner }) => !inner.calculate_value(vars)?,
+            Proposition::Implication(Implication { left, right }) => {
+                !left.calculate_value(vars)? || right.calculate_value(vars)?
+            }
+            Proposition::BiImplication(BiImplication { left, right }) => {
+                left.calculate_value(vars)? == right.calculate_value(vars)?
+            }
+            Proposition::Disjunction(Disjunction { left, right }) => {
+                left.calculate_value(vars)? || right.calculate_value(vars)?
+            }
+            Proposition::Conjunction(Conjunction { left, right }) => {
+                left.calculate_value(vars)? && right.calculate_value(vars)?
+            }
+        };
+        Ok(result)
+    }
+}
+
+#[derive(Debug, Default)]
+pub struct TableGenerator {
+    vars: RefCell<BTreeMap<String, bool>>,
+}
+
+impl TableGenerator {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn generate_truth_table(&self, proposition: &Proposition) -> Result<()> {
+        let vars = proposition.get_variables();
+        *self.vars.borrow_mut() = vars.iter().fold(BTreeMap::new(), |mut acc, v| {
+            acc.insert(v.clone(), false);
+            acc
+        });
+        if self.number_of_vars() > 16 {
+            return Err(RaaError::TooManyVariables);
+        }
+        let var_part = self.generate_table_header()?;
+        let prp_part = proposition.to_string();
+        println!("{var_part} {prp_part}");
+        println!("{}", "-".repeat(var_part.len() + prp_part.len()));
+        for v in 0..2usize.pow(self.number_of_vars()) {
+            self.generate_table_line(v, proposition)?;
+        }
+        Ok(())
+    }
+
+    fn generate_table_header(&self) -> Result<String> {
+        let mut line = String::new();
+        self.vars.borrow().keys().try_for_each(|var| {
+            write!(line, "{var} | ").map_err(|e| RaaError::FormatError { source: e })
+        })?;
+        Ok(line)
+    }
+
+    #[inline]
+    fn number_of_vars(&self) -> u32 {
+        self.vars.borrow().len() as u32
+    }
+
+    fn generate_table_line(&self, v: usize, proposition: &Proposition) -> Result<()> {
+        let n = self.number_of_vars();
+        let mut bit = if n == 0 { 0 } else { 1 << (n - 1) };
+        self.vars.borrow_mut().iter_mut().for_each(|(var, val)| {
+            // Extract the variable value from the bits of number v which is increased for each line
+            let b = v & bit != 0;
+            *val = b;
+            let t = if b { "T" } else { "F" };
+            print!("{t:w$} | ", w = var.len());
+            bit >>= 1;
+        });
+        let b = proposition.calculate_value(&self.vars.borrow())?;
+        let t = if b { "T" } else { "F" };
+        print!(" {t}");
+        println!();
+        Ok(())
+    }
+}