mirror of
https://github.com/Z3Prover/z3
synced 2026-07-05 14:56:11 +00:00
5bd485eb03
Fixes soundness/completeness of the TPTP frontend for polymorphic (TF1/TH1)
problems, reducing TPTP-v9.2.1 BUG verdicts from 28 to 4.
* Treat regular-forall "! [A: $tType] : ..." as genuine type quantification
(bind A via mk_type_var) instead of monomorphizing it to the universe sort.
This is the standard THF/TH1 way to quantify over types, and monomorphizing
it silently prevented theory_polymorphism from instantiating the axioms.
* Use the plain smt solver (mk_smt_solver_factory) for problems that contain
type variables. The strategic solver's tactic preprocessing eliminates the
unconstrained conjecture instance before the core can link it to its
polymorphic axiom, yielding a spurious CounterSatisfiable.
* Detect value-indexed dependent type families ("T > $tType"), which the
parametric-polymorphism encoding cannot represent soundly, and downgrade
both sat and unsat verdicts to GaveUp (previously produced unsound Theorems,
e.g. SEV600/601/602).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| extra_cmds | ||
| basic_cmds.cpp | ||
| basic_cmds.h | ||
| CMakeLists.txt | ||
| cmd_context.cpp | ||
| cmd_context.h | ||
| cmd_context_to_goal.cpp | ||
| cmd_context_to_goal.h | ||
| cmd_util.cpp | ||
| cmd_util.h | ||
| echo_tactic.cpp | ||
| echo_tactic.h | ||
| eval_cmd.cpp | ||
| eval_cmd.h | ||
| parametric_cmd.cpp | ||
| parametric_cmd.h | ||
| pdecl.cpp | ||
| pdecl.h | ||
| README | ||
| simplifier_cmds.cpp | ||
| simplifier_cmds.h | ||
| simplify_cmd.cpp | ||
| simplify_cmd.h | ||
| tactic_cmds.cpp | ||
| tactic_cmds.h | ||
| tactic_manager.cpp | ||
| tactic_manager.h | ||
| tptp_frontend.cpp | ||
| tptp_frontend.h | ||
Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0. It is also provides the solver abstraction to plugin solvers in this kind of front-end.