Model-checker

This release significantly refactors the code base to accommodate greater modularity for defining semantic clauses for different operators across different semantic theories. In addition to making it easy to add new operators with novel semantic clauses, this version makes it easy to compare define and compare different semantic theories. The CLI has been updated to generate new projects when run with no arguments so that users can easily adapt the default semantic theory which is used as a template. A number of definitions have also been exposed for easy importing.

Future patches will extend the utilities included for comparing theories and will add default unit tests to the project template so as to streamline implementation.

https://pypi.org/project/model-checker/

Z3's quantifiers have been replaced by functions which generate finite conjunctions and disjunctions, leading to a massive performance gain. The following new features have also been included:

- The user can specify a `max_time` and is prompted to increase the time if the `model-checker` times out.
- The user can set an `optimize` variable with override flag `-o` to have the model-checker find a model with the smallest number of atomic elements within the `max_time`.
- The user can set the `contingent` variable with override flag `-c` to require all propositions to be contingent, i.e., to have some possible verifier and some possible falsifier. Since the null state cannot verify nor falsify a contingent proposition, constraints on propositions to only have non-null verifiers and falsifiers have been removed.

In addition to these features, the unit tests have been expanded to now include 120 examples which are divided by logical operators.

This release provides more detailed printing and interprets conclusions disjunctively.