mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-11 07:40:31 +00:00
Code Activity

Fix build: add dummy_simple_solver to nseq_zipt.cpp fixture, fix assert_expr in seq_nielsen.cpp

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 22:47:49 +00:00
parent 09f5d637b0
commit 0efb7402e8
2 changed files with 15 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/test/nseq_zipt.cpp
View file

@ -29,6 +29,18 @@ Abstract:
#include <functional>
#include <chrono>
// -----------------------------------------------------------------------
// Trivial simple_solver stub: optimistically assumes integer constraints
// are always feasible (returns l_true without actually checking).
// -----------------------------------------------------------------------
class 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.
@ -159,6 +171,7 @@ struct nseq_fixture {
ast_manager m;
euf::egraph eg;
euf::sgraph sg;
dummy_simple_solver dummy_solver;
seq::nielsen_graph ng;
seq_util su;
str_builder sb;
@ -168,7 +181,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), 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); }

2
src/test/seq_nielsen.cpp
View file

@ -27,7 +27,7 @@ public:
dummy_simple_solver() : seq::simple_solver() {}
void push() override {}
void pop(unsigned n) override {}
void assert(expr *constraint) override {}
void assert_expr(expr *constraint) override {}
lbool check() override {
return l_true;
}