diff -U 3 abcd-original/classic_abcd_solver.cpp ./classic_abcd_solver.cpp --- abcd-original/classic_abcd_solver.cpp 2006-09-26 01:26:01.000000000 -0700 +++ ./classic_abcd_solver.cpp 2006-10-04 19:42:05.000000000 -0700 @@ -269,12 +269,12 @@ ProveResult meetBest(ProveResult res1, ProveResult res2) { - return (ProveResult) std::min(res1, res2); + return (ProveResult) std::max(res1, res2); } ProveResult meetWorst(ProveResult res1, ProveResult res2) { - return (ProveResult) std::max(res1, res2); + return (ProveResult) std::min(res1, res2); } void print_result(ProveResult r, std::ostream& os) @@ -557,16 +557,26 @@ IneqEdge* in_edge = (*in_iter); assert(in_edge->getDst() == dest); ProveResult res; - if ( _mem_distance.hasLeqBoundResult(dest, bound) ) { - res = _mem_distance.getLeqBoundResult(dest, bound); - }else{ - res = prove(in_edge->getSrc(), - _bound_alloc.create_dec_const(bound, - in_edge->getLength()), - prn_level + 1); - in_iter++; - } + assert(!_mem_distance.hasLeqBoundResult(dest, bound)); + res = prove(in_edge->getSrc(), + _bound_alloc.create_dec_const(bound, + in_edge->getLength()), + prn_level + 1); + in_iter++; for (; in_iter != in_last; in_iter++) { + if(((res >= Reduced) && (meet_f == meetBest)) || + ((res == False) && (meet_f == meetWorst))) { + // For any x, meetBest(True, x) == True + // meetBest(Reduced, x) >= Reduced + // and meetWorst(False, x) == False + if (Log::isEnabled() ) { + Printer prn(prn_level, Log::out()); + prn.prnStr("skipping remaining preds, proven: "); + print_result(res, Log::out()); + Log::out() << std::endl; + } + break; + } in_edge = (*in_iter); assert(in_edge->getDst() == dest); IOpnd* pred = in_edge->getSrc(); @@ -829,7 +839,7 @@ g.addEdge(2, 3, 1); g.addEdge(3, 1, 0); g.addEdge(20, 2, -1); - g.addEdge(0, 10, 0); + g.addEdge(21, 10, 0); g.addEdge(10, 11, 0); g.addEdge(11, 12, 0); g.addEdge(12, 13, 1); diff -U 3 abcd-original/classic_abcd_solver.h ./classic_abcd_solver.h --- abcd-original/classic_abcd_solver.h 2006-09-26 01:26:01.000000000 -0700 +++ ./classic_abcd_solver.h 2006-10-04 19:33:51.000000000 -0700 @@ -34,6 +34,7 @@ {} IOpnd() { assert(0); } + virtual ~IOpnd() {}; void setPhi(bool s = true) { _phi = s; } bool isPhi() const { return _phi; } @@ -196,9 +197,9 @@ }; enum ProveResult { - True = 0, + True = 2, Reduced = 1, - False = 2 + False = 0 }; typedef ProveResult (*meet_func_t)(ProveResult, ProveResult);