~trn/reduce-algebra

ref: 14ea731d477b4075bd3d025b2cba565b29a68aa4 reduce-algebra/packages/redlog/cl/clsimpl.red -rw-r--r-- 15.6 KiB
14ea731d — Jeffrey H. Johnson Merge branch 'svn/trunk' a month ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
module clsimpl;
% Common logic simplification. This is a generic implementation of the "standard simplifier"
% described in  "Simplification of Quantifier-Free Formulae over Ordered Fields", J. Symb. Comput.
% 24(2):209–231, 1997, https://doi.org/10.1006/jsco.1997.0123.

revision('clsimpl, "$Id$");

copyright('clsimpl, "(c) 1995-2021 A. Dolzmann, T. Sturm");

% Redistribution and use in source and binary forms, with or without
% modification, are permitted provided that the following conditions
% are met:
%
%    * Redistributions of source code must retain the relevant
%      copyright notice, this list of conditions and the following
%      disclaimer.
%    * Redistributions in binary form must reproduce the above
%      copyright notice, this list of conditions and the following
%      disclaimer in the documentation and/or other materials provided
%      with the distribution.
%
% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

rl_provideService rl_simpl = cl_simpl
   using rl_negateat, rl_simplat1, rl_smupdknowl, rl_smrmknowl, rl_smcpknowl,
   rl_smmkatl, rl_ordatp, rl_susipost, rl_susitf, rl_susibin, rl_b2terml,
   rl_simplb, rl_b2atl, rl_bsatp;

asserted procedure cl_simpl(f: Formula, atl: List, n: Integer): Formula;
   % Common logic simplify. [f] is a formula; [atl] is a list of atomic
   % formulas, which are considered to describe a theory; [n] is an integer.
   % Depends on switch [!*rlsiso]. Returns the identifier [inctheo] or a
   % formula. [inctheo] means that [atl] is inconsistent. Else the result is
   % [f], simplified (wrt. [atl]). For non-negative [n], simplification stops
   % at level [n].
   begin scalar w;
      atl := cl_simplifyTheory atl;
      if rl_excp atl then
         return atl;
      w := rl_smupdknowl('and, atl, nil, n+1);
      if w eq 'false then
         return rl_exc("inconsistent theory");
      return cl_simpl1(f, w, n, nil)
   end;

asserted procedure cl_simplifyTheory(atl: List): List;
   % Common logic simplify theory. [atl] is a THEORY. Returns either a
   % list $l$ of atomic formulas, or the identifier [inctheo]. In the
   % first case the conjunction over $l$ is equivalent to the
   % conjuction over [atl], and $l$ contains only simplified atomic
   % formulas. The return value [inctheo] means that the conjunction
   % over [atl] is equivalent to [false].
   begin scalar atf, w, natl, !*rlsiexpla;
      while atl do <<
         atf := pop atl;
         w := cl_simplat(atf, nil);
         if w eq 'false then <<
            atf := 'inctheo;
            atl := nil
         >> else if w neq 'true then
            natl := w . natl
      >>;
      if atf eq 'inctheo then
         return rl_exc("inconsistent theory");
      return natl
   end;

asserted procedure cl_simpl1(f: Formula, knowl: Any, n: Integer, sop: Id): Formula;
   % Common logic simplify. [f] is a formula; [knowl] is an IRL; [n] is an
   % integer; [sop] is a CL operator. Depends on switch [!*rlsiso]. Returns a
   % formula. Simplifies [f] recursively using [knowl].
   begin scalar op;
      if eqn(n, 0) then
         return f;
      op := rl_op f;
      if rl_tvalp op then
         return f;
      if rl_junctp op then
         return cl_simplifyAndOr(f, knowl, n);
      if op eq 'not then
         return cl_simplifyNot(f, knowl, n);
      if rl_quap op then
         return cl_simplifyQuantifier(f, knowl, n);
      if rl_bquap op then
         return rl_simplifyBoundedQuantifier(f, knowl, n);
      if op eq 'impl then
         return cl_simplifyImplication(rl_arg2l f, rl_arg2r f,knowl, n);
      if op eq 'repl then
         return cl_simplifyImplication(rl_arg2r f, rl_arg2l f, knowl, n);
      if op eq 'equiv then
         return cl_simplifyEquivalence(rl_arg2l f, rl_arg2r f, knowl, n);
      ASSERT( cl_atfp f );
      return cl_simplifyAtom(f, knowl, n, sop)
   end;

asserted procedure cl_simplifyAtom(f: AtFormula, knowl: Any, n: Integer, sop: Id): Formula;
   begin scalar w, op, newknowl;
      w := cl_simplat(f, sop);
      op := rl_op w;
      if rl_junctp op then
         return cl_simplifyAndOr(w, knowl, n);
      if rl_tvalp op then
         return w;
      ASSERT( cl_atfp w );
      newknowl := rl_smupdknowl('and, {w}, rl_smcpknowl knowl, n);
      if newknowl eq 'false then
         return 'false;
      w := rl_smmkatl('and, knowl, newknowl, n);
      if w eq 'false then
         return 'false;
      return rl_smkn('and, w)
   end; 

asserted procedure cl_simplifyQuantifier(f: Formula, knowl: Any, n: Integer): Formula;
   begin scalar q, x, w;
      q := rl_op f;
      x := rl_var f;
      knowl := rl_smrmknowl(knowl, x);
      w := cl_simpl1(rl_mat f, knowl, n-1, q);
      if not (x memq cl_fvarl1 w) then
         % This test covers truth values.
         return w;
      return rl_mkq(q, x, w)
   end;

asserted procedure cl_simplifyNot(f: Formula, knowl: Any, n: Integer): Formula;
   begin scalar result;
      result := cl_simpl1(rl_arg1 f, knowl, n-1, 'not);
      if rl_tvalp result then
         return cl_flip result;
      if cl_atfp result then
         return rl_negateat result;
      return cl_involutiveNot result
   end;  

asserted procedure cl_involutiveNot(f: Formula): Formula;
   % Common logic negate applying the law of involutivity. [f] is a
   % formula. Returns $\phi$ if [f] is of the form $\lnot \phi$,
   % $\lnot [f]$ else.
   if rl_op f eq 'not then rl_arg1 f else rl_mk1('not, f);

asserted procedure cl_simplifyAndOr(f: Formula, knowl: Any, n: Integer): Formula;
   % Common logic simplify conjunction or disjunction.
   begin scalar op, junct, break, w, atl, col, newknowl, a, wop, argl, sicol, natl;
      newknowl := rl_smcpknowl knowl;
      op := rl_op f;
      junct := rl_argn f;
      break := cl_cflip('false, op eq 'and);
      for each subf in junct do <<
         w := if cl_atfp subf then cl_simplat(subf, op) else subf;
         if cl_atfp w then
            atl := w . atl
         else
            col := w . col
      >>;
      newknowl := rl_smupdknowl(op, atl, newknowl, n);
      if newknowl eq 'false then
         return break;
      col := reversip col;
      while col do <<
         a := pop col;
         w := cl_simpl1(a, newknowl, n-1, op);
         wop := rl_op w;
         if wop eq break then <<
            a := break;
            col := nil
         >> else if wop eq op then <<
            argl := rl_argn w;
            while argl and cl_atfp car argl do <<
               natl := car argl . natl;
               argl := cdr argl
            >>;
            if natl then <<
               col := nconc(reversip sicol,col);
               sicol := nil
            >>;
            sicol := nconc(sicol,reverse argl)  % must be constructive
         >> else if rl_cxp wop then
            (if wop neq cl_flip break then sicol := w . sicol)
         else <<
            ASSERT( cl_atfp w );
            col := nconc(reversip sicol, col);
            sicol := nil;
            natl := {w}
         >>;
         if natl then <<
            newknowl := rl_smupdknowl(op, natl, newknowl, n);
            if newknowl eq 'false then <<
               a := break;
               col := nil
            >>;
            natl := nil
         >>
      >>;
      if a eq break then
         return break;
      atl := rl_smmkatl(op, knowl, newknowl, n);
      if atl eq break then
         return break;
      % It might be better to avoid duplicates right away.
      w := sicol;
      sicol := nil;
      for each x in w do
         sicol := lto_insert(x, sicol);
      if !*rlsiso then <<
         atl := sort(atl, 'rl_ordatp);
         sicol := sort(sicol, 'cl_ordp)
      >>;
      return rl_smkn(op, nconc(atl, sicol))
   end;

asserted procedure cl_simplifyImplication(prem: Formula, concl: Formula, knowl: Any, n: Integer): Formula;
   begin scalar w, newknowl;
      if concl eq 'true then
         return 'true;
      prem := cl_simpl1(prem, knowl, n-1, 'prem);
      if prem eq 'false then
         return 'true;
      concl := cl_simpl1(concl, knowl, n-1, 'concl);
      if concl eq 'true then
         return 'true;
      if prem eq 'true then
         return concl;
      if concl eq 'false then
         return cl_involutiveNot prem;
      ASSERT( not rl_tvalp prem and not rl_tvalp concl );
      if prem = concl then
         return 'true;
      if cl_atfp prem and cl_atfp concl then <<
         w := cl_simpl1(rl_nnf rl_mk2('impl, prem, concl), knowl, n-1, nil);
         if rl_tvalp w or cl_atfp w then
            return w;
         return rl_mk2('impl, prem, concl)
      >> else if cl_atfp prem and cl_cxfp concl then <<
         newknowl := rl_smupdknowl('and, {prem}, rl_smcpknowl knowl, n);
         if newknowl eq 'false then
            return 'true;
         return rl_mk2('impl, prem, cl_simpl1(concl, newknowl, n-1, 'concl))
      >> else if cl_cxfp prem and cl_atfp concl then <<
         newknowl := rl_smupdknowl('or, {concl}, rl_smcpknowl knowl, n);
         if newknowl eq 'false then
            return 'true;
         return rl_mk2('impl, cl_simpl1(prem, newknowl, n-1, 'concl), concl)
      >> else <<
         ASSERT( cl_cxfp prem and cl_cxfp concl );
         return rl_mk2('impl, prem, concl)
      >>
   end;

asserted procedure cl_simplifyEquivalence(lhs: Formula, rhs: Formula, knowl: Any, n: Integer): Formula;
   begin scalar w;
      lhs := cl_simpl1(lhs, knowl, n-1, 'equiv);
      rhs := cl_simpl1(rhs, knowl, n-1, 'equiv);
      if lhs eq 'true then
         return rhs;
      if rhs eq 'true then
         return lhs;
      if lhs eq 'false then
         return cl_involutiveNot rhs;
      if rhs eq 'false then
         return cl_involutiveNot lhs;
      if lhs = rhs then
         return 'true;
      if cl_atfp lhs and cl_atfp rhs then <<
         w := cl_simpl1(rl_nnf rl_mk2('equiv, lhs, rhs), knowl, n, nil);
         if rl_tvalp w or cl_atfp w then
            return w
      >>;
      return if cl_ordp(lhs, rhs) then
         rl_mk2('equiv, lhs, rhs)
      else
         rl_mk2('equiv, rhs, lhs)
   end;

asserted procedure cl_simplat(atf: AtFormula, sop: Id): QfFormula;
   % Common logic simplify atomic formula. The result is equivalent to atf.
   % sop contains the logical operator of the boolean level where atf
   % occurred. This can help to decide about splitting or not splitting atf.
   if not !*rlidentify then
      rl_simplat1(atf, sop)
   else
      cl_apply2ats(rl_simplat1(atf, sop), 'cl_identifyat);

asserted procedure cl_identifyathfn(atf: Atom): List2;
   {rl_op atf, cl_varl1 atf};

asserted procedure cl_identifyat(atf: Atom): Atom;
   % Common logic identify atomic formula. [atf] is an atomic formula.
   % Returns an atomic formula equal to [atf].
   begin scalar w;
      if rl_tvalp atf then return atf;
      if (w := lto_hmember(atf, cl_identify!-atl!*, 'cl_identifyathfn)) then
         return car w;
      cl_identify!-atl!* := lto_hinsert(atf, cl_identify!-atl!*, 'cl_identifyathfn);
      return atf
   end;

% The following code implements the ordering of formulas used for sorting the
% boolean levels.

asserted procedure cl_ordp(f1: Formula, f2: Formula): ExtraBoolean;
   % Common logic order predicate. This is a strict total ordering.
   begin scalar op1,op2;
      op1 := rl_op f1;
      op2 := rl_op f2;
      if not rl_cxp op1 and not rl_cxp op2 then
         return rl_ordatp(f1, f2);
      if not rl_cxp op1 and rl_cxp op2 then
         return t;
      if rl_cxp op1 and not rl_cxp op2 then
         return nil;
      % Both [op1] and [op2] are non-atomic now.
      if op1 neq op2 then
         return cl_ordopp(op1, op2);
      if rl_tvalp op1 then
         return t;
      if rl_quap op1 then
         return if rl_var f1 neq rl_var f2 then
            not(ordp(rl_var f1, rl_var f2) and rl_var f1 neq rl_var f2)
         else
            cl_ordp(rl_mat f1, rl_mat f2);
      if rl_bquap op1 then
         return rl_BQordp(f1, f2);
      ASSERT( rl_junctp f1 and op1 = op2 );
      return cl_ordpl(rl_argn f1, rl_argn f2)
   end;

asserted procedure cl_ordpl(fl1: List, fl2: List): ExtraBoolean;
   % Common logic order predicate on lists. Generalizes cl_ordp to lists.
   if not fl2 then
      nil
   else if not fl1 then
      t
   else if car fl1 neq car fl2 then
      cl_ordp(car fl1, car fl2)
   else
      cl_ordpl(cdr fl1, cdr fl2);

asserted procedure cl_ordopp(op1: Id, op2: Id): ExtraBoolean;
   % Common logic ordered operator predicate. [op1] and [op2] are first-order
   % operators. Returns t iff op1 < op2.
   op2 memq cdr (op1 memq '(and or not impl repl equiv bex ball ex all true false));

% The following code implements a "generic smart simplification". All black
% boxes for the smart simplification are implemented generically using only a
% single non-generic black box rl_negateat. rl_negateat must return an atomic
% formula.

asserted procedure cl_smcpknowl(knowl: Alist): Alist;
   % Common logic smart simplifier copy knowledge. [knowl] is a
   % knowledge base. Returns a toplevel copy of [knowl].
   for each p in knowl collect p;

asserted procedure cl_smrmknowl(knowl: Alist, v: Id): Alist;
   % Common logic smart simplifier remove knowledge. [knowl] is a
   % knowledge base; [v] is a variable. Returns a knowledge base.
   % Removes all knowledge involving [v] from the knowledge base.
   nil;

asserted procedure cl_smupdknowl(op: Id, atl: List, knowl: Alist, n: Integer): Alist;
   % Common logic smart simplifier update knowledge. [op] is one of the
   % operators [and], [or]; [atl] is a list of atomic formulas; [knowl] is
   % knowledge base; [n] is an integer. Returns a knowledge base. If [op] is
   % [and], then all knowledge in [atl] is added to the [knowl] with the tag
   % [n]. If [op] is [or], then the negation of all knowledge in [atl] is added
   % to [knowl].
   begin scalar at;
      while atl do <<
         at := car atl;
         atl := cdr atl;
         knowl := cl_smupdknowl1(op, at, knowl, n);
         if knowl eq 'false then <<
            atl := nil;
            at := 'break
         >>
      >>;
      if at eq 'break then
         return 'false
      else
         return knowl
   end;

asserted procedure cl_smupdknowl1(op: Id, at: Atom, knowl: Alist, n: Integer): Alist;
   begin scalar ent, contra;
      if op eq 'or then <<
         ent := rl_negateat at;
         contra := at
      >> else <<
         ent := at;
         contra := rl_negateat at
      >>;
      if assoc(contra, knowl) then
         return 'false;
      if assoc(ent, knowl) then
         return knowl;
      return knowl := (ent . n) . knowl
   end;

asserted procedure cl_smmkatl(op: Id, knowl: Alist, newknowl: Alist, n: Integer): List;
   % Common logic smart simplifier make atomic formula list. [op] is
   % one of the operators [and], [or]; [knowl], [newknowl] are
   % knowledge bases; [n] is an integer. Returns a list of atomic
   % formulas. All knowledge tagged with [n] is extraced from
   % [newknowl] and returned as a list of atomic formulas.
   begin scalar res;
      res := for each pair in newknowl join
         if cdr pair = n then {car pair};
      if op eq 'or then
         res := for each at in res collect rl_negateat at;
      return res
   end;

endmodule;  % [clsimpl]

end;  % of file