Marco Gario
Marco Gario
In https://github.com/pysmt/pysmt/issues/731#issuecomment-1200380943, we discussed how having a non-deterministic answer in `get_logic` can lead to problems. We do not expect the logic detection in `get_logic` to pick "the best" logic, but...
Pass logic to _verify_ackermannization so we can check for preconditions there and ensure we use the same logic throughout the test. Fixes https://github.com/pysmt/pysmt/issues/731
`pysmt/test/test_rewritings.py:test_ackermannization_for_examples` fails non-deterministically. Kudos @enmag for the [analysis](https://github.com/pysmt/pysmt/pull/730#issuecomment-1200018521): > The difference seems to be in the order of the filtered_logics, which corresponds to the list of pysmt-supported logics greater than...
Complete the deprecation of instance-based walkers by removing the Walker.functions dictionary.
The `functions` dictionary in the `Walker` was used to map each nodetype to the corresponding `walk` method. We called this "instance based walkers" because each instance could (in principle) associate...
Let's spend a few weeks to clean-up the project and focus on some key issues! I propose we break this down into two phase: ### 1. Prioritizing (until June 1st...
Continuation of #478, due to orphaning of source repo. Open issues: - Implementation of simplifier - Testcases
+, *, =, and & are all examples of commutative operations. In pySMT we treat the expression `a = b` as a different expression than `b = a`. This is...
Makes the boilerplate of the benchmarking framework easier to use. It would be nice to: - Include the SMT-LIB files as git submodules - Provide some way to diff two...
This should provide support for Enums at pySMT level. Ideally, these are then bit-blasted during the conversion to the solver. Alternatively, the encoding might try to use whatever theory is...