refactor: necessary rule -> per branch behavior

Author: andob

prover/src/formula/to_string.rs

@@ -49,7 +49,8 @@ impl FormulaFormatOptions
             return FormulaFormatOptions
             {
                 notations: *default_notations.borrow(),
-                should_show_possible_worlds: false,
+                //todo should_show_possible_worlds: false,
+                should_show_possible_worlds: true,
                 should_show_sign: false,
                 should_show_fuzzy_tags: false,
             }

prover/src/logic/common_modal_logic.rs

@@ -169,7 +169,7 @@ impl <LOGIC : Logic> Modality<LOGIC>
             already_iterated_possible_worlds: BTreeSet::new(),
         };
 
-        let result = self.reapply_necessity(factory, &mut reapplication_data, PossibleWorld::zero());
+        let result = self.reapply_necessity(factory, &mut reapplication_data, None, PossibleWorld::zero());
         factory.push_necessity_reapplication(reapplication_data);
 
         return result;
@@ -190,7 +190,7 @@ impl <LOGIC : Logic> Modality<LOGIC>
                 //necessary reapplication should happen only if we're on one of some specific paths
                 if reapplication.input_leafs_node_ids.iter().any(|leaf_node_id| path.contains_node_with_id(*leaf_node_id))
                 {
-                    let output_from_necessity = self.reapply_necessity(factory, &mut reapplication, forked_world);
+                    let output_from_necessity = self.reapply_necessity(factory, &mut reapplication, Some(node), forked_world);
                     output_results.push(output_from_necessity);
                 }
             }
@@ -204,6 +204,7 @@ impl <LOGIC : Logic> Modality<LOGIC>
     fn reapply_necessity(&self,
         factory : &mut RuleApplyFactory,
         reapplication_data : &mut NecessityReapplicationData,
+        possibility_node : Option<&ProofTreeNode>,
         forked_world : PossibleWorld,
     ) -> LogicRuleResult
     {
@@ -232,7 +233,10 @@ impl <LOGIC : Logic> Modality<LOGIC>
                 .map(|node| node.formula.get_possible_world())
                 .collect::<BTreeSet<PossibleWorld>>();
 
-            possible_worlds_on_path.insert(forked_world);
+            if let Some(node) = possibility_node && path.contains(node)
+            {
+                possible_worlds_on_path.insert(forked_world);
+            }
 
             for formula in &output_formulas
             {

prover/src/tree/path.rs

@@ -107,11 +107,11 @@ impl Display for ProofTreePath
         {
             if index < last_index
             {
-                write!(f, "{} -> ", node.formula).unwrap();
+                write!(f, "{} -> ", node.formula)?;
             }
             else
             {
-                write!(f, "{}", node.formula).unwrap();
+                write!(f, "{}", node.formula)?;
             }
         }