mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-12 00:00:33 +00:00
Code Activity

Merge branch 'c3' into copilot/implement-int-bounds-var-bound-watcher

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-03-10 16:33:25 -07:00 • committed by GitHub
commit 53d5d98341
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/test/nseq_zipt.cpp
View file

@ -38,6 +38,18 @@ public:
lbool check() override { return l_true; }
};
// -----------------------------------------------------------------------
// Trivial simple_solver stub: optimistically assumes integer constraints
// are always feasible (returns l_true without actually checking).
// -----------------------------------------------------------------------
class zipt_dummy_simple_solver : public seq::simple_solver {
public:
void push() override {}
void pop(unsigned) override {}
void assert_expr(expr*) override {}
lbool check() override { return l_true; }
};
// -----------------------------------------------------------------------
// Helper: build a string snode from a notation string.
// Uppercase = fresh variable, lowercase/digit = concrete character.
@ -168,7 +180,7 @@ struct nseq_fixture {
ast_manager m;
euf::egraph eg;
euf::sgraph sg;
nseq_zipt_dummy_solver solver;
zipt_dummy_simple_solver dummy_solver;
seq::nielsen_graph ng;
seq_util su;
str_builder sb;
@ -178,7 +190,7 @@ struct nseq_fixture {
static ast_manager& init(ast_manager& m) { reg_decl_plugins(m); return m; }
nseq_fixture()
: eg(init(m)), sg(m, eg), ng(sg, solver), su(m), sb(sg), rb(m, su, sg)
: eg(init(m)), sg(m, eg), ng(sg, dummy_solver), su(m), sb(sg), rb(m, su, sg)
{}
euf::snode* S(const char* s) { return sb.parse(s); }