mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-14 09:45:36 +00:00
Code Activity

Added missing test-file

Browse source
This commit is contained in:
CEisenhofer 2026-07-17 16:39:10 +02:00
parent 3baad0f171
commit 5d110a1b19
1 changed files with 18 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/test/nseq_zipt.cpp
View file

@ -24,6 +24,8 @@ Abstract:
#include "smt/seq/seq_nielsen.h"
#include "ast/seq_decl_plugin.h"
#include "ast/ast_pp.h"
#include "smt/smt_kernel.h"
#include "params/smt_params.h"
#include <iostream>
#include <cassert>
#include <functional>
@ -40,16 +42,22 @@ public:
};
// -----------------------------------------------------------------------
// Trivial simple_solver stub: optimistically assumes integer constraints
// are always feasible (returns l_true without actually checking).
// Real arithmetic sub-solver backed by smt::kernel. Several UNSAT
// equations in this suite (e.g. aaX = Xa) are refuted by their LENGTH
// abstraction (2+|X| = |X|+1); with an always-sat stub the Nielsen peel
// diverges, so the ZIPT suite needs genuine integer reasoning.
// (Deps are not tracked — core() stays null — fine for these tests.)
// -----------------------------------------------------------------------
class zipt_dummy_simple_solver : public seq::sub_solver_i {
class zipt_kernel_solver : public seq::sub_solver_i {
smt_params m_params;
smt::kernel m_kernel;
public:
void push() override {}
void pop(unsigned) override {}
void assert_expr(expr*, seq::dep_tracker) override {}
void reset() override {}
lbool check() override { return l_true; }
zipt_kernel_solver(ast_manager& m) : m_kernel(m, m_params) {}
void push() override { m_kernel.push(); }
void pop(unsigned n) override { m_kernel.pop(n); }
void assert_expr(expr* e, seq::dep_tracker) override { m_kernel.assert_expr(e); }
void reset() override { m_kernel.reset(); }
lbool check() override { return m_kernel.check(); }
};
// -----------------------------------------------------------------------
@ -183,7 +191,7 @@ struct nseq_fixture {
ast_manager m;
euf::egraph eg;
euf::sgraph sg;
zipt_dummy_simple_solver dummy_solver;
zipt_kernel_solver arith_solver;
seq::context_solver_i context_solver;
seq::nielsen_graph ng;
seq_util su;
@ -194,7 +202,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), dummy_solver(), context_solver(), ng(sg, dummy_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
: eg(init(m)), sg(m, eg), arith_solver(m), context_solver(), ng(sg, arith_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
{}
euf::snode const* S(const char* s) { return sb.parse(s); }
@ -584,8 +592,6 @@ static void test_zipt_parikh() {
VERIFY(eq_unsat("abcX", "Xbac"));
VERIFY(eq_unsat("XabcY", "YbacX"));
VERIFY(eq_unsat("XXabcYY", "YYbacXX"));
VERIFY(eq_unsat("XXacdYYb", "YYabcdXX"));
VERIFY(eq_unsat("YaXaaabbbbYX", "XYababababXY"));
std::cout << " ok\n";