mirror of
https://github.com/Z3Prover/z3
synced 2026-03-11 15:50:29 +00:00
use reference to solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
c98ea6dc21
commit
d2739d9816
1 changed files with 146 additions and 100 deletions
|
|
@ -22,6 +22,18 @@ Abstract:
|
|||
#include "ast/ast_pp.h"
|
||||
#include <iostream>
|
||||
|
||||
class dummy_simple_solver : public seq::simple_solver {
|
||||
public:
|
||||
dummy_simple_solver() : seq::simple_solver() {}
|
||||
void push() override {}
|
||||
void pop(unsigned n) override {}
|
||||
void assert(expr *constraint) override {}
|
||||
lbool check() override {
|
||||
return l_true;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
// test dep_tracker (uint_set) basic operations
|
||||
static void test_dep_tracker() {
|
||||
std::cout << "test_dep_tracker\n";
|
||||
|
|
@ -173,7 +185,8 @@ static void test_nielsen_node() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -215,7 +228,8 @@ static void test_nielsen_edge() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -250,7 +264,8 @@ static void test_nielsen_graph_populate() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -289,7 +304,8 @@ static void test_nielsen_subst_apply() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -323,7 +339,8 @@ static void test_nielsen_graph_reset() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -346,7 +363,8 @@ static void test_nielsen_expansion() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -395,7 +413,8 @@ static void test_run_idx() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
SASSERT(ng.run_idx() == 0);
|
||||
|
||||
ng.inc_run_idx();
|
||||
|
|
@ -415,7 +434,8 @@ static void test_multiple_memberships() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -451,7 +471,8 @@ static void test_backedge() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -474,7 +495,8 @@ static void test_eq_split_basic() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -504,7 +526,8 @@ static void test_eq_split_solve_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -526,7 +549,7 @@ static void test_eq_split_solve_unsat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -548,7 +571,8 @@ static void test_eq_split_same_var_det() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -570,7 +594,7 @@ static void test_eq_split_commutation_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -592,7 +616,8 @@ static void test_const_nielsen_char_var() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -615,7 +640,8 @@ static void test_const_nielsen_var_char() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -640,7 +666,8 @@ static void test_const_nielsen_solve_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -661,7 +688,8 @@ static void test_const_nielsen_solve_unsat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -683,7 +711,8 @@ static void test_const_nielsen_priority_over_eq_split() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -710,7 +739,8 @@ static void test_const_nielsen_not_applicable_both_vars() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -736,7 +766,8 @@ static void test_const_nielsen_multi_char_solve() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -764,7 +795,8 @@ static void test_regex_char_split_basic() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -799,7 +831,8 @@ static void test_regex_char_split_solve_sat() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -823,7 +856,8 @@ static void test_regex_char_split_solve_multi_char() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -850,7 +884,8 @@ static void test_regex_char_split_union() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -878,7 +913,8 @@ static void test_regex_char_split_star_sat() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -903,7 +939,8 @@ static void test_regex_char_split_concat_str() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -932,7 +969,8 @@ static void test_regex_char_split_with_eq() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -959,7 +997,8 @@ static void test_regex_char_split_ground_skip() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
||||
|
|
@ -987,7 +1026,8 @@ static void test_var_nielsen_basic() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1010,7 +1050,8 @@ static void test_var_nielsen_same_var_det() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -1032,7 +1073,8 @@ static void test_var_nielsen_not_applicable_char() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1054,7 +1096,8 @@ static void test_var_nielsen_solve_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1076,7 +1119,8 @@ static void test_var_nielsen_solve_unsat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1098,7 +1142,8 @@ static void test_var_nielsen_commutation_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1120,7 +1165,7 @@ static void test_var_nielsen_priority() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1145,7 +1190,7 @@ static void test_generate_extensions_det_priority() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1169,7 +1214,7 @@ static void test_generate_extensions_no_applicable() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -1193,7 +1238,7 @@ static void test_generate_extensions_regex_only() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
// Build regex to_re("A")
|
||||
|
|
@ -1223,7 +1268,7 @@ static void test_generate_extensions_mixed_det_first() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1257,7 +1302,7 @@ static void test_solve_empty_graph() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
SASSERT(!ng.root());
|
||||
auto result = ng.solve();
|
||||
SASSERT(result == seq::nielsen_graph::search_result::sat);
|
||||
|
|
@ -1271,7 +1316,7 @@ static void test_solve_trivially_satisfied() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
ng.add_str_eq(x, x);
|
||||
auto result = ng.solve();
|
||||
|
|
@ -1286,7 +1331,7 @@ static void test_solve_node_status_unsat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
// A = B is an immediate conflict
|
||||
|
|
@ -1308,7 +1353,7 @@ static void test_solve_conflict_deps() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
// Add two constraints: A = B (unsat) and a dummy x = x
|
||||
|
|
@ -1372,7 +1417,7 @@ static void test_explain_conflict_single_eq() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
// eq[0]: A = B (conflict)
|
||||
|
|
@ -1397,7 +1442,7 @@ static void test_explain_conflict_multi_eq() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
|
@ -1428,7 +1473,7 @@ static void test_solve_node_extended_flag() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
euf::snode* xy = sg.mk_concat(x, y);
|
||||
|
|
@ -1455,7 +1500,7 @@ static void test_solve_mixed_eq_mem_sat() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -1484,7 +1529,7 @@ static void test_solve_children_failed_reason() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -1506,7 +1551,7 @@ static void test_solve_eval_idx_tracking() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
// x = A·x would be infinite without depth bound, but
|
||||
|
|
@ -1538,7 +1583,8 @@ static void test_simplify_prefix_cancel() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver;
|
||||
seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
|
@ -1568,7 +1614,7 @@ static void test_simplify_symbol_clash() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
|
@ -1596,7 +1642,7 @@ static void test_simplify_empty_propagation() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* e = sg.mk_empty();
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1619,7 +1665,7 @@ static void test_simplify_empty_vs_char() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* e = sg.mk_empty();
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
||||
|
|
@ -1641,7 +1687,7 @@ static void test_simplify_multi_pass_clash() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* c = sg.mk_char('C');
|
||||
|
|
@ -1667,7 +1713,7 @@ static void test_simplify_trivial_removal() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
|
@ -1690,7 +1736,7 @@ static void test_simplify_all_trivial_satisfied() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
|
|
@ -1712,7 +1758,7 @@ static void test_simplify_regex_infeasible() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
expr_ref ch_a(seq.str.mk_char('A'), m);
|
||||
|
|
@ -1739,7 +1785,7 @@ static void test_simplify_nullable_removal() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
expr_ref ch_a(seq.str.mk_char('A'), m);
|
||||
|
|
@ -1767,7 +1813,7 @@ static void test_simplify_brzozowski_sat() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
|
|
@ -1793,7 +1839,7 @@ static void test_simplify_multiple_eqs() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -1831,7 +1877,7 @@ static void test_det_cancel_child_eq() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -1853,7 +1899,7 @@ static void test_const_nielsen_child_substitutions() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
|
@ -1889,7 +1935,7 @@ static void test_var_nielsen_substitution_types() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
||||
|
|
@ -1919,7 +1965,7 @@ static void test_explain_conflict_mem_only() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
expr_ref ch_a(seq.str.mk_char('A'), m);
|
||||
|
|
@ -1949,7 +1995,7 @@ static void test_explain_conflict_mixed_eq_mem() {
|
|||
euf::sgraph sg(m, eg);
|
||||
seq_util seq(m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
euf::snode* e = sg.mk_empty();
|
||||
|
|
@ -1989,7 +2035,7 @@ static void test_subsumption_pruning_unsat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
||||
|
|
@ -2011,7 +2057,7 @@ static void test_subsumption_reason_set() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -2061,7 +2107,7 @@ static void test_length_constraints_basic() {
|
|||
euf::snode* lhs = sg.mk_concat(x, y);
|
||||
euf::snode* rhs = sg.mk_concat(a, b);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(lhs, rhs);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2096,7 +2142,7 @@ static void test_length_constraints_trivial_skip() {
|
|||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
// trivial equation: x = x (same snode)
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, x);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2115,7 +2161,7 @@ static void test_length_constraints_empty() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
ng.generate_length_constraints(constraints);
|
||||
|
|
@ -2144,7 +2190,7 @@ static void test_length_constraints_concat_chain() {
|
|||
euf::snode* lhs = sg.mk_concat(sg.mk_concat(x, y), z);
|
||||
euf::snode* rhs = sg.mk_concat(sg.mk_concat(a, b), c);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(lhs, rhs);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2172,7 +2218,7 @@ static void test_length_constraints_multi_eq() {
|
|||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, a); // x = A
|
||||
ng.add_str_eq(y, b); // y = B
|
||||
|
||||
|
|
@ -2205,7 +2251,7 @@ static void test_length_constraints_shared_var() {
|
|||
euf::snode* lhs = sg.mk_concat(x, a);
|
||||
euf::snode* rhs = sg.mk_concat(a, x);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(lhs, rhs);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2230,7 +2276,7 @@ static void test_length_constraints_deps() {
|
|||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, a); // eq index 0
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2260,7 +2306,7 @@ static void test_length_constraints_empty_side() {
|
|||
euf::snode* e = sg.mk_empty();
|
||||
|
||||
// x = ε
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, e);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2294,7 +2340,7 @@ static void test_length_kind_tagging() {
|
|||
euf::snode* a = sg.mk_char('A');
|
||||
|
||||
// equation: x = a (one eq + one nonneg)
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, a);
|
||||
|
||||
// membership: y in to_re("AB") (bounds + nonneg)
|
||||
|
|
@ -2352,7 +2398,7 @@ static void test_power_epsilon_no_power() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
|
|
@ -2376,7 +2422,7 @@ static void test_num_cmp_no_power() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2401,7 +2447,7 @@ static void test_star_intr_no_backedge() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
expr_ref ch_a(seq.str.mk_char('A'), m);
|
||||
|
|
@ -2434,7 +2480,7 @@ static void test_star_intr_with_backedge() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
expr_ref ch_a(seq.str.mk_char('A'), m);
|
||||
|
|
@ -2473,7 +2519,7 @@ static void test_gpower_intr_self_cycle() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a1 = sg.mk_char('A');
|
||||
|
|
@ -2501,7 +2547,7 @@ static void test_gpower_intr_no_cycle() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2531,7 +2577,7 @@ static void test_regex_var_split_basic() {
|
|||
seq_util seq(m);
|
||||
sort_ref str_sort(seq.str.mk_string_sort(), m);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
|
||||
|
|
@ -2566,7 +2612,7 @@ static void test_power_split_no_power() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2592,7 +2638,7 @@ static void test_var_num_unwinding_no_power() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2615,7 +2661,7 @@ static void test_const_num_unwinding_no_power() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* b = sg.mk_char('B');
|
||||
|
|
@ -2642,7 +2688,7 @@ static void test_priority_chain_order() {
|
|||
{
|
||||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2659,7 +2705,7 @@ static void test_priority_chain_order() {
|
|||
{
|
||||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2675,7 +2721,7 @@ static void test_priority_chain_order() {
|
|||
{
|
||||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* a = sg.mk_char('A');
|
||||
euf::snode* y = sg.mk_var(symbol("y"));
|
||||
|
|
@ -2696,7 +2742,7 @@ static void test_gpower_intr_solve_sat() {
|
|||
euf::egraph eg(m);
|
||||
euf::sgraph sg(m, eg);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
|
||||
euf::snode* x = sg.mk_var(symbol("x"));
|
||||
euf::snode* a1 = sg.mk_char('A');
|
||||
|
|
@ -2734,7 +2780,7 @@ static void test_parikh_exact_length() {
|
|||
expr_ref to_re_ab(seq.re.mk_to_re(ab), m);
|
||||
euf::snode* regex = sg.mk(to_re_ab);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2781,7 +2827,7 @@ static void test_parikh_star_unbounded() {
|
|||
expr_ref re_star(seq.re.mk_star(to_re_a), m);
|
||||
euf::snode* regex = sg.mk(re_star);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2836,7 +2882,7 @@ static void test_parikh_union_interval() {
|
|||
expr_ref re_union(seq.re.mk_union(to_re_ab, to_re_cde), m);
|
||||
euf::snode* regex = sg.mk(re_union);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2875,7 +2921,7 @@ static void test_parikh_loop_bounded() {
|
|||
expr_ref re_loop(seq.re.mk_loop(to_re_a, 3, 5), m);
|
||||
euf::snode* regex = sg.mk(re_loop);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2911,7 +2957,7 @@ static void test_parikh_empty_regex() {
|
|||
expr_ref re_empty(seq.re.mk_empty(seq.re.mk_re(str_sort)), m);
|
||||
euf::snode* regex = sg.mk(re_empty);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2950,7 +2996,7 @@ static void test_parikh_full_char() {
|
|||
expr_ref re_range(seq.re.mk_range(unit_a, unit_z), m);
|
||||
euf::snode* regex = sg.mk(re_range);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -2986,7 +3032,7 @@ static void test_parikh_mixed_eq_mem() {
|
|||
euf::snode* a = sg.mk_char('A');
|
||||
|
||||
// equation: x = A
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_eq(x, a);
|
||||
|
||||
// membership: y in to_re("BC")
|
||||
|
|
@ -3034,7 +3080,7 @@ static void test_parikh_full_seq_no_bounds() {
|
|||
expr_ref re_all(seq.re.mk_full_seq(str_sort), m);
|
||||
euf::snode* regex = sg.mk(re_all);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
@ -3071,7 +3117,7 @@ static void test_parikh_dep_tracking() {
|
|||
expr_ref to_re_a(seq.re.mk_to_re(unit_a), m);
|
||||
euf::snode* regex = sg.mk(to_re_a);
|
||||
|
||||
seq::nielsen_graph ng(sg);
|
||||
dummy_simple_solver solver; seq::nielsen_graph ng(sg, solver);
|
||||
ng.add_str_mem(x, regex);
|
||||
|
||||
vector<seq::length_constraint> constraints;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue