Since OpenSMT does not garbage-collect unused terms, we have to be more careful with creating unnecessary terms.
When the number of terms grows too large (in the order of hundred of thousands), it causes slowdown in OpenSMT in surprising places. Namely, OpenSMT in some places creates a vector with size equal to the number of all known terms, even though it actually needs to remember some information for only a tiny fraction of all the terms.
This starts to show in performance investigations in Golem, where we often create large number of very simple queries.
This PR avoids term creation in two places in Spacer.
When testing local reachability, we avoid creating unnecessary negations for proof obligations.
In proof production, we avoid creating unnecessary equalities, equating variables with their values (when we can just directly simplify the rest of the query with these substitutions).
More details are in the individual commit messages.
Since OpenSMT does not garbage-collect unused terms, we have to be more careful with creating unnecessary terms. When the number of terms grows too large (in the order of hundred of thousands), it causes slowdown in OpenSMT in surprising places. Namely, OpenSMT in some places creates a vector with size equal to the number of all known terms, even though it actually needs to remember some information for only a tiny fraction of all the terms. This starts to show in performance investigations in Golem, where we often create large number of very simple queries.
This PR avoids term creation in two places in Spacer.
More details are in the individual commit messages.