1module ibalpkapur; % Author Stefan Kaeser 2 3revision('ibalpkapur, "$Id: ibalpkapur.red 3961 2017-03-19 08:24:03Z thomas-sturm $"); 4 5copyright('ibalpkapur, "(c) 2007-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm"); 6 7% Redistribution and use in source and binary forms, with or without 8% modification, are permitted provided that the following conditions 9% are met: 10% 11% * Redistributions of source code must retain the relevant 12% copyright notice, this list of conditions and the following 13% disclaimer. 14% * Redistributions in binary form must reproduce the above 15% copyright notice, this list of conditions and the following 16% disclaimer in the documentation and/or other materials provided 17% with the distribution. 18% 19% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 20% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 21% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 22% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 23% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 24% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 25% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 26% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 27% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 28% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 29% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 30% 31 32% own switches and global vars 33fluid '(ibalp_kapuroptions!* !*ibalp_kapurgb !*rlkapurchktaut !*rlkapurchkcont); 34switch ibalp_kapurgb,rlkapurchktaut,rlkapurchkcont; 35 36% debug switches 37fluid '(!*ibalp_kapurgbdegd !*ibalp_kapurdisablegb); 38switch ibalp_kapurgbdegd,ibalp_kapurdisablegb; 39 40% import needed switches and global settings 41fluid '(!*rlverbose !*modular vdpsortmode!*); 42 43procedure ibalp_setkapuroption(opt,val); 44 % Set Kapur option. [opt] is an identifier. [val] is any. Returns 45 % any (old setting or nil). 46 begin scalar oldopt,oldval; 47 if oldopt := atsoc(opt,ibalp_kapuroptions!*) then << 48 oldval := cdr oldopt; 49 cdr oldopt := val 50 >> 51 else 52 ibalp_kapuroptions!* := (opt . val) . ibalp_kapuroptions!*; 53 return oldval 54 end; 55 56procedure ibalp_getkapuroption(opt); 57 % Get Kapur option. [opt] is an identifier. Returns any. 58 lto_catsoc(opt,ibalp_kapuroptions!*); 59 60procedure ibalp_initkapuroptions(); 61 % Initialise Kapur options. Returns a list. 62 << 63 ibalp_kapuroptions!* := { 64 ('torder . vdpsortmode!*), 65 ('polygenmode . 'kapur)}; % other are 'direct, 'knf, 'kapurknf 66 if !*rlkapurchktaut and !*rlkapurchkcont then 67 ibalp_setkapuroption('checkmode,'full) 68 else if !*rlkapurchktaut then 69 ibalp_setkapuroption('checkmode,'taut) 70 else if !*rlkapurchkcont then 71 ibalp_setkapuroption('checkmode,'cont) 72 else 73 ibalp_setkapuroption('checkmode,'sat) 74 >>; 75 76procedure ibalp_kapur(f,umode); 77 % Kapur algebraic interface. [f] is a formula. [checkmode] is an 78 % identifier. [umode] is an identifier. Returns a formula. 79 begin scalar oldmod,oldswitch,newf; 80 oldmod := setmod 2; 81 oldswitch := !*modular; 82 on1 'modular; 83 ibalp_initkapuroptions(); 84 ibalp_setkapuroption('polygenmode,umode); 85 if !*rlverbose then << 86 ioto_tprin2t "++++ Starting ibalp_kapur"; 87 ioto_prin2t {"Polynomial generation method: ", 88 ibalp_getkapuroption 'polygenmode}; 89 ioto_tprin2t "-------------------------" 90 >>; 91 f := cl_simpl(f,nil,-1); % fast simplify once 92 if ibalp_getkapuroption 'checkmode memq '(taut full) then << 93 if !*rlverbose then ioto_prin2t "---- Check for tautology"; 94 newf := ibalp_regformula(ibalp_kapur1(f,0),0,f) 95 >>; 96 if ibalp_getkapuroption 'checkmode memq '(cont full sat) and 97 not rl_tvalp rl_op newf then << 98 if !*rlverbose then ioto_prin2t "---- Check for contradiction"; 99 newf := ibalp_regformula(ibalp_kapur1(f,1),1,f) 100 >>; 101 setmod oldmod; 102 if null oldswitch then off1 'modular; 103 return newf 104 end; 105 106procedure ibalp_regformula(pl,trthval,origf); 107 % Regenerate formula. [pl] is a list of polynomials. [trthval] is 0 108 % or 1. [origf] is a formula. Returns a formula. 109 if eqn(trthval,0) then 110 if 1 member pl then 111 'true 112 else 113 origf 114 else 115 if 1 member pl then 116 'false 117 else if ibalp_getkapuroption 'checkmode eq 'sat then 118 'true 119 else 120 origf; 121 122procedure ibalp_kapur1(f,trthval); 123 % Kapur subprocedure 1. [f] is a formula. [trthval] is 0 if check 124 % for tautology or 1 if check for contradiction. Returns a Groebner 125 % Basis of an equivalent set of polynomials. 126 begin scalar polylist; 127 if rl_qnum f > 0 then f := cl_qe(f,nil); 128 if !*rlverbose then ioto_prin2t "--- Generate polynomials..."; 129 polylist := ibalp_polyset(f,trthval); 130 polylist := nconc(polylist,ibalp_genidemppolylist polylist); 131 if !*rlverbose then << 132 ioto_prin2t {"-- Generated ",length polylist," polynomials"}; 133 ioto_prin2t {"--- Compute Groebner Basis (",vdpsortmode!*,")..."} 134 >>; 135 polylist := ibalp_groebnereval polylist; 136 if !*rlverbose then << 137 ioto_prin2t {"-- Generated ",length polylist," polynomials"} 138 >>; 139 return polylist 140 end; 141 142procedure ibalp_polyset(f,trthval); 143 % Generate set of polynomials. [f] is a formula. [trthval] is 0 or 144 % 1. Returns a list of polynomials equivalent to [f]. 145 if ibalp_getkapuroption 'polygenmode eq 'knf then 146 ibalp_pset3knf(f,trthval) 147 else if ibalp_getkapuroption 'polygenmode eq 'direct then 148 ibalp_psetdirekt(f,trthval) 149 else if ibalp_getkapuroption 'polygenmode memq '(kapur kapurknf) then 150 ibalp_psetkapur(f,trthval) 151 else 152 ibalp_psetkapur(f,trthval); 153 154procedure ibalp_formulaform(p); 155 % Formula Form. [p] is a polynomial without exponents. Returns a 156 % formula. 157 if eqn(p,1) then 158 'true 159 else if eqn(p,0) then 160 'false 161 else if idp p then 162 ibalp_1mk2('equal,p) 163 else if eqcar(p,'times) then 164 rl_smkn('and,for each x in cdr p collect ibalp_formulaform x) 165 else if eqcar(p,'plus) then 166 rl_mk1('not,rl_mk2('equiv,ibalp_formulaform cadr p, 167 ibalp_formulaform kpoly_norm ('plus . cddr p))); 168 169procedure ibalp_polyform(f); 170 % Polynomial form. [f] is a quantifier-free formula. Returns a 171 % polynomial. 172 begin scalar a,b; 173 if rl_tvalp rl_op f then 174 return if rl_op f eq 'true then 1 else 0; 175 if ibalp_atfp f then 176 return ibalp_polyformatf f; 177 if rl_op f eq 'not then 178 return kpoly_plus {1,ibalp_polyform rl_arg1 f}; 179 if rl_junctp rl_op f then << 180 if rl_op f eq 'and then 181 return kpoly_times ibalp_polyformlist rl_argn f; 182 return kpoly_plus {1,kpoly_times for each j in 183 ibalp_polyformlist rl_argn f collect kpoly_plus {1,j}} 184 >>; 185 a := ibalp_polyform rl_arg2l f; 186 b := ibalp_polyform rl_arg2r f; 187 if rl_op f eq 'impl then 188 return kpoly_plus {1,kpoly_times {a,b},ibalp_clonestruct a}; 189 if rl_op f eq 'repl then 190 return kpoly_plus {1,kpoly_times {a,b},ibalp_clonestruct b}; 191 if rl_op f eq 'equiv then 192 return kpoly_plus {1,a,b}; 193 if rl_op f eq 'xor then 194 return kpoly_plus {a,b} 195 end; 196 197procedure ibalp_polyformatf(f); 198 % Polynomial form of an atomic formula. [f] is an atomic formula. 199 % Returns a polynomial. 200 if ibalp_op f eq 'equal then 201 if eqn(ibalp_arg2r f,1) then 202 ibalp_arg2l f 203 else 204 kpoly_plus {1,ibalp_arg2l f} 205 else % ibalp_op eq 'neq 206 if eqn(ibalp_arg2r f,0) then 207 ibalp_arg2l f 208 else 209 kpoly_plus {1,ibalp_arg2l f}; 210 211procedure ibalp_remnested(pl,op); 212 % Remove nested. [l] is a list. [op] is an identifier. Returns a 213 % list where no sublist ist starting with [op] anymore by merging 214 % into [pl] (applying the associative law). 215 for each j in pl join 216 if eqcar(j,op) then 217 ibalp_remnested(cdr j,op) 218 else 219 {j}; 220 221procedure ibalp_polyformlist(l); 222 % Polynomialform list. [l] is a list of formulae. Returns a list of 223 % polynomials. 224 for each x in l collect ibalp_polyform x; 225 226procedure ibalp_groebnereval(pl); 227 % Groebner Basis evaluation. [pl] is a list of polynomials. Returns 228 % a list of polynomials which is a Groebner Basis of [pl]. 229 if null pl then 230 {0} 231 else if !*ibalp_kapurdisablegb then 232 pl 233 else if !*ibalp_kapurgbdegd then 234 ibalp_gbdegd(pl,20) 235 else if !*ibalp_kapurgb then 236 ibalp_gb pl 237 else 238 cdr groebnereval {'list . pl}; 239 240procedure ibalp_torderp(a,b); 241 % Termorder predicate. [a] and [b] are monomials. Returns boolean. 242 if eqn(b,0) then 243 t 244 else if eqn(a,0) then 245 nil 246 else if eqn(b,1) then 247 t 248 else if eqn(a,1) then 249 nil 250 else if a = b then 251 t 252 else if ibalp_getkapuroption 'torder eq 'lex then 253 ibalp_torderlexp(a,b) 254 else if ibalp_getkapuroption 'torder eq 'gradlex then 255 ibalp_tordergradlexp(a,b) 256 else %use gradlex per default 257 ibalp_tordergradlexp(a,b); 258 259procedure ibalp_torderlexp(a,b); 260 % Termorder Lexicographic. [a] and [b] are monomials different from 261 % 0 or 1. Returns boolean. 262 if atom a and atom b then 263 ordop(a,b) 264 else if atom a and pairp b then 265 if a eq cadr b then nil else ordop(a,cadr b) 266 else if pairp a and atom b then 267 ordop(cadr a,b) 268 else if pairp a and pairp b and cdr a and cdr b then 269 if cadr a eq cadr b then 270 if cddr a and cddr b then 271 ibalp_torderp('times . cddr a,'times . cddr b) 272 else if cddr a then 273 t 274 else if cddr b then 275 nil 276 else 277 t 278 else 279 ordop(cadr a,cadr b) 280 else 281 if cdr a then t else nil; 282 283procedure ibalp_tordergradlexp(a,b); 284 % Termorder Gradlex. [a] and [b] are monomials different from 0 or 285 % 1. Returns boolean. 286 if atom a and atom b then 287 ordop(a,b) 288 else if atom a and pairp b then 289 nil 290 else if atom b and pairp a then 291 t 292 else if length a > length b then 293 t 294 else if length a < length b then 295 nil 296 else if pairp a and pairp b and cdr a and cdr b then 297 if cadr a eq cadr b then 298 if cddr a and cddr b then 299 ibalp_tordergradlexp('times . cddr a,'times . cddr b) 300 else if cddr a then 301 t 302 else if cddr b then 303 nil 304 else 305 t 306 else 307 ordop(cadr a,cadr b); 308 309procedure ibalp_gbdegd(pl,maxdeg); 310 % Degree-d Groebner Basis. [pl] is a non-empty list of polynomials. 311 % [maxdeg] is a positive integer. Returns a list of polynomials 312 % which is a Degree-[maxdeg] Groebner Basis of [pl]. 313 begin scalar glist,glistend,slist,pol,newrule,srule; 314 glist := {krule_poly2rule car pl}; 315 glistend := glist; 316 slist := cdr pl; 317 while slist do << 318 pol := car slist; 319 slist := cdr slist; 320 pol := ibalp_gbreducepoly(pol,glist); 321 if not eqn(pol,0) then << 322 newrule := krule_poly2rule pol; 323 % add new rule at the end of gb 324 cdr glistend := (newrule . nil); 325 glistend := cdr glistend; 326 % check if new overlap should be added 327 for each j in glist do << 328 srule := ibalp_gboverlaprules(j,newrule,nil); 329 if (atom car srule and not(eqn(car srule,0) or eqn(car srule,1))) 330 or (listp car srule and length cdar srule < maxdeg + 1) then 331 slist := (krule_rule2poly srule) . slist 332 >> 333 >> 334 >>; 335 return for each j in glist collect krule_rule2poly j 336 end; 337 338procedure ibalp_gb(pl); 339 % Groebner Basis. [pl] is a list of polynomials. Returns a list of 340 % polynomials which is a Groebner Basis of [pl]. 341 begin scalar allrules,newrules,newrule,newrules2; 342 if null pl then return '(0); 343 if null cdr pl then return pl; 344 allrules := ibalp_gbinitrules pl; 345 newrules := cdr allrules; 346 while newrules do << 347 if !*rlverbose then ioto_tprin2t {"- ",length newrules," new rules"}; 348 newrules2 := newrules; 349 newrules := nil; 350 for each j in newrules2 do for each k in allrules do << 351 newrule := ibalp_gboverlaprules(j,k,append(allrules,newrules)); 352 if newrule = '(1 . 0) then << 353 if !*rlverbose then ioto_tprin2t "-- 1 in GB generation"; 354 allrules := '((1 . 0)); 355 newrules := nil 356 >> else if eqn(cdr newrule,1) and eqcar(car newrule,'times) then 357 newrules := nconc(for each k in cdar newrule collect (k . 1), 358 newrules) 359 else if newrule neq '(0 . 0) then << 360 if !*rlverbose then 361 ioto_tprin2t {car newrule," -> ",cdr newrule}; 362 newrules := newrule . newrules 363 >> 364 >>; 365 if newrules then << 366 newrules := ibalp_gbsimplifyall newrules; 367 allrules := ibalp_gbsimplifyall append(allrules,newrules) 368 >> 369 >>; 370 return for each j in allrules collect krule_rule2poly j 371 end; 372 373procedure ibalp_gbsimplifyall(rules); 374 % Groebner Basis simplify all rules. [rules] is a non-empty list of 375 % rules. Returns a list of rules, where every rule is in normalform 376 % in regard to all other rules in the list. 377 begin scalar currule,beforr,afterr,newp; integer curlength,cntr; 378 if !*rlverbose then ioto_tprin2t {"-- Simplifing ",length rules," Rules"}; 379 if null cdr rules then return rules; 380 curlength := 1; 381 cntr := 0; 382 currule := rules; 383 beforr := rules; 384 afterr := cdr rules; 385 while cdr beforr do << 386 curlength := add1 curlength; 387 beforr := cdr beforr 388 >>; 389 while cntr < curlength do << 390 newp := ibalp_gbreducepoly(krule_rule2poly car currule,afterr); 391 if eqn(newp,1) then << 392 currule := {krule_poly2rule 1}; 393 cntr := curlength + 25 394 >> else if eqn(newp,0) then << 395 curlength := sub1 curlength; 396 currule := afterr; 397 afterr := cdr afterr 398 >> else << 399 cdr beforr := (krule_poly2rule newp) . nil; 400 cntr := if cadr beforr = car currule then add1 cntr else 0; 401 beforr := cdr beforr; 402 currule := afterr; 403 afterr := cdr afterr 404 >> 405 >>; 406 return currule 407 end; 408 409procedure ibalp_gboverlaprules(r1,r2,rlist); 410 % Groebner Basis overlap rules. [r1] and [r2] are rules. [rlist] is 411 % a list of rules. Returns a rule which is the result of [r1] and 412 % [r2] beeing overlapped and the S-Polynomial is reduced using 413 % [rlist]. 414 begin scalar spoly,head1,tail1,head2,tail2; 415 if ibalp_gboverlapruleszcritp(r1,r2) then return krule_poly2rule 0; 416 head1 := krule_head r1; 417 head2 := krule_head r2; 418 tail1 := krule_tail r1; 419 tail2 := krule_tail r2; 420 spoly := 421 if head1 = head2 then 422 kpoly_plus {tail1,tail2} 423 else if atom head1 and pairp head2 and head1 memq cdr head2 then 424 kpoly_plus {tail2,kpoly_times {tail1,delete(head1,head2)}} 425 else if atom head2 and pairp head1 and head2 memq cdr head1 then 426 kpoly_plus {tail1,kpoly_times {tail2,delete(head2,head1)}} 427 else << 428 spoly := kpoly_times union(cdr head1,cdr head2); % lcm 429 kpoly_plus {ibalp_gbapplyrule(spoly,r1),ibalp_gbapplyrule(spoly,r2)} 430 >>; 431 return krule_poly2rule ibalp_gbreducepoly(spoly,rlist) 432 end; 433 434procedure ibalp_gboverlapruleszcritp(r1,r2); 435 % Groebner Basis overlap rules zero criteria Predicate. [r1] and 436 % [r2] are rules. Returns non-nil if the S-Polynomial of [r1] and 437 % [r2] can be reduced to 0 easily. 438 (r1 = r2) or 439 (atom car r1 and atom car r2 and not(eqcar(r1,car r2))) or 440 (eqn(cdr r1,0) and eqn(cdr r2,0)) or 441 (atom car r1 and pairp car r2 and not(car r1 memq cdar r2)) or 442 (atom car r2 and pairp car r1 and not(car r2 memq cdar r1)) or 443 (pairp car r1 and pairp car r2 and null intersection(cdar r1,cdar r2)); 444 445procedure ibalp_gbreducepoly(p,rules); 446 % Groebner Basis reduce polynomial. [p] is a polynomial. [rules] is 447 % a list of rules. Returns a polynomial which is in normalform 448 % according to the [rules]. 449 begin scalar chnge,p1,p2; 450 chnge := t; 451 p1 := p; 452 p2 := p; 453 while chnge do << 454 chnge := nil; 455 for each j in rules do p1 := ibalp_gbapplyrule(p1,j); 456 if p1 neq p2 then << 457 chnge := t; 458 p2 := p1 459 >> 460 >>; 461 return p1 462 end; 463 464procedure ibalp_gbapplyrule(p,rule); 465 % Groebner Basis apply rule. [p] is a polynomial. [rule] is a rule. 466 % Returns a polynomial. 467 begin scalar w; 468 if rule = krule_poly2rule 1 then return 0; 469 if kpoly_monomialp p then return ibalp_gbapplyrulem(p,rule); 470 w := cdr p; 471 while w do 472 if ibalp_torderp(car w,krule_head rule) then << 473 car w := ibalp_gbapplyrulem(car w,rule); 474 w := cdr w 475 >> 476 else 477 w := nil; 478 return kpoly_plus cdr p 479 end; 480 481procedure ibalp_gbapplyrulem(m,rule); 482 % Groebner Basis apply rule monomial. [m] is a monomial. [rule] is 483 % a rule. Returns a polynomial. 484 if rule = krule_poly2rule 1 then 485 0 486 else if atom m then 487 if eqcar(rule,m) then krule_tail rule else m 488 else if atom krule_head rule then 489 if krule_head rule memq m then 490 kpoly_times {lto_delq(krule_head rule,m),krule_tail rule} 491 else 492 m 493 else if kpoly_mondivp(m,krule_head rule) then << 494 for each j in cdr krule_head rule do m := lto_delq(j,m); 495 kpoly_times {m,krule_tail rule} 496 >> else 497 m; 498 499procedure ibalp_gbinitrules(pl); 500 % Groebner Basis init ruleslist. [pl] is a non-empty list of 501 % polynomials. Returns a list of rules, generated by the 502 % polynomials in [pl]. 503 begin scalar rules,newp; 504 rules := {krule_poly2rule car pl}; 505 pl := cdr pl; 506 while pl do << 507 newp := ibalp_gbreducepoly(car pl,rules); 508 pl := cdr pl; 509 if eqn(newp,1) then << 510 if !*rlverbose then ioto_tprin2t "-- 1 in Ideal Initialisation"; 511 rules := {krule_poly2rule 1}; 512 pl := nil 513 >> 514 else if not eqn(newp,0) then 515 rules := (krule_poly2rule newp) . rules 516 >>; 517 rules := ibalp_gbsimplifyall rules; 518 return rules 519 end; 520 521procedure ibalp_genpolyform(f,trthval); 522 % Generate polynomial form. [f] is a quantifier free formula. 523 % [trthval] is 0 or 1. Returns a polynomial without exponents. 524 if eqn(trthval,1) then 525 kpoly_plus {1,ibalp_polyform f} 526 else 527 ibalp_polyform f; 528 529procedure ibalp_genidemppolylist(l); 530 % Generate idempotential polynomial list. [l] is a list of 531 % polynomials. Returns a list of polynomials containing the 532 % idempotential polynomials for each variable in [l]. 533 begin scalar vl; 534 for each j in l do 535 if idp j then 536 vl := lto_insert(j,vl) 537 else if eqcar(j,'times) then 538 for each k in cdr j do vl := lto_insert(k,vl) 539 else if eqcar(j,'plus) then 540 for each k in cdr j do 541 if idp k then 542 vl := lto_insert(k,vl) 543 else if eqcar(k,'times) then 544 for each m in cdr k do 545 vl := lto_insert(m,vl); 546 return for each j in vl collect kpoly_idemppoly j; 547 end; 548 549% umode 3KNF 550 551procedure ibalp_pset3knf(f,trthval); 552 % Generate set of polynomials 3KNF. [f] is a formula. [trthval] is 553 % 0 or 1. Returns a list of polynomials by transforming [f] into a 554 % into a conjunctive clausal form, containing max 3 variables per 555 % clause. 556 begin scalar newf; 557 newf := if eqn(trthval,1) then f else rl_mk1('not,f); 558 newf := ibalp_pset3knfnf newf; 559 newf := ibalp_pset3knf2(newf,nil); 560 newf := if rl_op newf eq 'and then 561 rl_mkn('and,for each j in rl_argn newf join 562 ibalp_pset3knf3(j,nil)) 563 else 564 rl_smkn('and,ibalp_pset3knf3(newf,nil)); 565 return 566 if rl_op newf eq 'and then 567 for each j in rl_argn newf collect ibalp_genpolyform(j,1) 568 else 569 {ibalp_genpolyform(newf,1)} 570 end; 571 572procedure ibalp_pset3knfnf(f); 573 % Generate set of polynomials 3KNF negated form. [f] is a formula. 574 % Returns a formula in negated form 575 if rl_tvalp rl_op f or ibalp_atfp f then 576 f 577 else if rl_op f eq 'not then 578 if ibalp_atfp rl_arg1 f then 579 f 580 else 581 ibalp_pset3knfnf1 rl_arg1 f 582 else if rl_junctp rl_op f then 583 rl_mkn(rl_op f, for each j in rl_argn f collect 584 ibalp_pset3knfnf j) 585 else if rl_op f eq 'impl then 586 rl_mk2('or,ibalp_pset3knf1 rl_mk1('not,rl_arg2l f), 587 ibalp_pset3knfnf rl_arg2r f) 588 else if rl_op f eq 'repl then 589 rl_mk2('or,ibalp_pset3knfnf rl_mk1('not,rl_arg2r f), 590 ibalp_pset3knfnf rl_arg2l f) 591 else 592 rl_mk2(rl_op f, ibalp_pset3knfnf rl_arg2l f, 593 ibalp_pset3knfnf rl_arg2r f); 594 595procedure ibalp_pset3knfnf1(f); 596 % Generate set of polynomials 3KNF negated form subprocedure 1. [f] 597 % is a formula, but not an atomic formula. Returns a formula in 598 % negated form assuming the operator before [f] was a 'not. 599 if rl_tvalp rl_op f then 600 cl_flip rl_op f 601 else if rl_op f eq 'not then 602 ibalp_pset3knfnf rl_arg1 f 603 else if rl_junctp rl_op f then 604 rl_mkn(cl_flip rl_op f, 605 for each j in rl_argn f collect ibalp_pset3knfnf rl_mk1('not,j)) 606 else if rl_op f eq 'impl then 607 rl_mk2('and,ibalp_pset3knfnf rl_arg2l f,ibalp_pset3knfnf 608 rl_mk1('not,rl_arg2r f)) 609 else if rl_op f eq 'repl then 610 rl_mk2('and,ibalp_pset3knfnf rl_mk1('not,rl_arg2l f), 611 ibalp_pset3knfnf rl_arg2r f) 612 else if rl_op f eq 'equiv then 613 rl_mk2('equiv,ibalp_pset3knfnf rl_mk1('not,rl_arg2l f), 614 ibalp_pset3knfnf rl_arg2r f) 615 else if rl_op f eq 'xor then 616 rl_mk2('equiv,ibalp_pset3knfnf rl_arg2l f,ibalp_pset3knfnf rl_arg2r f); 617 618procedure ibalp_pset3knf2(f,intree); 619 % Generate set of polynomials 3KNF subprocedure 2. [f] is a formula 620 % in negated form. [intree] is boolean. Returns a formula where 621 % only the top-level operator 'and is n-ary. 622 begin scalar partlists,g; 623 if rl_tvalp rl_op f or rl_op f eq 'not or ibalp_atfp f then 624 return f; 625 if null intree and rl_op f eq 'and then 626 return rl_smkn('and, for each j in rl_argn f join << 627 g := ibalp_pset3knf2(j,nil); 628 if rl_op g eq 'and then rl_argn g else {g} 629 >>); 630 if rl_junctp rl_op f and lto_lengthp(rl_argn f,3,'geq) then << 631 if lto_lengthp(rl_argn f,4,'geq) then << 632 partlists := ibalp_splitlist rl_argn f; 633 return rl_mk2(rl_op f, 634 ibalp_pset3knf2(rl_mkn(rl_op f,car partlists),t), 635 ibalp_pset3knf2(rl_mkn(rl_op f,cdr partlists),t)) 636 >>; 637 return rl_mk2(rl_op f,ibalp_pset3knf2(car rl_argn f,t), 638 rl_mk2(rl_op f,ibalp_pset3knf2(cadr rl_argn f,t), 639 ibalp_pset3knf2(caddr rl_argn f, t))) 640 >>; 641 return rl_mk2(rl_op f,ibalp_pset3knf2(rl_arg2l f,t), 642 ibalp_pset3knf2(rl_arg2r f,t)); 643 end; 644 645procedure ibalp_pset3knf3(f,clausevar); 646 % Generate set of polynomials 3KNF subprocedure 3. [f] is a formula 647 % in binary tree negated form. [clausevar] is an identifier or nil. 648 % Returns a list of formulae with max three vars in each clause. 649 begin scalar nvarl,nvarr,returnlist; 650 if rl_tvalp rl_op f then 651 return {f}; 652 if rl_op f eq 'not or ibalp_atfp f then 653 return {f}; 654 if null clausevar then << 655 clausevar := ibalp_1mk2('equal,gensym()); 656 returnlist := clausevar . returnlist 657 >>; 658 if rl_op rl_arg2l f eq 'not or ibalp_atfp rl_arg2l f then 659 nvarl := rl_arg2l f 660 else << 661 nvarl := ibalp_1mk2('equal,gensym()); 662 returnlist := nconc(returnlist,ibalp_pset3knf3(rl_arg2l f,nvarl)) 663 >>; 664 if rl_op rl_arg2r f eq 'not or ibalp_atfp rl_arg2r f then 665 nvarr := rl_arg2r f 666 else << 667 nvarr := ibalp_1mk2('equal,gensym()); 668 returnlist := nconc(returnlist,ibalp_pset3knf3(rl_arg2r f,nvarr)) 669 >>; 670 return rl_mk2('equiv,clausevar,rl_mk2(rl_op f,nvarl,nvarr)) . returnlist; 671 end; 672 673% umode Kapur 674 675procedure ibalp_psetkapur(f,trthval); 676 % Generate set of polynomials Kapur. [f] is a formula. [trthval] is 677 % 0 or 1. Returns a list of polynomials by transforming [f] using 678 % Kapur and Narendrans optimized Method. [trthval] is the trthvalue 679 % which should be achieved. 680 if rl_op f eq 'not then 681 ibalp_psetkapur(rl_arg1 f,ibalp_flip01 trthval) 682 else if eqn(trthval,1) then 683 ibalp_psetkapurcont f 684 else 685 ibalp_psetkapurtaut f; 686 687procedure ibalp_psetkapurtaut(f); 688 % Generate set of polynomials Kapur tautology. [f] is a formula. 689 % Returns a list of polynomials. 690 if rl_op f eq 'impl then 691 nconc(ibalp_psetkapur(rl_arg2l f,1),ibalp_psetkapur(rl_arg2r f,0)) 692 else if rl_op f eq 'repl then 693 nconc(ibalp_psetkapur(rl_arg2l f,0),ibalp_psetkapur(rl_arg2r f,1)) 694 else if rl_op f eq 'or then 695 for each j in rl_argn f join ibalp_psetkapur(j,0) 696 else if rl_op f eq 'and then 697 ibalp_psetkapurnary(f,0) 698 else 699 ibalp_psetkapurnoopt(f,0); 700 701procedure ibalp_psetkapurcont(f); 702 % Generate set of polynomials Kapur contradiction. [f] is a formula. 703 % Returns a list of polynomials. 704 if rl_op f eq 'and then 705 for each j in rl_argn f join ibalp_psetkapur(j,1) 706 else if rl_op f eq 'impl and rl_op rl_arg2r f eq 'and then 707 ibalp_psetkapurdistleft(f,1) 708 else if rl_op f eq 'repl and rl_op rl_arg2l f eq 'and then 709 ibalp_psetkapurdistright(f,1) 710 else if rl_op f eq 'or then 711 ibalp_psetkapurnary(f,1) 712 else 713 ibalp_psetkapurnoopt(f,1); 714 715procedure ibalp_psetkapurnary(f,trthval); 716 % Generate set of polynomials Kapur n-Ary subprocedure 1. [f] is a 717 % formula with an n-ary toplevel operator. [trthval] is 0 or 1. 718 % Returns a list of polynomials by spliting a n-ary boolean 719 % formulae into two equivalent polynomials adding auxiliary vars. 720 begin scalar distop; 721 distop := cl_flip rl_op f; 722 if lto_lengthp(rl_argn f,4,'geq) then 723 return ibalp_psetkapurnary1(f,trthval); 724 if lto_lengthp(rl_argn f,2,'eqn) then 725 return 726 if rl_op rl_arg2r f eq distop then 727 ibalp_psetkapurdistleft(f,trthval) 728 else if rl_op rl_arg2l f eq distop then 729 ibalp_psetkapurdistright(f,trthval) 730 else 731 ibalp_psetkapurnoopt(f,trthval); 732 return ibalp_psetkapurnoopt(f,trthval) 733 end; 734 735procedure ibalp_psetkapurnary1(f,trthval); 736 % Generate set of polynomials Kapur n-Ary subprocedure 1. [f] is a 737 % formula with an n-ary toplevel operator. [trthval] is 0 or 1. 738 % Returns a list of polynomials by spliting a n-ary boolean 739 % formulae into two equivalent polynomials adding auxiliary vars. 740 begin scalar partlists,newvar,l1,l2; 741 partlists := ibalp_splitlist rl_argn f; 742 l1 := car partlists; 743 l2 := cdr partlists; 744 newvar := gensym(); 745 l1 := rl_mkn(rl_op f,ibalp_1mk2('equal,newvar) . l1); 746 l2 := rl_mkn(rl_op f,rl_mk1('not,ibalp_1mk2('equal,newvar)) . l2); 747 return nconc(ibalp_psetkapur(l1,trthval),ibalp_psetkapur(l2,trthval)) 748 end; 749 750procedure ibalp_psetkapurnoopt(f,trthval); 751 % Generate set of polynomials Kapur without possible optimizations. 752 % [f] is a formula. [trthval] is 0 or 1. Returns a list of 753 % polynomials. 754 begin scalar p; 755 if ibalp_getkapuroption 'polygenmode eq 'kapurknf then 756 return ibalp_pset3knf(f,trthval); 757 p := ibalp_genpolyform(f,trthval); 758 return if not eqn(p,0) then {p} 759 end; 760 761procedure ibalp_psetkapurdistleft(f,trthval); 762 % Generate set of polynomials Kapur left distributivity. [f] is a 763 % formula. [trthval] is 0 or 1. Returns a list of polynomials by 764 % applying the distributivity rule first. 765 for each j in rl_argn rl_arg2r f join 766 ibalp_psetkapur(rl_mk2(rl_op f,rl_arg2l f,j),trthval); 767 768procedure ibalp_psetkapurdistright(f,trthval); 769 % Generate set of polynomials Kapur right distributivity. [f] is a 770 % formula. [trthval] is 0 or 1. Returns a list of polynomials by 771 % applying the distributivity rule first. 772 for each j in rl_argn rl_arg2l f join 773 ibalp_psetkapur(rl_mk2(rl_op f,rl_arg2r f,j),trthval); 774 775procedure ibalp_psetdirekt(f, trthval); 776 % Generate set of polynomials directly. [f] is a formula. [trthval] 777 % is 0 or 1. Returns a list of polynomials. 778 {ibalp_genpolyform(f,trthval)}; 779 780procedure ibalp_splitlist(l); 781 % Split list. [l] is a list. Returns a pair of lists. Devides a 782 % list into two lists of equal length containing all elements of 783 % [l]. 784 begin scalar elm,l2; integer lgt,cnt; 785 if null l then 786 return (nil . nil); 787 if null cdr l then 788 return (l . nil); 789 lgt := length l; 790 cnt := 1; 791 elm := l; 792 while cnt < lgt / 2 do << 793 cnt := add1 cnt; 794 elm := cdr elm 795 >>; 796 l2 := cdr elm; 797 cdr elm := nil; 798 return (l . l2); 799 end; 800 801procedure ibalp_clonestruct(s); 802 % Clone structure. [s] is any. Returns any, which is a clone of [s] 803 % in a constructive way. 804 if atom s then s else (ibalp_clonestruct car s) . (ibalp_clonestruct cdr s); 805 806endmodule; %ibalpkapur 807 808module krule; 809% Kapur Rewriterules 810 811% DS 812% <RULE> ::= (<MONOMIAL> . <POLY>) 813 814procedure krule_head(r); 815 % Headmonomial. [r] is a rule. Returns the head of the rule. 816 car r; 817 818procedure krule_tail(r); 819 % Tailpolynomial. [r] is a rule. Returns the tail of the rule. 820 cdr r; 821 822procedure krule_genrule(h,tt); 823 % Generate rule. [h] is a monomial, [t] is a polynomial. Returns a 824 % rule with [h] as head and [t] as tail. 825 (h . tt); 826 827procedure krule_rule2poly(r); 828 % Convert rule into a polynomial. [r] is a rule. Returns a 829 % polynomial. 830 kpoly_plus {krule_head r,krule_tail r}; 831 832procedure krule_poly2rule(p); 833 % Convert a polynomial into a rule. [p] is a polynomial. Returns a 834 % rule or 'failed if no unique head monomial can be choosen. 835 begin scalar monlist; 836 if kpoly_monomialp p then return (p . 0); 837 monlist := sort(cdr p,'ibalp_torderp); 838 return krule_genrule(car monlist,kpoly_plus cdr monlist) 839 end; 840 841endmodule; %[krule] 842 843 844module kpoly; 845% Kapur Polynomials 846 847% DS 848% <POLY> ::= <MONOMIAL> | ('plus,...,<MONOMIAL>,...) 849% <MONOMIAL> ::= 0 | 1 | <ID> | ('times,...,<ID>,...) 850 851procedure kpoly_times(l); 852 % Polynomial times. [l] is a non-empty list of polynomials. Returns 853 % the product of the polynomials in [l]. 854 begin scalar setlvar,setlsum,curpoly; 855 l := ibalp_remnested(l,'times); 856 if 0 member l then return 0; 857 for each j in l do 858 if atom j and not eqn(j,1) then 859 setlvar := lto_insert(j,setlvar) 860 else if eqcar(j,'plus) then 861 setlsum := lto_insert(j,setlsum); 862 setlvar := sort(setlvar,'ordop); 863 if null setlsum then 864 return kpoly_norm ('times . setlvar); 865 if null setlvar and null cdr setlsum then 866 return car setlsum; 867 if setlvar then 868 curpoly := kpoly_norm ('times . setlvar) 869 else << 870 curpoly := car setlsum; 871 setlsum := cdr setlsum 872 >>; 873 while setlsum do << 874 curpoly := kpoly_times2(curpoly,car setlsum); 875 setlsum := if not eqn(curpoly,0) then cdr setlsum 876 >>; 877 return curpoly 878 end; 879 880procedure kpoly_times2(p1,p2); 881 % Polynomial times 2. [p1] and [p2] are polynomials. Returns a 882 % polynomial which is the product of [p1] and [p2]. 883 if kpoly_monomialp p1 and kpoly_monomialp p2 then 884 kpoly_times2monoms(p1,p2) 885 else if kpoly_monomialp p1 then 886 kpoly_times2monomsum(p1,p2) 887 else if kpoly_monomialp p2 then 888 kpoly_times2monomsum(p2,p1) 889 else 890 kpoly_times2sums(p1,p2); 891 892procedure kpoly_times2sums(s1,s2); 893 % Polynomial times 2 sums. [s1] and [s2] are lists starting with 894 % 'plus. Returns a polynomial being the multiplication of [s1] and 895 % [s2]. 896 kpoly_plus for each j in cdr s1 collect 897 kpoly_times2monomsum(j,s2); 898 899procedure kpoly_times2monomsum(m,s); 900 % Polynomial times2 monomial and sum. [m] is a monomial. [s] is a 901 % list starting with 'plus. Returns a polynomial which is the 902 % product of [m] and [s]. 903 if kpoly_monomialp s then 904 kpoly_times2monoms(m,s) 905 else 906 kpoly_plus for each j in cdr s collect 907 kpoly_times2monoms(m,j); 908 909procedure kpoly_times2monoms(m1,m2); 910 % Polynomial times 2 monomials. [m1] and [m2] are monomials. 911 % Returns a monomial containing all identifiers of [s1] and [s2]. 912 % The result list is sorted lexicographically. 913 begin scalar setl; 914 if atom m1 then 915 if eqn(m1,1) then 916 return m2 917 else 918 setl := lto_insert(m1,setl) 919 else 920 for each j in cdr m1 do setl := lto_insert(j,setl); 921 if atom m2 then 922 if eqn(m2,1) then 923 return m1 924 else 925 setl := lto_insert(m2,setl) 926 else 927 for each j in cdr m2 do setl := lto_insert(j,setl); 928 return kpoly_norm ('times . sort(setl,'ordop)) 929 end; 930 931procedure kpoly_plus(l); 932 % Polynomial plus. [l] is a non-empty list of polynomials. Returns 933 % a polynomial equated the addition of the polynomials in [l]. The 934 % result is sorted using current torder. 935 begin scalar tmpl,w; 936 tmpl := sort(ibalp_remnested(l,'plus),'ibalp_torderp); 937 w := tmpl; 938 % remove multiple occurences 939 while w and cdr w do 940 if eqn(car w,0) then << 941 car w := cadr w; 942 cdr w := cddr w 943 >> else if car w = cadr w then 944 if cddr w then << 945 car w := caddr w; 946 cdr w := cdddr w 947 >> else << 948 car w := 0; 949 cdr w := nil 950 >> 951 else 952 w := cdr w; 953 tmpl := delete(0,tmpl); 954 return kpoly_norm ('plus . tmpl) 955 end; 956 957procedure kpoly_monomialp(p); 958 % Monomial predicate. [p] is a polynomial. Returns non-nil if [p] 959 % is an atom or a list starting with 'times. 960 atom p or eqcar(p,'times); 961 962procedure kpoly_idemppoly(var); 963 % Idempotential polynomial. [var] is an identifier. Returns the 964 % polynomial var^2 + var. 965 {'plus,{'times,var,var},var}; 966 967procedure kpoly_norm(p); 968 % Normalise. [p] is a polynomial. Returns a polynomial which 969 % is in a normalized form (no list if atom). 970 if atom p then 971 p 972 else if null cdr p then 973 if eqcar(p,'times) then 1 else 0 974 else if null cddr p then 975 cadr p 976 else 977 p; 978 979procedure kpoly_mondivp(m1,m2); 980 % Monomial divide predicate. Returns non-nil if [m2] divides [m1]. 981 begin scalar e1,e2,rsl; 982 if eqn(m1,0) or eqn(m2,1) or m1 = m2 then return t; 983 if eqn(m2,0) then return nil; 984 if atom m1 and atom m2 then return m1 = m2; 985 if atom m1 then return nil; 986 if atom m2 then return m2 member m1; 987 e1 := cdr m1; 988 e2 := cdr m2; 989 rsl := t; 990 while e1 and e2 and rsl do 991 if car e1 = car e2 then << 992 e1 := cdr e1; 993 e2 := cdr e2 994 >> 995 else if ordop(car e1,car e2) then 996 e1 := cdr e1 997 else 998 rsl := nil; 999 return null e2 and rsl 1000 end; 1001 1002endmodule; %kpoly 1003 1004end; % of file 1005