[llvm] r197713 - Stay classy (and legal) LLVM. Remove links to 3rd party SMT solver whose links may not be permanent.

[Hal Finkel]

Philip,

He removed them at my request; I replied to his original commit and raised the following objection:

> Kay,
> 
> While I'm a big fan of SMT solvers, I don't think putting these links in the source code is a good idea.
> 
>  1. While Z3 is a great SMT solver, it is specifically made available for personal and non-commercial use only (see http://rise4fun.com/termsofuse), and we have a lot of contributors and users for whom that is an issue.
> 
>  2. Who knows what the lifetime of those 'permalinks' will actually be. We should record the relevant details in some place that we control.
> 
> Please record whatever input or output is relevant in the bug report, and remove the references to Z3 and the links from the source code.
> 
> Thanks again,
> Hal

 -Hal

----- Original Message -----
> From: "Philip Reames" <listmail at philipreames.com>
> To: "Kay Tiong Khoo" <kkhoo at perfwizard.com>, llvm-commits at cs.uiuc.edu
> Sent: Thursday, December 19, 2013 1:00:45 PM
> Subject: Re: [llvm] r197713 - Stay classy (and legal) LLVM. Remove links to	3rd party SMT solver whose links may not
> be permanent.
> 
> Out of curiosity, what was the motivation for this change?  I don't
> see
> the advantage in removing them.  To my knowledge, there's no legal
> reason to do so either.
> 
> Philip
> 
> On 12/19/13 10:35 AM, Kay Tiong Khoo wrote:
> > Author: kkhoo
> > Date: Thu Dec 19 12:35:54 2013
> > New Revision: 197713
> >
> > URL: http://llvm.org/viewvc/llvm-project?rev=197713&view=rev
> > Log:
> > Stay classy (and legal) LLVM. Remove links to 3rd party SMT solver
> > whose links may not be permanent.
> >
> > Modified:
> >      llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
> >
> > Modified:
> > llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
> > URL:
> > http://llvm.org/viewvc/llvm-project/llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp?rev=197713&r1=197712&r2=197713&view=diff
> > ==============================================================================
> > --- llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
> > (original)
> > +++ llvm/trunk/lib/Transforms/InstCombine/InstCombineCompares.cpp
> > Thu Dec 19 12:35:54 2013
> > @@ -1210,8 +1210,7 @@ Instruction *InstCombiner::visitICmpInst
> >             // We can also fold a signed comparison if the mask
> >             value and
> >             // comparison value are not negative. These constraints
> >             may not be
> >             // obvious, but we can prove that they are correct
> >             using an SMT
> > -          // solver such as "Z3" :
> > -          // http://rise4fun.com/Z3/DyMp
> > +          // solver.
> >             if (!ICI.isSigned() || (!AndCst->isNegative() &&
> >             !RHS->isNegative()))
> >               CanFold = true;
> >           } else if (ShiftOpcode == Instruction::LShr) {
> > @@ -1219,8 +1218,7 @@ Instruction *InstCombiner::visitICmpInst
> >             // signed. We can also fold a signed comparison if the
> >             shifted mask
> >             // value and the shifted comparison value are not
> >             negative.
> >             // These constraints may not be obvious, but we can
> >             prove that they
> > -          // are correct using an SMT solver such as "Z3" :
> > -          // http://rise4fun.com/Z3/Tslfh
> > +          // are correct using an SMT solver.
> >             if (!ICI.isSigned())
> >               CanFold = true;
> >             else {
> >
> >
> > _______________________________________________
> > llvm-commits mailing list
> > llvm-commits at cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits
> 
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits
> 

-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory