find_proposition

[benbrastmckie]

I managed to get an error for the line commented below:

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))}
        # B: I managed to get an error here
        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)

Here is the error:

  File "/home/benjamin/Documents/Philosophy/Projects/ModelChecker/Code/src/new
_checker/exposed_things.py", line 154, in __init__
    self.verifiers, self.falsifiers = self.find_proposition()
                                      ^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/benjamin/Documents/Philosophy/Projects/ModelChecker/Code/src/new
_checker/exposed_things.py", line 231, in find_proposition
    V = {bit for bit in all_bits if model.evaluate(sem.verify(bit, atom))}
                                    ^^^^^^^^^^^^^^
AttributeError: 'AstVector' object has no attribute 'evaluate'

[mbuit82]

Interesting—what was the code you ran to get the error?

[benbrastmckie]

premises = ["\\neg (A \\vee B)", "(C \\wedge D)"]
conclusions = ["\\neg B"]

[mbuit82]

Ah it looks like that valid entailments (ie no models found) were not carried over from the old code—I just implemented a fix that now prints a message when there is no model found