diff --git a/LICENSE.md b/2016/LICENSE.md similarity index 100% rename from LICENSE.md rename to 2016/LICENSE.md diff --git a/2016/README.md b/2016/README.md new file mode 100644 index 0000000..9202b0d --- /dev/null +++ b/2016/README.md @@ -0,0 +1,20 @@ +# Handy Logic Doodahs-Truth Trees +## Authors +2016: +Matt Peveler + +## About +This is a flask app (with a python module backing it) that can be used to solve generate a truth tree for any given number of formulas and one goal. This is part of the handy logic doodahs series of Automated Theorem Provers. + +![Flask App](https://raw.githubusercontent.com/MasterOdin/TruthTrees/master/static/screenshot.png) + +It uses a functional format for inputting logical formulas. This is the base identity for inputs: +``` +A +not(A) +and(A, B) +or(A, B) +if(A, B) +iff(A, B) +``` +where `A` and `B` can either be atomic statements or a functional operator. All operators are either unary (not) or binary (and, or, if, iff) and there is no support for a generalized notation. This means that ```and(A, B, C)``` will thrown an error. diff --git a/server.py b/2016/server.py similarity index 100% rename from server.py rename to 2016/server.py diff --git a/static/favicon.ico b/2016/static/favicon.ico similarity index 100% rename from static/favicon.ico rename to 2016/static/favicon.ico diff --git a/static/github-mark.png b/2016/static/github-mark.png similarity index 100% rename from static/github-mark.png rename to 2016/static/github-mark.png diff --git a/static/screenshot.png b/2016/static/screenshot.png similarity index 100% rename from static/screenshot.png rename to 2016/static/screenshot.png diff --git a/templates/error.html b/2016/templates/error.html similarity index 100% rename from templates/error.html rename to 2016/templates/error.html diff --git a/templates/footer.html b/2016/templates/footer.html similarity index 100% rename from templates/footer.html rename to 2016/templates/footer.html diff --git a/templates/form.html b/2016/templates/form.html similarity index 100% rename from templates/form.html rename to 2016/templates/form.html diff --git a/templates/header.html b/2016/templates/header.html similarity index 100% rename from templates/header.html rename to 2016/templates/header.html diff --git a/templates/index.html b/2016/templates/index.html similarity index 100% rename from templates/index.html rename to 2016/templates/index.html diff --git a/templates/node.html b/2016/templates/node.html similarity index 100% rename from templates/node.html rename to 2016/templates/node.html diff --git a/templates/tree.html b/2016/templates/tree.html similarity index 100% rename from templates/tree.html rename to 2016/templates/tree.html diff --git a/truthtrees.py b/2016/truthtrees.py similarity index 100% rename from truthtrees.py rename to 2016/truthtrees.py diff --git a/2019/LICENSE.md b/2019/LICENSE.md new file mode 100644 index 0000000..2472024 --- /dev/null +++ b/2019/LICENSE.md @@ -0,0 +1,21 @@ +The MIT License (MIT) + +Copyright (c) 2016 Matthew Peveler + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. \ No newline at end of file diff --git a/2019/README.md b/2019/README.md new file mode 100644 index 0000000..062c405 --- /dev/null +++ b/2019/README.md @@ -0,0 +1,30 @@ +# Handy Logic Doodahs-Truth Trees Manual Creation +## Authors +2016: +Matt Peveler + +2019: +Ji hann Hong +Terry Nguyen + +## About +This is a flask app (with a python module backing it) that can be used to manually create a truth tree. + +This project is built off of Matt Peveler's Handy Logic Doodas-Truth Trees program. +https://github.com/Bram-Hub/HLD-TT + +GitLab repository. +https://gitlab.com/GHanSolo42/truth_tree + +![Flask App](https://raw.githubusercontent.com/MasterOdin/TruthTrees/master/static/screenshot.png) + +It uses a functional format for inputting logical formulas. This is the base identity for inputs: +``` +A +not(A) +and(A, B) +or(A, B) +if(A, B) +iff(A, B) +``` +where `A` and `B` can either be atomic statements or a functional operator. All operators are either unary (not) or binary (and, or, if, iff) and there is no support for a generalized notation. This means that ```and(A, B, C)``` will thrown an error. diff --git a/2019/__init__.py b/2019/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/2019/cli_manual_entry b/2019/cli_manual_entry new file mode 100644 index 0000000..00d0044 --- /dev/null +++ b/2019/cli_manual_entry @@ -0,0 +1,49 @@ +$ Welcome to the truth tree project + +tree/ $ make_root +Creating Root +type \stop to stop adding statements + +tree/ $ Statement 1 -> A +tree/ $ Statement 2 -> iff(A, B) +tree/ $ Statement 3 -> \stop +Done. Going to root +tree/root/ $ \print +(representation of tree) +tree/root/ $ cd ../ +tree/ $ cd root +tree/root/ $ +tree/root/ $ \branch +Creating branch based on what? + +1: A +2: iff(A, B) + +tree/root/ $ Branching on -> 2 +Creating branches 2.1 and 2.2 +tree/root/2.1/ $ cd ../ +tree/root/ $ cd 2.2 +tree/root/2.2/ $ make_statements +Adding statements +type \stop to stop adding statements +tree/root/2.2/ $ -> A +tree/root/2.2/ $ -> B +tree/root/2.2/ $ -> \stop +tree/root/2.2/ $ \open +tree/root/2.2/ marked as open +tree/root/2.2/ (open) $ cd ../ +tree/root/ $ cd 2.1/ +tree/root/2.1/ $ make_statements +Adding statements +type \stop to stop adding statements +tree/root/2.1/ $ -> ~A +tree/root/2.1/ $ -> ~B +tree/root/2.1/ $ -> \stop +tree/root/2.1/ $ \close +tree/root/2.1/ marked as open +tree/root/2.1/ (closed) $ verify +Success! + + + + diff --git a/2019/developmentSpring2019.md b/2019/developmentSpring2019.md new file mode 100644 index 0000000..267965b --- /dev/null +++ b/2019/developmentSpring2019.md @@ -0,0 +1,37 @@ +# Goal +The goal of the project is to create a replacement or alternative to the +java TruthTree generator on BramHub. + +# Development +Currently, the program allows for basic commands for making the truth tree. +Compared to the java program, users can checkmark off formulas after it has been successfully decompose. + +For this semester, the front end and back end was develop using Matt Peveler work as a base. The tree class was altered to allow for manual editing and verification for marking parents and checkmarking was added. The front end uses flask to give a view of the tree. + +## Currently Known Bugs +* Mark_close is not edit safe + * If a user closes a node based on two formula, and then delete one of the + formula, the node would still be marked as closed. +* Mark_open is not edit safe + * If a user were to verify a branch is open, then delete or add a formula + which violate the branch being open, the branch would remain open. +* Form Resubmission is still allowed + +# Possible Future Improvements +* Use a better formula parser + * forsetti isn't the most reliable +* Print out the parent formula id after marking parent in Flask App + * A Quality of Life change to allow users to know which formula has which parents +* More commands + * Add commands such as edit and export +* Export and Import Tree + * In theory, the history in the TreeShell class can be exported text file + * Then this text file can be used to recreate the tree +* Create an adapter that takes in formula input and change it into something forsetti can parse + * Allow user to type (a & b) instead of and(a,b) +* Refactor to eliminate duplicates due to color classes, styles +* Re-integrate auto-solve truth tree from original fork +* Center the Tree in CSS +* Bi-conditionals should be tested more + + diff --git a/2019/how to use.md b/2019/how to use.md new file mode 100644 index 0000000..dd9d3f1 --- /dev/null +++ b/2019/how to use.md @@ -0,0 +1,100 @@ +# Languages used +Back-end: Python3.6+ +Front-end: HTML, Javascript + +# How to install: +1. Clone the repository into a folder +2. Install requirements + 1. ```pip install -r requirements.txt``` + +# How to run server: + * Set up Python path + * Linux: ```export PYTHONPATH=${PYTHONPATH}:/truth_tree``` + * Run web_server.py in the src folder and go to the ip address + * ```python3.6 web_server.py``` + * Development Mode (Auto-Template Refresh) ```FLASK_APP=web_server_test.py FLASK_DEBUG=1 python3.6 -m flask run``` + * Insert commands into Command to create the tree + * Try typing ```help``` + +# How to run cli: + * Set up Python path + * Linux: ```export PYTHONPATH=${PYTHONPATH}:/truth_tree``` + * Run cli.py in the src folder + * ```python3.6 cli.py``` + +# How to run tests: + * Set up Python path + * Linux: ```export PYTHONPATH=${PYTHONPATH}:/truth_tree``` + * Move into tests folder + * Run a tests file + * Example: ```python3.6 tests.py``` + +# Current Supported Commands: +* add_root_formula + * Add a "premise" to the truth tree + * Command to add a & b as a premise: + * add_root_formula and(a,b) + * Command to add c | (d & e) as a premise: + * add_root_formula or(c, and(d,e)) +* add_formula + * Add a formula to the current node + * Command to add a | b: + * add_formula or(a,b) + * Command to add ac -> bd: + * add_formula if(ac,bd) +* go_to + * Change the current node + * Command to set node 2 as current node: + * go_to 2 + * Command to set node 1 as current node: + * go_to 1 + +* delete_formula + * Delete a formula using the formula id + * Command to delete formula 1: + * delete_formula 1 + +* undo + * Undo the last command + * Command to undo + * undo + +* redo + * Redo a command + * Command to redo + * redo + +* close + * Close the current node using formula's in its ancestry + * Closing current node using formula 5 and 3: + * close 5 3 + +* branch + * Branch on the current node using a formula + * Command to branch on current node using formula 1: + * branch 1 + +* mark_parent + * Allow user to mark the parent of a formula + * Command to set formula 5 parent as 3 + * mark_parent 5 1 + +* checkmark + * Allow user to checkmark a formula after decomposing it + * Command to checkmark formula 3 + * checkmark 3 + +* mark_open + * Allow user to mark the current node as open + * Command to mark open + * Mark open + +* check_all_closed: + * Allow user to check if all branches have been closed properly + * Command to check + * check_all_closed + +* reset: + * Reset the tree. (WARNING will not be able to undo) + * Reset + * reset \ No newline at end of file diff --git a/2019/notation.md b/2019/notation.md new file mode 100644 index 0000000..b0f1c3e --- /dev/null +++ b/2019/notation.md @@ -0,0 +1,6 @@ +and(A, B) is equivalent to (A and B) +or(A, B) is equivalent to (A or B) +not(A) is equivalent ~A +if(A, B) is equivalent to (A -> B) +iff(A, B) is equivalent to (A <-> B) + diff --git a/2019/requirements.txt b/2019/requirements.txt new file mode 100644 index 0000000..586c145 --- /dev/null +++ b/2019/requirements.txt @@ -0,0 +1,2 @@ +flask +forseti diff --git a/2019/src/Example/Example1.txt b/2019/src/Example/Example1.txt new file mode 100644 index 0000000..86af218 --- /dev/null +++ b/2019/src/Example/Example1.txt @@ -0,0 +1,16 @@ +add_root_formula(if(K, not(K))) +add_root_formula(not(not(K))) +add_formula(K) +mark_parent 3 2 +checkmark 2 +branch 1 +go_to 2 +add_formula(not(K)) +mark_parent 4 1 +close 4 3 +go_to 3 +add_formula(not(K)) +mark_parent 5 1 +close 5 3 +checkmark 1 +check_all_closed \ No newline at end of file diff --git a/2019/src/Example/Example2.txt b/2019/src/Example/Example2.txt new file mode 100644 index 0000000..f2addf7 --- /dev/null +++ b/2019/src/Example/Example2.txt @@ -0,0 +1,13 @@ +add_root_formula(if(R, R)) +add_root_formula(not(R)) +branch 1 +go_to 2 +add_formula(not(R)) +mark_parent 3 1 +go_to 3 +add_formula R +mark_parent 4 1 +checkmark 1 +close 4 2 +go_to 2 +mark_open diff --git a/2019/src/__init__.py b/2019/src/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/2019/src/cli.py b/2019/src/cli.py new file mode 100644 index 0000000..c799268 --- /dev/null +++ b/2019/src/cli.py @@ -0,0 +1,852 @@ +import cmd +import forseti.parser +import shlex +import sys + +from src import truthtrees +from src import util +from src import treeformulas + + +class TreeShell(cmd.Cmd): + def __init__(self, completekey='tab', stdin=None, stdout=None): + super().__init__(completekey=completekey, stdin=stdin, stdout=stdout) + self.intro = "Welcome to the tree shell.\nType help or ? to list commands.\n" + self.prompt = "~/ $ " + self.tree = truthtrees.TruthTree() + self.root = self.tree.root + self.current_node = self.root + self.history = list() + self.history_arg = list() + self.current_command = 0 + self.PREMISE_FORMULA = truthtrees.TreeFormula(None, "PREMISE", 0, 0) + self.PREMISE_FORMULA.valid = True + self.finish = False + + def do_reset(self, arg): + """ + Allow the user to reset the tree. + WARNING: Cannot be undone + + Usage: + reset + """ + self.reset() + + def reset(self): + """ + Reset the tree and the history + """ + self.intro = "Welcome to the tree shell.\nType help or ? to list commands.\n" + self.prompt = "~/ $ " + self.tree = truthtrees.TruthTree() + self.root = self.tree.root + self.current_node = self.root + self.history = list() + self.history_arg = list() + self.current_command = 0 + self.finish = False + print("Resetting tree and command history", file=self.stdout) + print(str(self.intro), file=self.stdout) + + def add_history(self, command, his_arg): + """ + @param: command is a string corresponding to the command being stored into history + @param: his_arg is a string the argumenent needed for undo-redo + """ + if self.current_command == 0: + self.history.clear() + self.history_arg.clear() + self.history.append(command) + self.history_arg.append(his_arg) + else: + g = self.history[0:self.current_command] + g.append(command) + self.history = g + v = self.history_arg[0: self.current_command] + v.append(his_arg) + self.history_arg = v + self.current_command += 1 + + def delete_leaf_branch_helper(self, argument): + """ + Delete the branch of a node only if its children are leaf nodes + @param: argument contains the unique id of the children sepereated by a space + @effect: The nodes with those unique id are deleted from the tree + """ + parent_unique_id, child_u_ids = util.history_parser(argument) + child_u_id1, child_u_id2 = util.history_parser(child_u_ids) + node = util.return_element_from_list(int(parent_unique_id), self.tree.node_memory) + print(len(self.tree.node_memory)) + self.tree.delete_node(int(child_u_id2)) + self.tree.delete_node(int(child_u_id1)) + node.children.clear() + + def do_delete_branch(self, arg): + """ + Delete branch on current node. + Current node children must be leaves + + Usage: + delete_branch + """ + if len(self.current_node.children) == 0: + print("Current node has no children", file=self.stdout) + return + + child1 = self.current_node.children[0] + child2 = self.current_node.children[1] + + if len(child1.children) != 0 or len(child2.children) != 0: + print("Current node's children are not leaves", file=self.stdout) + return + + self.tree.delete_node(child2.unique_id) + self.tree.delete_node(child1.unique_id) + print(f"Deleted node {child1.node_id} and {child2.node_id}", file=self.stdout) + self.add_history(f"delete_branch", f"{self.current_node.unique_id} {child1.unique_id} {child2.unique_id}") + return + + def delete_formula_again(self, arguments): + """ + Helper function to help delete a formula again. Used for redo and undo. + + @param: arguments is the unique_id of the formula to be deleted + """ + tf = util.return_element_from_list(int(arguments), self.tree.formulas_memory) + self.tree.delete_formula(tf) + + def redo_branch(self, arguments): + """ + Helper function to redo a branch again. + + arguments: + argument is in the form "[parent_unique__id] [child_unique_id1] [child_unique_id2]" + """ + parent_u_id, child_nodes = util.history_parser(arguments) + child1_u_id, child2_u_id = util.history_parser(child_nodes) + parent_node = util.return_element_from_list(int(parent_u_id), self.tree.node_memory) + + self.tree.readd_node(child1_u_id) + self.tree.readd_node(child2_u_id) + self.tree.readjust_formula_id() + + def do_go_to(self, arg): + """ + Moves to a node + + Usage: go_to [node_id] + """ + if not arg.isdigit(): + print(f"Invalid argument: {arg}", file=self.stdout) + return + + node_id = int(arg) + n = util.return_element_from_list(node_id, self.tree.nodes) + if n is None: + print(f"Node {node_id} does not exist", file=self.stdout) + return + + print(f"Going to node {node_id}", file=self.stdout) + self.add_history(f"go_to {node_id}", f"{self.current_node.node_id}") + self.current_node = self.tree.nodes[node_id] + return + + def do_print_tree(self, arg): + """ + Print the Tree to the cli + + Usage: + print_tree + """ + tree = self.tree.print() + return tree + + def do_print_current_node(self, arg): + """ + Print the current node to the cli + + Usage: + print_current_node + """ + self.current_node.print() + + def do_add_root_formula(self, arg): + """ + Add formula to the root + + Usage: + add_root_formula [formula] + """ + if self.root.closed: + print("Root node is closed", file=self.stdout) + return + formula, error = util.parse_formula(arg) + arg = arg.replace(' ','') + if formula: + print(f"Adding formula {formula} as {len(self.tree.formulas)}", file=self.stdout) + tf = self.tree.add_premise_formula(arg, formula) + tf.parent = self.PREMISE_FORMULA + tf.valid = True + self.add_history(f"add_root_formula {arg}", f"{tf.unique_id}") + return + print(f"{error}", file=self.stdout) + return + + def do_add_formula(self, arg): + """ + Add formula to the root + + Usage: + add_formula [formula] + """ + if self.current_node.closed: + print("Current node is closed", file=self.stdout) + return + # Validate Formula + formula, error = util.parse_formula(arg) + if formula: + arg = arg.replace(' ','') + print(f"Adding formula {formula} as {len(self.tree.formulas)}", file=self.stdout) + tf = self.tree.add_formula(self.current_node, arg, formula) + self.add_history(f"add_formula {arg}", f"{tf.unique_id}") + return + print(f"{error}", file=self.stdout) + return + + def do_delete_formula(self, arg): + """ + Delete formula based on id + + Usage: + delete_formula [formula_id] + """ + + if not arg.isdigit(): + print(f"Invalid argument: {arg}") + return + + formula_id = int(arg) + tf = util.return_element_from_list(formula_id, self.tree.formulas) + + if tf is None: + print(f"Formula {formula_id} not found", file=self.stdout) + return + + if len(tf.node_children) > 0: + output_str = "Cannot delete. Formula branched to nodes " + for n in tf.node_children: + output_str += str(n.node_id) + " " + print(output_str, file=self.stdout) + return + + self.tree.delete_formula(tf) + self.add_history(f"delete_formula {tf.node.node_id}", f"{tf.unique_id}") + print( f"Deleting formula {formula_id}", file=self.stdout) + return + + def do_branch(self, arg): + """ + Branch on current node using a formula + + Usage: + branch [formula_id] + """ + if self.current_node.closed: + print("Current Node is closed", file=self.stdout) + return + + if not arg.isdigit(): + print("Invalid Argument", file=self.stdout) + return + + arg = arg.replace(' ','') + tf = util.return_element_from_list(int(arg), self.tree.formulas) + + if tf is None: + print("Formula not found", file=self.stdout) + return + + if not self.current_node.in_ancestry(tf): + print("Formula not in ancestry", file=self.stdout) + return + + main_connector, dummy, dummy = tf.decompose() + if main_connector == "and" or main_connector is None: + print("Formula does not branch", file=self.stdout) + return + + try: + self.tree.branch(self.current_node, tf) + child1 = self.current_node.children[0] + child2 = self.current_node.children[1] + self.add_history(f"branch {arg}", f"{self.current_node.unique_id} {child1.unique_id} {child2.unique_id}") + print(f"branched on node {self.current_node.node_id} to create node {child1.node_id} and {child2.node_id}", file=self.stdout) + except truthtrees.TreeError as te: + print(str(te), file=self.stdout) + return + + def do_print_formulas(self, arg): + """ + Print all of the formula to the cli + + Usage: + print_formulas + """ + self.tree.print_formulas() + + def do_print_history(self, arg): + """ + Print the history of tree commands to the cli + + Usage: + print_history + """ + print("\n\nHistory:") + for i in range(len(self.history)): + if self.history[i]: + print(f"{i}: {self.history[i]}") + + def do_EOF(self, arg): + print("\nExiting. Bye-bye") + return True + + def do_undo(self, dummy): + """ + Undo the previous command on the trees + + Usage: + undo + """ + if self.current_command == 0: + print("Nothing to undo", file=self.stdout) + return + self.current_command -= 1 + last_command = self.history[self.current_command] + command, arguments = util.history_parser(last_command) + arg = self.history_arg[self.current_command] + + if command is None: + command = last_command + + if command == "add_root_formula": + tf = util.return_element_from_list(int(arg), self.tree.formulas_memory) + self.tree.delete_formula(tf) + elif command == "add_formula": + self.delete_formula_again(arg) + elif command == "go_to": + self.current_node = self.tree.nodes[int(arg)] + elif command == "branch": + self.delete_leaf_branch_helper(arg) + elif command == "delete_formula": + self.tree.undelete_formula(arg) + elif command == "checkmarked": + tf = util.return_element_from_list(int(arg), self.tree.formulas_memory) + tf.uncheckmark() + elif command == "closed": + node = util.return_element_from_list(int(arg), self.tree.nodes_memory) + node.closed = False + elif command == f"marked_formula_parent": + child_id, parent_id = util.history_parser(arg) + child_f = util.return_element_from_list(int(child_id), self.tree.formulas_memory) + child_f.remove_parent() + elif command == "All_Closed" or command == "Mark_Open": + print("Tree is finished. Nothing to undo.", file=self.stdout) + self.current_command += 1 + return + elif command == f"delete_branch": + self.redo_branch(arg) + else: + print(f"ERROR: Undo for {command} not yet implemented", file=self.stdout) + return + print("undo successful", file=self.stdout) + return + + def do_redo(self, arg): + """ + Redo the previously undo command + + Usage: + redo + """ + if self.current_command >= len(self.history): + print("Nothing to redo", file=self.stdout) + return + else: + last_command = self.history[self.current_command] + command, arguments = util.history_parser(last_command) + arg = self.history_arg[self.current_command] + + if command is None: + command = last_command + + if command == "add_root_formula": + self.tree.undelete_formula(arg) + elif command == "add_formula": + self.tree.undelete_formula(arg) + elif command == "go_to": + self.current_node = self.tree.nodes[int(arguments)] + elif command == "branch": + self.redo_branch(arg) + elif command == "delete_formula": + self.delete_formula_again(arg) + elif command == "checkmarked": + tf = util.return_element_from_list(int(arg), self.tree.formulas_memory) + tf.checkmark() + elif command == "closed": + node = util.return_element_from_list(int(arg), self.tree.formulas_memory) + node.closed = True + elif command == f"marked_formula_parent": + child_id, parent_id = util.history_parser(arguments) + parent_f = util.return_element_from_list(int(parent_id), self.tree.formulas) + child_f = util.return_element_from_list(int(child_id), self.tree.formulas) + parent_f.children.append(child_f) + child_f.parent = parent_f + if parent_f.valid: + child_f.valid = True + child_f.mark_child_valid() + elif command == "All_Closed" or command == "Mark_Open": + print("Tree is finished. Nothing to undo.", file=self.stdout) + self.current_command -= 1 + return + elif command == "delete_branch": + self.delete_leaf_branch_helper(arg) + else: + print(f"ERROR: Redo for {command} not yet implemented", file=self.stdout) + return + self.current_command += 1 + print("redo successful", file=self.stdout) + return + + def do_mark_parent(self, arg): + """ + Mark a parent for a formula + + Usage: + mark_formula [child_node] [parent_node] + """ + output_string = "" + child_id, parent_id = util.history_parser(arg) + if child_id is None: + print("Invalid Argument. Needs two arguments", file=self.stdout) + return + child_id.replace(' ','') + parent_id.replace(' ','') + if not parent_id.isdigit(): + print(f"Invalid Argument {parent_id}", file=self.stdout) + return + if not child_id.isdigit(): + print(f"Invalid Argument {child_id}", file=self.stdout) + return + if child_id <= parent_id: + print("Child Node should have id greater then parent", file=self.stdout) + return + parent_formula = util.return_element_from_list(int(parent_id), self.tree.formulas) + child_formula = util.return_element_from_list(int(child_id), self.tree.formulas) + if parent_formula is None: + print(f"Formula {parent_id} not found", file=self.stdout) + return + if child_formula is None: + print(f"Formula {child_id} not found", file=self.stdout) + return + if child_formula.parent and child_formula.parent.arg == "PREMISE": + print(f"Formula {child_id} is a premise and therefore does not need a parent", file=self.stdout) + return + + if parent_formula == child_formula: + parent_formula.add_formula_children(child_formula) + print( f"Marked formula {child_id}'s parent as {parent_id}", file=self.stdout) + self.add_history(f"marked_formula_parent {child_id} {parent_id}", f"{child_formula.unique_id} {parent_formula.unique_id}") + return + if parent_formula.in_decomposition(child_formula): + main_connector, dummy, dummy = parent_formula.decompose() + if main_connector == "or" or main_connector == "if": + if child_formula.node.parent_formula is None: + string = f"Cannot decompose parent_formula into root node" + print(string, file=self.stdout) + return + if child_formula.node.parent_formula is None or child_formula.node.parent_formula != parent_formula: + print(f"Node decomposed from {child_formula.node.parent_formula.formula_id} not {parent_formula.formula_id}", file=self.stdout) + return + parent_formula.add_formula_children(child_formula) + print( f"Marked formula {child_id}'s parent as {parent_id}", file=self.stdout) + self.add_history(f"marked_formula_parent {child_id} {parent_id}", f"{child_formula.unique_id} {parent_formula.unique_id}") + return + + string = f"Formula {child_formula} does not decompose from {parent_formula} " + print(string, file=self.stdout) + return + + def do_close(self, arg): + """ + Closes Current Node using formula from it's ancestry + + Usage: + close [formula_id1] [formula_id2] + """ + child_id, parent_id = util.history_parser(arg) + if child_id is None: + return "Invalid Argument. Needs two arguments" + child_id.replace(' ','') + parent_id.replace(' ','') + + # Error checking + if not child_id.isdigit(): + print(f"Invalid Argument {child_id}") + return + if not parent_id.isdigit(): + print(f"Invalid Argument {parent_id}") + return + + formula_1 = util.return_element_from_list(int(parent_id), self.tree.formulas) + formula_2 = util.return_element_from_list(int(child_id), self.tree.formulas) + + # Error Checking + if not formula_1: + print(f"Formula {parent_id} not found", file=self.stdout) + return + if not formula_2: + print(f"Formula {child_id} not found", file=self.stdout) + return + if not formula_1.valid: + print(f"Formula {parent_id} does not have parent", file=self.stdout) + return + if not formula_2.valid: + print(f"Formula {child_id} does not have parent", file=self.stdout) + return + if not self.current_node.in_ancestry(formula_1): + print(f"Formula {parent_id} is not in acestory of current node", file=self.stdout) + return + if not self.current_node.in_ancestry(formula_2): + print(f"Formula {child_id} is not in acestory of current node", file=self.stdout) + return + + #Checking if negation of formula 1 equal formula 2 + not_formula_1 = truthtrees.TreeFormula(f"not({formula_1.arg})", "d") + if not_formula_1 == formula_2: + self.current_node.closed = True + print(f"Current Node Successfully Closed", file=self.stdout) + self.add_history(f"closed {self.current_node.node_id}", None) + return + else: + print(f"Formula are not negation of each other", file=self.stdout) + return + + def do_reopen(self, arg): + """ + Reopen a closed node + + Usage: + reopen [node-id] + """ + if arg.isdigit(): + node =util.return_element_from_list(int(arg), self.tree.nodes) + if node is None: + print(f"Node {arg} not found", file=self.stdout) + elif node.closed: + node.closed = False + self.add_history(f"reopen {arg}", None) + print(f"reopen {arg}", file=self.stdout) + else: + print(f"Node {arg} not closed", file=self.stdout) + else: + print(f"Invalid Argument", file=self.stdout) + return + + def and_check(self,formula, formula_l, node, in_current): + """ + Helper function for checkmark + Go through the tree and check if the formula list are in the correct position of the tree + """ + if node.closed: + return True + #Collecting + for f in formula_l: + if f.node.node_id == node.node_id: + in_current.append(f) + + if len(in_current) == 1: + if in_current[0] == formula: + return True + + if len(in_current) >= 2: + and_total = f"and({in_current[0].arg},{in_current[1].arg})" + if truthtrees.TreeFormula(and_total, "d") == formula: + return True + + for i in range(2,len(in_current)): + if truthtrees.TreeFormula(f"and({and_total},{in_current[i].arg})", "d") == formula: + return True + + if len(node.children) == 0: + return False + l = list(in_current) + r = list(in_current) + return self.and_check(formula, formula_l, node.children[0],l) and self.and_check(formula, formula_l, node.children[1],r) + + def or_check(self, formula, formula_l, node): + """ + Helper function for checkmark + Go through the tree and check if the formula list are in the correct position of the tree + """ + if node.closed: + return True + if len(node.children) == 0: + print(f"Not branched on {node.node_id}") + return False + + #Collecting + in_left = list() + in_right = list() + left_child_id = node.children[0].node_id + right_child_id = node.children[1].node_id + for f in formula_l: + if f.node.node_id == left_child_id: + if f.node.parent_formula.unique_id != formula.unique_id: + return False + in_left.append(f) + if f.node.node_id == right_child_id: + if f.node.parent_formula.unique_id != formula.unique_id: + return False + in_right.append(f) + + if len(in_left) > 0 and len(in_right) > 0: + left_conjunction = "" + right_conjunction ="" + + if len(in_left) >= 2: + left_conjunction = f"and({in_left[0].arg},{in_left[1].arg})" + for i in range(2, len(in_left)): + left_conjunction = f"and({in_left[i].arg},{left_conjunction})" + + if len(in_right) >= 2: + right_conjunction = f"and({in_right[0].arg},{in_right[1].arg})" + for i in range(2, len(in_right)): + right_conjunction = f"and({in_right[i].arg},{right_conjunction})" + + if len(in_right) == 1: + right_conjunction = in_right[0].arg + + if len(in_left) == 1: + left_conjunction = in_left[0].arg + + if truthtrees.TreeFormula(f"or({left_conjunction},{right_conjunction})", "d") == formula: + return True + + return self.or_check(formula, formula_l, node.children[0]) and self.or_check(formula, formula_l, node.children[1]) + + def do_checkmark(self, arg): + """ + Checkmark a formula based on it's children + + Usage: + checkmark [node-id] + """ + # Error checking + if not arg.isdigit(): + print(f"Invalid Argument {arg}") + return + + formula_1 = util.return_element_from_list(int(arg), self.tree.formulas) + node = util.return_element_from_list(formula_1.node.node_id, self.tree.nodes) + + # Error checking + if formula_1 is None: + print(f"Formula {arg} not found", file=self.stdout) + return + + # Formula is already checkmarked + if formula_1.checkmarked: + print(f"Formula {arg} is already heckmarked", file=self.stdout) + return + + # Checking if checkmark is possible + main_connector, arg1, arg2 = formula_1.decompose() + if main_connector is None: + formula_1.checkmark() + print(f"Formula {arg} checkmarked", file=self.stdout) + self.add_history(f"checkmarked {arg}", f"{formula_1.unique_id}") + return + elif main_connector == "and": + in_current = list() + if self.and_check(formula_1, formula_1.children, node, in_current): + formula_1.checkmark() + print(f"Formula {arg} checkmarked", file=self.stdout) + self.add_history(f"checkmarked {arg}", f"{formula_1.unique_id}") + return + else: + print(f"Cannot checkmark", file=self.stdout) + return + elif main_connector == "or": + if self.or_check(formula_1, formula_1.children, node): + formula_1.checkmark() + print(f"Formula {arg} checkmarked", file=self.stdout) + self.add_history(f"checkmarked {arg}", f"{formula_1.unique_id}") + return + else: + print(f"Cannot checkmark", file=self.stdout) + return + # Checking for iff + else: + in_current = list() + if self.or_check(formula_1, formula_1.children, node): + formula_1.checkmark() + print(f"Formula {arg} checkmarked", file=self.stdout) + self.add_history(f"checkmarked {arg}", f"{formula_1.unique_id}") + return + elif self.and_check(formula_1, formula_1.children, node, in_current): + formula_1.checkmark() + print(f"Formula {arg} checkmarked", file=self.stdout) + self.add_history(f"checkmarked {arg}", f"{formula_1.unique_id}") + return + else: + print(f"Cannot checkmark", file=self.stdout) + return + + def find_path(self, n, l): + """ + Helper Function for mark open. + Store the path from the current node to the root node + + @return: A list of node_id that is in the path from the current node to the root + """ + l.insert(0, n.node_id) + if n.node_id == 1: + return + self.find_path(n.parent, l) + + def do_mark_open(self, arg): + """ + Mark the current node as open + + Usage: + mark_open + """ + if len(self.current_node.children) != 0: + print("Current Node has children", file=self.stdout) + return + + path_to_root = list() + self.find_path(self.current_node, path_to_root) + for node_id in path_to_root: + node = util.return_element_from_list(node_id, self.tree.nodes) + for formula in node.formulas: + if formula.checkmarked: + continue + if formula.parent is None: + print(f"Formula {formula.formula_id} doesn't have a parent", file=self.stdout) + return + main_connector, decom1, decom2 = formula.decompose() + if main_connector is None: + continue + + if len(formula.children) == 0: + string = f"Formula {formula.formula_id} has not decomposed" + print(string, file=self.stdout) + return + + and_conjecture = "" + for f in formula.children: + if f.node.node_id in path_to_root: + if and_conjecture == "": + and_conjecture = f.arg + else: + and_conjecture = f"and({and_conjecture},{f.arg})" + if main_connector == "and": + if truthtrees.TreeFormula(and_conjecture, "d") == formula: + continue + else: + print(f"Incorrect decomposition of {formula.formula_id}", file=self.stdout) + return + if main_connector == "or": + if formula.in_decomposition(truthtrees.TreeFormula(and_conjecture, "d")): + count = 0 + for cn in formula.node_children: + if cn.node_id in path_to_root: + count += 1 + if count == 0: + string = f"{formula.formula_id} has not been decomposed into this branch yet" + print(string, file=self.stdout) + return + continue + else: + print(f"Incorrect decomposition of {formula.formula_id}", file=self.stdout) + return + else: + if truthtrees.TreeFormula(and_conjecture, "d") == formula: + continue + if formula.in_decomposition(truthtrees.TreeFormula(and_conjecture, "d")): + continue + else: + print(f"Incorrect decomposition of {formula.formula_id}", file=self.stdout) + return + self.finish = True + self.add_history("Mark_Open", None) + self.current_node.open = True + print(f"Finish. Path to {self.current_node.node_id} open.", file=self.stdout) + return + + def find_closed_branch(self, node): + """ + Helper function for check all closed + + """ + if node.parent_formula is not None and not node.parent_formula.checkmarked: + return False, f"Formula {node.parent_formula.formula_id} is not checkmarked" + if len(node.children) == 0: + if node.closed: + return True, None + else: + return False, f"Node {node.node_id} not closed" + success1, failure1 = self.find_closed_branch(node.children[0]) + success2, failure2 = self.find_closed_branch(node.children[1]) + if success1 and success2: + return True, None + if success1: + return False, failure2 + return False, failure1 + + def do_check_all_closed(self, arg): + """ + Check if all branches are closed + + Usage: + check_all_closed + """ + success, failure = self.find_closed_branch(self.root) + if success: + self.finish = True + self.add_history("All_Closed", None) + print(f"Finish. All Branches closed", file=self.stdout) + return "True" + print(failure, file=self.stdout) + return "False" + + def do_check_any_open(self, arg): + """ + Check if any branches are open + + Usage: + check_any_open + """ + success = False + for node in self.tree.nodes: + if node is None: + continue + if len(node.children) == 0: + if node.open: + success = True + if success: + self.finish = True + self.add_history("1_Open", None) + print(f"Finish. At least 1 branch open", file=self.stdout) + return "True" + else: + print("No Branches Marked Open.", file=self.stdout) + return "False" + +if __name__ == '__main__': + try: + TreeShell(stdout=sys.stdout).cmdloop() + except KeyboardInterrupt: + print("\nExiting. Bye-bye") diff --git a/2019/src/static/favicon.ico b/2019/src/static/favicon.ico new file mode 100644 index 0000000..7aa48e8 Binary files /dev/null and b/2019/src/static/favicon.ico differ diff --git a/2019/src/static/github-mark.png b/2019/src/static/github-mark.png new file mode 100644 index 0000000..8b25551 Binary files /dev/null and b/2019/src/static/github-mark.png differ diff --git a/2019/src/static/screenshot.png b/2019/src/static/screenshot.png new file mode 100644 index 0000000..53a6ad3 Binary files /dev/null and b/2019/src/static/screenshot.png differ diff --git a/2019/src/static/style.css b/2019/src/static/style.css new file mode 100644 index 0000000..eaa32a1 --- /dev/null +++ b/2019/src/static/style.css @@ -0,0 +1,126 @@ +html { + margin: 0px; +} + +header { + margin: 0; + padding: 0; +} + +h1, h2, p { + margin: 0; +} + +body { + margin: 0px; + padding: 0px; + border: 0px; + height: 100vh; +} + +.tree { + overflow: hidden; +} + +.tree ul { + padding-top: 20px; + position: relative; + transition: all 0.5s; + -webkit-transition: all 0.5s; + -moz-transition: all 0.5s; + + /* overflow: hidden; */ +} + +.tree li { + float: left; + margin: 0 auto; + + text-align: center; + list-style-type: none; + position: relative; + padding: 20px 5px 0 5px; + + transition: all 0.5s; + -webkit-transition: all 0.5s; + -moz-transition: all 0.5s; +} + +.tree li::before, .tree li::after{ + content: ''; + position: absolute; + top: 0; + right: 50%; + border-top: 1px solid #ccc; + width: 50%; + height: 20px; +} +.tree li::after{ + right: auto; + left: 50%; + border-left: 1px solid #ccc; +} + +.tree li:only-child::after, .tree li:only-child::before { + display: none; +} + +.tree li:only-child{ padding-top: 0;} + +.tree li:first-child::before, .tree li:last-child::after{ + border: 0 none; +} +.tree li:last-child::before{ + border-right: 1px solid #ccc; + border-radius: 0 5px 0 0; + -webkit-border-radius: 0 5px 0 0; + -moz-border-radius: 0 5px 0 0; +} +.tree li:first-child::after{ + border-radius: 5px 0 0 0; + -webkit-border-radius: 5px 0 0 0; + -moz-border-radius: 5px 0 0 0; +} +.tree ul ul::before{ + content: ''; + position: absolute; top: 0; left: 50%; + border-left: 1px solid #ccc; + width: 0; height: 20px; +} + +.yellow{ + background-color: yellow; +} + +.white{ + background-color: white; +} + +.tree li div{ + border: 1px solid #ccc; + padding: 5px 10px; + text-decoration: none; + color: #666; + font-family: arial, verdana, tahoma, serif; + font-size: 15px; + display: inline-block; + + border-radius: 5px; + -webkit-border-radius: 5px; + -moz-border-radius: 5px; + + transition: all 0.5s; + -webkit-transition: all 0.5s; + -moz-transition: all 0.5s; + + +} +.tree li div:hover, .tree li div:hover+ul li div { + background: #c8e4f8; color: #000; border: 1px solid #94a0b4; +} +.tree li div:hover+ul li::after, +.tree li div:hover+ul li::before, +.tree li div:hover+ul::before, +.tree li div:hover+ul ul::before{ + border-color: #94a0b4; +} \ No newline at end of file diff --git a/2019/src/templates/formula_black.html b/2019/src/templates/formula_black.html new file mode 100644 index 0000000..9aa423b --- /dev/null +++ b/2019/src/templates/formula_black.html @@ -0,0 +1 @@ +{{ formula }} \ No newline at end of file diff --git a/2019/src/templates/formula_blue.html b/2019/src/templates/formula_blue.html new file mode 100644 index 0000000..ce5bb94 --- /dev/null +++ b/2019/src/templates/formula_blue.html @@ -0,0 +1 @@ +{{ formula }} \ No newline at end of file diff --git a/2019/src/templates/my-form.html b/2019/src/templates/my-form.html new file mode 100644 index 0000000..e456de5 --- /dev/null +++ b/2019/src/templates/my-form.html @@ -0,0 +1,106 @@ + + + + + + + + + +
+
+
+
+

Command Log

+
+
+
    + {% for item in log %} +
  • {{ item }}
    • + {% endfor %} +
+
+
+
+
+

Valid Command History

+
+
+
    + {% for item in command_history %} +
  • {{ item }}
    • + {% endfor %} +
+
+
+
+
+ + {{verify_message }} +
+
+

Tree

+ Yellow Highlight = Current Node, Blue Text = Validated Formula +
+
+
+
    + + {{ tree }} +
+
+
+
+
+
+
+
{{ message }}
+
+
+
+ +
+
+
+
+ +
+
+
+
+ +
+
+
+
+ + + + + + + \ No newline at end of file diff --git a/2019/src/templates/node.html b/2019/src/templates/node.html new file mode 100644 index 0000000..c9d87f0 --- /dev/null +++ b/2019/src/templates/node.html @@ -0,0 +1,15 @@ +
  • +
    + {{ node }}
    + {% for formula in formulas %} + {{ formula }}
    + {% endfor %} +
    + {% if children|length > 0 %} +
      + {% for child in children %} + {{ child }} + {% endfor %} +
    + {% endif %} +
    • \ No newline at end of file diff --git a/2019/src/templates/selected_node.html b/2019/src/templates/selected_node.html new file mode 100644 index 0000000..36feb56 --- /dev/null +++ b/2019/src/templates/selected_node.html @@ -0,0 +1,15 @@ +
  • +
    + {{ node }}
    + {% for formula in formulas %} + {{ formula }}
    + {% endfor %} +
    + {% if children|length > 0 %} +
      + {% for child in children %} + {{ child }} + {% endfor %} +
    + {% endif %} +
    • \ No newline at end of file diff --git a/2019/src/templates/verify_failed.html b/2019/src/templates/verify_failed.html new file mode 100644 index 0000000..4e89407 --- /dev/null +++ b/2019/src/templates/verify_failed.html @@ -0,0 +1,5 @@ +
    + × +

    {{ verify_message }}

    +
    \ No newline at end of file diff --git a/2019/src/templates/verify_success.html b/2019/src/templates/verify_success.html new file mode 100644 index 0000000..18b9a25 --- /dev/null +++ b/2019/src/templates/verify_success.html @@ -0,0 +1,5 @@ +
    + × +

    {{ verify_message }}

    +
    \ No newline at end of file diff --git a/2019/src/tests/__init__.py b/2019/src/tests/__init__.py new file mode 100644 index 0000000..e69de29 diff --git a/2019/src/tests/decompose_test.py b/2019/src/tests/decompose_test.py new file mode 100644 index 0000000..510e455 --- /dev/null +++ b/2019/src/tests/decompose_test.py @@ -0,0 +1,89 @@ +from src.cli import TreeShell +import unittest +from src import util +from src.treeformulas import * + +class TestDecompose(unittest.TestCase): + def test_predicate(self): + connector, decom1, decom2 = decompose_formula_argument("a") + self.assertEqual(connector, None) + self.assertEqual(decom1, "a") + + def test_simple(self): + connector, decom1, decom2 = decompose_formula_argument("A") + self.assertEqual(connector, None) + self.assertEqual(decom1, "A") + + def test_complicated_and(self): + connector, decom1, decom2 = decompose_formula_argument("and(or(a,c),if(b,c))") + self.assertEqual(connector, "and") + self.assertEqual(decom1, "or(a,c)") + self.assertEqual(decom2, "if(b,c)") + + def test_not(self): + connector, decom1, decom2 = decompose_formula_argument("not(a)") + self.assertEqual(connector, None) + self.assertEqual(decom1, "not(a)") + self.assertEqual(decom2, None) + + def test_not_demorgan(self): + connector, decom1, decom2 = decompose_formula_argument("not(and(a,b))") + self.assertEqual(connector, "or") + self.assertEqual(decom1, "not(a)") + self.assertEqual(decom2, "not(b)") + + connector, decom1, decom2 = decompose_formula_argument("not(or(a,b))") + self.assertEqual(connector, "and") + self.assertEqual(decom1, "not(a)") + self.assertEqual(decom2, "not(b)") + + def test_double_not(self): + connector, decom1, decom2 = decompose_formula_argument("not(not(a))") + self.assertEqual(connector, None) + self.assertEqual(decom1, "a") + self.assertEqual(decom2, None) + + def test_not_conditional(self): + connector, decom1, decom2 = decompose_formula_argument("not(if(a,b))") + self.assertEqual(connector, "and") + self.assertEqual(decom1, "a") + self.assertEqual(decom2,"not(b)") + + def test_not_iff(self): + connector, decom1, decom2 = decompose_formula_argument("not(iff(a,b))") + self.assertEqual(connector, "iff") + self.assertEqual(decom2, "and(a,not(b))") + self.assertEqual(decom1, "and(not(a),b)") + + def test_and(self): + connector, decom1, decom2 = decompose_formula_argument("and(a,b)") + self.assertEqual(connector, "and") + self.assertEqual(decom1, "a") + self.assertEqual(decom2, "b") + + def test_or(self): + connector, decom1, decom2 = decompose_formula_argument("or(1,2)") + self.assertEqual(connector, "or") + self.assertEqual(decom1, "1") + self.assertEqual(decom2, "2") + + def test_if(self): + connector, decom1, decom2 = decompose_formula_argument("if(a,b)") + self.assertEqual(connector, "or") + self.assertEqual(decom1, "not(a)", decom1) + self.assertEqual(decom2, "b", decom2) + + def test_iff(self): + connector, decom1, decom2 = decompose_formula_argument("iff(a,b)") + self.assertEqual(connector, "iff") + self.assertEqual(decom1, "and(a,b)", decom1) + self.assertEqual(decom2, "and(not(a),not(b))", decom2) + + def test_alternate_iff(self): + decom1, decom2 = decompose_iff_into_if("iff(a,b)") + self.assertEqual(decom1, "or(not(a),b)", decom1) + self.assertEqual(decom2, "or(a,not(b))", decom2) + +if __name__ == "__main__": + unittest.main() + diff --git a/2019/src/tests/edit_verify_test.py b/2019/src/tests/edit_verify_test.py new file mode 100644 index 0000000..3c07664 --- /dev/null +++ b/2019/src/tests/edit_verify_test.py @@ -0,0 +1,139 @@ +from src.cli import TreeShell +import unittest + +class TestVerificationEdits(unittest.TestCase): + def test_undo_delete_branch(self): + """ + Testing undo and redo interaction with delete_branch + """ + print("\n\nUndo Test branch delete=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_go_to("1") + + shell.do_delete_branch("") + self.assertEqual(len(shell.tree.formulas[1].children), 0) + self.assertEqual(len(shell.current_node.children), 0) + + shell.do_undo("") + print(shell.tree.formulas) + self.assertEqual(len(shell.tree.formulas[1].children), 1) + self.assertEqual(len(shell.current_node.children), 2) + + def test_checkmark_edits(self): + """ + Testing undo and redo interaction with checkmark system + """ + print("\n\nUndo Test checkmark edit1=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_mark_parent("2 1") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_checkmark("1") + self.assertTrue(shell.tree.formulas[1].checkmarked) + + #Using undo and redo on checkmark + shell.do_undo(None) + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_redo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + + shell.do_delete_formula("2") + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_undo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + shell.do_redo(None) + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_undo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + + def test_checkmark_edits2(self): + """ + Testing delete_formula interaction with checkmark system + """ + print("\n\nUndo Test checkmark edits 2=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("and(a,b)") + shell.do_add_formula("a") + shell.do_mark_parent("2 1") + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_checkmark("1") + self.assertTrue(shell.tree.formulas[1].checkmarked) + + #Using undo and redo on checkmark + shell.do_undo(None) + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_redo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + + shell.do_delete_formula("1") + shell.do_undo(None) + shell.do_delete_formula("2") + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_undo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + + def test_BiCondition(self): + print("\n\nBiconditional Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_formula("iff(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_add_formula("b") + shell.do_go_to("3") + shell.do_add_formula("not(a)") + shell.do_add_formula("not(b)") + shell.do_mark_parent("2 1") + shell.do_mark_parent("3 1") + shell.do_mark_parent("4 1") + shell.do_mark_parent("5 1") + shell.do_checkmark("1") + shell.do_add_root_formula("iff(a,b)") + shell.do_mark_parent("2 1") + shell.do_checkmark("1") + + self.assertTrue(shell.tree.formulas[1].checkmark) + self.assertTrue(shell.tree.formulas[2].checkmark) + for i in range(1, len(shell.tree.formulas)): + self.assertTrue(shell.tree.formulas[i].valid) + + shell.do_undo(None) + self.assertFalse(shell.tree.formulas[1].checkmarked) + shell.do_undo(None) + for i in range(2, len(shell.tree.formulas)): + self.assertFalse(shell.tree.formulas[i].valid, i) + + shell.do_redo(None) + for i in range(2, len(shell.tree.formulas)): + self.assertTrue(shell.tree.formulas[i].valid, i) + + shell.do_redo(None) + self.assertTrue(shell.tree.formulas[1].checkmarked) + shell.do_go_to("2") + shell.do_mark_open("") + self.assertTrue(shell.finish) + + + + +if __name__ == "__main__": + unittest.main() + + diff --git a/2019/src/tests/formula_equality_test.py b/2019/src/tests/formula_equality_test.py new file mode 100644 index 0000000..52b6c1b --- /dev/null +++ b/2019/src/tests/formula_equality_test.py @@ -0,0 +1,92 @@ +from src.cli import TreeShell +from src.truthtrees import TreeFormula +import unittest +import src.util + +class TestFormulaEquality(unittest.TestCase): + def test_and_commutativity(self): + tf = TreeFormula("And(a,b )") + tf2 = TreeFormula("and( b, a)") + self.assertEqual(tf, tf2) + + def test_and_commutativity_complicated(self): + tf = TreeFormula("And(a,and(b,c) )") + tf2 = TreeFormula("and( and(c,b), a)") + self.assertEqual(tf, tf2) + + def test_and_commutativity2(self): + tf = TreeFormula("And(a,and(b,c) )") + tf2 = TreeFormula("and( and(a, b), c)") + self.assertEqual(tf, tf2) + + def test_or_commutativity(self): + tf = TreeFormula("or(a,b )") + tf2 = TreeFormula("OR( b, a)") + self.assertEqual(tf, tf2) + + def test_simple(self): + tf = TreeFormula("a") + tf2 = TreeFormula("A") + self.assertNotEqual(tf, tf2) + + def test_demorgan_and(self): + tf = TreeFormula("not(and(a,b))") + tf2 = TreeFormula("or(not(a),not(b))") + self.assertEqual(tf, tf2) + + def test_demorgan_or(self): + tf = TreeFormula("not(or(a,b))") + tf2 = TreeFormula("and(not(a),not(b))") + self.assertEqual(tf, tf2) + + def test_if(self): + tf = TreeFormula("if(a,b)") + tf2 = TreeFormula("or(not(a),b)") + self.assertEqual(tf, tf2) + + def test_demorgan_if(self): + tf = TreeFormula("not(if(a,b))") + tf2 = TreeFormula("and(a, not(b))") + tf3 = TreeFormula("and(not(b), a)") + self.assertEqual(tf, tf2) + self.assertEqual(tf, tf3) + + def test_complicated_not_if(self): + tf = TreeFormula("not(if(a,b))") + tf2 = TreeFormula("not(or(not(a), b))") + self.assertEqual(tf, tf2) + + def test_iff(self): + tf = TreeFormula("iff(a,b)") + tf2 = TreeFormula("or(and(a,b), and(not(a), not(b)))") + self.assertEqual(tf, tf2) + self.assertEqual(tf2, tf) + + def test_complicated_iff(self): + tf = TreeFormula("iff(a,b)") + tf2 = TreeFormula("and(if(a,b),if(b,a))") + self.assertEqual(tf, tf2) + self.assertEqual(tf2, tf) + + def test_if2(self): + tf = TreeFormula("if(a,b)") + tf2 = TreeFormula("if(b,a)") + self.assertNotEqual(tf, tf2) + + def test_iff2(self): + tf = TreeFormula("iff(a,b)") + tf2 = TreeFormula("iff(b,a)") + self.assertEqual(tf, tf2) + + def test_iff3(self): + tf = TreeFormula("iff(not(a),not(b))") + tf2 = TreeFormula("iff(b,a)") + self.assertEqual(tf, tf2) + + def test_and9(self): + tf = TreeFormula("and(and(a,b),and(b,a))") + tf2 = TreeFormula("and(a,b)") + self.assertEqual(tf, tf2) + +if __name__ == "__main__": + unittest.main() \ No newline at end of file diff --git a/2019/src/tests/in_decomposition_test.py b/2019/src/tests/in_decomposition_test.py new file mode 100644 index 0000000..5ca7475 --- /dev/null +++ b/2019/src/tests/in_decomposition_test.py @@ -0,0 +1,120 @@ +from src.cli import TreeShell +from src.truthtrees import TreeFormula +import unittest +import src.util +import src.treeformulas + + +class TestInDecomposition(unittest.TestCase): + def test_and(self): + form1 = TreeFormula("a") + form2 = TreeFormula("and(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_and2(self): + form1 = TreeFormula("b") + form2 = TreeFormula("and(a,and(b,c))") + self.assertTrue(form2.in_decomposition(form1)) + + def test_and3(self): + form1 = TreeFormula("and(b,c)") + form2 = TreeFormula("and(a,and(b,c))") + self.assertTrue(form2.in_decomposition(form1)) + + def test_or(self): + form1 = TreeFormula("a") + form2 = TreeFormula("or(a,b)") + self.assertTrue( form2.in_decomposition(form1)) + + def test_or2(self): + form1 = TreeFormula("b") + form2 = TreeFormula("or(a,or(b,c))") + self.assertTrue(form2.in_decomposition(form1)) + + def test_or3(self): + form1 = TreeFormula("or(b,c)") + form2 = TreeFormula("or(a,or(b,c))") + self.assertTrue(form2.in_decomposition(form1)) + + def test_not_in(self): + form1 = TreeFormula("b") + form2 = TreeFormula("or(a,and(b,c))") + self.assertFalse(form2.in_decomposition(form1)) + + def test_complicated(self): + form1 = TreeFormula("and(a,and(b,c))") + form2 = TreeFormula("or(a,and(b,and(a,c)))") + self.assertTrue( form2.in_decomposition(form1)) + + def test_not_in2(self): + form1 = TreeFormula("b") + form2 = TreeFormula("and(a,or(b,c))") + self.assertFalse( form2.in_decomposition(form1)) + + def test_not_in3(self): + form1 = TreeFormula("b") + form2 = TreeFormula("a") + self.assertFalse( form2.in_decomposition(form1)) + + def test_if(self): + form1 = TreeFormula("a") + form2 = TreeFormula("if(a,b)") + self.assertFalse( form2.in_decomposition(form1)) + + def test_if2(self): + form1 = TreeFormula("or(not(a),b)") + form2 = TreeFormula("if(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_if3(self): + form1 = TreeFormula("or(not(a),b)") + form2 = TreeFormula("if(a,b)") + self.assertTrue(form1.in_decomposition(form2)) + + def test_if4(self): + form1 = TreeFormula("or(if(a,b),b)") + form2 = TreeFormula("if(a,b)") + self.assertTrue(form1.in_decomposition(form2)) + + def test_not_in4(self): + form1 = TreeFormula("or(if(b,a),b)") + form2 = TreeFormula("if(a,b)") + self.assertFalse(form1.in_decomposition(form2)) + + def test_not_iff(self): + form1 = TreeFormula("if(a,b)") + form2 = TreeFormula("iff(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_not_iff2(self): + form1 = TreeFormula("if(b,a)") + form2 = TreeFormula("iff(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_not_iff3(self): + form1 = TreeFormula("a") + form2 = TreeFormula("iff(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_not_iff4(self): + form1 = TreeFormula("not(a)") + form2 = TreeFormula("iff(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_not_iff4(self): + form1 = TreeFormula("or(and(not(a),not(b)),and(a,b))") + form2 = TreeFormula("iff(a,b)") + self.assertTrue(form2.in_decomposition(form1)) + + def test_and7(self): + tf = TreeFormula("and(and(a,b),and(b,a))") + tf2 = TreeFormula("and(a,b)") + self.assertTrue(tf2.in_decomposition(tf)) + + def test_and8(self): + tf = TreeFormula("and(and(a,b),and(b,a))") + tf2 = TreeFormula("and(a,b)") + self.assertTrue(tf.in_decomposition(tf2)) + +if __name__ == "__main__": + unittest.main() \ No newline at end of file diff --git a/2019/src/tests/tests.py b/2019/src/tests/tests.py new file mode 100644 index 0000000..b37b792 --- /dev/null +++ b/2019/src/tests/tests.py @@ -0,0 +1,309 @@ +from src.cli import TreeShell +import unittest + + +class TestCLI(unittest.TestCase): + + def test_history(self): + print("\nHistory Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + print(shell.tree.formulas) + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("not(A)") + shell.do_add_formula("B") + shell.do_go_to("3") + shell.do_add_formula("B") + shell.do_delete_formula("3") + shell.do_go_to("1") + shell.do_delete_branch("") + shell.do_delete_formula("1") + self.assertEqual(len(shell.history), 11) + print("\n\nPrinting History\n\n") + shell.do_print_history("") + + def test_simple_function_deletion(self): + print("\n Deletion Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + print(shell.tree.formulas) + shell.do_add_root_formula("if(A, B)") + shell.do_add_root_formula("if(A, B)") + shell.do_add_formula("if(A, B)") + shell.do_delete_formula("2") + self.assertEqual(len(shell.tree.formulas), 4) + shell.do_delete_formula("1") + self.assertEqual(len(shell.tree.formulas), 3) + shell.do_delete_formula("1") + self.assertEqual(len(shell.tree.formulas), 2) + shell.do_delete_formula("1") + self.assertEqual(len(shell.tree.formulas), 1) # All formulas are deleted at this point + + def test_root_id_set_one(self): + print("\n Root ID Test===================================") + shell = TreeShell() + shell.reset() + # print(f"shell.root.node_id == 1: {shell.root.node_id == 1}") + self.assertEqual(shell.root.node_id, 1) + + def test_can_branch_on_root(self): + print("\n Branch on Root Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("") + + def test_can_traverse_between_nodes(self): + print("\n Node Tranversal Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("1") + shell.do_go_to("2") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_go_to("3") + self.assertEqual(shell.current_node.node_id, 3) + shell.do_go_to("1") + self.assertEqual(shell.current_node.node_id, 1) + + def test_can_add_formula_on_middle_node(self): + print("\n Add Formula in Middle Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("1") + shell.do_go_to("2") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_add_formula("and(C, D)") + + def test_can_branch_on_middle_node(self): + print("\n Branch in Middle Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("1") + shell.do_go_to("2") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_add_formula("and(C, D)") + shell.do_branch("2") + self.assertEqual(len(shell.current_node.children), 0) + shell.do_add_formula("or(C, D)") + shell.do_branch("3") + self.assertEqual(len(shell.current_node.children), 2) + + def test_can_branch_on_middle_node_twice(self): + print("\n Branch in Middle Twice Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("1") + + shell.do_go_to("2") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_print_current_node(None) + + shell.do_add_formula("or(C, D)") + shell.do_branch("2") + + shell.do_go_to("3") + self.assertEqual(shell.current_node.node_id, 3) + shell.do_add_formula("or(E, D)") + shell.do_branch("3") + shell.do_print_tree(None) + + def test_can_branch_on_middle_node_twice2(self): + print("\n Branch in Middle Complicated 2 Test===================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(A, B)") + shell.do_branch("1") + + shell.do_go_to("2") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_print_current_node(None) + + shell.do_add_formula("and(C, D)") + shell.do_add_formula("and(E, G)") + shell.do_add_formula("and(H, J)") + shell.do_add_formula("or(K, L)") + shell.do_branch("5") + + shell.do_go_to("3") + self.assertEqual(shell.current_node.node_id, 3) + shell.do_add_formula("or(E, D)") + shell.do_add_formula("and(P, I)") + shell.do_branch("6") + + shell.do_go_to("7") + shell.do_add_formula("and(Q, T)") + shell.do_add_formula("and(W, Y)") + shell.do_add_formula("and(E, U)") + shell.do_add_formula("and(R, I)") + + shell.do_go_to("4") + shell.do_add_formula("iff(W, Y)") + shell.do_add_formula("iff(E, U)") + shell.do_add_formula("iff(R, I)") + shell.do_print_formulas(None) + + def test_redo(self): + print("\n\nRedo Test=======================================================") + shell = TreeShell() + shell.reset() + + # Testing add_root_formula + shell.do_add_root_formula("if(A, B)") + shell.do_undo("") + shell.do_print_formulas("") + + self.assertEqual(len(shell.tree.formulas), 1) + shell.do_redo("") + self.assertEqual(len(shell.tree.formulas), 2) + shell.do_undo("") + + # Testing add_formula + shell.do_add_formula("if(A, B)") + shell.do_undo("") + + shell.do_redo("") + + self.assertEqual(len(shell.tree.formulas), 2) + shell.do_undo("") + + # Testing go_to + shell.do_add_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_undo("") + + shell.do_redo("") + self.assertEqual(shell.current_node.node_id, 2) + shell.do_undo("") + self.assertEqual(shell.current_node.node_id, 1) + + # Testing branch + shell.do_undo("") + self.assertEqual(len(shell.current_node.children), 0) + shell.do_redo("") + self.assertEqual(len(shell.current_node.children), 2) + shell.do_undo("") + + shell.do_undo("") + + # Testing delete + shell.do_add_formula("and(a, b)") + shell.do_delete_formula("1") + shell.do_undo("") + self.assertNotEqual(len(shell.tree.formulas), 1) + shell.do_redo("") + self.assertEqual(len(shell.tree.formulas), 1) + + shell.do_print_history("") + + def test_undo(self): + print("\n\nUndo Test=======================================================") + shell = TreeShell() + shell.reset() + + # Testing add_root_formula + shell.do_add_root_formula("if(A, B)") + shell.do_undo("") + shell.do_print_formulas("") + self.assertEqual(len(shell.tree.formulas), 1) + + # Testing add_formula + shell.do_add_formula("if(A, B)") + shell.do_undo("") + shell.do_print_formulas("") + self.assertEqual(len(shell.tree.formulas), 1) + + # Testing go_to + shell.do_branch("") + shell.do_go_to("2") + shell.do_undo("") + self.assertEqual(shell.current_node.node_id, 1) + + # Testing branch + shell.do_undo("") + self.assertEqual(len(shell.current_node.children), 0) + + # Testing delete + shell.do_add_root_formula("and(a, b)") + shell.do_delete_formula("1") + shell.do_undo("") + self.assertNotEqual(shell.tree.formulas[1], None) + self.assertEqual(shell.tree.formulas[1].parent.formula, "PREMISE") + + shell.do_undo("") + shell.do_print_current_node("") + + shell.do_add_formula("a") + shell.do_add_formula("b") + shell.do_delete_formula("1") + shell.do_undo(None) + print(shell.current_node) + + def test_undo2(self): + print("\n\nUndo Test=======================================================") + shell = TreeShell() + shell.reset() + + shell.do_add_formula("or(a,b)") + shell.do_add_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("3") + shell.do_add_formula("c") + shell.do_delete_formula("2") + print(shell.tree.formulas) + print(shell.tree.nodes[1]) + + def test_undo3(self): + print("\n\nUndo Test 3=======================================================") + shell = TreeShell() + shell.reset() + + shell.do_add_formula("or(a,b)") + shell.do_add_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("c") + shell.do_go_to("3") + shell.do_add_formula("c") + shell.do_delete_formula("4") + shell.do_delete_formula("3") + shell.do_undo("") + shell.do_delete_formula("3") + shell.do_undo("") + print(shell.tree.formulas) + print(shell.tree.nodes[1]) + + def test_undo4(self): + print("\n\nUndo Test 4=======================================================") + shell = TreeShell() + shell.reset() + + shell.do_add_formula("or(a,b)") + shell.do_add_formula("or(a,b)") + shell.do_branch("1") + shell.do_add_formula("b") + shell.do_delete_formula("3") + shell.do_go_to("2") + shell.do_add_formula("b") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_delete_formula("4") + shell.do_delete_formula("3") + shell.do_delete_formula("2") + shell.do_undo("") + shell.do_undo("") + shell.do_undo("") + shell.do_delete_formula("3") + shell.do_undo("") + print(shell.tree.formulas) + print(shell.tree.nodes[1]) + +if __name__ == "__main__": + unittest.main() \ No newline at end of file diff --git a/2019/src/tests/verify_test.py b/2019/src/tests/verify_test.py new file mode 100644 index 0000000..0e10caa --- /dev/null +++ b/2019/src/tests/verify_test.py @@ -0,0 +1,190 @@ +from src.cli import TreeShell +import unittest +from src import util +import src.treeformulas + +class VerificationTest(unittest.TestCase): + def test_mark_parent_formula(self): + print("\n\nMark Parent Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("and(a,b)") + shell.do_add_formula("a") + shell.do_mark_parent("2 1") + shell.do_mark_parent("1 2") + shell.do_add_formula("and(b,a)") + shell.do_mark_parent("3 1") + shell.do_mark_parent("3 2") + self.assertTrue(util.return_element_from_list(3, shell.tree.formulas).valid) + + def test_closing(self): + print("\n\nClosing Test======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("and(a,b)") + shell.do_add_root_formula("not(a)") + shell.do_add_formula("a") + shell.do_mark_parent("3 1") + shell.do_close("2 3") + + def test_checkmark(self): + print("\n\nCheckmark and Test======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("and(a,b)") + shell.do_add_formula("a") + shell.do_mark_parent("2 1") + shell.do_checkmark("1") + self.assertFalse(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_checkmark("1") + self.assertTrue(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + + def test_checkmark_or(self): + print("\n\nCheckmark OR Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_mark_parent("2 1") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_checkmark("1") + self.assertTrue(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + + def test_checkmark_or_two_layer(self): + print("\n\nCheckmark OR Two Layer Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_add_root_formula("or(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_branch("2") + shell.do_go_to("4") + shell.do_add_formula("a") + shell.do_go_to("5") + shell.do_add_formula("b") + shell.do_mark_parent("3 2") + shell.do_mark_parent("4 2") + shell.do_go_to("3") + shell.do_branch("2") + shell.do_go_to("6") + shell.do_add_formula("b") + shell.do_mark_parent("5 2") + shell.do_go_to("7") + shell.do_add_formula("a") + shell.do_mark_parent("6 2") + shell.do_checkmark("2") + self.assertTrue(util.return_element_from_list(2, shell.tree.formulas).checkmarked) + + def test_checkmark_if(self): + print("\n\nCheckmark if Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("if(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("not(a)") + shell.do_mark_parent("2 1") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_mark_parent("3 1") + shell.do_checkmark("1") + self.assertTrue(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + + def test_checkmark_iff(self): + print("\n\nCheckmark iff Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("iff(a,b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("not(a)") + shell.do_add_formula("not(b)") + shell.do_mark_parent("2 1") + shell.do_mark_parent("3 1") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_add_formula("a") + shell.do_mark_parent("4 1") + shell.do_mark_parent("5 1") + shell.do_checkmark("1") + self.assertTrue(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + + def test_checkmark_iff2(self): + print("\n\nCheckmark iff Test=======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("iff(a,b)") + + shell.do_branch("") + shell.do_go_to("2") + shell.do_add_formula("if(a,b)") + shell.do_add_formula("if(b,a)") + shell.do_mark_parent("2 1") + shell.do_mark_parent("3 1") + shell.do_go_to("3") + shell.do_add_formula("if(b,a)") + shell.do_add_formula("if(a,b)") + shell.do_mark_parent("4 1") + shell.do_mark_parent("5 1") + + shell.do_checkmark("1") + self.assertTrue(util.return_element_from_list(1, shell.tree.formulas).checkmarked) + + def test_all_branch_closed(self): + print("\n\nClosing all branch Test======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("and(a,b)") + shell.do_add_root_formula("not(a)") + shell.do_add_formula("a") + shell.do_mark_parent("3 1") + shell.do_close("2 3") + shell.do_check_all_closed("") + self.assertTrue(shell.finish) + + def test_all_branch_closed_2(self): + print("\n\nClosing all branch Test======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_add_root_formula("not(a)") + shell.do_add_root_formula("not(b)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_mark_parent("4 1") + shell.do_close("4 2") + shell.do_go_to("3") + shell.do_add_formula("b") + shell.do_mark_parent("5 1") + shell.do_close("5 3") + shell.do_checkmark("1") + shell.do_check_all_closed("") + self.assertTrue(shell.finish) + + def test_open_branch(self): + print("\n\nOpen Branch Test======================================================") + shell = TreeShell() + shell.reset() + shell.do_add_root_formula("or(a,b)") + shell.do_add_root_formula("or(c,d)") + shell.do_branch("1") + shell.do_go_to("2") + shell.do_add_formula("a") + shell.do_mark_parent("3 1") + shell.do_branch("2") + shell.do_go_to("4") + shell.do_add_formula("c") + shell.do_mark_parent("4 2") + shell.do_mark_open("") + self.assertTrue(shell.finish) + +if __name__ == "__main__": + unittest.main() \ No newline at end of file diff --git a/2019/src/treeformulas.py b/2019/src/treeformulas.py new file mode 100644 index 0000000..625602c --- /dev/null +++ b/2019/src/treeformulas.py @@ -0,0 +1,363 @@ +# -*- coding: utf-8 -*- + +from __future__ import print_function, unicode_literals +import argparse +from forseti.formula import Formula, Predicate, Symbol, Not, And, Or, If, Iff +import forseti.parser +from six import string_types +from src import util + +""" +TreeFormula is an object used to represent a boolean expression in predicate logic. + +TreeFormula is used in TruthTree class. + +Currently, TreeFormula can be decomposed, check for equality, and can check +if another TreeFormula is in it's decomposition. +""" + +def pretty_print(formula): + """ + :param formula: + :return: + """ + if isinstance(formula, Symbol) or isinstance(formula, Predicate): + text = str(formula) + elif isinstance(formula, Not): + text = "¬" + pretty_print(formula.args[0]) + else: + temp = [] + for arg in formula.args: + temp.append(pretty_print(arg)) + if isinstance(formula, And): + text = " ∧ ".join(temp) + elif isinstance(formula, Or): + text = " ∨ ".join(temp) + elif isinstance(formula, If): + text = " → ".join(temp) + elif isinstance(formula, Iff): + text = " ↔ ".join(temp) + else: + raise TypeError("Invalid Formula Type: " + str(type(formula))) + text = "(" + text + ")" + return text.strip() + +class TreeFormula(object): + def __init__(self, arg, formula = None, vis_id = None, mem_id = None): + """ + @param: arg is a forsetti parseable formula + @param: formula is the the string corresponding to what forsetti parses arg to + @param: vis_id is the id corresponding to the id that is printed in the truth tree + @param: mem_id is the unique id of the formula object + @effect: Create the TreeFormula of the description above + """ + if formula is None: + formula = util.parse_formula(arg) + self.formula = formula + self.node = None + self.arg = arg + self.formula_id = vis_id + self.checkmarked = False + self.closed = False + self.valid = False + self.parent = None + self.children = list() + self.unique_id = mem_id + self.node_children = list() + self.parent_checkmark = False + + def checkmark(self): + """ + Checkmark the current formula + + @effect: self.checkmark becomes True + @effect: All of the children of self parent_checkmark paremeter is marked True + """ + self.checkmarked = True + for tf in self.children: + tf.parent_checkmark = True + + def uncheckmark(self): + """ + Uncheckmark the current formula + + @effect: self.checkmark becomes False + @effect: All of the children of self parent_checkmark paremeter is marked False + """ + self.checkmarked = False + for tf in self.children: + tf.parent_checkmark = False + + def remove_parent(self): + """ + Remove the parent from self + + @effect: self is removed from self.parent's children + @effect: self.parent is set to None + """ + if self.parent: + if self.parent.formula != "PREMISE": + self.parent.children.remove(self) + if self.parent.valid: + self.valid = False + self.mark_child_not_valid() + self.parent = None + + def verify(self): + """ + Returns if a formula is valid + + Formula is valid if: + 1) It is a premise + 2) Its parent is valid + + @return: True if formula is valid. False elsewise. + """ + if self.valid: + return True + if self.parent: + if self.parent.formula == "PREMISE": + return True + else: + return self.parent.verify() + return False + + def decompose(self): + """ + Decompose the current formula into its decomposition + + @return: + Return up to two sets of formula where each set is a possible decompositon and a main connector + Return the main connector of the decomposition (Either or, and, iff, None) + Return two formula that are decomposition of the formula using arguments returned from decompose_formula_argument + """ + main_connector, decom1, decom2 = decompose_formula_argument(self.arg) + return main_connector, TreeFormula(decom1, "Dummy"), TreeFormula(decom2, "Dummy") + + def __repr__(self): + return f"{self.formula_id}: {self.formula}" + + def __eq__(self, other): + if (self is None and other is None): + return True + if (self is None): + return False + if (other is None): + return False + if (self.arg == other.arg): + return True + + # Finding the main connector of the formulas + original_connector1, v = util.find_main_connector(self.arg) + original_connector2, v = util.find_main_connector(other.arg) + + # Checking the decomposition of both formulas + main_connector1, other_decom1, other_decom2 = self.decompose() + main_connector2, form2_decom1, form2_decom2 = other.decompose() + + #Converting iff to either its or counter-part or it and counter-part + if main_connector1 == "iff" and main_connector2 == "or": + main_connector1 = "or" + if main_connector2 == "iff" and main_connector1 == "or": + main_connector2 = "or" + if main_connector1 == "iff" and main_connector2 == "and": + main_connector1 = "and" + v1, v2 = decompose_iff_into_if(self.arg) + other_decom1 = TreeFormula(v1, "Dummy") + other_decom2 = TreeFormula(v2, "Dummy") + if main_connector2 == "iff" and main_connector1 == "and": + main_connector2 = "and" + v1, v2 = decompose_iff_into_if(other.arg) + form2_decom1 = TreeFormula(v1, "Dummy") + form2_decom2 = TreeFormula(v2, "Dummy") + + #If main connector is different + if (main_connector1 != main_connector2): + return False + + # Comparing literals + if main_connector1 is None: + return other_decom1.arg == form2_decom1.arg + + #If decompositions are the same + if (other_decom1 == form2_decom1 and other_decom2 == form2_decom2) or (other_decom1 == form2_decom2 and other_decom2 == form2_decom1): + return True + + #Try decomposing more + if (original_connector1 == "and" and original_connector2 == "and"): + return other.in_decomposition_lte(self) and self.in_decomposition_lte(other) + if (original_connector1 == "or" and original_connector2 == "or"): + return other.in_decomposition_lte(self) and self.in_decomposition_lte(other) + + #Not equal + return False + + def in_decomposition(self, other): + """ + Check to see if other is in self's decomposition + + @return: + True if other is in decomposition of self. + Also return True if self == other + """ + if other == self: + return True + return self.in_decomposition_lte(other) + + def in_decomposition_lte(self, other): + """ + Helper Function for in_decomposition. Checks if other is actuallly in self decomposition + + @return: True if other is in self decomposition + False elsewise + """ + # Decomposing self + dummy, self_decom1, self_decom2 = self.decompose() + original_connector, dummy = util.find_main_connector(self.arg) + + # Testing if other is equal to decom 1 or 2 + if other == self_decom1: + return True + # self is a literal and cannot be decomposed + if self_decom2.arg is None: + return False + if other == self_decom2: + return True + + # Attempt to see if other is in self decomposition's decomposition + original_connector1, dummy = util.find_main_connector(self_decom1.arg) + original_connector2, dummy = util.find_main_connector(self_decom2.arg) + f1_in_decom1 = False + f1_in_decom2 = False + if original_connector1 == original_connector: + f1_in_decom1 = self_decom1.in_decomposition(other) + if original_connector2 == original_connector and not f1_in_decom1: + f1_in_decom2 = self_decom2.in_decomposition(other) + + # Success + if f1_in_decom1 or f1_in_decom2: + return True + + # Attempting to see if other decomposition's are in self decompositions (only if original connectors are the same) + f1_original_connector1, dummy = util.find_main_connector(other.arg) + if f1_original_connector1 == original_connector: + dummy, other_decom1, other_decom2 = other.decompose() + return self.in_decomposition(other_decom1) and self.in_decomposition(other_decom2) + + # The two decompositions of iff + if original_connector == "iff": + a1, a2 = decompose_iff_into_if(self.arg) + return TreeFormula(a1, "Dummy").in_decomposition(other) or TreeFormula(a2, "Dummy").in_decomposition(other) + if f1_original_connector1 == "iff": + dummy, a1, a2 = decompose_formula_argument(other.arg) + return self.in_decomposition(TreeFormula(a1, "Dummy")) and self.in_decomposition(TreeFormula(a2, "Dummy"),) + + return False + + def mark_child_not_valid(self): + """ + Mark the children of self as not being valid + + @effect: Mark children formula of self (and their children) as being invalid + """ + for f in self.children: + f.valid = False + f.mark_child_not_valid() + + def mark_child_valid(self): + """ + Mark the children of self as being valid + + @effect: Mark children formula of self (and their children) as being valid + """ + for f in self.children: + f.valid = True + f.mark_child_valid() + + def add_formula_children(self, child_formula): + """ + Add child_formula as a child of self + + @param: child_formula is the formula to be added to self + @effect: child_formula is added to self.children and mark validity as necessary + """ + if child_formula.parent: + child_formula.remove_parent() + child_formula.parent = self + self.children.append(child_formula) + child_formula.valid = child_formula.verify() + if child_formula.valid: + child_formula.mark_child_valid() + +def decompose_formula_argument(arg): + """ + @param: arg is a string contained in TreeFormula's arg parameter + @return: + Return three strings + First string corresponds to the main connector (and, or, iff, None) + The two remaining strings are the decomposition arguments for TreeFormula + Return None, None, None if arg is not supported + """ + arg = util.argument_parse(arg) + main_connector, arg = util.find_main_connector(arg) + + # arg is a literal + if main_connector is None: + return None, arg, None + + if main_connector == "not": + arg = util.argument_parse(arg) + inner_parenthesis_index = arg.find('(') + if(inner_parenthesis_index == -1): + return None, f"not({arg})", None + else: + inner_connector = arg[0: inner_parenthesis_index].lower() + arg = arg[inner_parenthesis_index + 1: len(arg) - 1] + if inner_connector == "and": + seperator = util.find_seperation(arg) + return "or", f"not({arg[0: seperator]})", f"not({arg[seperator+1: len(arg)]})" + if inner_connector == "or": + seperator = util.find_seperation(arg) + return "and", f"not({arg[0: seperator]})", f"not({arg[seperator+1: len(arg)]})" + if inner_connector == "not": + return None, arg, None + if inner_connector == "if": + seperator = util.find_seperation(arg) + return "and", arg[0: seperator], f"not({arg[seperator+1 : len(arg)]})" + if inner_connector == "iff": + seperator = util.find_seperation(arg) + return "iff", f"and(not({arg[0: seperator]}),{arg[seperator+1 : len(arg)]})", f"and({arg[0: seperator]},not({arg[seperator+1 : len(arg)]}))" + return None, None, None + if main_connector == "and": + seperator = util.find_seperation(arg) + return main_connector, arg[0: seperator], arg[seperator+1: len(arg)] + if main_connector == "or": + seperator = util.find_seperation(arg) + return main_connector, arg[0: seperator], arg[seperator+1: len(arg)] + if main_connector == "if": + seperator = util.find_seperation(arg) + return "or", f"not({arg[0:seperator]})", arg[seperator+1: len(arg)] + if main_connector == "iff": + seperator = util.find_seperation(arg) + return "iff", f"and({arg[0: seperator]},{arg[seperator+1: len(arg)]})", f"and(not({arg[0: seperator]}),not({arg[seperator+1: len(arg)]}))" + return None, None, None + +def decompose_iff_into_if(arg): + """ + Returns if form of iff + + @param: arg is a string in the form iff(a,b) + @return: + Return two string: + or(not(a),b) + or(a,not(b)) + """ + arg = util.argument_parse(arg) + first_parenthesis_index = arg.find('(') + + # Seperating the main connector and it's arguments + main_connector = arg[0: first_parenthesis_index].lower() + arg = arg[first_parenthesis_index + 1: len(arg) - 1] + seperator = util.find_seperation(arg) + return f"or(not({arg[0: seperator]}),{arg[seperator+1: len(arg)]})", f"or({arg[0: seperator]},not({arg[seperator+1: len(arg)]}))" + diff --git a/2019/src/truthtrees.py b/2019/src/truthtrees.py new file mode 100644 index 0000000..c47cc19 --- /dev/null +++ b/2019/src/truthtrees.py @@ -0,0 +1,415 @@ +# -*- coding: utf-8 -*- + +from __future__ import print_function, unicode_literals +import argparse +from forseti.formula import Formula, Predicate, Symbol, Not, And, Or, If, Iff +import forseti.parser +from six import string_types +from src import util +from src.treeformulas import * + +class TreeError(Exception): + pass + +class TreeNode(object): + def __init__(self, node_id=None, unique_id = None): + """ + @param: node_id is an integer corresponding to the printed id of the node + @param: unique_id is the id of the node object + @effect: Create a node class + """ + self.formulas = [] + self.parent = None + self.children = [] + self.closed = False + self.open = False + self.number = None + self.node_id = node_id + self.unique_id = unique_id + self.parent_formula = None + + def __repr__(self): + s = f"\nFormulas:\n" + for formula in self.formulas: + s += f" {formula}\n" + s += f"Closed: {self.closed}\n" + s += f"ID: {self.node_id}\n" + s += f"Parent: {self.parent.node_id if self.parent is not None else None}\n" + s += f"Children: {[child.node_id for child in self.children]}\n" + return s + + def print(self): + print(self) + + def insert_formula(self, tf): + """ + Add a formula into the correct location based on formula_id + + @param: tf is a TreeFormula object that is going to be inserted into the node + @effect: tf is inserted into self.formulas in the correct location + """ + for i in range(len(self.formulas)): + if tf.formula_id <= self.formulas[i].formula_id: + self.formulas.insert(i, tf) + return + self.formulas.append(tf) + + def add_formula(self, formula): + """ + Add a formula to the node. + + @param: formula is a TreeFormula + @effect: + formula is added to the node + formula node is marked as self + """ + formula.node = self + self.formulas.append(formula) + + def has_formula(self, check_formula): + """ + Check to see if check_formula is in the current node + + @param: check_formula is a TreeFormula object + @return: True if check_formula is in self.formulas + """ + for formula in self.formulas: + if formula.formula == check_formula: + return True + if self.parent is not None: + return self.parent.has_formula(check_formula) + return False + + def add_child(self, child_id, unique_id): + """ + Add a child node to the self + + @parem: child_id and unique_id are integer corresponding to the id of child to be added + @effect: Create a TreeNode using child_id and unique_id and add it to self.children + @return: Return the node added + """ + if self.closed: + return [[], []] + elif len(self.children) == 2: + raise TreeError(f"Cannot add another child to {self.node_id}") + else: + child_node = TreeNode(child_id, unique_id) + child_node.parent = self + child_node.node_id = child_id + child_node.parent.children.append(child_node) + return child_node + + def in_ancestry(self, formula): + """ + Check if a formula is in the ancestry of the node + + @param: formula is a TreeFormula object + @return: Returns True if formula is in the current node or if it is in one of its ancestry node + """ + if formula in self.formulas: + return True + if self.parent: + return self.parent.in_ancestry(formula) + return False + +class TreeFormulaError(Exception): + pass + +class TruthTree(object): + def __init__(self): + self.root = TreeNode() + self.root.unique_id = 1 + self.root.node_id = 1 + self.nodes = list() + self.formulas = list() + self.node_memory = list() + self.formulas_memory = list() + self.offset_list() + self.nodes.append(self.root) + self.node_memory.append(self.root) + + def offset_list(self): + """ + Helper function for TruthTree __init__ + + Offset all of the lists in the truthtree so that id matches index + + @effect: Add None to all of the list in TreeFormula + """ + self.nodes.append(None) + self.formulas.append(None) + self.node_memory.append(None) + self.formulas_memory.append(None) + + def print(self): + """ + For DEBUGGING + + Print out the list of nodes + + @return: Return an output_string that corresponds to what is being printed + """ + output_string = "Printing List of Nodes.\n" + print("Printing List of Nodes") + for node in self.nodes: + if node: + output_string += str(node) + node.print() + return output_string + + def print_formulas(self): + """ + For DEBUGGING + + Print all of the formula in the Tree + """ + for formula in self.formulas: + if formula: + print(formula) + + def add_formula(self, node, arg, formula = None): + """ + Add a formula to node + + @param: node is a TreeNode + @param: arg is the arg argument for the TreeFormula object + @param: formula is a string corresponding to the forsetti parsed arg + @effect: Create a TreeFormula object using arg and Formula and add it to node + @return: Return the TreeFormula added to the node + """ + tf = TreeFormula(arg, formula, len(self.formulas), len(self.formulas_memory)) + node.add_formula(tf) + self.formulas.append(tf) + self.formulas_memory.append(tf) + return tf + + def add_premise_formula(self, arg, formula = None): + """ + Add a premise to the tree + + @param: arg is the arg argument for the TreeFormula object + @param: formula is a string corresponding to the forsetti parsed arg + @effect: Create a TreeFormula object using arg and Formula and add it to node + @return: Return the TreeFormula added to the node + """ + index = 1 + while (index < len(self.formulas)): + if self.formulas[index].parent is None: + break + if self.formulas[index].parent.formula != "PREMISE": + break + index += 1 + + + tf = TreeFormula(arg, formula, index, len(self.formulas_memory)) + tf.node = self.root + self.root.insert_formula(tf) + self.formulas.insert(index, tf) + self.formulas_memory.append(tf) + self.readjust_formula_id() + return tf + + + + def readjust_formula_id(self, lowerbound = 1): + """ + Readjust the formula id of all formulas in self.formulas + + @effect: Make all of the TreeFormula's formula_id match there location in self.formulas + """ + for i in range(lowerbound, len(self.formulas)): + if self.formulas[i]: + self.formulas[i].formula_id = i + + def readjust_node_id(self, lowerbound = 1): + """ + Readjust the formula id of all nodess in self.nodess + + @effect: Make all of the TreeNode's node_id match there location in self.nodes + """ + for i in range(lowerbound, len(self.nodes)): + if self.nodes[i]: + self.nodes[i].node_id = i + + + def delete_formula(self, formula): + """ + Remove a formula from the tree + @param: formula is a TruthFormula object + @effect: Remove formula from self.formulas and adjust formula id's as needed + @effect: Remove formula from its parent and children + @effect: Uncheckmark parent if delete_formula is used to checkmark parent + @effect: Invalidate all children if formula was valid + """ + + # Looking for TreeFormula to remove from node + f_list = self.node_memory[formula.node.unique_id].formulas + index = -1 + # Searching for a match + for i in range(len(f_list)): + if f_list[i].formula_id == formula.formula_id: + index = i + break + f_list.pop(index) + + # Removing the formula from it's parent and children + if formula.parent and formula.parent.formula != "PREMISE": + parent = formula.parent + formula.remove_parent() + formula.parent = parent + for f in formula.children: + f.parent = None + f.parent_checkmark = False + if formula.parent_checkmark: + formula.parent.checkmarked = False + formula.mark_child_not_valid() + + # Remove formula from the tree + self.formulas.pop(formula.formula_id) + self.readjust_formula_id(formula.formula_id) + + def delete_node(self, u_node_id): + """ + Delete a node from the tree. Helper function for deleting a branch + + @param: u_node_id is an int corresponding the unique_id of the node to be deleted + @effect: The node coresponding to u_node_id is deleted and all formulas stored in the node is deleted from the Tree + """ + node = self.node_memory[u_node_id] + + # Delete the formulas from the tree, but keep the formulas in node for restoration later + copy = list(node.formulas) + for f in node.formulas: + self.delete_formula(f) + node.formulas = copy + + # Remove node from parent_formula + parent_formula = node.parent_formula + parent_formula.node_children.remove(node) + + # Remove the node from parent + node.parent.children.remove(node) + + # Remove the node from the Tree node list + self.nodes.pop(node.node_id) + self.readjust_node_id(node.node_id) + + def readd_node(self, u_node_id): + """ + Re-add a previously deleted node + + @effect: Restore a node from being delted + @effect: Add node back to TruthTree + @effect: Restore the formulas in the node + """ + child_node = util.return_element_from_list(int(u_node_id), self.node_memory) + child_node.parent.children.append(child_node) + self.nodes.insert(child_node.node_id, child_node) + child_node.parent_formula.node_children.append(child_node) + print(len(child_node.formulas)) + for f in child_node.formulas: + self.undelete_formula_helper(f.unique_id) + + def undelete_formula(self, unique_id): + """ + Function to readd a formula + + @param: unique_id is the id corresponding to the unique id of the formula to be readded + @effect: The TreeFormula with unique_id is readded to the tree and node that it was deleted from + @effect: Restore any validity marking and checkmarking from the formula being deleted + """ + tf = util.return_element_from_list(int(unique_id), self.formulas_memory) + node = util.return_element_from_list(tf.node.node_id, self.nodes) + self.undelete_formula_helper(unique_id) + node.insert_formula(tf) + + def undelete_formula_helper(self, unique_id): + """ + Helper Function for undelete_formula + + @effect: Add formula with unique_id back into TruthTree + @effect: Restore all checkmark and valid marking if necessary + """ + # Find the formula + tf = util.return_element_from_list(int(unique_id), self.formulas_memory) + + # Insert formula into TruthTree + self.formulas.insert(int(tf.formula_id), tf) + self.readjust_formula_id(int(tf.formula_id)) + + # Restore parent if needed + if tf.parent and tf.parent.formula != "PREMISE": + parent = util.return_element_from_list(tf.parent.formula_id, self.formulas) + parent.children.append(tf) + for f in tf.children: + f.parent = tf + + # Checkmark again and mark valid again if necessary + if tf.valid: + tf.mark_child_valid() + if tf.checkmarked: + for f in tf.children: + f.parent_checkmark = True + if tf.parent_checkmark: + tf.parent.checkmarked = True + + def branch(self, node, formula = None): + """ + Branch on a node using a parent formula + + @param: Node is a TreeNode that is being branched on + @param: formula is the "parent" formula of the branch + return: true on successful branch + false on not successful + """ + print(f"Branching on node {node.node_id}") + child_node_id1 = len(self.nodes) + child_node_id2 = len(self.nodes)+1 + child_node1 = node.add_child(child_node_id1, len(self.node_memory)) + child_node2 = node.add_child(child_node_id2, len(self.node_memory)+1) + print(f"Adding nodes {child_node_id1} and {child_node_id2}") + self.nodes.append(child_node1) + self.nodes.append(child_node2) + self.node_memory.append(child_node1) + self.node_memory.append(child_node2) + child_node1.parent_formula = formula + child_node2.parent_formula = formula + formula.node_children.append(child_node1) + formula.node_children.append(child_node2) + +# def runner(formulas, goal): +# """ + +# :param formulas: +# :type formulas: List[string_types] +# :param goal: +# :type goal: string_types +# :return: +# """ + +# if isinstance(formulas, string_types): +# formulas = [formulas] + +# if not isinstance(goal, string_types): +# raise TypeError("Expected str for goal, got " + str(type(goal))) + +# parsed_formulas = [] +# for formula in formulas: +# formula = formula.strip() +# if len(formula) == 0: +# continue +# parsed_formulas.append(forseti.parser.parse(formula)) + +# goal = forseti.parser.parse(goal) +# return TruthTree(parsed_formulas, goal) + +# if __name__ == "__main__": +# PARSER = argparse.ArgumentParser(description="Generate Truth Table for a logical formula") +# PARSER.add_argument('--formulas', metavar='formula', type=str, nargs="*", help='Logical formula') +# PARSER.add_argument('--goal', metavar='goal', type=str, help='Goal Formula') +# PARSER_ARGS = PARSER.parse_args() +# SHORT_TRUTH_TABLE = runner(PARSER_ARGS.formulas, PARSER_ARGS.goal) +# if SHORT_TRUTH_TABLE.root.is_closed(): +# print("Argument is valid") +# else: +# print("Argument is invalid") diff --git a/2019/src/util.py b/2019/src/util.py new file mode 100644 index 0000000..5cbc225 --- /dev/null +++ b/2019/src/util.py @@ -0,0 +1,97 @@ +import cmd +import forseti.parser +import shlex + +from src import truthtrees + +def parse_formula(formula_string): + """ + Parse a formula string using the forseti parser. + + @param: formula_string is a string that can be + @return: + None and error message if formula can't be parsed + Formula and None if formula can be parsed + """ + formula = None + try: + formula = forseti.parser.parse(formula_string) + except SyntaxError as se: + print(se) + return None, se + return formula, None + +def return_element_from_list(i, l): + """ + Returns an element from the list + + @param: i is an integer corresponding to the index of the element in the list + @param: l is a list of elements + return: + element of the list if 0 <= i <= len(l) - 1 + None otherwise + """ + if(i < 0 or i >= len(l)): + return None + else: + return l[i] + +def history_parser(arg): + """ + @param: arg is a string that contains the words seperated by spaces + @return: Returns two strings. The first word removed from arg and everything after the space + """ + v = -1 + try: + v = arg.index(' ') + except ValueError: + return None, None + first_word = arg[0:v] + remain = arg[v + 1: len(arg)] + return first_word, remain + +def find_main_connector(arg): + """ + Find the main_connector of an formula argument and the arguments + + @param: arg is a string that can be parsed by forsetti parser + """ + arg = argument_parse(arg) + first_parenthesis_index = arg.find('(') + if first_parenthesis_index == -1: + return None, arg + main_connector = arg[0: first_parenthesis_index].lower() + arg = arg[first_parenthesis_index + 1: len(arg) - 1] + return main_connector, arg + +def argument_parse(arg): + """ + Small helper function to get rid of excess parenthesis at the begining and end and any whitespace. + + @param: arg is a string + @return: arg with the spaces and parenthesis around arg removed + """ + a = arg.replace(' ','') + while a[0] == '(' and a[len(arg) - 1] == ')': + a = a[1 : len(a) - 1] + return a + + +def find_seperation(arg): + """ + Helper Function for decompose + + @param: arg is a string corresponding to two function statement sepereated by a comma + Example: "and(and(a,c),b),or(ab,b)" + @return: + return the index of the comma seperating the functions or -1 if no such comma exist + """ + open_parenthesis = 0 + for i in range(len(arg)): + if arg[i] == '(': + open_parenthesis += 1 + elif arg[i] == ')': + open_parenthesis -= 1 + elif arg[i] == ',' and open_parenthesis == 0: + return i + return -1 diff --git a/2019/src/web_server.py b/2019/src/web_server.py new file mode 100644 index 0000000..f34d079 --- /dev/null +++ b/2019/src/web_server.py @@ -0,0 +1,115 @@ +from cli import TreeShell +from flask import Flask, Markup, render_template, request, redirect, url_for +import sys +from truthtrees import pretty_print +import io + +app = Flask(__name__) + +log = io.StringIO() + +shell = TreeShell(stdout=log) + +closed_string = "X" +open_string = "O" + + +@app.route('/', methods=['POST', 'GET']) +def my_form(): + """ + This is the function: + * calls a shell command(s) based on the inputs and + * render nodes, formulas, and the tree to be displayed in html + * reloads the page with the updates + """ + if request.method == 'GET': + shell.stdout.write(str(shell.intro)+"\n") + log = shell.stdout.getvalue().split('\n') + return render_template('my-form.html', log=log, command_history=shell.history) + elif request.method == 'POST': + text = request.form.get('text') + reset = request.form.get('reset') + verify = request.form.get('verify') + if reset: + shell.onecmd("reset") + log = shell.stdout.getvalue().split('\n') + tree_render = render_node(shell.tree.root, shell.current_node.node_id) + return render_template('my-form.html', command_history=shell.history, log=log, tree=tree_render) + elif verify: + closed_verify = shell.onecmd("check_all_closed") + open_verify = shell.onecmd("check_any_open") + if closed_verify == "True" or open_verify == "True": + verify_message = "Verified Success!" + verify_render = Markup(render_template("verify_success.html", verify_message=verify_message)) + elif closed_verify == "False" and open_verify == "False": + verify_message = "Verified Failed. Check the Log" + verify_render = Markup(render_template("verify_failed.html", verify_message=verify_message)) + log = shell.stdout.getvalue().split('\n') + tree_render = render_node(shell.tree.root, shell.current_node.node_id) + return render_template('my-form.html', command_history=shell.history, log=log, tree=tree_render, verify_message=verify_render) + + if text == "": + log = shell.stdout.getvalue().split('\n') + tree_render = render_node(shell.tree.root, shell.current_node.node_id) + message = "No Command Entered" + return render_template('my-form.html', command_history=shell.history, log=log, tree=tree_render, message=message) + + shell.onecmd(text) + log = shell.stdout.getvalue().split('\n') + tree_render = render_node(shell.tree.root, shell.current_node.node_id) + return render_template('my-form.html', command_history=shell.history, log=log, tree=tree_render) + +def render_node(node, current_node_id): + """ + This function compiles the templates and messages with respect to nodes + """ + children = [] + for child in node.children: + children.append(render_node(child, current_node_id)) + + formulas = [] + for formula in node.formulas: + formula_render = render_formula(formula) + formulas.append(formula_render) + + if node.closed: + print("closing") + formulas.append(Markup(closed_string)) + elif node.open: + print("opening") + formulas.append(Markup(open_string)) + + node_html = 'node.html' + if node.node_id == current_node_id: + node_html = 'selected_node.html' + + node_name = f'Node: {node.node_id}' + + return Markup(render_template(node_html, formulas=formulas, children=children, node=node_name)) + +def render_formula(formula): + """ + This function compiles the correct templates and messages with respect to the way formulas are displayed + """ + formula_html = None + + color_form = "formula_black.html" + if formula.valid: + color_form = "formula_blue.html" + + string = f"{formula.formula_id}: {pretty_print(formula.formula)}" + + html_output = render_template(color_form, formula=string) + + if formula.checkmarked: + html_output += " ✓" + + return Markup(html_output) + + +@app.route('/test', methods=['GET', 'POST']) +def alpha(): + return "hello" + +if __name__=='__main__': + app.run() \ No newline at end of file diff --git a/README.md b/README.md index 9202b0d..b572a57 100644 --- a/README.md +++ b/README.md @@ -1,20 +1,7 @@ -# Handy Logic Doodahs-Truth Trees -## Authors -2016: -Matt Peveler +# Truth Tree Interface/Solver -## About -This is a flask app (with a python module backing it) that can be used to solve generate a truth tree for any given number of formulas and one goal. This is part of the handy logic doodahs series of Automated Theorem Provers. +# 2016 folder: +Matt Peveler's Auto Truth Tree Solver -![Flask App](https://raw.githubusercontent.com/MasterOdin/TruthTrees/master/static/screenshot.png) - -It uses a functional format for inputting logical formulas. This is the base identity for inputs: -``` -A -not(A) -and(A, B) -or(A, B) -if(A, B) -iff(A, B) -``` -where `A` and `B` can either be atomic statements or a functional operator. All operators are either unary (not) or binary (and, or, if, iff) and there is no support for a generalized notation. This means that ```and(A, B, C)``` will thrown an error. +# 2019 folder: +Ji hann Hong and Terry Nguyens Truth Tree Web-based Interface \ No newline at end of file