Benchmark Derived Operators

[benbrastmckie]

I'm moving this thought from the comments to come back to when we are read:

It would be nice to do some benchmarking in order to compare equivalent derived and primitive operators.
Ideally there would be little difference in speed between the two even for complicated operators.
But it would be good to provide evidence of this.

[mbuit82]

Sounds good—Im moving our longer discussion of defined operators here in case its relevant during benchmarking:

# NOTE: moved this to consolidate
# M: I thought I'd give a shot defining operators in terms of other operators.
# It is possible, but it maybe isn't as clean as would be nice. 
# I think it would be possible to define a subclass of the Operator class
# called DerivedOperator, and operators defined in terms of others would
# be subclasses of that class. Then in hidden_stuff we'd deal with all the
# code that's kind of messy below—maybe a user would only need to specify
# something along the lines of e.g. A -> B := ~A v B, and the rest would automatically
# be filled out

# B: I like the DerivedOperator class idea, but feel this should be purely syntactic
# at least that is how it is in logic where A -> B := ~A v B this means that the LHS
# abbreviates the RHS. it is odd to hid the conversion in the semantics so that
# A -> B := ~A v B means that the LHS will be interpreted as if it were the RHS.
# With that said, using python does open new possibilities that might not be so bad
# to explore. However, there is another reason to avoid defined operators which is
# that it is good for the semantics clause to be as human intelligible and easy to
# motivate as possible. it also doesn't need to take more code (see below)
# M: Hey, sorry I merged and saw the changes. I figured out a way to make the DerivedOperator
# class that's a lot cleaner on the user—all the need to do is define a (lambda) function
# see below (i did that before seeing these comments). Let me know what you think
# (doesn't have to be a lambda function, I just like them (as you may have noticed by now lol))

# M: @B, this is the DerivedOperator class that hides all of the redefining stuff
# B: I was thinking more about this class and change my mind that it should be syntactic.
# I like the idea that defining A -> B := ~A v B means that the RHS will be interpreted
# as if it were the RHS. this permits distinct syntactic expressions to have identical
# semantic clauses. the alternative is to eliminate one expression for another which 
# would make printing the prefix/infix sentence a little odd since if you feed it a 
# premise like A -> B, you'd expect this to be printed out, not ~A v B. 
    # M: This is what happens under the current implementation—ie A and B are printed for A -> B
# B: I guess one could
# store the original prefix sentence, then convert to its definition using that to find
# find the z3 constraints, then when it comes time to print, process the original?
    # M: I think that's basically what ends up happening here
# B: this more or less amounts to the more purely semantic approach here. the only cost is that
# whereas in logic a defined symbol is strictly speaking excluded from the object language
# here we have defined operators as syntactic primitives with derived semantic clauses.
    # M: ah I see—so you're considering the object language to be everything the user interacts
    # with? 
# in any case, I think this is a reasonable way to proceed, though perhaps worth thinking
# what a purely syntactic approach would look like.
# M: Good to DISCUSS on Friday—to me it seems the current approach is purely syntactic though
# I think I'm not understanding the issue fully (also it doesn't help that the code below
# isn't exactly straightforward)

[benbrastmckie]

I just got the following Sobel sequence to run in .016 seconds:

# CF_CM12: SOBEL SEQUENCE
N = 3
premises = [
    '(A \\boxright X)',
    '\\neg ((A \\wedge B) \\boxright X)',
    '(((A \\wedge B) \\wedge C) \\boxright X)',
    '\\neg ((((A \\wedge B) \\wedge C) \\wedge D) \\boxright X)',
    '(((((A \\wedge B) \\wedge C) \\wedge D) \\wedge E) \\boxright X)',
    '\\neg ((((((A \\wedge B) \\wedge C) \\wedge D) \\wedge E) \\wedge F) \\boxright X)',
    '(((((((A \\wedge B) \\wedge C) \\wedge D) \\wedge E) \\wedge F) \\wedge G) boxright X)', # 327.2 seconds on the MIT servers; now .01244 seconds
]
conclusions = []
contingent_bool = True
disjoint_bool = False

In the old model checker, it took the MIT servers 327.2 seconds. This bodes well.

[mbuit82]

Wow, that's impressive! Is it because of the finite quantifiers now?

[benbrastmckie]

It had finite quantifiers in the old version and this definitely sped things up. I haven't done any systematic comparisons, but is running really fast which is great. I might add a timers for building model_constraints and model_structure just to get a better sense of what is going on.

I will also try to get the optimizer to work from before since this will help a lot to test where certain models time out in complexity. I'm thinking of testing the derived and primitive versions of different operators to see if there is any difference in speed. Given how fast it is already, I'm not expecting it to be significant, but it would be good to show this.

[mbuit82]

Sounds good! DefinedOperator should be completely up and running now if you pull again, I fixed some bugs I was having with \\Diamond. Please do let me know if you find any bugs though because I am not confident DerivedOperator's completely debugged yet lol