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