solver: remove stp support entirely

The version of STP vendored in the repo is over 10 years old, and Yices2 is the
default. Even though it has other complications (like GPLv3), it's pointless to
keep both of these around when the real path forward is to most likely support
arbitrary solvers via smtlib.

Delete this incredibly old snapshot and all references to it, and enjoy the
improved compile times, and just rely on Yices for now.

Signed-off-by: Austin Seipp <[email protected]>

.gitattributes

@@ -2,7 +2,6 @@
 # in statistics about this repo
 #
 src/Parsec/**  linguist-vendored
-src/vendor/stp/src/**  linguist-vendored
 testsuite/**  linguist-vendored
 doc/**  linguist-documentation
 

.github/workflows/build-and-test-macos.yml

@@ -101,7 +101,7 @@ jobs:
           popd
       # Check that .ghci has all the right flags to load the source.
       # This is important for text editor integration & tools like ghcid
-      # NB stp, yices and htcl must be built first, so do this after Build.
+      # NB yices and htcl must be built first, so do this after Build.
       - name: Check GHCI :load
         run: |
           cd src/comp

.github/workflows/build-and-test-ubuntu.yml

@@ -86,7 +86,7 @@ jobs:
           popd
       # Check that .ghci has all the right flags to load the source.
       # This is important for text editor integration & tools like ghcid
-      # NB stp, yices and htcl must be built first, so do this after Build.
+      # NB yices and htcl must be built first, so do this after Build.
       - name: Check GHCI :load
         run: |
           cd src/comp

COPYING

@@ -3,15 +3,6 @@ under the BSD-3-Clause license, as indicated at the end of this file.
 Individual files or directories may specify their own copyright and
 license.  The following are known to have other authors and licenses:
 
-* STP - Constraint solver
-  * The files in src/vendor/stp/src/ are adapted from a snapshot of STP
-  * See LICENSES/LICENSE.stp and LICENSES/LICENSE.stp_components
-  * The source and license were obtained from the SVN repository [1]
-    at revision 1643 on 2012-04-18.  A patch at [2] obtained on
-    2014-04-21 was also applied.
-      [1] https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
-      [2] https://github.com/stp/stp/commit/ece1a55fb367bd905078baca38476e35b4df06c3
-
 * The Yices SMT Solver
   * The files in src/vendor/yices/ define a Haskell interface for using
     the Yices library (via its C API); there is also code for a

INSTALL.md

@@ -147,18 +147,6 @@ library to compile:
         autoconf \
         gperf
 
-Building the BSC tools will also recurse into a directory for the STP SMT
-solver. This is currently an old snapshot of the STP source code, including the
-code for various libraries that it uses. In the future, this may be replaced
-with a submodule instantiation of the repository for [the STP SMT
-solver](https://github.com/stp/stp). When that happens, additional requirements
-from that repository will be added.
-Building the STP library is optional (see below).
-The current snapshot requires Perl, to
-generate two source files. It also needs flex and bison:
-
-    $ apt-get install flex bison
-
 The `check-smoke` target runs a test using an external Verilog simulator, which is
 [Icarus Verilog] by default. You can install Icarus on Debian/Ubuntu with:
 
@@ -226,29 +214,6 @@ compile in parallel, define `GHCJOBS` in the environment to that number:
 
     $ make GHCJOBS=4
 
-### Optionally avoiding the compile of STP or Yices
-
-The BSC tools expect to dynamically link with specific versions of STP and Yices,
-found in `inst/lib/SAT/`.  By default, the build process will compile both
-libraries and install them in that directory.  However, the BSC tools only need
-one SMT solver; Yices is used by default, and STP can be selected via a flag.
-Most users will never need to switch solvers, or even be aware of the option.
-Thus, the build process offers the option of not compiling the STP library,
-and instead installing a stub file, that the BSC tools will recognize and will
-not allow the user to select that solver.  This option is chosen by assigning
-a non-empty value to `STP_STUB`:
-
-    $ make STP_STUB=1
-
-This can be used if STP does not build on your system or if you want to avoid
-the work of building the library.  A similar `YICES_STUB` option exists, for
-skipping the build of the Yices library:
-
-    $ make YICES_STUB=1
-
-The BSC tools do need at least one SMT solver, so only one of these options
-should be used.
-
 ## Test the BSC toolchain
 
 The following command will run a smoke test to ensure the compiler and

doc/user_guide/user_guide.tex

@@ -2171,7 +2171,6 @@ \subsection{Compiler optimizations}
 \label{flag-optundeterminedvals}
 \begin{centerboxverbatim}
 -opt-undetermined-vals      aggressive optimization of undetermined values
--sat-stp                    use STP SMT for disjoint testing and SAT 
 -sat-yices                  use Yices SMT for disjoint testing and SAT
 \end{centerboxverbatim}
 
@@ -2191,7 +2190,6 @@ \subsection{Compiler optimizations}
 flag on may produce better hardware in Verilog, but can result in the
 Bluesim and Verilog simulations producing different intermediate values.
 
-\index{-sat-stp@\te{-sat-stp} (compiler flag)}
 \index{-sat-yices@\te{-sat-yices} (compiler flag)}
 It is possible to change the underlying proof engine used by the
 compiler.  You should not use these flags 

release/Makefile

@@ -26,8 +26,6 @@ LICFILES = $(addprefix $(LICDIR)/, \
 	LICENSE.ghc \
 	LICENSE.hbc \
 	LICENSE.parsec \
-	LICENSE.stp \
-	LICENSE.stp_components \
 	LICENSE.yices \
 	LICENSE.yices-painless \
 	)

release/tarball-COPYING

@@ -11,12 +11,8 @@ indicated in the files themselves.  If not otherwise specified, they
 are copyright Bluespec Inc and licensed under the BSD-3-Clause
 license, as indicated at the end of this file.
 
-The library objects in the SAT directory, for STP and Yices, are
-licensed and copyright as follows:
-
-* STP - Constraint solver
-  * The library is built from an adapted snapshot of STP
-  * See LICENSES/LICENSE.stp and LICENSES/LICENSE.stp_components
+The library objects in the SAT directory for Yices are licensed
+and copyright as follows:
 
 * The Yices SMT Solver
   * The library is built from the Yices GitHub repository
@@ -28,10 +24,6 @@ under the BSD-3-Clause license, as indicated at the end of this file.
 They are also built with the following code or APIs with their own
 copyright and licensing:
 
-* STP - Constraint solver
-  * BSC tools are linked with the library
-  * See LICENSES/LICENSE.stp
-
 * The Yices SMT Solver
   * BSC tools are linked with the library
   * See LICENSES/LICENSE.yices

src/Makefile

@@ -9,12 +9,10 @@ ifndef NO_DEPS_CHECKS
 CC_TOOLS=$(CC) $(CXX) $(LD)
 BSC_TOOLS=ghc ghc-pkg
 YICES_TOOLS=gperf autoconf
-STP_TOOLS=flex bison
 
 TOOLS=$(CC_TOOLS) \
       $(BSC_TOOLS) \
-      $(YICES_TOOLS) \
-      $(STP_TOOLS) \
+      $(YICES_TOOLS)
 
 GHC_PKGS=regex-compat syb old-time split
 
@@ -54,7 +52,6 @@ all: install
 
 .PHONY: install clean full_clean
 install clean full_clean:
-	$(MAKE)  -C vendor/stp   PREFIX=$(PREFIX)  $@
 	$(MAKE)  -C vendor/yices PREFIX=$(PREFIX)  $@
 	$(MAKE)  -C vendor/htcl  PREFIX=$(PREFIX)  $@
 	# we need to build targets from here sequentially, as they operate in the same workspace
@@ -68,4 +65,3 @@ install clean full_clean:
 	$(MAKE)  -C bluetcl    PREFIX=$(PREFIX)  $@
 	$(MAKE)  -C bluesim    PREFIX=$(PREFIX)  $@
 	$(MAKE)  -C Verilator  PREFIX=$(PREFIX)  $@
-

src/comp/.ghci

@@ -23,17 +23,13 @@
 :set -i../comp:../comp/Libs:../comp/GHC:../comp/GHC/posix:../Parsec
 
 -- Shared libraries and FFI bindings
-:set -i../vendor/stp/include_hs
 :set -i../vendor/yices/include_hs
 :set -i../vendor/htcl
 
 :set -I/usr/include/tcl
 :set -L../vendor/htcl
 :set -lhtcl
 
-:set -L../vendor/stp/lib
-:set -lstp
-
 :set -L../vendor/yices/lib
 :set -lyices