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>
When merging two type substitutions, util::unify(substitution, substitution,
substitution) inserted bindings without an occurs-check. Merging maps such as
A |-> list(B) and B |-> list(A) produced a self-referential binding
B |-> list(list(B)), and applying that substitution recursed forever, causing
a stack overflow during the first polymorphic instantiation round.
This was exposed by encoding TPTP $tType quantification as polymorphism
(8ee8a3cda): mutually-recursive polymorphic types in THF problems (e.g.
COM/DAT/ITP Coq-derived files) triggered 60 stack-overflow crashes during
check_sat.
Add occurs-checks so a binding that would make the substitution cyclic causes
the merge to fail (the instantiation is soundly skipped). Values are resolved
against the current substitution before insertion, preserving the acyclic
invariant.
Verified: the 60 previously-crashing TPTP files now terminate cleanly;
92/92 unit tests pass.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
In polymorphism::substitution::operator()(sort*), each substituted
sub-sort was held only in a local sort_ref that was destroyed at the end
of the loop iteration, while its raw pointer was retained in the
parameter vector passed to mk_sort. When the sub-sort's refcount dropped
to zero, its memory was freed and then reused by the next allocation,
producing a self-referential sort. Structural sort traversals such as
has_type_var (which has no cycle detection) then recursed infinitely,
manifesting as a stack overflow.
Pin each intermediate sub-sort in a sort_ref_vector so it stays alive
until after mk_sort has taken its own references.
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.
