169 val rat0 = rat_of_int 0; |
169 val rat0 = rat_of_int 0; |
170 |
170 |
171 (* PRE: ex[v] must be 0! *) |
171 (* PRE: ex[v] must be 0! *) |
172 fun eval (ex:rat list) v (a:int,le,cs:int list) = |
172 fun eval (ex:rat list) v (a:int,le,cs:int list) = |
173 let val rs = map rat_of_int cs |
173 let val rs = map rat_of_int cs |
174 val rsum = foldl ratadd (rat0,map ratmul (rs ~~ ex)) |
174 val rsum = Library.foldl ratadd (rat0,map ratmul (rs ~~ ex)) |
175 in (ratmul(ratadd(rat_of_int a,ratneg rsum), ratinv(el v rs)), le) end; |
175 in (ratmul(ratadd(rat_of_int a,ratneg rsum), ratinv(el v rs)), le) end; |
176 (* If el v rs < 0, le should be negated. |
176 (* If el v rs < 0, le should be negated. |
177 Instead this swap is taken into account in ratrelmin2. |
177 Instead this swap is taken into account in ratrelmin2. |
178 *) |
178 *) |
179 |
179 |
215 in if ratle(lb',ub) then lb' else raise NoEx end |
215 in if ratle(lb',ub) then lb' else raise NoEx end |
216 else let val ub' = ratrounddown ub |
216 else let val ub' = ratrounddown ub |
217 in if ratle(lb,ub') then ub' else raise NoEx end; |
217 in if ratle(lb,ub') then ub' else raise NoEx end; |
218 |
218 |
219 fun findex1 discr (ex,(v,lineqs)) = |
219 fun findex1 discr (ex,(v,lineqs)) = |
220 let val nz = filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs; |
220 let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs; |
221 val ineqs = foldl elim_eqns ([],nz) |
221 val ineqs = Library.foldl elim_eqns ([],nz) |
222 val (ge,le) = partition (fn (_,_,cs) => el v cs > 0) ineqs |
222 val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs |
223 val lb = ratrelmax(map (eval ex v) ge) |
223 val lb = ratrelmax(map (eval ex v) ge) |
224 val ub = ratrelmin(map (eval ex v) le) |
224 val ub = ratrelmin(map (eval ex v) le) |
225 in nth_update (choose2 (nth_elem(v,discr)) (lb,ub)) (v,ex) end; |
225 in nth_update (choose2 (List.nth(discr,v)) (lb,ub)) (v,ex) end; |
226 |
226 |
227 fun findex discr = foldl (findex1 discr); |
227 fun findex discr = Library.foldl (findex1 discr); |
228 |
228 |
229 fun elim1 v x = |
229 fun elim1 v x = |
230 map (fn (a,le,bs) => (ratadd(a,ratneg(ratmul(el v bs,x))), le, |
230 map (fn (a,le,bs) => (ratadd(a,ratneg(ratmul(el v bs,x))), le, |
231 nth_update rat0 (v,bs))); |
231 nth_update rat0 (v,bs))); |
232 |
232 |
237 fun pick_vars discr (ineqs,ex) = |
237 fun pick_vars discr (ineqs,ex) = |
238 let val nz = filter_out (fn (_,_,cs) => forall (equal rat0) cs) ineqs |
238 let val nz = filter_out (fn (_,_,cs) => forall (equal rat0) cs) ineqs |
239 in case nz of [] => ex |
239 in case nz of [] => ex |
240 | (_,_,cs) :: _ => |
240 | (_,_,cs) :: _ => |
241 let val v = find_index (not o equal rat0) cs |
241 let val v = find_index (not o equal rat0) cs |
242 val d = nth_elem(v,discr) |
242 val d = List.nth(discr,v) |
243 val pos = ratge0(el v cs) |
243 val pos = ratge0(el v cs) |
244 val sv = filter (single_var v) nz |
244 val sv = List.filter (single_var v) nz |
245 val minmax = |
245 val minmax = |
246 if pos then if d then ratroundup o fst o ratrelmax |
246 if pos then if d then ratroundup o fst o ratrelmax |
247 else ratexact true o ratrelmax |
247 else ratexact true o ratrelmax |
248 else if d then ratrounddown o fst o ratrelmin |
248 else if d then ratrounddown o fst o ratrelmin |
249 else ratexact false o ratrelmin |
249 else ratexact false o ratrelmin |
253 val ex' = nth_update x (v,ex) |
253 val ex' = nth_update x (v,ex) |
254 in pick_vars discr (ineqs',ex') end |
254 in pick_vars discr (ineqs',ex') end |
255 end; |
255 end; |
256 |
256 |
257 fun findex0 discr n lineqs = |
257 fun findex0 discr n lineqs = |
258 let val ineqs = foldl elim_eqns ([],lineqs) |
258 let val ineqs = Library.foldl elim_eqns ([],lineqs) |
259 val rineqs = map (fn (a,le,cs) => (rat_of_int a, le, map rat_of_int cs)) |
259 val rineqs = map (fn (a,le,cs) => (rat_of_int a, le, map rat_of_int cs)) |
260 ineqs |
260 ineqs |
261 in pick_vars discr (rineqs,replicate n rat0) end; |
261 in pick_vars discr (rineqs,replicate n rat0) end; |
262 |
262 |
263 (* ------------------------------------------------------------------------- *) |
263 (* ------------------------------------------------------------------------- *) |
335 (* (3) Otherwise, chooses a variable in the inequality to minimize the *) |
335 (* (3) Otherwise, chooses a variable in the inequality to minimize the *) |
336 (* blowup (number of consequences generated) and eliminates it. *) |
336 (* blowup (number of consequences generated) and eliminates it. *) |
337 (* ------------------------------------------------------------------------- *) |
337 (* ------------------------------------------------------------------------- *) |
338 |
338 |
339 fun allpairs f xs ys = |
339 fun allpairs f xs ys = |
340 flat(map (fn x => map (fn y => f x y) ys) xs); |
340 List.concat(map (fn x => map (fn y => f x y) ys) xs); |
341 |
341 |
342 fun extract_first p = |
342 fun extract_first p = |
343 let fun extract xs (y::ys) = if p y then (SOME y,xs@ys) |
343 let fun extract xs (y::ys) = if p y then (SOME y,xs@ys) |
344 else extract (y::xs) ys |
344 else extract (y::xs) ys |
345 | extract xs [] = (NONE,xs) |
345 | extract xs [] = (NONE,xs) |
356 type history = (int * lineq list) list; |
356 type history = (int * lineq list) list; |
357 datatype result = Success of injust | Failure of history; |
357 datatype result = Success of injust | Failure of history; |
358 |
358 |
359 fun elim(ineqs,hist) = |
359 fun elim(ineqs,hist) = |
360 let val dummy = print_ineqs ineqs; |
360 let val dummy = print_ineqs ineqs; |
361 val (triv,nontriv) = partition is_trivial ineqs in |
361 val (triv,nontriv) = List.partition is_trivial ineqs in |
362 if not(null triv) |
362 if not(null triv) |
363 then case Library.find_first is_answer triv of |
363 then case Library.find_first is_answer triv of |
364 NONE => elim(nontriv,hist) |
364 NONE => elim(nontriv,hist) |
365 | SOME(Lineq(_,_,_,j)) => Success j |
365 | SOME(Lineq(_,_,_,j)) => Success j |
366 else |
366 else |
367 if null nontriv then Failure(hist) |
367 if null nontriv then Failure(hist) |
368 else |
368 else |
369 let val (eqs,noneqs) = partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
369 let val (eqs,noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
370 if not(null eqs) then |
370 if not(null eqs) then |
371 let val clist = foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) |
371 let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) |
372 val sclist = sort (fn (x,y) => int_ord(abs(x),abs(y))) |
372 val sclist = sort (fn (x,y) => int_ord(abs(x),abs(y))) |
373 (filter (fn i => i<>0) clist) |
373 (List.filter (fn i => i<>0) clist) |
374 val c = hd sclist |
374 val c = hd sclist |
375 val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = |
375 val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) = |
376 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
376 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
377 val v = find_index_eq c ceq |
377 val v = find_index_eq c ceq |
378 val (ioth,roth) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) |
378 val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0) |
379 (othereqs @ noneqs) |
379 (othereqs @ noneqs) |
380 val others = map (elim_var v eq) roth @ ioth |
380 val others = map (elim_var v eq) roth @ ioth |
381 in elim(others,(v,nontriv)::hist) end |
381 in elim(others,(v,nontriv)::hist) end |
382 else |
382 else |
383 let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
383 let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
384 val numlist = 0 upto (length(hd lists) - 1) |
384 val numlist = 0 upto (length(hd lists) - 1) |
385 val coeffs = map (fn i => map (el i) lists) numlist |
385 val coeffs = map (fn i => map (el i) lists) numlist |
386 val blows = map calc_blowup coeffs |
386 val blows = map calc_blowup coeffs |
387 val iblows = blows ~~ numlist |
387 val iblows = blows ~~ numlist |
388 val nziblows = filter (fn (i,_) => i<>0) iblows |
388 val nziblows = List.filter (fn (i,_) => i<>0) iblows |
389 in if null nziblows then Failure((~1,nontriv)::hist) |
389 in if null nziblows then Failure((~1,nontriv)::hist) |
390 else |
390 else |
391 let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
391 let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
392 val (no,yes) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) ineqs |
392 val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0) ineqs |
393 val (pos,neg) = partition(fn (Lineq(_,_,l,_)) => el v l > 0) yes |
393 val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => el v l > 0) yes |
394 in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end |
394 in elim(no @ allpairs (elim_var v) pos neg, (v,nontriv)::hist) end |
395 end |
395 end |
396 end |
396 end |
397 end; |
397 end; |
398 |
398 |
418 local |
418 local |
419 exception FalseE of thm |
419 exception FalseE of thm |
420 in |
420 in |
421 fun mkthm sg asms just = |
421 fun mkthm sg asms just = |
422 let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} = Data.get_sg sg; |
422 let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} = Data.get_sg sg; |
423 val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => |
423 val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) => |
424 map fst lhs union (map fst rhs union ats)) |
424 map fst lhs union (map fst rhs union ats)) |
425 ([], mapfilter (fn thm => if Thm.no_prems thm |
425 ([], List.mapPartial (fn thm => if Thm.no_prems thm |
426 then LA_Data.decomp sg (concl_of thm) |
426 then LA_Data.decomp sg (concl_of thm) |
427 else NONE) asms) |
427 else NONE) asms) |
428 |
428 |
429 fun add2 thm1 thm2 = |
429 fun add2 thm1 thm2 = |
430 let val conj = thm1 RS (thm2 RS LA_Logic.conjI) |
430 let val conj = thm1 RS (thm2 RS LA_Logic.conjI) |
466 |
466 |
467 fun simp thm = |
467 fun simp thm = |
468 let val thm' = trace_thm "Simplified:" (full_simplify simpset thm) |
468 let val thm' = trace_thm "Simplified:" (full_simplify simpset thm) |
469 in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end |
469 in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end |
470 |
470 |
471 fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms)) |
471 fun mk(Asm i) = trace_thm "Asm" (List.nth(asms,i)) |
472 | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) |
472 | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (List.nth(atoms,i))) |
473 | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD)) |
473 | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD)) |
474 | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
474 | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
475 | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD)) |
475 | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD)) |
476 | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
476 | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
477 | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) |
477 | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) |
494 end |
494 end |
495 end; |
495 end; |
496 |
496 |
497 fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i; |
497 fun coeff poly atom = case assoc(poly,atom) of NONE => 0 | SOME i => i; |
498 |
498 |
499 fun lcms is = foldl lcm (1,is); |
499 fun lcms is = Library.foldl lcm (1,is); |
500 |
500 |
501 fun integ(rlhs,r,rel,rrhs,s,d) = |
501 fun integ(rlhs,r,rel,rrhs,s,d) = |
502 let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s |
502 let val (rn,rd) = rep_rat r and (sn,sd) = rep_rat s |
503 val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)) |
503 val m = lcms(map (abs o snd o rep_rat) (r :: s :: map snd rlhs @ map snd rrhs)) |
504 fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end |
504 fun mult(t,r) = let val (i,j) = rep_rat r in (t,i * (m div j)) end |
591 (map fst lhs) union ((map fst rhs) union ats) |
591 (map fst lhs) union ((map fst rhs) union ats) |
592 |
592 |
593 fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) = |
593 fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) = |
594 (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats) |
594 (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats) |
595 |
595 |
596 fun discr initems = map fst (foldl add_datoms ([],initems)); |
596 fun discr initems = map fst (Library.foldl add_datoms ([],initems)); |
597 |
597 |
598 fun refutes sg (pTs,params) ex = |
598 fun refutes sg (pTs,params) ex = |
599 let |
599 let |
600 fun refute (initems::initemss) js = |
600 fun refute (initems::initemss) js = |
601 let val atoms = foldl add_atoms ([],initems) |
601 let val atoms = Library.foldl add_atoms ([],initems) |
602 val n = length atoms |
602 val n = length atoms |
603 val mkleq = mklineq n atoms |
603 val mkleq = mklineq n atoms |
604 val ixs = 0 upto (n-1) |
604 val ixs = 0 upto (n-1) |
605 val iatoms = atoms ~~ ixs |
605 val iatoms = atoms ~~ ixs |
606 val natlineqs = mapfilter (mknat pTs ixs) iatoms |
606 val natlineqs = List.mapPartial (mknat pTs ixs) iatoms |
607 val ineqs = map mkleq initems @ natlineqs |
607 val ineqs = map mkleq initems @ natlineqs |
608 in case elim(ineqs,[]) of |
608 in case elim(ineqs,[]) of |
609 Success(j) => |
609 Success(j) => |
610 (trace_msg "Contradiction!"; refute initemss (js@[j])) |
610 (trace_msg "Contradiction!"; refute initemss (js@[j])) |
611 | Failure(hist) => |
611 | Failure(hist) => |