The polymorphism theory routed polymorphic (\) problems through
theory_polymorphism, which instantiated axioms during search. Two leaks:
1. In inst::instantiate, insert_ref_map was constructed with an expr_ref
argument, so its template parameter D deduced to expr_ref instead of
expr*. Trail objects are region-allocated and freed without running
destructors, so the embedded expr_ref never released its reference,
leaking one AST subtree per instantiation. Pass e_inst.get() so D is
expr*, matching the raw hashtable + manual inc_ref/dec_ref pattern.
2. trail_stack's destructor does not call reset(), so level-0 trail items
(including the inc_ref balancing entries for m_from_instantiation) were
never undone when the theory was destroyed. Added a ~theory_polymorphism
destructor that calls m_trail.reset().
Also keeps a defensive alias check in util::unify and a fresh per-iteration
substitution in inst::instantiate.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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.
