Optimization

[benbrastmckie]

I've added benchmarking to test_complete.py in order to begin comparing results. Here is how the proposition constraints were originally defined:

    prop_const = ForAll(X, proposition(X))
    solv.add(prop_const)
    print(f"Proposition constraint: {world_const}")

This ran with an execution time of .71 sec. I then replaced this constraint with:

def prop_const(atom):
    sent_to_prop =[
        ForAll(
            [x, y],
            Implies(And(verify(x, atom), verify(y, atom)), verify(fusion(x, y), atom)),
        ),
        ForAll(
            [x, y],
            Implies(And(falsify(x, atom), falsify(y, atom)), falsify(fusion(x, y), atom)),
        ),
        ForAll(
            [x, y],
            Implies(And(verify(x, atom), falsify(y, atom)), Not(compatible(x, y))),
        ),
    ]
    return sent_to_prop

    for sent_letter in input_sentence_letters:
        print(f"\nSentence {sent_letter} yields the general constraints:\n")
        for const in prop_const(sent_letter):
            solv.add(const)
            print(f"{const}\n")

This ran with an execution time of .18 seconds. This makes me curious what kind of improvements can be gained by removing all occurrences of Exists from the Z3 constraints generated by the functions in semantics.py, replacing these with unique variables instead.

[benbrastmckie]

I add documentation instructions to General.md regarding using MIT's compute. It is very easy to log in. I tried adding the exhaustive constraint, but the process was killed. This suggests that there is something deeper going on.

[benbrastmckie]

I'm going to store various loose ends to come back to that pertain to Z3 optimization is this issue, the first of which was from when I was experimenting with different non-trivial proposition constraints.

# NOTE: if null verifiers are permitted, then null state verifies A
# but possible state c does not?
premises = ['A','B']
conclusions = ['(A boxright B)']

Here are some examples where the unsat_core looks satisfiable:

# # NOTE: unsat_core seems satisfiable
# premises = []
# conclusions = ['(A vee neg A)']

# # NOTE: unsat_core seems satisfiable
# premises = []
# conclusions = ['neg (A wedge neg A)']