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

Merge pull request #1646 from NikolajBjorner/master

Browse source 
Remove depedencies on interp
This commit is contained in:
Nikolaj Bjorner 2018-05-25 10:25:31 -07:00 • committed by GitHub
commit 434ff31629
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
69 changed files with 45 additions and 26535 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/ast.cpp
View file

@ -646,7 +646,6 @@ basic_decl_plugin::basic_decl_plugin():
m_iff_decl(nullptr),
m_xor_decl(nullptr),
m_not_decl(nullptr),
m_interp_decl(nullptr),
m_implies_decl(nullptr),
m_proof_sort(nullptr),
@ -865,7 +864,6 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_iff_decl = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true);
m_xor_decl = mk_bool_op_decl("xor", OP_XOR, 2, true, true);
m_not_decl = mk_bool_op_decl("not", OP_NOT, 1);
m_interp_decl = mk_bool_op_decl("interp", OP_INTERP, 1);
m_implies_decl = mk_implies_decl();
m_proof_sort = m->mk_sort(symbol("Proof"), sort_info(id, PROOF_SORT));
@ -890,7 +888,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("or", OP_OR));
op_names.push_back(builtin_name("xor", OP_XOR));
op_names.push_back(builtin_name("not", OP_NOT));
op_names.push_back(builtin_name("interp", OP_INTERP));
op_names.push_back(builtin_name("=>", OP_IMPLIES));
if (logic == symbol::null) {
// user friendly aliases
@ -902,7 +899,6 @@ void basic_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("||", OP_OR));
op_names.push_back(builtin_name("equals", OP_EQ));
op_names.push_back(builtin_name("equiv", OP_IFF));
op_names.push_back(builtin_name("@@", OP_INTERP));
}
}
@ -923,7 +919,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_and_decl);
DEC_REF(m_or_decl);
DEC_REF(m_not_decl);
DEC_REF(m_interp_decl);
DEC_REF(m_iff_decl);
DEC_REF(m_xor_decl);
DEC_REF(m_implies_decl);
@ -1056,7 +1051,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
@ -1099,7 +1093,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;

4
src/ast/ast.h
View file

@ -1041,7 +1041,7 @@ enum basic_sort_kind {
};
enum basic_op_kind {
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP,
OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
@ -1063,7 +1063,6 @@ protected:
func_decl * m_iff_decl;
func_decl * m_xor_decl;
func_decl * m_not_decl;
func_decl * m_interp_decl;
func_decl * m_implies_decl;
ptr_vector<func_decl> m_eq_decls; // cached eqs
ptr_vector<func_decl> m_ite_decls; // cached ites
@ -2054,7 +2053,6 @@ public:
app * mk_true() const { return m_true; }
app * mk_false() const { return m_false; }
app * mk_bool_val(bool b) { return b?m_true:m_false; }
app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
func_decl* mk_and_decl() {