mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5eb23e1e7a
commit
58411f64e8
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include"arith_decl_plugin.h"
|
||||
#include"array_decl_plugin.h"
|
||||
#include"bv_decl_plugin.h"
|
||||
#include"seq_decl_plugin.h"
|
||||
#include"ast_pp.h"
|
||||
#include"for_each_expr.h"
|
||||
|
||||
|
@ -29,6 +30,7 @@ struct check_logic::imp {
|
|||
arith_util m_a_util;
|
||||
bv_util m_bv_util;
|
||||
array_util m_ar_util;
|
||||
seq_util m_seq_util;
|
||||
bool m_uf; // true if the logic supports uninterpreted functions
|
||||
bool m_arrays; // true if the logic supports arbitrary arrays
|
||||
bool m_bv_arrays; // true if the logic supports only bv arrays
|
||||
|
@ -40,7 +42,7 @@ struct check_logic::imp {
|
|||
bool m_quantifiers; // true if the logic supports quantifiers
|
||||
bool m_unknown_logic;
|
||||
|
||||
imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m) {
|
||||
imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m) {
|
||||
reset();
|
||||
}
|
||||
|
||||
|
@ -168,9 +170,12 @@ struct check_logic::imp {
|
|||
m_bvs = true;
|
||||
m_quantifiers = true;
|
||||
}
|
||||
else if (logic == "UF_S") {
|
||||
else if (logic == "QF_S") {
|
||||
m_uf = true;
|
||||
m_bvs = true;
|
||||
m_ints = true;
|
||||
m_arrays = true;
|
||||
m_reals = true;
|
||||
m_quantifiers = false;
|
||||
}
|
||||
else {
|
||||
|
@ -424,6 +429,9 @@ struct check_logic::imp {
|
|||
else if (m.is_builtin_family_id(fid)) {
|
||||
// nothing to check
|
||||
}
|
||||
else if (fid == m_seq_util.get_family_id()) {
|
||||
// nothing to check
|
||||
}
|
||||
else {
|
||||
fail("logic does not support theory");
|
||||
}
|
||||
|
|
|
@ -544,6 +544,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
|
|||
s == "QF_FP" ||
|
||||
s == "QF_FPBV" ||
|
||||
s == "QF_BVFP" ||
|
||||
s == "QF_S" ||
|
||||
s == "HORN";
|
||||
}
|
||||
|
||||
|
|
|
@ -312,6 +312,8 @@ namespace smt {
|
|||
d.m_phase_available = true;
|
||||
d.m_phase = !l.sign();
|
||||
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
|
||||
TRACE("relevancy",
|
||||
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";);
|
||||
if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
|
||||
m_atom_propagation_queue.push_back(l);
|
||||
|
||||
|
@ -805,8 +807,10 @@ namespace smt {
|
|||
void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) {
|
||||
enode * r2 = n2->get_root();
|
||||
enode * r1 = n1->get_root();
|
||||
if (!r1->has_th_vars() && !r2->has_th_vars())
|
||||
if (!r1->has_th_vars() && !r2->has_th_vars()) {
|
||||
TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_owner()->get_id() << " #" << n2->get_owner()->get_id() << "\n";);
|
||||
return;
|
||||
}
|
||||
|
||||
theory_id from_th = null_theory_id;
|
||||
|
||||
|
|
|
@ -469,6 +469,9 @@ bool theory_seq::simplify_and_solve_eqs() {
|
|||
return change;
|
||||
}
|
||||
|
||||
void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
|
||||
}
|
||||
|
||||
bool theory_seq::internalize_atom(app* a, bool) {
|
||||
return internalize_term(a);
|
||||
}
|
||||
|
@ -598,7 +601,7 @@ void theory_seq::set_incomplete(app* term) {
|
|||
}
|
||||
|
||||
theory_var theory_seq::mk_var(enode* n) {
|
||||
if (!m_util.is_seq(n->get_owner()) ||
|
||||
if (!m_util.is_seq(n->get_owner()) &&
|
||||
!m_util.is_re(n->get_owner())) {
|
||||
return null_theory_var;
|
||||
}
|
||||
|
@ -608,6 +611,7 @@ theory_var theory_seq::mk_var(enode* n) {
|
|||
else {
|
||||
theory_var v = theory::mk_var(n);
|
||||
get_context().attach_th_var(n, this, v);
|
||||
get_context().mark_as_relevant(n);
|
||||
return v;
|
||||
}
|
||||
}
|
||||
|
@ -1005,6 +1009,10 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
|
|||
else if (m_util.str.is_in_re(e, e1, e2)) {
|
||||
// TBD
|
||||
}
|
||||
else if (m.is_eq(e, e1, e2)) {
|
||||
new_eq_eh(ctx.get_enode(e1)->get_th_var(get_id()),
|
||||
ctx.get_enode(e1)->get_th_var(get_id()));
|
||||
}
|
||||
else {
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
|
|
@ -128,6 +128,7 @@ namespace smt {
|
|||
virtual final_check_status final_check_eh();
|
||||
virtual bool internalize_atom(app*, bool);
|
||||
virtual bool internalize_term(app*);
|
||||
virtual void internalize_eq_eh(app * atom, bool_var v);
|
||||
virtual void new_eq_eh(theory_var, theory_var);
|
||||
virtual void new_diseq_eh(theory_var, theory_var);
|
||||
virtual void assign_eq(bool_var v, bool is_true);
|
||||
|
|
Loading…
Reference in a new issue