* Initial plan
* Migrate iterator-based for loops to range-based for loops in 11 files
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix compilation error in aig_exporter.cpp - use correct iterator API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to z3++.h as requested
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>
* Initial plan
* Add advanced sequence operations to C# API
- Add MkSeqMap: Map function over sequence
- Add MkSeqMapi: Map function over sequence with index
- Add MkSeqFoldLeft: Fold left operation on sequence
- Add MkSeqFoldLeftI: Fold left with index on sequence
These functions match Python's SeqMap, SeqMapI, SeqFoldLeft, and SeqFoldLeftI and provide feature parity with other language 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>
* restore more aggressive pruning in search tree
* restore where we close children to be correct
* add core strengthening check
* fix recursion bug
* less strict core propagation
* old search tree version
* restore search tree patch
* remove flag
* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree
* clean up code, fix deadlock
* delete test files
* clean up
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
* restore more aggressive pruning in search tree
* restore where we close children to be correct
* add core strengthening check
* fix recursion bug
* less strict core propagation
* old search tree version
* restore search tree patch
* remove flag
---------
Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>
* 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>
* Initial plan
* Convert plain enums to enum class in EUF module
- Convert eq_status in euf::ac_plugin to enum class
- Convert undo_kind in euf::ac_plugin to enum class
- Convert undo_t in euf::arith_plugin to enum class
- Convert to_merge_t in euf::egraph to enum class
- Update all usage sites to use scoped enum syntax
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Convert more plain enums to enum class
- Convert state enum in substitution class
- Convert instruction enum in generic_model_converter class
- Convert eq_type enum in bit2int class
- Update all usage sites to use scoped enum syntax
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>
* Initial plan
* Add API coherence improvements for C#, Python, C++, and TypeScript
- C#: Add SubstituteFuns method to Expr class
- Python: Add update method to ExprRef class
- C++: Add update method to expr class
- TypeScript: Add complete Statistics API with Statistics interface, StatisticsEntry interface, StatisticsImpl class, and statistics() methods for Solver, Optimize, and Fixedpoint
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add Z3_stats import and Statistics types to TypeScript bindings
- Add Z3_stats to imports in types.ts and high-level.ts
- Add Statistics and StatisticsEntry to type imports in high-level.ts
- Fixes missing type references identified in 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>
* Initial plan
* Add [[nodiscard]] to AST factory functions and modernize iterator loops
- Added [[nodiscard]] attribute to key factory functions in ast.h:
- All mk_app() variants for creating application nodes
- All mk_func_decl() variants for creating function declarations
- All mk_const() variants for creating constants
- All mk_sort() variants for creating sorts
- mk_var() for creating variables
- mk_quantifier(), mk_forall(), mk_exists(), mk_lambda() for quantifiers
- mk_label(), mk_pattern() and related functions
- Converted iterator loops to range-based for loops in:
- src/util/region.cpp: pop_scope()
- src/util/dec_ref_util.h: dec_ref_key_values(), dec_ref_keys(), dec_ref_values()
- src/util/mpf.h: dispose()
- src/util/numeral_buffer.h: reset()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Modernize additional iterator loops to range-based for loops
- Converted iterator loops to range-based for loops in:
- src/api/api_ast_map.cpp: Z3_ast_map_keys() and Z3_ast_map_to_string()
- src/api/c++/z3++.h: optimize copy constructor and add() method
- src/opt/wmax.cpp: mk_assumptions()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to z3++.h for C++ version compatibility
Revert the range-based for loop changes in src/api/c++/z3++.h to maintain
compatibility with older C++ versions that users may rely on. The C++ API
wrapper must support down-level C++ standards for backward compatibility.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Trigger CI build
[skip ci] is not used to ensure CI runs
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
