mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 17:14:43 +00:00
Code Activity
20355 commits 29 branches 53 tags 204 MiB
Commit graph

20355 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
01da01edf8 work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
1b65129fdd work on seed_properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
538cc7abe5 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
d40ccc9be5 renaming 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
13ef5a660c ttt 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
1aa282437d preprocess the input of levelwise to drop a level 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
4f56a98586 rename explain::main_operator to compute_conflict_explanation 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ba62a55cc0 trying to figure out right indices 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7fc072984a refactor lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
94a2583af8 refact lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7098863435 refact lws 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ac7299b425 define indexed root expression 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e4f609715f refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
dfa87e68dc refactor 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ed5d9364d7 add trace tag for levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
a6a02ee0b1 pass nlsat::solver to levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
ae6ae57f5f use new display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
d8917ffe12 create free function display functions 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e7193501d4 pass pmanager 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
cdc5272040 pass anum_manager to levelwise, crash on sign 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
7fca133f6f t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
23328e8226 more accurate init of the relation between polynomial properties 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
e5b9643b01 use std::map instead of std::unordered_map 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
8f066e1573 t 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
4ac0bf5007 define symbolic_interval 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
0ca9c2eb93 more scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
3aba50f48d closer to the paper 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
bbd304e1a5 scaffolding 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:13 -10:00
Lev Nachmanson
26ea9391a9 scaffoldin 2026-01-14 07:45:12 -10:00
Lev Nachmanson
2eecf2a3d4 t2 2026-01-14 07:45:12 -10:00
Lev Nachmanson
16d80a6f8d t1 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:12 -10:00
Lev Nachmanson
53c52a4f65 t0 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:45:12 -10:00
Lev Nachmanson
ece691285e throw an algebraic exception on a failure of m_limit.inc() instead of returning sign_zero 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-01-14 07:23:26 -10:00
Nuno Lopes
888d2fc480 copilot: don't use std::format and try using clang-tidy 2026-01-14 09:17:49 +00:00
Lev Nachmanson
d5e0216070 Revert "Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage" 
This reverts commit d9bdb6b83c, reversing
changes made to 8b188621a5.
 2026-01-13 18:18:07 -10:00
Copilot
3bf271bb42
Enhance Code Conventions Analyzer for empty constructors and non-virtual destructors (#8192) 
* Initial plan

* Enhance Code Conventions Analyzer for empty constructors and non-virtual destructors

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-13 18:57:10 -08:00
Lev Nachmanson
d9bdb6b83c
Merge pull request #8190 from Z3Prover/copilot/fix-std-format-usage 
Modernize string formatting from std::ostringstream to std::format
 2026-01-13 13:54:00 -10:00
copilot-swe-agent[bot]
0c2ea345fb Fix spacing in error message 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-01-13 21:36:14 +00:00
copilot-swe-agent[bot]
64957e2b0e Modernize more files to use std::format: bv_decl_plugin, dl_decl_plugin, datatype_decl_plugin, seq_decl_plugin 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-01-13 21:34:47 +00:00
copilot-swe-agent[bot]
99a40e79d4 Modernize ostringstream to std::format in ast.cpp and array_decl_plugin.cpp 
Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
 2026-01-13 21:29:51 +00:00
copilot-swe-agent[bot]
d274181c1f Initial plan 2026-01-13 21:07:21 +00:00
Nikolaj Bjorner
8b188621a5 coerce bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 11:45:57 -08:00
Nikolaj Bjorner
c78d5405d1 update iterator pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 11:33:15 -08:00
Simon Jeanteur
deaced1711
Subterms Theory (#8115) 
* somewhaat failed attempt at declaring subterm predicate

I can't really figure out how to link the smt parser to the rest of the
machinenery, so I will stop here and try from the other side. I'll start
implmenting the logic and see if it brings me back to the parser.

* initial logic implmentation

Very primitive, but I don't like have that much work uncommitted.

* parser implementation

* more theory

* Working base

* subterm reflexivity

* a few optimization

Skip adding obvious equalities or disequality

* removed some optimisations

* better handling of backtracking

* stupid segfault

Add m_subterm to the trail

* Update src/smt/theory_datatype.h

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/ast/rewriter/datatype_rewriter.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update src/smt/theory_datatype.cpp

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* review

* forgot to update `iterate_subterm`'s signature

* fix iterator segfault

* Remove duplicate include statement

Removed duplicate include of 'theory_datatype.h'.

* Replace 'optional' with 'std::option' in datatype_decl_plugin.h

* Add is_subterm_predicate matcher to datatype_decl_plugin

* Change std::option to std::optional for m_subterm

* Update pdecl.h

* Change has_subterm to use has_value method

* Update pdecl.cpp

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
 2026-01-13 10:53:17 -08:00
Copilot
7377d28c30
Replace empty destructors with = default for compiler optimization (#8189) 
* Initial plan

* Replace empty destructors with = default

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-13 10:50:10 -08:00
Nikolaj Bjorner
a0bca2b71a
Add workflow_dispatch trigger to wip.yml 2026-01-13 10:49:33 -08:00
Nikolaj Bjorner
1806e8bb33
Update pyodide.yml 2026-01-13 10:48:34 -08:00
Copilot
635c7ea32e
Extend code-conventions-analyzer workflow with Z3-specific C++ modernization patterns (#8187) 
* Initial plan

* Update code-conventions-analyzer workflow with modern C++ preferences

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-13 09:35:57 -08:00
Nikolaj Bjorner
5d0be96fd1 update RCFNum 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 09:22:43 -08:00
Nikolaj Bjorner
c2cf11672a update python example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-01-13 09:17:01 -08:00