| 881 | } |
| 882 | |
| 883 | void basic_decl_plugin::finalize() { |
| 884 | #define DEC_REF(FIELD) if (FIELD) { m_manager->dec_ref(FIELD); } |
| 885 | #define DEC_ARRAY_REF(FIELD) m_manager->dec_array_ref(FIELD.size(), FIELD.begin()) |
| 886 | DEC_REF(m_bool_sort); |
| 887 | DEC_REF(m_true_decl); |
| 888 | DEC_REF(m_false_decl); |
| 889 | DEC_REF(m_and_decl); |
| 890 | DEC_REF(m_or_decl); |
| 891 | DEC_REF(m_not_decl); |
| 892 | DEC_REF(m_xor_decl); |
| 893 | DEC_REF(m_implies_decl); |
| 894 | DEC_ARRAY_REF(m_eq_decls); |
| 895 | DEC_ARRAY_REF(m_ite_decls); |
| 896 | |
| 897 | DEC_ARRAY_REF(m_oeq_decls); |
| 898 | DEC_REF(m_proof_sort); |
| 899 | DEC_REF(m_undef_decl); |
| 900 | DEC_REF(m_true_pr_decl); |
| 901 | DEC_REF(m_asserted_decl); |
| 902 | DEC_REF(m_goal_decl); |
| 903 | DEC_REF(m_modus_ponens_decl); |
| 904 | DEC_REF(m_reflexivity_decl); |
| 905 | DEC_REF(m_symmetry_decl); |
| 906 | DEC_REF(m_transitivity_decl); |
| 907 | DEC_REF(m_quant_intro_decl); |
| 908 | DEC_REF(m_and_elim_decl); |
| 909 | DEC_REF(m_not_or_elim_decl); |
| 910 | DEC_REF(m_rewrite_decl); |
| 911 | DEC_REF(m_pull_quant_decl); |
| 912 | DEC_REF(m_push_quant_decl); |
| 913 | DEC_REF(m_elim_unused_vars_decl); |
| 914 | DEC_REF(m_der_decl); |
| 915 | DEC_REF(m_quant_inst_decl); |
| 916 | DEC_ARRAY_REF(m_monotonicity_decls); |
| 917 | DEC_ARRAY_REF(m_transitivity_star_decls); |
| 918 | DEC_ARRAY_REF(m_distributivity_decls); |
| 919 | DEC_ARRAY_REF(m_assoc_flat_decls); |
| 920 | DEC_ARRAY_REF(m_rewrite_star_decls); |
| 921 | |
| 922 | DEC_REF(m_hypothesis_decl); |
| 923 | DEC_REF(m_iff_true_decl); |
| 924 | DEC_REF(m_iff_false_decl); |
| 925 | DEC_REF(m_commutativity_decl); |
| 926 | DEC_REF(m_def_axiom_decl); |
| 927 | DEC_REF(m_lemma_decl); |
| 928 | DEC_ARRAY_REF(m_unit_resolution_decls); |
| 929 | |
| 930 | DEC_REF(m_def_intro_decl); |
| 931 | DEC_REF(m_iff_oeq_decl); |
| 932 | DEC_REF(m_skolemize_decl); |
| 933 | DEC_REF(m_mp_oeq_decl); |
| 934 | DEC_REF(m_assumption_add_decl); |
| 935 | DEC_REF(m_lemma_add_decl); |
| 936 | DEC_REF(m_th_assumption_add_decl); |
| 937 | DEC_REF(m_th_lemma_add_decl); |
| 938 | DEC_REF(m_redundant_del_decl); |
| 939 | DEC_ARRAY_REF(m_apply_def_decls); |
| 940 | DEC_ARRAY_REF(m_nnf_pos_decls); |
no outgoing calls
no test coverage detected