Quell more clang warnings

[bpfoley]

Quiten a bunch of warnings when building with Clang on macOS 10.15.

[rgov]

Hm, what's the blame for this? I would prefer to remove dead code, especially if this is pretty old. Otherwise we should revisit why this was skipped.

[bpfoley]

It was disabled in 175338a

It's exported as DLL_PUBLIC Result bvSignedModulusBothWays, and wrapped in a couple of places, and elsewhere in the code there's a commented out

    else if (k == SBVMOD)
    {
      // This propagator is very slow. It needs to be reimplemented.
      // result = bvSignedModulusBothWays(children, output, n.GetSTPMgr());
      mult_like = true;
    }

[rgov]

Thanks for making more changes and I'm sorry for letting this sit so long. Could you look at the one remaining issue for me please?

[rgov]

Could you elaborate on the removal of signed? I believe in C the signedness of the char type is architecture defined. On ARM for instance it is unsigned by default, so this could change the behavior on ARM systems.

[bpfoley]

Yes. I mention this in the commit message. PowerPC is one of the architectures that makes the unusual choice of having char unsigned by default.

I removed the signed because clang (on an x86_64 machine) was complaining about mixing pointers to signed and unsigned chars. Specifically

[ELIDED]/lib/extlib-abc/aig/cnf/cnfData.c:4594:24: warning: assigning to
      'char *' from 'signed char *' converts between pointers to integer types with different sign
      [-Wpointer-sign]
            pSops[i++] = pPrev;
                       ^ ~~~~~

[msoos]

First of all, thanks for your interest in the code! I think I just would like to point out two things:

1. The code does indeed need some love and I'm glad you are doing this!
2. Unfortunately these are minor (but interesting and useful!) changes. What the code also needs is to go "deeper" and fix and improve it in significant ways.

So I really do like you doing this, and I'm hoping you'll do (2), too? It would be really nice! :)

[aytey]

@msoos do you have some thoughts on areas that "need some love"?

I guess what you're saying is that clang is giving "superficial" (i.e., genuine, but quite shallow) issues, whereas you're aware of some more widespread/deep-seated kind of issues that a static analysis tool might not report on.

If I knew some places that needed some help, I might be able to take a look in some spare cycles. However, I'd rather address stuff you already know is "bad" than try to find my own ones and fix stuff you don't have a problem with!

[msoos]

Hi,

Static analysis tools don't normally find algorithmic inefficiencies, deep technical bugs, incorrect data structures, etc. Those are the more complicated issues, and the ones that could significantly improve our performance.

A really interesting algorithmic fix would be to obtain the toplevel variables set by CryptoMiniSat, inject it into the AST, and simplify the AST based on that. Currently, we have: SMT -> SAT But we could have: SMT <-> SAT i.e. a tighter integration. I know that Armin Biere's very successful SMT solver does this. Doing that would be really nice. You can obtain these toplevel-assigned variables from CryptoMiniSat with get_zero_assigned_lits/

I think it's important to do e.g. compiler warning fixing as a first step towards more complicated changes. It allows oneself to familiarize with the code, play with it. So I think it's good -- but it should be followed up with deeper, more technical fixes so we don't loose the know-how that we accumulated fixing the small things. Unfortunately, I have seen before when only warnings were fixed, not followed with more deep issues fixed, which saddens me, but I think that's just life, we have to gamble a bit :)

Just my 2 cents,

Mate

[aytey]

Do you have any examples of 'fix' rather than 'improve'?

[msoos]

Sure, please fix the speed of solving :) The point being, of course, is that the most valuable thing we have here is time: both time to spend on improving STP and time waiting for it to finish solving a problem. We could always pay 1000 mathematicians, put them in a big office and ask them to solve our problems -- the NSA does this, of course, and so do many others. But we don't have the money to do that. So we spend our time writing code so we don't have to spend our time waiting for the answers. From this perspective, improving the speed is fixing. So, please fix the code! It's wrong, it could be much faster using known, documented, and implemented techniques :)

Note that the issues fixed here mostly don't cause breaking, depending what you mean by breaking. It runs on my system, though takes long and gives me warnings. Works for me. So... what is fixing, and what is improving? Why is removing compiler warnings fixing (even though it didn't stop from compiling), but making sure some problems that couldn't be solved before but can be now is not fixing? What is fixing? What is improving?

Ahh... philosophical questions! Unfortunately, trying to resolve this mystery will just spend more of our most precious resource, time! So I'll get back to... dunno... fixing? improving? CryptoMiniSat :D It cannot solve some problems, and needs fixing!

[aytey]

I think my point here is:

• fixing == changing the code for the better without modifying the functionality of the core tool

• improving == changing the code to add new features such that the tool now does more (or is quicker!) than it used to

I'd say integrating STP "better" with CMS (like Boolector does) changes the functionality of the tool.

My belief is that it is easier for people to get started on working on STP if there are areas that could be "fixed" (to be "better") vs. improved by implementing new features.

Are you aware of where Boolector's used of "fixed" literals is documented? I mean, it is in the code for btor_sat_fixed, but it isn't clear to me (even knowing what I know about the Boolector code!) how that is used to simplify the AIG.

[rgov]

@andrewvaughanj Do you want to shepherd this? I think most of the changes are worth taking. Not entirely sure on the signed char conversion bit.

[aytey]

I'm worried I have a different opinion to you guys though ... my opinion here is that we should not be fixing issues in external libraries.

I would much prefer it if @bpfoley could make his changes against https://github.com/berkeley-abc/abc and then make STP work against the latest release (or master!) of abc. Having our own changes makes it hard to update against the upstream.

The same applies to Bit-Vector; we have STP changes against Bit-Vector, which now makes it a lot harder for us to update to latest Bit-Vector.