avoid redundant recursion in proposition definition

Future feature:

def find_proposition(self):
    all_bits = self.model_structure.all_bits
    model = self.model_structure.z3_model
    sem = self.semantics
    if len(self.prefix_sentence) == 1:
        atom = self.prefix_sentence[0]
        V = {bit for bit in all_bits if model.evaluate(sem.verify(bit, atom))}
        F = {bit for bit in all_bits if model.evaluate(sem.falsify(bit, atom))}
        return V, F
    operator, prefix_args = self.prefix_sentence[0], self.prefix_sentence[1:]
    children_subprops = [Defined(arg, self.model_structure) for arg in prefix_args]
    return operator.find_verifiers_and_falsifiers(*children_subprops)
    # # DISCUSS: this seems very close; just needs debugging and build prop dictionary here
    # # B: might as well add to proposition dictionary here
    # current_props = {str(p.prefix_sentence):p for p in self.model_structure.all_propositions}
    # children_subprops = []
    # for arg in prefix_args:
    #     if str(arg) in current_props:
    #         children_subprops.append(current_props[str(arg)])
    #     else:
    #         children_subprops.append(Proposition(arg, self.model_structure))

benbrastmckie / ModelChecker

avoid redundant recursion in proposition definition #46