1structure OmegaShell :> OmegaShell = 2struct 3 4open HolKernel boolLib intSyntax integerTheory 5 6(* Takes a closed Presburger arithmetic term over the integers and 7 tries to decide it using the Omega procedure. 8 9 Terms that are Presburger over the naturals or have free variables, 10 or both, are dealt with by the procedures in IntDP_Munge. 11 12 This code makes the decision as to whether or not OmegaSimple can be 13 used, and also performs the necessary normalisation of the input. 14*) 15 16infix THENC THEN ORELSEC |-> 17infixr --> ## 18 19val lhand = rand o rator 20 21val REWRITE_CONV = GEN_REWRITE_CONV TOP_DEPTH_CONV bool_rewrites 22 23fun ERR f msg = HOL_ERR { origin_structure = "OmegaShell", 24 origin_function = f, 25 message = msg} 26 27(* ---------------------------------------------------------------------- 28 check_for_early_equalities t 29 30 t is of the form ?v1..vn. T, and T has been purged of all negations 31 and connectives other than /\ and \/. 32 Before throwing ourselves into DNF-ication, we check to see if T 33 can be seen as 34 (c * vi = ....) /\ P vi 35 If so, the OmegaEq simplification might usefully be applied. Moreover 36 we may save on having to do it multiple times in lots of different 37 disjuncts if we do it now rather than later. 38 ---------------------------------------------------------------------- *) 39 40val check_for_early_equalities = OmegaMath.OmegaEq 41 42 43 44 45fun IS_NOT_EXISTS_CONV tm = if is_exists tm then NO_CONV tm else ALL_CONV tm 46 47(* ---------------------------------------------------------------------- 48 normalise t 49 50 Normalises t, where t is of the form 51 ?v1..vn. T 52 and T is a closed term involving usual boolean operators and leaf terms 53 that are relational operators over integers. T is put into DNF, and 54 the leaf terms are all normalised as well. 55 ---------------------------------------------------------------------- *) 56 57val normalise = let 58 fun push_exs tm = let 59 val vs = map (#1 o dest_var) (#1 (strip_exists tm)) 60 in 61 CooperSyntax.push_in_exists THENC EVERY_DISJ_CONV (RENAME_VARS_CONV vs) 62 end tm 63 open OmegaMath 64in 65 STRIP_QUANT_CONV (Canon.NNF_CONV leaf_normalise false THENC 66 REPEATC (CHANGED_CONV CSimp.csimp THENC 67 REWRITE_CONV [])) THENC 68 push_exs THENC 69 EVERY_DISJ_CONV 70 (check_for_early_equalities THENC 71 (IS_NOT_EXISTS_CONV ORELSEC 72 (STRIP_QUANT_CONV Canon.PROP_DNF_CONV THENC 73 push_exs THENC 74 EVERY_DISJ_CONV (TRY_CONV eliminate_negative_divides) THENC 75 EVERY_DISJ_CONV (TRY_CONV eliminate_positive_divides)))) 76end 77 78(* ---------------------------------------------------------------------- 79 simple t 80 81 Takes a closed term of form ?v1..vn. T and decides it using the 82 OmegaSimple method. 83 ---------------------------------------------------------------------- *) 84 85fun callsimple t = 86 (OmegaSimple.simple_CONV ORELSEC 87 (OmegaSymbolic.eliminate_an_existential THENC 88 EVERY_DISJ_CONV callsimple)) t 89 90val simple = 91 TRY_CONV (STRIP_QUANT_CONV OmegaMath.cond_removal) THENC 92 normalise THENC 93 EVERY_DISJ_CONV (REWRITE_CONV [] THENC 94 (IS_NOT_EXISTS_CONV ORELSEC 95 (OmegaMath.OmegaEq THENC 96 (IS_NOT_EXISTS_CONV ORELSEC callsimple)))) 97 98 99(* decide strategy is given a goal term which has already been prenexed *) 100 101fun decide_strategy tm = let 102 open CooperSyntax OmegaMath 103in 104 case goal_qtype tm of 105 qsUNIV => PRENEX_CONV THENC flip_foralls THENC 106 RAND_CONV simple THENC CooperMath.REDUCE_CONV 107 | qsEXISTS => PRENEX_CONV THENC simple THENC CooperMath.REDUCE_CONV 108 | EITHER => CooperMath.REDUCE_CONV 109 | NEITHER => OmegaSymbolic.findelim_deep_existential THENC 110 REWRITE_CONV [] THENC decide_strategy 111end tm 112 113 114(* in order to do prenexing, we need to remove quantifiers that hide 115 within conditional guards. There's a lot of faff happening here: 116 why not just do away with conditional expressions from the outset? 117 118 Two reasons: 119 * rewriting the wrong way will double the term size because one 120 rewrite is right for CNF and the other is right for DNF. 121 * conditional expressions that repeat the same guard should have 122 the case-split done on the guard just once. *) 123fun remove_qs_from_guards tm = let 124 val (g, t, e) = dest_cond tm 125in 126 if CooperSyntax.goal_qtype g <> CooperSyntax.EITHER then 127 REWR_CONV COND_EXPAND tm 128 else NO_CONV tm 129end 130 131val decide_closed_presburger = 132 TOP_DEPTH_CONV remove_qs_from_guards THENC 133 DEPTH_CONV EXISTS_UNIQUE_CONV THENC 134 REWRITE_CONV [IMP_DISJ_THM] THENC 135 decide_strategy 136 137(* utility function for assessing how big a term will result when something 138 is converted to DNF naively : 139fun dnf_size t = 140 if is_disj t then 141 (op+ o (dnf_size ## dnf_size) o dest_disj) t 142 else if is_conj t then 143 (op* o (dnf_size ## dnf_size) o dest_conj) t 144 else 1 145 146*) 147 148 149end (* struct *) 150