3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 19:45:41 +00:00

Set pi.avoid_skolems=false for TPTP solver runs (#10100)

The TPTP frontend was not forcing `pi.avoid_skolems=false`, so TPTP
problems could be solved with the default pattern-inference behavior
instead of the intended frontend-specific setting. This change applies
the override directly to the solver used by TPTP runs.

- **What changed**
- After constructing the TPTP solver, the frontend now sets
`pi.avoid_skolems=false` via solver parameters before `check_sat`.
- The override is scoped to the TPTP solver instance instead of mutating
process-global parameter state.

- **Why this shape**
- Keeps the TPTP behavior explicit at the point where the solver is
created.
  - Avoids leaking the parameter change into unrelated solver contexts.

- **Code sketch**
  ```c++
  ctx.set_solver_factory(mk_smt_strategic_solver_factory());
  params_ref solver_params;
  solver_params.set_bool("pi.avoid_skolems", false);
  ctx.get_solver()->updt_params(solver_params);
  ```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-12 19:21:25 -07:00 committed by GitHub
parent 0000e16851
commit 0b8335e776
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -2934,6 +2934,9 @@ static unsigned read_tptp_stream(std::istream& in, char const* current_file) {
p.assert_distinct_objects();
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
params_ref solver_params;
solver_params.set_bool("pi.avoid_skolems", false);
ctx.get_solver()->updt_params(solver_params);
// Optional: dump the parsed goal as an SMT-LIB2 benchmark (env Z3_TPTP_DUMP_SMT2
// gives the output file path). Used to produce SMTLIB versions of TPTP instances.