this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
remove bv_eq_axioms as an external option to toggle.
Diseqalities have to be enforced for extensionality.
There are no internal code paths where the option is set to false.
An initial update to support polymorphism from SMTLIB3 and the API (so far C, Python).
The WIP SMTLIB3 format is assumed to be supporting the following declaration
```
(declare-type-var A)
```
Whenever A is used in a type signature of a function/constant or bound quantified variable, it is taken to mean that all instantiations of A are included in the signature and assertions.
For example, if the function f is declared with signature A -> A, then there is a version of f for all instances of A.
The semantics of polymorphism appears to follow previous proposals: the instances are effectively different functions.
This may clash with some other notions, such as the type signature forall 'a . 'a -> 'a would be inhabited by a unique function (the identity), while this is not enforced in this version (and hopefully never because it is more busy work).
The C API has the function 'Z3_mk_type_variable' to create a type variable and applying functions modulo polymorphic type signatures is possible.
The kind Z3_TYPE_VAR is added to sort discriminators.
This version is considered as early alpha. It passes a first rudimentary unit test involving quantified axioms, declare-fun, define-fun, and define-fun-rec.
check-assumptions with compound formulas create fresh proxy variables both during compilation to internal format and for the assumptions. These fresh variables may occur in lemmas that are created during search. The lemmas are garbage for future check-sats, but the solver needs to be allowed to invoke GC. Adding a GC call before a check-sat with assumptions allows removing some lemmas every time a new assumptions are used. Eager GC when using assumptions is used elsewhere, for example in cube&conquer scenarios where lemmas learned from one set of assumptions are less likely to be useful for other assumptions.
With the GC invocation memory grows at a lesser pace. However, it is not entirely free of memory increases. To avoid memory bloat, have the solver pre-compile the assumptions by defining them as propositional variables, add assertions that the propositional variables are equivalent to the compound formulas and use the propositional variables as assumptions. The same propositional variables come with no extra overhead when invoking check-assumptions. The lemmas are then over the same fixed vocabulary. It is generally a good idea to recycle useful lemmas during the enumeration pass.
destructive equality resolution uses an occurs check function that is only safe for quantifier-free formulas. In the special case where a bound variable is Boolean and occurs on a side of an equality the other side cannot have a quantifier.
- scan_for_linear returns true if it finds a new linear equation. It then should break GB.
- if scan_for_linear returns false, it should still allow try_modify_eqs.
This behavior was masked by requiring scan_for_linear to always be true before
allowing try_to_modify_eqs.
based on repro from Guido Martinez @mtzguido
deals with fluke regression for F* reported by Guido Martinez
Background:
The automatic pattern inference facility looks for terms that contains all bound variables of a quantifier. It may end up with a term that contains all bound variables but the extracted term can be simplified.
Example. The pattern
(ApplyTT (ApplyTT @x3!1 (ApplyTT @x4!0 (:var 1))) (ApplyTT @x4!0 (:var 0)))
can be decomposed into a multi-pattern
(ApplyTT @x4!0 (:var 1))) (ApplyTT @x4!0 (:var 0))
The multi-pattern may enable a quantifier instantiation while the original pattern does not. The multi-pattern should be preferred.
The regression showed up based on a change that should not be considered harmful but turned out to be noticeable.
The change was a simplification of and-or expressions based on sorting. This played with the case split queue used by F* (smt.case_split = 3) that uses a top-level case split of clauses to avoid redundant branches. The net effect was that without sorting, the benchmarks would always choose the opportune branch that enabled matching against the larger term. With sorting it would mostly choose inopportune branches.
