mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

add QF_DT

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-17 01:39:39 +02:00
parent a0d0812b0c
commit 8ff1e070be
5 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/normal_forms/pull_quant.cpp
View file

@ -244,7 +244,7 @@ struct pull_quant::imp {
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
proof * p1 = 0;
if (n != q1) {
proof * p0 = m_manager.mk_pull_quant(to_quantifier(n)->get_expr(), to_quantifier(new_expr));
proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr));
p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
}
proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));

9
src/cmd_context/check_logic.cpp
View file

@ -37,6 +37,7 @@ struct check_logic::imp {
datatype_util m_dt_util;
pb_util m_pb_util;
bool m_uf; // true if the logic supports uninterpreted functions
bool m_dt; // true if the lgoic supports dattypes
bool m_arrays; // true if the logic supports arbitrary arrays
bool m_bv_arrays; // true if the logic supports only bv arrays
bool m_reals; // true if the logic supports reals
@ -53,6 +54,7 @@ struct check_logic::imp {
void reset() {
m_uf = false;
m_dt = false;
m_arrays = false;
m_bv_arrays = false;
m_reals = false;
@ -105,6 +107,10 @@ struct check_logic::imp {
m_uf = true;
m_bvs = true;
}
else if (logic == "QF_DT") {
m_uf = true;
m_dt = true;
}
else if (logic == "QF_AUFLIA") {
m_uf = true;
m_arrays = true;
@ -187,6 +193,7 @@ struct check_logic::imp {
m_bvs = true;
m_uf = true;
m_ints = true;
m_dt = true;
m_nonlinear = true; // non-linear 0-1 variables may get eliminated
}
else {
@ -443,7 +450,7 @@ struct check_logic::imp {
else if (fid == m_seq_util.get_family_id()) {
// nothing to check
}
else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
else if (fid == m_dt_util.get_family_id() && m_dt) {
// nothing to check
}
else if (fid == m_pb_util.get_family_id() && m_logic == "QF_FD") {

8
src/smt/smt_setup.cpp
View file

@ -125,6 +125,8 @@ namespace smt {
setup_QF_FPBV();
else if (m_logic == "QF_S")
setup_QF_S();
else if (m_logic == "QF_DT")
setup_QF_DT();
else
setup_unknown();
}
@ -190,6 +192,8 @@ namespace smt {
setup_AUFLIRA();
else if (m_logic == "UFNIA")
setup_UFNIA();
else if (m_logic == "QF_DT")
setup_QF_DT();
else if (m_logic == "LRA")
setup_LRA();
else
@ -210,6 +214,10 @@ namespace smt {
m_params.m_random_initial_activity = IA_RANDOM;
}
void setup::setup_QF_DT() {
setup_QF_UF();
}
void setup::setup_QF_BVRE() {
setup_QF_BV();
setup_QF_LIA();

1
src/smt/smt_setup.h
View file

@ -54,6 +54,7 @@ namespace smt {
// setup_<logic>(static_features & st) can only be used if the logical context will perform a single
// check.
//
void setup_QF_DT();
void setup_QF_UF();
void setup_QF_UF(static_features const & st);
void setup_QF_RDL();

4
src/solver/smt_logics.cpp
View file

@ -141,7 +141,7 @@ bool smt_logics::logic_has_fpa(symbol const & s) {
}
bool smt_logics::logic_has_uf(symbol const & s) {
return s == "QF_UF" || s == "UF";
return s == "QF_UF" || s == "UF" || s == "QF_DT";
}
bool smt_logics::logic_has_horn(symbol const& s) {
@ -153,5 +153,5 @@ bool smt_logics::logic_has_pb(symbol const& s) {
}
bool smt_logics::logic_has_datatype(symbol const& s) {
return s == "QF_FD" || s == "ALL";
return s == "QF_FD" || s == "ALL" || s == "QF_DT";
}