mirror of
https://github.com/Z3Prover/z3
synced 2026-03-07 22:04:53 +00:00
0bdec633d7
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>
295 lines
8.2 KiB
C++
295 lines
8.2 KiB
C++
#include<iostream>
|
|
#include<time.h>
|
|
#include<string>
|
|
#include<cstring>
|
|
#include "util/util.h"
|
|
#include "util/trace.h"
|
|
#include "util/debug.h"
|
|
#include "util/timeit.h"
|
|
#include "util/warning.h"
|
|
#include "util/memory_manager.h"
|
|
#include "util/gparams.h"
|
|
|
|
|
|
//
|
|
// Unit tests fail by asserting.
|
|
// If they return, we assume the unit test succeeds
|
|
// and print "PASS" to indicate success.
|
|
//
|
|
|
|
#define TST(MODULE) { \
|
|
std::string s("test "); \
|
|
s += #MODULE; \
|
|
void tst_##MODULE(); \
|
|
if (do_display_usage) \
|
|
std::cout << " " << #MODULE << "\n"; \
|
|
for (int i = 0; i < argc; ++i) \
|
|
if (test_all || strcmp(argv[i], #MODULE) == 0) { \
|
|
enable_debug(#MODULE); \
|
|
timeit timeit(true, s.c_str()); \
|
|
tst_##MODULE(); \
|
|
std::cout << "PASS" << std::endl; \
|
|
} \
|
|
}
|
|
|
|
#define TST_ARGV(MODULE) { \
|
|
std::string s("test "); \
|
|
s += #MODULE; \
|
|
void tst_##MODULE(char** argv, int argc, int& i); \
|
|
if (do_display_usage) \
|
|
std::cout << " " << #MODULE << "(...)\n"; \
|
|
for (int i = 0; i < argc; ++i) \
|
|
if (strcmp(argv[i], #MODULE) == 0) { \
|
|
enable_trace(#MODULE); \
|
|
enable_debug(#MODULE); \
|
|
timeit timeit(true, s.c_str()); \
|
|
tst_##MODULE(argv, argc, i); \
|
|
std::cout << "PASS" << std::endl; \
|
|
} \
|
|
}
|
|
|
|
void error(const char * msg) {
|
|
std::cerr << "Error: " << msg << "\n";
|
|
std::cerr << "For usage information: test /h\n";
|
|
exit(1);
|
|
}
|
|
|
|
void display_usage() {
|
|
std::cout << "Z3 unit tests [version 1.0]. (C) Copyright 2006 Microsoft Corp.\n";
|
|
std::cout << "Usage: test [options] [module names]\n";
|
|
std::cout << "\nMisc.:\n";
|
|
std::cout << " /h prints this message.\n";
|
|
std::cout << " /v:level be verbose, where <level> is the verbosity level.\n";
|
|
std::cout << " /w enable warning messages.\n";
|
|
std::cout << " /a run all unit tests that don't require arguments.\n";
|
|
#if defined(Z3DEBUG) || defined(_TRACE)
|
|
std::cout << "\nDebugging support:\n";
|
|
#endif
|
|
#ifdef _TRACE
|
|
std::cout << " /tr:tag enable trace messages tagged with <tag>.\n";
|
|
#endif
|
|
#ifdef Z3DEBUG
|
|
std::cout << " /dbg:tag enable assertions tagged with <tag>.\n";
|
|
#endif
|
|
std::cout << "\nModule names:\n";
|
|
}
|
|
|
|
void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) {
|
|
int i = 1;
|
|
if (argc == 1) {
|
|
display_usage();
|
|
do_display_usage = true;
|
|
}
|
|
while (i < argc) {
|
|
char * arg = argv[i];
|
|
char * eq_pos = nullptr;
|
|
|
|
if (arg[0] == '-' || arg[0] == '/') {
|
|
char * opt_name = arg + 1;
|
|
char * opt_arg = nullptr;
|
|
char * colon = strchr(arg, ':');
|
|
if (colon) {
|
|
opt_arg = colon + 1;
|
|
*colon = 0;
|
|
}
|
|
if (strcmp(opt_name, "h") == 0 ||
|
|
strcmp(opt_name, "?") == 0) {
|
|
display_usage();
|
|
do_display_usage = true;
|
|
return;
|
|
}
|
|
else if (strcmp(opt_name, "v") == 0) {
|
|
if (!opt_arg)
|
|
error("option argument (/v:level) is missing.");
|
|
long lvl = strtol(opt_arg, nullptr, 10);
|
|
set_verbosity_level(lvl);
|
|
}
|
|
else if (strcmp(opt_name, "w") == 0) {
|
|
enable_warning_messages(true);
|
|
}
|
|
else if (strcmp(opt_name, "a") == 0) {
|
|
test_all = true;
|
|
}
|
|
#ifdef _TRACE
|
|
else if (strcmp(opt_name, "tr") == 0) {
|
|
if (!opt_arg)
|
|
error("option argument (/tr:tag) is missing.");
|
|
enable_trace(opt_arg);
|
|
}
|
|
#endif
|
|
#ifdef Z3DEBUG
|
|
else if (strcmp(opt_name, "dbg") == 0) {
|
|
if (!opt_arg)
|
|
error("option argument (/dbg:tag) is missing.");
|
|
enable_debug(opt_arg);
|
|
}
|
|
#endif
|
|
}
|
|
else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) {
|
|
char * key = arg;
|
|
*eq_pos = 0;
|
|
char * value = eq_pos+1;
|
|
try {
|
|
gparams::set(key, value);
|
|
}
|
|
catch (z3_exception& ex) {
|
|
std::cerr << ex.what() << "\n";
|
|
}
|
|
}
|
|
i++;
|
|
}
|
|
}
|
|
|
|
|
|
int main(int argc, char ** argv) {
|
|
memory::initialize(0);
|
|
bool do_display_usage = false;
|
|
bool test_all = false;
|
|
parse_cmd_line_args(argc, argv, do_display_usage, test_all);
|
|
TST(random);
|
|
TST(symbol_table);
|
|
TST(region);
|
|
TST(symbol);
|
|
TST(heap);
|
|
TST(hashtable);
|
|
TST(rational);
|
|
TST(inf_rational);
|
|
TST(ast);
|
|
TST(optional);
|
|
TST(bit_vector);
|
|
TST(fixed_bit_vector);
|
|
TST(tbv);
|
|
TST(doc);
|
|
TST(udoc_relation);
|
|
TST(string_buffer);
|
|
TST(map);
|
|
TST(diff_logic);
|
|
TST(uint_set);
|
|
TST_ARGV(expr_rand);
|
|
TST(list);
|
|
TST(small_object_allocator);
|
|
TST(timeout);
|
|
TST(proof_checker);
|
|
TST(simplifier);
|
|
TST(bit_blaster);
|
|
TST(var_subst);
|
|
TST(simple_parser);
|
|
TST(api);
|
|
TST(api_algebraic);
|
|
TST(api_polynomial);
|
|
TST(api_pb);
|
|
TST(api_datalog);
|
|
TST(parametric_datatype);
|
|
TST(cube_clause);
|
|
TST(old_interval);
|
|
TST(get_implied_equalities);
|
|
TST(arith_simplifier_plugin);
|
|
TST(matcher);
|
|
TST(object_allocator);
|
|
TST(mpz);
|
|
TST(mpq);
|
|
TST(mpf);
|
|
TST(total_order);
|
|
TST(dl_table);
|
|
TST(dl_context);
|
|
TST(dlist);
|
|
TST(dl_util);
|
|
TST(dl_product_relation);
|
|
TST(dl_relation);
|
|
TST(parray);
|
|
TST(stack);
|
|
TST(escaped);
|
|
TST(buffer);
|
|
TST(chashtable);
|
|
TST(egraph);
|
|
TST(ex);
|
|
TST(nlarith_util);
|
|
TST(api_ast_map);
|
|
TST(api_bug);
|
|
TST(api_special_relations);
|
|
TST(arith_rewriter);
|
|
TST(check_assumptions);
|
|
TST(smt_context);
|
|
TST(theory_dl);
|
|
TST(model_retrieval);
|
|
TST(model_based_opt);
|
|
TST(factor_rewriter);
|
|
TST(smt2print_parse);
|
|
TST(substitution);
|
|
TST(polynomial);
|
|
TST(polynomial_factorization);
|
|
TST(upolynomial);
|
|
TST(algebraic);
|
|
TST(algebraic_numbers);
|
|
TST(ackermannize);
|
|
TST(monomial_bounds);
|
|
TST(nla_intervals);
|
|
TST(horner);
|
|
TST(prime_generator);
|
|
TST(permutation);
|
|
TST(nlsat);
|
|
TST(13);
|
|
TST(zstring);
|
|
if (test_all) return 0;
|
|
TST(ext_numeral);
|
|
TST(interval);
|
|
TST(value_generator);
|
|
TST(value_sweep);
|
|
TST(vector);
|
|
TST(f2n);
|
|
TST(hwf);
|
|
TST(trigo);
|
|
TST(bits);
|
|
TST(mpbq);
|
|
TST(mpfx);
|
|
TST(mpff);
|
|
TST(horn_subsume_model_converter);
|
|
TST(model2expr);
|
|
TST(hilbert_basis);
|
|
TST(heap_trie);
|
|
TST(karr);
|
|
TST(no_overflow);
|
|
// TST(memory);
|
|
TST(datalog_parser);
|
|
TST_ARGV(datalog_parser_file);
|
|
TST(dl_query);
|
|
TST(quant_solve);
|
|
TST(rcf);
|
|
TST(polynorm);
|
|
TST(qe_arith);
|
|
TST(expr_substitution);
|
|
TST(sorting_network);
|
|
TST(theory_pb);
|
|
TST(simplex);
|
|
TST(sat_user_scope);
|
|
TST_ARGV(ddnf);
|
|
TST(ddnf1);
|
|
TST(model_evaluator);
|
|
TST(get_consequences);
|
|
TST(pb2bv);
|
|
TST_ARGV(sat_lookahead);
|
|
TST_ARGV(sat_local_search);
|
|
TST_ARGV(cnf_backbones);
|
|
TST(bdd);
|
|
TST(pdd);
|
|
TST(pdd_solver);
|
|
TST(scoped_timer);
|
|
TST(solver_pool);
|
|
//TST_ARGV(hs);
|
|
TST(finder);
|
|
TST(totalizer);
|
|
TST(distribution);
|
|
TST(euf_bv_plugin);
|
|
TST(euf_arith_plugin);
|
|
TST(euf_sgraph);
|
|
TST(euf_seq_plugin);
|
|
TST(sls_test);
|
|
TST(scoped_vector);
|
|
TST(sls_seq_plugin);
|
|
TST(seq_nielsen);
|
|
TST(nseq_basic);
|
|
TST(ho_matcher);
|
|
TST(finite_set);
|
|
TST(finite_set_rewriter);
|
|
TST(fpa);
|
|
}
|