copilot-swe-agent[bot]
|
17894601ba
|
refactor: use constructor delegation in dep_tracker to eliminate duplicate initialization
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-03-05 17:57:41 +00:00 |
|
CEisenhofer
|
2be1b175cc
|
Updated benchmarking script
|
2026-03-05 18:42:31 +01:00 |
|
CEisenhofer
|
608227a27e
|
Fixed definition extension rule
|
2026-03-05 18:33:58 +01:00 |
|
CEisenhofer
|
d8871e5c1e
|
Eliminate common suffix for simplification
|
2026-03-05 18:19:58 +01:00 |
|
CEisenhofer
|
5a95b40bdb
|
Canceling out common variables is a simplification step now
|
2026-03-05 18:17:04 +01:00 |
|
CEisenhofer
|
272000a466
|
Minor code changes
|
2026-03-05 18:04:51 +01:00 |
|
CEisenhofer
|
7dcebcdb0a
|
A bit cleanup
|
2026-03-05 17:14:54 +01:00 |
|
CEisenhofer
|
c5e7cbc29d
|
Fix to_dot
|
2026-03-05 16:58:58 +01:00 |
|
copilot-swe-agent[bot]
|
2eebe57467
|
Extract handle_empty_side helper in seq_nielsen to eliminate duplicate code
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-03-05 03:21:02 +00:00 |
|
CEisenhofer
|
5ce56e2e04
|
Ported graphviz debug output
|
2026-03-04 20:33:56 +01:00 |
|
CEisenhofer
|
b2838b472d
|
We don't need to handle negative membership constraints explicitly
|
2026-03-04 19:07:36 +01:00 |
|
CEisenhofer
|
4e7d83f996
|
Deleted leftover code from subsumption
|
2026-03-04 17:42:14 +01:00 |
|
CEisenhofer
|
e4787e57f6
|
Use correct parameters for iterative deepening
Updated spec
|
2026-03-04 17:37:04 +01:00 |
|
copilot-swe-agent[bot]
|
5003cece9d
|
Implement Parameter integration for theory_nseq (smt.nseq.max_depth)
Co-authored-by: CEisenhofer <56730610+CEisenhofer@users.noreply.github.com>
|
2026-03-04 15:45:55 +00:00 |
|
Nikolaj Bjorner
|
5aa3713d19
|
first end-pass. Atomic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2026-03-04 02:05:26 -08:00 |
|
copilot-swe-agent[bot]
|
927b03615c
|
Fix dangling pointer in fresh variable name construction in generate_extensions()
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-03-03 21:53:55 +00:00 |
|
copilot-swe-agent[bot]
|
0bdec633d7
|
Implement ZIPT string solver skeleton (theory_nseq)
Add theory_nseq, a Nielsen-graph-based string solver plugin for Z3.
## New files
- src/smt/nseq_state.h/.cpp: constraint store bridging SMT context to
Nielsen graph with manual push/pop backtracking
- src/smt/nseq_regex.h/.cpp: regex membership handling via Brzozowski
derivatives (stub delegates to sgraph::brzozowski_deriv)
- src/smt/nseq_model.h/.cpp: model generation stub
- src/smt/theory_nseq.h/.cpp: main theory class implementing smt::theory
with its own private egraph/sgraph, returns FC_GIVEUP as skeleton
- src/test/nseq_basic.cpp: unit tests covering instantiation, parameter
validation, trivial-equality SAT, and node simplification
## Extensions to seq_nielsen.h/.cpp
- Add search_result enum and solve() iterative-deepening DFS entry point
- Add search_dfs() recursive DFS driver
- Add simplify_node(), generate_extensions(), collect_conflict_deps()
- Add nielsen_node::simplify_and_init(): trivial removal, empty
propagation, prefix matching, symbol clash detection
- Add nielsen_node::is_satisfied(), is_subsumed_by()
- Implement Det, Const Nielsen, and Eq-split modifiers in
generate_extensions()
## Integration
- smt_params.cpp: accept 'nseq' as valid string_solver value
- smt_params_helper.pyg: document 'nseq' option
- smt_setup.h/.cpp: add setup_nseq(), wire into setup_QF_S() and
setup_seq_str()
- smt/CMakeLists.txt: add new sources and smt_seq dependency
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
|
2026-03-03 21:50:21 +00:00 |
|
copilot-swe-agent[bot]
|
7c328647de
|
Move seq_nielsen from src/ast/rewriter to src/smt/seq with new smt_seq component
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
|
2026-03-03 00:17:10 +00:00 |
|