mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity
20560 commits 46 branches 56 tags 170 MiB
Commit graph

17190 commits

Author SHA1 Message Date
Lev Nachmanson
b77bf3c97e use std::map instead of std::unordered_map 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:41 -10:00
Lev Nachmanson
7030832273 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
0800dd9bc7 define symbolic_interval 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
9d5295fa97 more scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
d41ba603c8 closer to the paper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
0fdbd2cba1 scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
2ea22b5972 scaffoldin 2026-01-31 15:56:40 -10:00
Lev Nachmanson
66a7eb24f7 t2 2026-01-31 15:56:40 -10:00
Lev Nachmanson
b53317bb9a t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Lev Nachmanson
9e51f34475 t0 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-31 15:56:40 -10:00
Copilot
89e2ceffd0
Use structured bindings for stack entries in theory_datatype (#8442) 
* Initial plan

* Refactor theory_datatype to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix structured binding syntax error in smt_justification.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-31 17:14:47 -08:00
Copilot
e7d46d2566
Refactor expr_stat to use structured bindings for traversal pairs (#8441) 
* Initial plan

* Refactor expr_stat.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix structured binding inside DEBUG_CODE macro in smt_justification.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-31 17:14:02 -08:00
Copilot
ff485eb545
Refactor sat_model_converter to use C++17 structured bindings (#8440) 
* Initial plan

* Refactor sat_model_converter to use C++17 structured bindings

- Updated model_converter::process_stack() to use structured bindings
- Updated model_converter::display() to use structured bindings
- Updated model_converter::expand() to use structured bindings in range-based loop
- All changes compile successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix build error in smt_justification.cpp structured binding

- Changed invalid syntax `enode_pair const & [n1, n2]` to `auto const& [n1, n2]`
- Wrapped for loop in extra parentheses to protect structured binding comma from macro expansion
- Build now completes successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix DEBUG_CODE macro issue with structured bindings

- Reverted DEBUG_CODE block to use .first/.second instead of structured bindings
- Structured bindings with commas cause issues in macros (treated as argument separators)
- Build now works in both debug and release modes

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-31 17:13:07 -08:00
Copilot
db6e15361b
Add Java APIs for polymorphic datatypes (#8438) 
* Initial plan

* Add Java APIs for polymorphic datatypes and type variables

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix code review issue and add documentation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add TypeVarSort.java to CMakeLists.txt for Java bindings

The CMake build was failing because TypeVarSort.java was not included in the Z3_JAVA_JAR_SOURCE_FILES list in src/api/java/CMakeLists.txt. Added it in alphabetical order between TupleSort.java and UninterpretedSort.java.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-31 15:31:36 -08:00
Nuno Lopes
b008b5e926 remove another use of rational::power_of_two() 2026-01-31 14:29:33 +00:00
Nuno Lopes
e1fc837141 minor simplification 2026-01-31 14:19:53 +00:00
Nuno Lopes
09370d7782 optimize has_sign_bit and mod2k to not compute powers of two 
this is very useful for bitvectors of large bitwidths
 2026-01-31 10:38:41 +00:00
Nuno Lopes
10043c37fd fix build 2026-01-30 16:38:23 +00:00
Nuno Lopes
5f835dd99c fix build 2026-01-30 16:29:30 +00:00
Nuno Lopes
095b2bdf59 code simplifications 2026-01-30 15:26:21 +00:00
Nuno Lopes
70a03c7784 constify a constant 
shrinks binary size by 4KB
 2026-01-30 15:01:53 +00:00
Nuno Lopes
7edc4e088a fix build 2026-01-30 14:21:57 +00:00
Copilot
4a1c2f44c5
Fix assertion violation in mpzzp_manager::eq from non-normalized values in peek_fresh (#8439) 
* Initial plan

* Normalize values in peek_fresh and newton_interpolator::add

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Simplify fix - only normalize in peek_fresh with assertions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete regressions/issue-8292.smt2

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-29 19:19:59 -08:00
Copilot
0519e6231c
Optimize iterator bit scanning and variable matching per TODO directives (#8416) 
* Initial plan

* Optimize approx_set iterator and variable_intersection populate

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

* Add clarifying comment for iterator optimization

Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nunoplopes <2998477+nunoplopes@users.noreply.github.com>
 2026-01-29 19:02:13 -08:00
Copilot
477e4d695d
Refactor SMT core: use structured bindings for enode_pair access (#8427) 
* Initial plan

* Refactor SMT core to use C++17 structured bindings for enode pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Use const& in structured bindings to avoid copying

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor variable unpacking in DEBUG_CODE

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-29 19:01:49 -08:00
Lev Nachmanson
adac953e87 - When removing a fresh var xt, collect all fresh defs that transitively reference it 
- Remove them all from m_fresh_k2xt_terms and m_row2fresh_defs
    - Mark rows containing those vars in m_changed_rows for recalculation
    - Move remove_irrelevant_fresh_defs() before the recalculate loop so all affected rows get recalculated

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-29 06:17:14 -10:00
Copilot
1ec30620ef
Refactor optimization and model to use C++17 structured bindings for pairs (#8426) 
* Initial plan

* Refactor pairs to use C++17 structured bindings in opt and model components

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:43:57 -08:00
Copilot
0b1d30e86f
[WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425) 
* Initial plan

* Refactor NLSAT solver to use structured bindings for variable bounds

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:42:40 -08:00
Copilot
ebed679287
Refactor dyn_ack.cpp to use structured bindings for app_pair/app_triple (#8359) 
* Initial plan

* Refactor dyn_ack.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Rename structured binding variables from app1/app2/app3 to a1/a2/a3

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:39:25 -08:00
Copilot
3f9fa59811
Refactor der.cpp topological sort to use structured bindings (#8401) 
* Initial plan

* Refactor der.cpp to use structured bindings for expression/index pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix comment to refer to 'e' instead of 't' after structured binding refactor

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-28 19:38:58 -08:00
Nikolaj Bjorner
203afaab07 address #8376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-27 20:22:41 -08:00
Copilot
1d49af5ee6
Refactor sat_solver to use C++17 structured bindings for pair destructuring (#8403) 
* Initial plan

* Refactor sat_solver.cpp to use structured bindings for pairs

- Line 1398: Changed priorities[i].second to use [priority, var]
- Lines 2154-2156: Changed p.first/p.second to use [l1, l2] for binary clauses
- Lines 4182-4184: Eliminated intermediate l1, l2 variables using [l1, l2] binding

This modernizes the code to use C++17 structured bindings instead of .first/.second member accesses.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:06:07 -08:00
Copilot
560985893e
Refactor bound_manager to use C++17 structured bindings (#8404) 
* Initial plan

* Refactor bound_manager to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:04:01 -08:00
Copilot
7747a17bb7
Refactor theory_array_base to use structured bindings for enode pairs (#8405) 
* Initial plan

* Refactor theory_array_base to use structured bindings for enode pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 20:03:18 -08:00
Copilot
ef5ee85bfd
Refactor pb_solver to use structured bindings for wliteral patterns (#8391) 
* Initial plan

* Refactor pb_solver.cpp to use C++17 structured bindings for wliteral patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix active2wlits to avoid unnecessary wliteral reconstruction

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 13:58:14 -08:00
Copilot
8cb403384e
Refactor theory_lra: Use structured bindings for pair patterns (#8387) 
* Initial plan

* Refactor theory_lra.cpp with structured bindings for pair patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 13:57:43 -08:00
Copilot
c4f75bc85a
Refactor seq_rewriter to use C++17 structured bindings (#8381) 
* Initial plan

* Refactor seq_rewriter.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback - move pair declaration inside loop

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:06:11 -08:00
Copilot
851e69d7d2
Refactor sat_th to use structured bindings for enode_pair patterns (#8386) 
* Initial plan

* Apply structured bindings to enode_pair patterns in sat_th.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:02:28 -08:00
Copilot
e4ba45925e
Refactor theory_seq to use structured bindings for pair patterns (#8390) 
* Initial plan

* Refactor theory_seq.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 12:01:29 -08:00
Copilot
ccc20449dc
Refactor bv_solver to use structured bindings for var_pos patterns (#8384) 
* Initial plan

* Refactor bv_solver.cpp to use C++17 structured bindings for var_pos patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: simplify bit_trail constructor and remove unnecessary pair reconstruction

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:48:21 -08:00
Copilot
ea1ebdeae0
Refactor smt_context to use structured bindings for pair decomposition (#8385) 
* Initial plan

* Refactor smt_context.cpp to use C++17 structured bindings for pair patterns

- Replace .first/.second access with structured bindings in reset_tmp_clauses()
- Replace .first/.second access with structured bindings in decide_clause()
- Replace .first/.second access with structured bindings in init_assumptions()
- Eliminate 3 intermediate variable assignments
- 4 refactoring sites across 3 functions
- Verified successful compilation and all tests pass

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:47:31 -08:00
Copilot
ffa8ef4cee
Refactor pb_rewriter to use structured bindings for expression/coefficient pairs (#8380) 
* Initial plan

* Refactor pb_rewriter to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 11:46:28 -08:00
Copilot
01948e168b
Add polymorphic datatype support to ML API (#8378) 
* Initial plan

* Add ML bindings for polymorphic datatypes (mk_type_variable and mk_polymorphic_sort)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add polymorphic datatype example for ML API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete examples/ml/polymorphic_datatype_example.ml

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-27 11:44:35 -08:00
Copilot
cd774b6fdb
Refactor sat_anf_simplifier to use C++17 structured bindings (#8358) 
* Initial plan

* Refactor sat_anf_simplifier.cpp to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-27 09:59:26 -08:00
Nikolaj Bjorner
76d46ee48a Revert "Refactor find_tactic_cmd to use std::optional<tactic_cmd*> (#8331)" 
This reverts commit 7b182c9440.
 2026-01-26 13:20:03 -08:00
Nikolaj Bjorner
3f26d42215 Revert "Refactor find_probe() to use std::optional (#8334)" 
This reverts commit 49817bc259.
 2026-01-26 13:19:56 -08:00
Nikolaj Bjorner
7a2eea6f40 Revert "Refactor find_psort_decl() to return std::optional<psort_decl*> (#8339)" 
This reverts commit 445f995c54.
 2026-01-26 13:19:51 -08:00
Copilot
0a68837ef2
Expose timestamp method in sls_context (#8347) 
* Initial plan

* Expose timestamp method in sls_context

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-01-26 11:27:27 -08:00
Nikolaj Bjorner
4a29326eaa
Reset timestamp for variables in sat_ddfw.cpp 2026-01-26 10:12:05 -08:00
Nikolaj Bjorner
d18cc5629a
Update timestamp on variable flip in ddfw 2026-01-26 10:11:14 -08:00