From 639d7d147b8df82c09e02446d05ce365b64c6ec1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jul 2026 20:20:32 -0700 Subject: [PATCH] Update seq_monadic.cpp --- src/ast/rewriter/seq_monadic.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 8fbb553441..f9ba950b07 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -18,6 +18,24 @@ Abstract: {true,false,=,<=,and,or,not} grammar the derivatives emit). The same guard algebra yields the concrete element used to build a witness sequence. +TODOs: +- track unsat cores and expose them as explain functionality +- if perf suffers: use DFS backtracking search instead of DNF expansion (space overhead) +- create a validation harness: expose certificates for correctness that can be checked. +- handle transitions into unions and concatenations over unions +- establish a perf harness +- extend with lower and upper bound constraints +- encapsulate within general interface: +create: undo_trail x dependency_manager x ast_manager -> regex_membership +add_constraint : expr* x expr* x dependency* -> void +add_lo: expr* x unsigned * dependency* -> void +add_hi: expr* x unsigned * dependency* ->void +check: void -> lbool +explain: void -> dependency* +model: void -> (expr* x expr*) vector or value: expr* -> expr* +perhaps: +substitute: expr* x expr* x dependency* -> void + Author: Nikolaj Bjorner / Margus Veanes 2026