mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
fix build, move seq_skolem
This commit is contained in:
Nikolaj Bjorner
parent
083d09aa81
commit
45af1bd243
9 changed files with 12 additions and 12 deletions
|
|
@ -14,7 +14,6 @@ z3_add_component(smt
|
|||
seq_ne_solver.cpp
|
||||
seq_offset_eq.cpp
|
||||
seq_regex.cpp
|
||||
seq_skolem.cpp
|
||||
smt_almost_cg_table.cpp
|
||||
smt_arith_value.cpp
|
||||
smt_case_split_queue.cpp
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ Revision History:
|
|||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/rewriter/seq_skolem.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/seq_skolem.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
|
|||
|
|
@ -20,8 +20,8 @@ Author:
|
|||
#include "util/state_graph.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/rewriter/seq_rewriter.h"
|
||||
#include "ast/rewriter/seq_skolem.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include "smt/seq_skolem.h"
|
||||
|
||||
/*
|
||||
*** Tracing and debugging in this module and related modules ***
|
||||
|
|
|
|||
|
|
@ -1,203 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
seq_skolem.cpp
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2020-4-16
|
||||
|
||||
--*/
|
||||
|
||||
#include "smt/seq_skolem.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
using namespace smt;
|
||||
|
||||
|
||||
seq_skolem::seq_skolem(ast_manager& m, th_rewriter& rw):
|
||||
m(m),
|
||||
m_rewrite(rw),
|
||||
seq(m),
|
||||
a(m) {
|
||||
m_prefix = "seq.p.suffix";
|
||||
m_suffix = "seq.s.prefix";
|
||||
m_accept = "aut.accept";
|
||||
m_tail = "seq.tail";
|
||||
m_seq_first = "seq.first";
|
||||
m_seq_last = "seq.last";
|
||||
m_indexof_left = "seq.idx.left";
|
||||
m_indexof_right = "seq.idx.right";
|
||||
m_aut_step = "aut.step";
|
||||
m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l
|
||||
m_post = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l
|
||||
m_eq = "seq.eq";
|
||||
m_max_unfolding = "seq.max_unfolding";
|
||||
m_length_limit = "seq.length_limit";
|
||||
m_is_empty = "re.is_empty";
|
||||
m_is_non_empty = "re.is_non_empty";
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk(symbol const& s, expr* e1, expr* e2, expr* e3, expr* e4, sort* range, bool rw) {
|
||||
expr* es[4] = { e1, e2, e3, e4 };
|
||||
unsigned len = e4?4:(e3?3:(e2?2:(e1?1:0)));
|
||||
if (!range) {
|
||||
range = e1->get_sort();
|
||||
}
|
||||
expr_ref result(seq.mk_skolem(s, len, es, range), m);
|
||||
if (rw)
|
||||
m_rewrite(result);
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_max_unfolding_depth(unsigned depth) {
|
||||
parameter ps[2] = { parameter(m_max_unfolding), parameter(depth) };
|
||||
func_decl* f = m.mk_func_decl(seq.get_family_id(), _OP_SEQ_SKOLEM, 2, ps, 0, (sort*const*) nullptr, m.mk_bool_sort());
|
||||
return expr_ref(m.mk_const(f), m);
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_length_limit(expr* e, unsigned d) {
|
||||
parameter ps[3] = { parameter(m_length_limit), parameter(d), parameter(e) };
|
||||
func_decl* f = m.mk_func_decl(seq.get_family_id(), _OP_SEQ_SKOLEM, 3, ps, 0, (sort*const*) nullptr, m.mk_bool_sort());
|
||||
return expr_ref(m.mk_const(f), m);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_length_limit(expr* p, unsigned& lim, expr*& s) const {
|
||||
if (!is_length_limit(p))
|
||||
return false;
|
||||
lim = to_app(p)->get_parameter(1).get_int();
|
||||
s = to_expr(to_app(p)->get_parameter(2).get_ast());
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
bool seq_skolem::is_skolem(symbol const& s, expr const* e) const {
|
||||
return seq.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s;
|
||||
}
|
||||
|
||||
void seq_skolem::decompose(expr* e, expr_ref& head, expr_ref& tail) {
|
||||
expr* e1 = nullptr, *e2 = nullptr;
|
||||
zstring s;
|
||||
rational r;
|
||||
|
||||
decompose_main:
|
||||
if (seq.str.is_empty(e)) {
|
||||
head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));
|
||||
tail = e;
|
||||
}
|
||||
else if (seq.str.is_string(e, s)) {
|
||||
head = seq.str.mk_unit(seq.str.mk_char(s, 0));
|
||||
tail = seq.str.mk_string(s.extract(1, s.length()-1));
|
||||
}
|
||||
else if (seq.str.is_unit(e)) {
|
||||
head = e;
|
||||
tail = seq.str.mk_empty(e->get_sort());
|
||||
m_rewrite(head);
|
||||
}
|
||||
else if (seq.str.is_concat(e, e1, e2) && seq.str.is_empty(e1)) {
|
||||
e = e2;
|
||||
goto decompose_main;
|
||||
}
|
||||
else if (seq.str.is_concat(e, e1, e2) && seq.str.is_string(e1, s) && s.length() > 0) {
|
||||
head = seq.str.mk_unit(seq.str.mk_char(s, 0));
|
||||
tail = seq.str.mk_concat(seq.str.mk_string(s.extract(1, s.length()-1)), e2);
|
||||
}
|
||||
else if (seq.str.is_concat(e, e1, e2) && seq.str.is_unit(e1)) {
|
||||
head = e1;
|
||||
tail = e2;
|
||||
m_rewrite(head);
|
||||
m_rewrite(tail);
|
||||
}
|
||||
else if (is_skolem(m_tail, e) && a.is_numeral(to_app(e)->get_arg(1), r)) {
|
||||
expr* s = to_app(e)->get_arg(0);
|
||||
expr* idx = a.mk_int(r.get_unsigned() + 1);
|
||||
head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
|
||||
tail = mk(m_tail, s, idx);
|
||||
m_rewrite(head);
|
||||
}
|
||||
else {
|
||||
head = seq.str.mk_unit(seq.str.mk_nth_i(e, a.mk_int(0)));
|
||||
tail = mk(m_tail, e, a.mk_int(0));
|
||||
m_rewrite(head);
|
||||
}
|
||||
}
|
||||
|
||||
bool seq_skolem::is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const {
|
||||
if (is_step(e)) {
|
||||
s = to_app(e)->get_arg(0);
|
||||
idx = to_app(e)->get_arg(1);
|
||||
re = to_app(e)->get_arg(2);
|
||||
i = to_app(e)->get_arg(3);
|
||||
j = to_app(e)->get_arg(4);
|
||||
t = to_app(e)->get_arg(5);
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool seq_skolem::is_tail_u(expr* e, expr*& s, unsigned& idx) const {
|
||||
expr* i = nullptr;
|
||||
rational r;
|
||||
return is_tail(e, s, i) && a.is_numeral(i, r) && r.is_unsigned() && (idx = r.get_unsigned(), true);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_tail(expr* e, expr*& s) const {
|
||||
expr* i = nullptr;
|
||||
return is_tail(e, s, i);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_tail(expr* e, expr*& s, expr*& idx) const {
|
||||
return is_tail(e) && (s = to_app(e)->get_arg(0), idx = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_eq(expr* e, expr*& a, expr*& b) const {
|
||||
return is_skolem(m_eq, e) && (a = to_app(e)->get_arg(0), b = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_pre(expr* e, expr*& s, expr*& i) {
|
||||
return is_skolem(m_pre, e) && (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
bool seq_skolem::is_post(expr* e, expr*& s, expr*& start) {
|
||||
return is_skolem(m_post, e) && (s = to_app(e)->get_arg(0), start = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_unit_inv(expr* n) {
|
||||
expr* u = nullptr;
|
||||
VERIFY(seq.str.is_unit(n, u));
|
||||
sort* s = u->get_sort();
|
||||
return mk(symbol("seq.unit-inv"), n, s);
|
||||
}
|
||||
|
||||
|
||||
expr_ref seq_skolem::mk_last(expr* s) {
|
||||
zstring str;
|
||||
if (seq.str.is_string(s, str) && str.length() > 0) {
|
||||
return expr_ref(seq.str.mk_char(str, str.length()-1), m);
|
||||
}
|
||||
sort* char_sort = nullptr;
|
||||
VERIFY(seq.is_seq(s->get_sort(), char_sort));
|
||||
return mk(m_seq_last, s, char_sort);
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_first(expr* s) {
|
||||
zstring str;
|
||||
if (seq.str.is_string(s, str) && str.length() > 0) {
|
||||
return expr_ref(seq.str.mk_string(str.extract(0, str.length()-1)), m);
|
||||
}
|
||||
return mk(m_seq_first, s);
|
||||
}
|
||||
|
||||
expr_ref seq_skolem::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t) {
|
||||
expr_ref_vector args(m);
|
||||
args.push_back(s).push_back(idx).push_back(re);
|
||||
args.push_back(a.mk_int(i));
|
||||
args.push_back(a.mk_int(j));
|
||||
args.push_back(t);
|
||||
return expr_ref(seq.mk_skolem(m_aut_step, args.size(), args.c_ptr(), m.mk_bool_sort()), m);
|
||||
}
|
||||
|
||||
|
|
@ -1,161 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
seq_skolem.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Skolem function support for sequences.
|
||||
Skolem functions are auxiliary funcions useful for axiomatizing sequence
|
||||
operations.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2020-4-16
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
class seq_skolem {
|
||||
ast_manager& m;
|
||||
th_rewriter& m_rewrite; // NB: would be nicer not to have this dependency
|
||||
seq_util seq;
|
||||
arith_util a;
|
||||
|
||||
symbol m_prefix, m_suffix;
|
||||
symbol m_tail;
|
||||
symbol m_seq_first, m_seq_last;
|
||||
symbol m_indexof_left, m_indexof_right; // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
|
||||
symbol m_aut_step; // regex unfolding state
|
||||
symbol m_accept; // regex
|
||||
symbol m_is_empty, m_is_non_empty; // regex emptiness check
|
||||
symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s)
|
||||
symbol m_eq; // equality atom
|
||||
symbol m_max_unfolding, m_length_limit;
|
||||
|
||||
public:
|
||||
|
||||
seq_skolem(ast_manager& m, th_rewriter& r);
|
||||
|
||||
expr_ref mk(symbol const& s, sort* range) { return mk(s, nullptr, nullptr, nullptr, nullptr, range); }
|
||||
expr_ref mk(symbol const& s, expr* e, sort* range) { return mk(s, e, nullptr, nullptr, nullptr, range); }
|
||||
expr_ref mk(symbol const& s, expr* e1, expr* e2, sort* range) { return mk(s, e1, e2, nullptr, nullptr, range); }
|
||||
expr_ref mk(symbol const& s, expr* e1, expr* e2, expr* e3, sort* range, bool rw = true) { return mk(s, e1, e2, e3, nullptr, range, rw); }
|
||||
expr_ref mk(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr, bool rw = true);
|
||||
|
||||
expr_ref mk(char const* s, sort* range) { return mk(s, nullptr, nullptr, nullptr, nullptr, range); }
|
||||
expr_ref mk(char const* s, expr* e, sort* range) { return mk(s, e, nullptr, nullptr, nullptr, range); }
|
||||
expr_ref mk(char const* s, expr* e1, expr* e2, sort* range) { return mk(s, e1, e2, nullptr, nullptr, range); }
|
||||
expr_ref mk(char const* s, expr* e1, expr* e2, expr* e3, sort* range) { return mk(s, e1, e2, e3, nullptr, range); }
|
||||
expr_ref mk(char const* s , expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr) {
|
||||
return mk(symbol(s), e1, e2, e3, e4, range);
|
||||
}
|
||||
|
||||
expr_ref mk_align(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align", e1, e2, e3, e4); }
|
||||
expr_ref mk_align_l(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.l", e1, e2, e3, e4); }
|
||||
expr_ref mk_align_r(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.r", e1, e2, e3, e4); }
|
||||
expr_ref mk_align_m(expr* e1, expr* e2, expr* e3, expr* e4) {
|
||||
expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr;
|
||||
if (is_align(e1, x1, x2) && is_align(e2, y1, y2)) {
|
||||
if (x2 == y2 && x1 != y1)
|
||||
return mk_align_m(x1, y1, e3, e4);
|
||||
}
|
||||
return mk("seq.align.m", e1, e2, e3, e4);
|
||||
}
|
||||
expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.c_ptr(), m.mk_bool_sort()), m); }
|
||||
expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); }
|
||||
expr_ref mk_is_non_empty(expr* r, expr* u, expr* n) { return mk(m_is_non_empty, r, u, n, m.mk_bool_sort(), false); }
|
||||
expr_ref mk_is_empty(expr* r, expr* u, expr* n) { return mk(m_is_empty, r, u, n, m.mk_bool_sort(), false); }
|
||||
|
||||
expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); }
|
||||
expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); }
|
||||
expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_left", t, s, offset); }
|
||||
expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.last_indexof_right", t, s, offset); }
|
||||
|
||||
expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
|
||||
expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
|
||||
expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); }
|
||||
expr_ref mk_last(expr* s);
|
||||
expr_ref mk_first(expr* s);
|
||||
expr_ref mk_pre(expr* s, expr* i) { return mk(m_pre, s, i); }
|
||||
expr_ref mk_eq(expr* a, expr* b) { return mk(m_eq, a, b, nullptr, nullptr, m.mk_bool_sort()); }
|
||||
expr_ref mk_prefix_inv(expr* s, expr* t) { return mk(m_prefix, s, t); }
|
||||
expr_ref mk_suffix_inv(expr* s, expr* t) { return mk(m_suffix, s, t); }
|
||||
expr_ref mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t);
|
||||
expr_ref mk_is_digit(expr* ch) { return mk(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()); }
|
||||
expr_ref mk_unit_inv(expr* n);
|
||||
expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); }
|
||||
expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); }
|
||||
expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); }
|
||||
expr_ref mk_max_unfolding_depth(unsigned d);
|
||||
expr_ref mk_length_limit(expr* e, unsigned d);
|
||||
|
||||
|
||||
bool is_skolem(symbol const& s, expr const* e) const;
|
||||
bool is_skolem(expr const* e) const { return seq.is_skolem(e); }
|
||||
|
||||
bool is_first(expr* e, expr*& u) { return is_skolem(m_seq_first, e) && (u = to_app(e)->get_arg(0), true); }
|
||||
bool is_last(expr* e, expr*& u) { return is_skolem(m_seq_last, e) && (u = to_app(e)->get_arg(0), true); }
|
||||
bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); }
|
||||
bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); }
|
||||
bool is_tail(expr* e) const { return is_skolem(m_tail, e); }
|
||||
bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); }
|
||||
bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); }
|
||||
bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); }
|
||||
bool is_indexof_left(expr* e, expr*& x, expr*& y) const {
|
||||
return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
bool is_indexof_right(expr* e, expr*& x, expr*& y) const {
|
||||
return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
|
||||
}
|
||||
|
||||
bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
|
||||
bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
|
||||
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }
|
||||
bool is_accept(expr* a, expr*& s, expr*& i, expr*& r, expr*& n) const {
|
||||
return is_accept(a) && to_app(a)->get_num_args() == 4 &&
|
||||
(s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1),
|
||||
r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3),
|
||||
true);
|
||||
}
|
||||
bool is_accept(expr* e, expr*& s, expr*& i, unsigned& idx, expr*& r) const {
|
||||
return is_accept(e) && to_app(e)->get_num_args() == 3 &&
|
||||
(s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1),
|
||||
r = to_app(e)->get_arg(2), true) &&
|
||||
a.is_unsigned(i, idx);
|
||||
}
|
||||
bool is_align(expr const* e) const { return is_skolem(symbol("seq.align.m"), e); }
|
||||
MATCH_BINARY(is_align);
|
||||
bool is_post(expr* e, expr*& s, expr*& start);
|
||||
bool is_pre(expr* e, expr*& s, expr*& i);
|
||||
bool is_eq(expr* e, expr*& a, expr*& b) const;
|
||||
bool is_tail(expr* e, expr*& s, expr*& idx) const;
|
||||
bool is_tail_u(expr* e, expr*& s, unsigned& idx) const;
|
||||
bool is_tail(expr* e, expr*& s) const;
|
||||
bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); }
|
||||
bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); }
|
||||
bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); }
|
||||
bool is_length_limit(expr* p, unsigned& lim, expr*& s) const;
|
||||
bool is_is_empty(expr* e) const { return is_skolem(m_is_empty, e); }
|
||||
bool is_is_non_empty(expr* e) const { return is_skolem(m_is_non_empty, e); }
|
||||
bool is_is_empty(expr* e, expr*& r, expr*& u, expr*& n) const {
|
||||
return is_skolem(m_is_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true);
|
||||
}
|
||||
bool is_is_non_empty(expr* e, expr*& r, expr*& u, expr*& n) const {
|
||||
return is_skolem(m_is_non_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true);
|
||||
}
|
||||
|
||||
void decompose(expr* e, expr_ref& head, expr_ref& tail);
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -29,7 +29,7 @@ Revision History:
|
|||
#include "smt/smt_theory.h"
|
||||
#include "smt/smt_arith_value.h"
|
||||
#include "smt/theory_seq_empty.h"
|
||||
#include "smt/seq_skolem.h"
|
||||
#include "ast/rewriter/seq_skolem.h"
|
||||
#include "smt/seq_axioms.h"
|
||||
#include "smt/seq_regex.h"
|
||||
#include "smt/seq_offset_eq.h"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue