mirror of
https://github.com/Z3Prover/z3
synced 2026-03-17 18:43:45 +00:00
move seq_model from smt/seq/ to smt/; fix seq_state.h add_str_mem typo
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
10a6029c0e
commit
7c80c3b3aa
6 changed files with 5 additions and 4 deletions
|
|
@ -65,6 +65,7 @@ z3_add_component(smt
|
|||
theory_intblast.cpp
|
||||
theory_lra.cpp
|
||||
theory_nseq.cpp
|
||||
seq_model.cpp
|
||||
theory_opt.cpp
|
||||
theory_pb.cpp
|
||||
theory_recfun.cpp
|
||||
|
|
|
|||
|
|
@ -2,7 +2,6 @@ z3_add_component(smt_seq
|
|||
SOURCES
|
||||
seq_regex.cpp
|
||||
seq_state.cpp
|
||||
seq_model.cpp
|
||||
seq_parikh.cpp
|
||||
seq_nielsen.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ namespace smt {
|
|||
m_eq_sources.push_back({n1, n2});
|
||||
}
|
||||
|
||||
void add_str_mem(euf::snode* str, euf::snode* regex, sat:literal lit) {
|
||||
void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) {
|
||||
seq::dep_tracker dep;
|
||||
m_str_mems.push_back(seq::str_mem(str, regex, nullptr, m_next_mem_id++, dep));
|
||||
m_mem_sources.push_back({lit});
|
||||
|
|
|
|||
|
|
@ -16,9 +16,10 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner) 2026-03-01
|
||||
|
||||
--*/
|
||||
#include "smt/seq/seq_model.h"
|
||||
#include "smt/seq_model.h"
|
||||
#include "smt/seq/seq_regex.h"
|
||||
#include "smt/seq/seq_state.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include "smt/smt_model_generator.h"
|
||||
#include "smt/proto_model/proto_model.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
|
@ -27,7 +27,7 @@ Author:
|
|||
#include "smt/seq/seq_nielsen.h"
|
||||
#include "smt/seq/seq_state.h"
|
||||
#include "smt/seq/seq_regex.h"
|
||||
#include "smt/seq/seq_model.h"
|
||||
#include "smt/seq_model.h"
|
||||
#include "smt/nseq_context_solver.h"
|
||||
|
||||
namespace smt {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue