Remove STP support

[thoughtpolice]

As noted by Julie in issue #16, STP is a historical default for the compiler to solve constraints, but recent Yices is now in use as well with the open source release. Since CUDD is also being removed, we can take this chance to just drop STP as well.

---

NOTE: This pull request depends on #25. I've included that here just to keep the relevant diff simpler to manage, since I had to remove CUDD to make things easier for myself to build. Once #25 is merged, I'll rebase this and turn it into a single commit.

[flokli]

@thoughtpolice you might want to update the README as well - it seems the only leftover perl script is in src/Verilog/copy_module.pl, but genkinds.pl gets removed here.

[flokli]

rebased on top of current master: https://github.com/flokli/bsc/tree/remove-stp

[quark17]

I'd like to leave in the ability to use STP, for those who want it. I propose that we remove the STP snapshot and replace it with a stub C file with empty functions for the API; Yices will be the default solver, but if STP is selected, BSC can check whether it's connected to a stub and report an error or revert to Yices. Then, if someone wants to use STP, they can make or get the real library and put it in the LD_LIBRARY_PATH, and BSC will be able to use it. I think I already have a stub C file, so I can make those changes.

[flokli]

Works for me, but I think bsc should fail if the STP solver is explicitly selected but not available.

[flokli]

@quark17 did you publish the STP stub somewhere? I'd be nice if we could wrap this up here as well :-)

[quark17]

Earlier, I thought that the STP code was preventing BSC from building in some environments. It seems that we've fixed that, so I feel there's less urgency to make any changes. I have just pushed changes that make Yices the default solver and allow Yices to be used everywhere that solvers are used (so STP is not used anywhere if the -sat-stp flag is not given). Beyond that, the current STP snapshot seems as good as a stub, to me? But I can dig up the stub code and add it.

[arjenroodselaar]

FWIW STP currently does not compile on MacOS/Clang. The error has to do with the template for hashable types:

c++ -I/usr/local/Cellar/gmp/6.1.2_2/include -I/opt/X11/include -O3 -DNDEBUG -fomit-frame-pointer -fPIC  -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -O3 -DNDEBUG -fomit-frame-pointer -fPIC  -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS -DEXT_HASH_MAP -Wno-deprecated   -c -o ASTUtil.o ASTUtil.cpp
In file included from ASTUtil.cpp:10:
In file included from ./UsefulDefs.h:31:
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/hash_map:240:17: error: no
      matching function for call to object of type 'const __gnu_cxx::hash<char *>'
        {return static_cast<const _Hash&>(*this)(__x);}
                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/__hash_table:2456:21: note: in
      instantiation of member function '__gnu_cxx::__hash_map_hasher<std::__1::pair<const char *, int>, __gnu_cxx::hash<char *>,
      true>::operator()' requested here
    size_t __hash = hash_function()(__k);
                    ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/hash_map:576:69: note: in
      instantiation of function template specialization 'std::__1::__hash_table<std::__1::pair<const char *, int>,
      __gnu_cxx::__hash_map_hasher<std::__1::pair<const char *, int>, __gnu_cxx::hash<char *>, true>,
      __gnu_cxx::__hash_map_equal<std::__1::pair<const char *, int>, BEEV::eqstr, true>, std::__1::allocator<std::__1::pair<const char *,
      int> > >::find<const char *>' requested here
    iterator       find(const key_type& __k)       {return __table_.find(__k);}
                                                                    ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/hash_map:691:20: note: in
      instantiation of member function '__gnu_cxx::hash_map<const char *, int, __gnu_cxx::hash<char *>, BEEV::eqstr,
      std::__1::allocator<std::__1::pair<const char *const, int> > >::find' requested here
    iterator __i = find(__k);
                   ^
ASTUtil.cpp:52:10: note: in instantiation of member function '__gnu_cxx::hash_map<const char *, int, __gnu_cxx::hash<char *>, BEEV::eqstr,
      std::__1::allocator<std::__1::pair<const char *const, int> > >::operator[]' requested here
        s[functionname] += 1;
         ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/__hash:38:12: note: candidate
      function not viable: 1st argument ('const typename pair<const char *, int>::first_type' (aka 'const char *const')) would lose const
      qualifier
    size_t operator()(char *__c) const _NOEXCEPT
           ^
In file included from ASTUtil.cpp:10:
In file included from ./UsefulDefs.h:31:
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/hash_map:237:17: error: no
      matching function for call to object of type 'const __gnu_cxx::hash<char *>'
        {return static_cast<const _Hash&>(*this)(__x.first);}
                ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/__hash_table:1935:21: note: in
      instantiation of member function '__gnu_cxx::__hash_map_hasher<std::__1::pair<const char *, int>, __gnu_cxx::hash<char *>,
      true>::operator()' requested here
    __nd->__hash_ = hash_function()(__nd->__value_);
                    ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/hash_map:695:41: note: in
      instantiation of member function 'std::__1::__hash_table<std::__1::pair<const char *, int>,
      __gnu_cxx::__hash_map_hasher<std::__1::pair<const char *, int>, __gnu_cxx::hash<char *>, true>,
      __gnu_cxx::__hash_map_equal<std::__1::pair<const char *, int>, BEEV::eqstr, true>, std::__1::allocator<std::__1::pair<const char *,
      int> > >::__node_insert_unique' requested here
    pair<iterator, bool> __r = __table_.__node_insert_unique(__h.get());
                                        ^
ASTUtil.cpp:52:10: note: in instantiation of member function '__gnu_cxx::hash_map<const char *, int, __gnu_cxx::hash<char *>, BEEV::eqstr,
      std::__1::allocator<std::__1::pair<const char *const, int> > >::operator[]' requested here
        s[functionname] += 1;
         ^
/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/../include/c++/v1/ext/__hash:38:12: note: candidate
      function not viable: 1st argument ('const char *const') would lose const qualifier
    size_t operator()(char *__c) const _NOEXCEPT
           ^
2 errors generated.
make[4]: *** [ASTUtil.o] Error 1
make[3]: *** [AST/libast.a] Error 2
make[2]: *** [install] Error 2
make[1]: *** [install] Error 2
make: *** [install] Error 2

So from a perspective of making the code base leaner I'd still argue for its removal/replacement by a proper stub. Having said that it compiles fine using GCC and I'll have another look at it at some point to figure out what's failing here, because this should just work.

[bpfoley]

I'd suggest comparing it with https://github.com/stp/stp, to see if/how they've fixed it.

[sequencer]

Or bumping to up-to-date stp master is a good option?

[bpfoley]

That's harder because STP has changed a lot, and they've completely redone their build system to use CMake.

[flokli]

If it's so hard, why not really ditch it now, and re-introduce once we have a less complicated interface like SMT-lib? It seems this requires significant refactoring efforts, and I currently don't really see the value in keeping it.

On top of that, we'll still have it in the git history ;-)

[quark17]

I'm not sure why @bpfoley says it's hard. While the source has improved a lot, it looked like the C API might still have the same functions, and not require much change in BSC. However, the text of the C API has changed enough that I couldn't quickly generate a useful diff and would need to spend time manually looking at the old an new APIs to see what's changed.

The reason to keep STP in the build is, in case there's a bug encountered in Yices, a user can switch to STP (without having to get a new build) and see if that gets them past the problem. Maybe this is unlikely to happen often?

I would certainly like to update to the new STP, instead of this snapshot. The downside is that it adds requirements for people who are building from source; additional dependencies as well as adding a new build tool (cmake).

I've been proposing incremental steps, but don't take that to mean that I think we should stop at any given step.

I'm willing to check in a stub, and have the Makefile choose either the snapshot or the stub, based on a variable which can be set on the command line. Depending on whether it's more important for the default build to have a working STP (for end users) or whether it's more important for people to build from the repo to have a cleaner default experience, we can set the default to be the stub or the snapshot. And at some point, the snapshot can be replaced with newer code, or all of this can be replaced by unvendoring STP or even by using a single common SMT interface (like SMT-Lib) so that people can plug in whatever they want.

[quark17]

FYI, in commits 49760f3 and b37ad3c, I added an STP stub, which is built and installed if you define STP_STUB. For example: make STP_STUB=1 The real STP is still built by default if the variable is not defined.