14.3.5 fix

Author: andob

prover/src/countermodel/alternative_algorithm/availability.rs

@@ -37,12 +37,14 @@ impl AlternativeCountermodelFinderAvailability
 
     pub fn get_available_first_order_logics() -> Vec<Rc<dyn Logic>>
     {
-        return Self::get_available_propositional_logics().iter()
-            .map(|propositional_logic| Rc::new(FirstOrderLogic
+        return vec!
+        [
+            Rc::new(FirstOrderLogic
             {
                 domain_type: FirstOrderLogicDomainType::ConstantDomain,
                 identity_type: FirstOrderLogicIdentityType::ContingentIdentity,
-                base_logic: propositional_logic.clone(),
-            }) as Rc<dyn Logic>).collect();
+                base_logic: Rc::new(PropositionalLogic{}),
+            }),
+        ];
     }
 }

prover/src/logic/first_order_logic/forall_quantifier_rule.rs

@@ -13,7 +13,7 @@ use crate::logic::first_order_logic::predicate_args_with_equivalences::create_eq
 use crate::logic::{LogicRule, LogicRuleResult};
 use crate::logic::rule_apply_factory::RuleApplyFactory;
 use crate::tree::node::ProofTreeNode;
-use crate::tree::node_factory::ProofTreeNodeID;
+use crate::tree::node_factory::{ProofTreeNodeFactory, ProofTreeNodeID};
 use crate::tree::path::ProofTreePath;
 use crate::tree::subtree::ProofSubtree;
 
@@ -118,18 +118,11 @@ impl ForAllQuantifierRule
         let logic_pointer = factory.get_logic().clone();
         let logic = logic_pointer.cast_to::<FirstOrderLogic>().unwrap();
 
-        for path in factory.tree.get_paths_that_goes_through_node(node)
+        let all_paths = factory.tree.get_paths_that_goes_through_node(node);
+        for path in all_paths.clone()
         {
             let mut output_nodes = ForAllQuantifierOutputNodes::new(logic.domain_type);
-            self.apply_for_all_quantification_impl(factory, &path, node, x, p, extras, &mut output_nodes);
-
-            if output_nodes.is_empty()
-            {
-                //there are no objects to be iterated, act similar to exists quantifier
-                let object_name_factory = ExistsQuantifierRule{}.get_object_name_factory(factory, node);
-                let (instantiated_p, instantiated_x) = p.instantiated(x, &object_name_factory, extras);
-                output_nodes.add(factory, instantiated_x.unwrap_or(x.clone()), instantiated_p, extras);
-            }
+            self.apply_for_all_quantification_impl(factory, &all_paths, &path, node, x, p, extras, &mut output_nodes);
 
             let subtree = output_nodes.to_proof_subtree(factory);
             output_subtrees.push((path.get_leaf_node_id(), subtree));
@@ -138,8 +131,8 @@ impl ForAllQuantifierRule
         return LogicRuleResult::Subtrees(output_subtrees);
     }
 
-    fn apply_for_all_quantification_impl(&self,
-        factory : &mut RuleApplyFactory, path : &ProofTreePath, node : &ProofTreeNode,
+    fn apply_for_all_quantification_impl(&self, factory : &mut RuleApplyFactory,
+        all_paths : &Vec<ProofTreePath>, path : &ProofTreePath, spawner_node : &ProofTreeNode,
         x : &PredicateArgument, p : &Formula, extras : &FormulaExtras,
         output_nodes : &mut ForAllQuantifierOutputNodes,
     )
@@ -163,12 +156,34 @@ impl ForAllQuantifierRule
             .map(|a| a.object_name.clone())
             .collect::<BTreeSet<SmolStr>>();
 
+        if object_names.is_empty()
+        {
+            //there are no objects to be iterated, act similar to exists quantifier
+            let object_name_factory = ExistsQuantifierRule{}.get_object_name_factory(factory, spawner_node);
+            let (instantiated_p, instantiated_x) = p.instantiated(x, &object_name_factory, extras);
+            output_nodes.add(factory, instantiated_x.unwrap_or(x.clone()), instantiated_p, extras);
+            return;
+        }
+
         for object_name in object_names
         {
             let (binded_p, binded_x) = p.binded(x, object_name, extras);
-            output_nodes.add(factory, binded_x.unwrap_or(x.clone()), binded_p, extras);
+
+            if !self.should_skip_outputting_binded_formula(all_paths, spawner_node, &binded_p)
+            {
+                output_nodes.add(factory, binded_x.unwrap_or(x.clone()), binded_p, extras);
+            }
         }
     }
+
+    fn should_skip_outputting_binded_formula(&self, all_paths : &Vec<ProofTreePath>,
+        spawner_node : &ProofTreeNode, binded_formula : &Formula) -> bool
+    {
+        return all_paths.iter().flat_map(|path| path.nodes.iter())
+            .filter(|node| node.spawner_node_id == spawner_node.id)
+            .find(|node| node.formula == *binded_formula)
+            .is_some();
+    }
 }
 
 pub fn get_args_that_definitely_exists(all_formulas_on_path : &Vec<Formula>, possible_world : PossibleWorld) -> BTreeSet<PredicateArgument>

prover/src/proof.rs

@@ -1,3 +1,4 @@
+use itertools::Itertools;
 use crate::formula::to_string::FormulaFormatOptions;
 use crate::graph::Graph;
 use crate::logic::{LogicName, LogicRuleCollection, LogicRuleResult};
@@ -45,21 +46,26 @@ impl ProofAlgorithm
         {
             let ram_consumption = measure_total_number_of_allocated_bytes(||
             {
-                let (box node, mut result) = self.consume_next_queue_node().unwrap();
+                if let Some((node, mut result)) = self.consume_next_queue_node()
+                {
+                    ExecutionLog::log(format!("Apply: <{}> {}\nResult: {}", node.id,
+                        node.formula.to_string_with_options(&formula_format_options),
+                        result.to_string_with_options(&formula_format_options)));
 
-                ExecutionLog::log(format!("Apply: <{}> {}\nResult: {}", node.id,
-                    node.formula.to_string_with_options(&formula_format_options),
-                    result.to_string_with_options(&formula_format_options)));
+                    self.proof_tree.append_logic_rule_result(&mut result, node.id);
 
+                    if !self.problem_flags.should_skip_contradiction_check
+                    {
+                        self.proof_tree.check_for_contradictions();
+                    }
 
-                self.proof_tree.append_logic_rule_result(&mut result, node.id);
+                    if self.decomposition_queue.is_node_reusable(&node) && result.is_empty()
+                    {
+                        self.decomposition_queue.ban_reusable_node(&node);
+                    }
 
-                if !self.problem_flags.should_skip_contradiction_check
-                {
-                    self.proof_tree.check_for_contradictions();
+                    self.decomposition_queue.push_logic_rule_result(result);
                 }
-
-                self.decomposition_queue.push_logic_rule_result(result);
             });
 
             let log_helper_data = ExecutionLogHelperData::flush();
@@ -89,12 +95,9 @@ impl ProofAlgorithm
             factory.set_spawner_node_id(Some(node.id));
 
             let result = self.logic_rules.apply(&mut factory, &node);
-            if !result.is_empty()
-            {
-                return Some((node, result));
-            }
 
-            return Some((node, LogicRuleResult::Empty));
+            return if !result.is_empty() { Some((node, result)) }
+            else { Some((node, LogicRuleResult::Empty)) };
         }
 
         return None;

prover/src/proof/decomposition_queue.rs

@@ -70,8 +70,7 @@ impl DecompositionPriorityQueue
             let reusable_node = self.reusable_nodes.remove(0);
             if !self.banned_reusable_nodes.contains(&reusable_node)
             {
-                self.consumable_nodes.push(reusable_node.clone());
-                self.banned_reusable_nodes.push(reusable_node);
+                self.consumable_nodes.push(reusable_node);
             }
         }
 
@@ -142,4 +141,17 @@ impl DecompositionPriorityQueue
             _ => false
         };
     }
+
+    pub fn is_node_reusable(&self, node : &Box<ProofTreeNode>) -> bool
+    {
+        return self.reusable_nodes.contains(node);
+    }
+
+    pub fn ban_reusable_node(&mut self, node : &Box<ProofTreeNode>)
+    {
+        if self.reusable_nodes.contains(node)
+        {
+            self.banned_reusable_nodes.push(node.clone());
+        }
+    }
 }

prover/src/tree/path.rs

@@ -19,6 +19,7 @@ pub struct ProofTreePathNodeData
     pub id : ProofTreeNodeID,
     pub is_contradictory : bool,
     pub formula : Formula,
+    pub spawner_node_id : ProofTreeNodeID,
 }
 
 impl ProofTreePathNodeData
@@ -30,6 +31,7 @@ impl ProofTreePathNodeData
             id: node.id,
             is_contradictory: node.is_contradictory,
             formula: node.formula.clone(),
+            spawner_node_id: node.spawner_node_id.unwrap_or_default()
         };
     }
 }