mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 15:47:29 +00:00
Code Activity

Add theory registration to smt_setup

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-15 08:57:50 +00:00
parent 6958bf2f01
commit 4cd6c808ac
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_setup.cpp
View file

@ -40,6 +40,7 @@ Revision History:
#include "smt/theory_pb.h"
#include "smt/theory_fpa.h"
#include "smt/theory_polymorphism.h"
#include "smt/theory_finite_set.h"
namespace smt {
@ -784,6 +785,10 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_char, m_context));
}
void setup::setup_finite_set() {
m_context.register_plugin(alloc(smt::theory_finite_set, m_context));
}
void setup::setup_special_relations() {
m_context.register_plugin(alloc(smt::theory_special_relations, m_context, m_manager));
}
@ -807,6 +812,7 @@ namespace smt {
setup_dl();
setup_seq_str(st);
setup_fpa();
setup_finite_set();
setup_special_relations();
setup_polymorphism();
setup_relevancy(st);

1
src/smt/smt_setup.h
View file

@ -102,6 +102,7 @@ namespace smt {
void setup_seq_str(static_features const & st);
void setup_seq();
void setup_char();
void setup_finite_set();
void setup_card();
void setup_sls();
void setup_i_arith();