mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-05 03:09:01 +00:00
Code Activity
22335 commits 60 branches 58 tags 215 MiB
Commit graph

18113 commits

Author SHA1 Message Date
CEisenhofer
87c5be8904 Fixed progress annotations 2026-03-12 11:22:42 +01:00
CEisenhofer
1351efe9af Unit cases 2026-03-12 11:13:18 +01:00
copilot-swe-agent[bot]
995e0e1f14 Deprecate injectivity_tactic.cpp: forward mk_injectivity_tactic to simplifier-based impl 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 05:32:32 +00:00
copilot-swe-agent[bot]
ec9fee969d Remove old special_relations_tactic class, use simplifier-based tactic as the sole special-relations tactic 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 05:30:57 +00:00
Lev Nachmanson
3176151cc2 rename bhn_opt to max_reg 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-03-11 19:18:45 -10:00
copilot-swe-agent[bot]
fb31b689ea Add special_relations_simplifier: new simplifier and tactic registration 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 04:39:05 +00:00
copilot-swe-agent[bot]
c303b56f04 Add injectivity_simplifier and register injectivity2 tactic + injectivity simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 04:37:17 +00:00
Lev Nachmanson
b8d6952e9e Enable som (sum of monomials) in optimizer simplification 
The optimizer's simplification pass did not expand products of sums
into sum-of-monomials form. This caused mathematically equivalent
expressions like (5-x)^2 vs (x-5)^2 to simplify into different
internal forms, where the former produced nested multiplies
(+ 5.0 (* -1.0 x)) that led to harder purification constraints
and solver timeouts.

Enabling som=true in the first simplification tactic normalizes
polynomial objectives into canonical monomial form, making the
optimizer robust to operand ordering.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-11 18:28:40 -10:00
copilot-swe-agent[bot]
9813b2adfb Merge branch 'c3' of https://github.com/Z3Prover/z3 into copilot/add-parikh-filter-implementation-again 2026-03-12 04:22:43 +00:00
Lev Nachmanson
ce7c7f458e Add max_rev test: BNH with reversed argument order in f1/f2 
Same as test_bnh_optimize but constructs f1 and f2 with reversed
parameter order in mk_add, mk_mul, mk_sub calls. Exposes optimizer
sensitivity to expression structure.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-11 18:15:57 -10:00
copilot-swe-agent[bot]
dac52ae4e0 remove smt_kernel.h dependency from seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-12 03:00:38 +00:00
Nikolaj Bjorner
6fa3c7eabb
Merge branch 'c3' into copilot/add-parikh-filter-implementation-again 2026-03-11 19:27:03 -07:00
Nikolaj Bjorner
3d36fb95ec
Merge branch 'c3' into copilot/update-simple-solver-incremental-mode 2026-03-11 19:24:21 -07:00
copilot-swe-agent[bot]
01f9709ff6 Add vector::resize tests including vector<rational> 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-03-11 23:54:01 +00:00
Lev Nachmanson
8e47c0d842 Fixed the assertion violation in mpz.cpp:602 when running with -tr:arith. 
**Root cause**: `vector::resize(SZ s, Args args...)` in `src/util/vector.h` took `args` by value and used `std::forward<Args>(args)` in a loop. The first iteration moved from `args`, leaving all subsequent elements with a moved-from state (`rational{0/0}` instead of
`rational{0/1}`). This corrupted the coefficient vector in the pretty printer, causing a division-by-zero assertion when multiplying.

**Fix**: Changed `resize` to take `Args const& args` and copy-construct each element instead of forwarding/moving.
 2026-03-11 12:43:59 -10:00
copilot-swe-agent[bot]
a51ba544ea Fix typo: rename m_parith to m_parikh in seq_nielsen.h/.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 19:08:11 +00:00
copilot-swe-agent[bot]
4b2f5e2bb0 Add seq_parikh unit tests: 32 tests covering stride, constraints, conflict, char_set 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 18:36:28 +00:00
copilot-swe-agent[bot]
30c2a9ccdc Address code review: add SASSERT for lo>hi, simplify is_to_re handling 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:23:00 +00:00
copilot-swe-agent[bot]
194dfe6c61 Port ZIPT Parikh features: minterm_to_char_set, char range constraints, fix stride soundness 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:21:27 +00:00
CEisenhofer
99727faf70 Model reconstruction 2026-03-11 18:13:16 +01:00
copilot-swe-agent[bot]
255d381b72 Make simple_solver incremental: use push/pop scopes in Nielsen DFS 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 17:09:34 +00:00
copilot-swe-agent[bot]
45a574d7fa Remove nseq_parith.h and nseq_parikh.cpp backwards-compat shims 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 15:48:05 +00:00
CEisenhofer
d23f376b39 Fixed a lot regarding powers, but there seems to be a model reconstruction bug left 2026-03-11 16:44:14 +01:00
CEisenhofer
6d0468861d Fixed git merge problems 2026-03-11 13:05:27 +01:00
CEisenhofer
2f46c8893e Another attempt to fix powers 2026-03-11 11:29:25 +01:00
copilot-swe-agent[bot]
213ddd36ba Rename nseq_parikh→seq_parikh; add m/seq/a member attributes to seq_parikh 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:41:16 +00:00
copilot-swe-agent[bot]
4ac5315846 Fix review: min>=max guard, ceiling-div overflow, SASSERT, accessor methods, comments 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:15:20 +00:00
copilot-swe-agent[bot]
eca5fcc7bb Integrate nseq_parith into nielsen_graph; add k upper bound and check_parikh_conflict 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 05:10:30 +00:00
copilot-swe-agent[bot]
35ee8f917d Remove redundant zero-guards before u_gcd calls in concat/intersection cases 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:26:26 +00:00
copilot-swe-agent[bot]
4cdfceabc5 Use u_gcd from util/mpz.h instead of local gcd definition 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:24:16 +00:00
copilot-swe-agent[bot]
d267e452a2 Add Clemens Eisenhofer as co-author to nseq_parith.h and nseq_parikh.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 04:21:30 +00:00
Lev Nachmanson
274d64299e Address PR review: add ENSURE checks, fix duplicate test, fix comment 
- Add ENSURE(result == Z3_L_TRUE) for each BNH optimization call and
  ENSURE(num_sat == 7) at the end so CI catches regressions.
- Remove test_bnh_optimize() from tst_api() to avoid duplicate
  execution under /a; keep standalone tst_bnh_opt() entry point.
- Fix Test 2 comment: it tests same-size backup, not backup-longer.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-10 16:58:24 -10:00
Lev Nachmanson
6d890fb026 Fix NLA optimization regression and relax restore_x 
- Relax restore_x() to handle backup/current size mismatches: when
  backup is shorter (new columns added), call
  move_non_basic_columns_to_bounds() to find a feasible solution.
- Fix 100x performance regression in nonlinear optimization: save LP
  optimum before check_nla and return it as bound regardless of NLA
  result, so opt_solver::check_bound() can validate via full re-solve
  with accumulated NLA lemmas.
- Refactor theory_lra::maximize() into three helpers: max_with_lp(),
  max_with_nl(), and max_result().
- Add mk_gt(theory_var, impq const&) overload for building blockers
  from saved LP optimum values.
- Add BNH multi-objective optimization test (7/7 sat in <1s vs 1/7
  in 30s before fix).
- Add restore_x test for backup size mismatch handling.

Fixes #8890

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
 2026-03-10 16:38:08 -10:00
copilot-swe-agent[bot]
334df71b11 Add nseq_parith.h and nseq_parikh.cpp: Parikh filter for ZIPT string solver 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-11 00:05:26 +00:00
Nikolaj Bjorner
53d5d98341
Merge branch 'c3' into copilot/implement-int-bounds-var-bound-watcher 2026-03-10 16:33:25 -07:00
copilot-swe-agent[bot]
57ede4cdcd Address code review: clarify add_lower/upper_int_bound return semantics; fix test assertion 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 23:29:15 +00:00
copilot-swe-agent[bot]
47f9be0270 Implement IntBounds/VarBoundWatcher + Constraint.Shared; fix pre-existing build errors 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 23:26:55 +00:00
Nikolaj Bjorner
3a71f28c6c
Rename dummy_simple_solver to zipt_dummy_simple_solver 2026-03-10 15:49:24 -07:00
copilot-swe-agent[bot]
0efb7402e8 Fix build: add dummy_simple_solver to nseq_zipt.cpp fixture, fix assert_expr in seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 22:47:49 +00:00
Nikolaj Bjorner
d2739d9816 use reference to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-10 15:22:50 -07:00
Nikolaj Bjorner
c98ea6dc21 make simple solver a reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-03-10 15:10:51 -07:00
copilot-swe-agent[bot]
5744958e46 Replace lp_simple_solver in nielsen with context_solver using smt::kernel (seq_len) 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 21:39:29 +00:00
Nikolaj Bjorner
a8269c7d98
Merge pull request #8930 from Z3Prover/copilot/introduce-constraints-on-s 
Use mod-based constraints for semi-linear regex length sets
 2026-03-10 13:33:43 -07:00
copilot-swe-agent[bot]
334e6da60d Guard mod constraint: skip for period <= 1 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 20:14:53 +00:00
copilot-swe-agent[bot]
2bae0f02c4 Replace fresh-variable semi-linear constraint with mod-based approach 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 19:48:18 +00:00
copilot-swe-agent[bot]
472d9bde6c Fix unused variable build warnings in theory_finite_set, theory_finite_set_size, theory_nseq 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:52:40 +00:00
Nikolaj Bjorner
83c8743ea7
Merge pull request #8925 from Z3Prover/copilot/add-theory-seq-len-solver 
Add theory_seq_len: partial sequence length axiomatization via semi-linear constraints
 2026-03-10 11:36:33 -07:00
copilot-swe-agent[bot]
d4b99730b9 Fix build error: remove stale dep_tracker method definitions from seq_nielsen.cpp 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:30:33 +00:00
copilot-swe-agent[bot]
56e9e9df57 Add theory_seq_len: partial axiom instantiation for sequence length constraints 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-03-10 18:02:04 +00:00
Nikolaj Bjorner
2e636ec25d
Merge branch 'c3' into copilot/replace-lp-solver-with-abstract-solver 2026-03-10 10:35:44 -07:00