mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 15:34:41 +00:00
Code Activity
20599 commits 54 branches 58 tags 179 MiB
Commit graph

20599 commits

This branch
This branch
All branches
Author SHA1 Message Date
Copilot
ae1945453f Add missing solver APIs to Java and C# bindings (#8464) 
* Initial plan

* Add missing solver APIs for Java and C#

- Issue 3: Add getTrailLevels() to Java and TrailLevels property to C#
- Issue 4: Add cube() iterator to Java (C# already had Cube())
- Issue 5: Add setInitialValue() to Java and SetInitialValue() to C#

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

* Fix code review feedback: eliminate redundant trail retrieval

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

* Improve documentation and efficiency based on code review

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-02-18 20:58:01 -08:00
Copilot
9758b7646f Remove redundant explicit default constructors (#8470) 
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
 2026-02-18 20:58:01 -08:00
Copilot
17c8958d70 Remove redundant default constructors when they're the only constructor (#8461) 
* Initial plan

* Modernize C++ constructors to use C++11 default member initialization - Phase 1

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

* Fix theory_pb.h struct definition - move reset() back inside struct

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

* Modernize C++ constructors to use C++11 default member initialization - Phase 2

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

* Fix opt_solver.h - revert rational initialization (complex type)

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

* Modernize C++ constructors to use C++11 default member initialization - Phase 3

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

* Fix sparse_matrix.h - explicitly initialize union member in default constructor

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

* Remove unnecessary default constructors when they're the only constructor

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-02-18 20:58:01 -08:00
Copilot
a01a624fa3 Add workflow to build and cache Z3 for reuse across CI (#8466) 
* Initial plan

* Add Z3 build cache workflow and documentation

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

* Address code review feedback: improve cache strategy and documentation

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

* Fix cache restore-keys and update size documentation

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

* Delete .github/workflows/example-cached-z3.yml

---------

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-02-18 20:58:01 -08:00
Copilot
31e4945922 Remove redundant non-virtual destructors with = default (#8462) 
* Initial plan

* Remove 6 non-virtual destructors with no code (= default)

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-02-18 20:58:01 -08:00
Copilot
d4e0a7fe21 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-02-18 20:58:01 -08:00
Copilot
abbc76b7ae 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-02-18 20:58:00 -08:00
Copilot
5291328f63 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-02-18 20:58:00 -08:00
Copilot
3abf005676 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-02-18 20:58:00 -08:00
Nuno Lopes
1f505788c2 remove another use of rational::power_of_two() 2026-02-18 20:58:00 -08:00
Nuno Lopes
152db47275 minor simplification 2026-02-18 20:58:00 -08:00
Nuno Lopes
6c3f9a3540 optimize has_sign_bit and mod2k to not compute powers of two 
this is very useful for bitvectors of large bitwidths
 2026-02-18 20:58:00 -08:00
Copilot
9771839005 Enable ad-hoc deeptest workflow execution via workflow_dispatch (#8448) 
* Initial plan

* Remove slash_command and blocking activation conditions from deeptest workflow

- Remove slash_command configuration to eliminate team membership and command position checks
- Simplify workflow to only support workflow_dispatch for ad-hoc execution
- Remove pre_activation job and complex activation conditions
- Update README to reflect workflow_dispatch-only usage
- Keep file_path input parameter for specifying source files to test

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-02-18 20:58:00 -08:00
Nuno Lopes
0c73df9579 fix build 2026-02-18 20:58:00 -08:00
Nuno Lopes
72ddc6269d fix build 2026-02-18 20:58:00 -08:00
Nuno Lopes
8adb3a031e code simplifications 2026-02-18 20:58:00 -08:00
Nuno Lopes
5941073cad constify a constant 
shrinks binary size by 4KB
 2026-02-18 20:58:00 -08:00
Nuno Lopes
c0af7c5566 fix build 2026-02-18 20:57:59 -08:00
Copilot
7e8c3fbee0 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-02-18 20:57:59 -08:00
Copilot
b2082736ba 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-02-18 20:57:59 -08:00
Copilot
78381bb285 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-02-18 20:57:59 -08:00
Copilot
3c34c5c4d7 Remove structured bindings refactoring from code conventions analyzer (#8428) 
* Initial plan

* Remove structured bindings focus from code conventions analyzer

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

* Regenerate code-conventions-analyzer.lock.yml after removing 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-02-18 20:57:59 -08:00
Copilot
6d9b5e83b3 Add DeepTest agentic workflow for automated test generation (#8432) 
* Initial plan

* Create DeepTest agentic workflow for test generation

Co-authored-by: saikat107 <2145576+saikat107@users.noreply.github.com>

* Add documentation for DeepTest workflow

Co-authored-by: saikat107 <2145576+saikat107@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: saikat107 <2145576+saikat107@users.noreply.github.com>
 2026-02-18 20:57:59 -08:00
Lev Nachmanson
33aa584a67 - 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-02-18 20:57:59 -08:00
Copilot
5586a689ff 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-02-18 20:57:59 -08:00
Copilot
bbf984f182 [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-02-18 20:57:59 -08:00
Copilot
abd488f173 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-02-18 20:57:59 -08:00
Copilot
1853cdeb3d 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-02-18 20:57:59 -08:00
Copilot
5dd01acb42 Migrate PyPI publishing to Trusted Publishing (OIDC) (#8420) 
* Initial plan

* Migrate publish-pypi job to PyPI Trusted Publishing (OIDC)

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-02-18 20:57:58 -08:00
Nikolaj Bjorner
78cb28d0cd address #8376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-18 20:57:58 -08:00
Copilot
03730b038c 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-02-18 20:57:58 -08:00
Copilot
64c436d959 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-02-18 20:57:58 -08:00
Copilot
fc6757a354 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-02-18 20:57:58 -08:00
Copilot
d214ea71be Integrate Serena MCP server for C++ semantic analysis in SpecBot (#8410) 
* Initial plan

* Add Serena MCP server integration to SpecBot workflow for C++ analysis

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

* Clean up Serena integration - remove unnecessary env variable (auto-detects C++)

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-02-18 20:57:58 -08:00
Copilot
bb50e346d5 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-02-18 20:57:58 -08:00
Copilot
20d9b8645b 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-02-18 20:57:58 -08:00
Copilot
d1489f0d13 Change code conventions workflow schedule from every 3 hours to daily (#8402) 
* Initial plan

* Update code conventions workflow to run once daily instead of every 3 hours

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-02-18 20:57:58 -08:00
Copilot
b091bae4d2 SpecBot: Output to Discussions instead of Pull Requests (#8399) 
* Initial plan

* Replace create-pull-request with create-discussion for SpecBot

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-02-18 20:57:58 -08:00
Copilot
828fe2d702 Configure SpecBot workflow to use BOT_PAT for pull request authentication (#8398) 
* Initial plan

* Add GH_TOKEN env variable with BOT_PAT to SpecBot workflow

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-02-18 20:57:58 -08:00
Copilot
307982b67e 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-02-18 20:57:58 -08:00
Copilot
49cb81d538 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-02-18 20:57:57 -08:00
Copilot
c7a4b6e4c4 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-02-18 20:57:57 -08:00
Copilot
8a3c2f51c3 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-02-18 20:57:57 -08:00
Copilot
dadd23a517 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-02-18 20:57:57 -08:00
Copilot
aab17272f1 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-02-18 20:57:57 -08:00
Copilot
290cb5f811 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-02-18 20:57:57 -08:00
Copilot
918946a253 [WIP] Add SpecBot workflow for code annotation with assertions (#8388) 
* Initial plan

* Add SpecBot agentic workflow for automatic specification mining

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

* Fix SpecBot network configuration and add documentation

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-02-18 20:57:57 -08:00
Copilot
fa34cb5ad5 Remove std::optional from Code Conventions Analyzer workflow (#8360) 
* Initial plan

* Remove std::optional from Code Conventions Analysis workflow

- Remove std::optional from Exception Control Flow alternatives
- Remove std::optional from Prioritize safety guidelines
- Recompile workflow to update lock file

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-02-18 20:57:57 -08:00
Copilot
b6dab1533b 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-02-18 20:57:57 -08:00
dependabot[bot]
531bb1c31f Bump actions/cache from 4.3.0 to 5.0.2 (#8350) 
Bumps [actions/cache](https://github.com/actions/cache) from 4.3.0 to 5.0.2.
- [Release notes](https://github.com/actions/cache/releases)
- [Commits](https://github.com/actions/cache/compare/v4.3.0...v5.0.2)

---
updated-dependencies:
- dependency-name: actions/cache
  dependency-version: 5.0.2
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2026-02-18 20:57:57 -08:00