stp: 2.3.3 -> 2.3.4; fix tests; fix aarch64 compatibility; fix Python...

{ lib

, stdenv

, cmake

, boost

, bison

, flex

, fetchFromGitHub

, fetchpatch

, perl

, python3

, zlib

, minisat

, cryptominisat

{

  lib,

  stdenv,

  cmake,

  boost,

  bison,

  flex,

  pkg-config,

  fetchFromGitHub,

  fetchpatch,

  symlinkJoin,

  perl,

  python3,

  zlib,

  minisat,

  cryptominisat,

  gmp,

  cadical,

  gtest,

  lit,

  outputcheck,

  nix-update-script,

  useCadical ? true,

}:

stdenv.mkDerivation rec {

stdenv.mkDerivation (finalAttrs: {

  pname = "stp";

  version = "2.3.3";

  version = "2.3.4";

  src = fetchFromGitHub {

    owner = "stp";

    repo = "stp";

    rev = version;

    hash = "sha256-B+HQF4TJPkYrpodE4qo4JHvlu+a5HTJf1AFyXTnZ4vk=";

    tag = "${finalAttrs.version}_cadical";

    hash = "sha256-fNx3/VS2bimlVwCejEZtNGDqVKnwBm0O2YkIUQm6eDM=";

  };

  patches = [

    # Fix missing type declaration

    # due to undeterminisitic compilation

    # of circularly dependent headers

    ./stdint.patch

    # Python 3.12+ compatibility for build: https://github.com/stp/stp/pull/450

    (fetchpatch {

      url = "https://github.com/stp/stp/commit/fb185479e760b6ff163512cb6c30ac9561aadc0e.patch";

      hash = "sha256-guFgeWOrxRrxkU7kMvd5+nmML0rwLYW196m1usE2qiA=";

    })

  ];

  postPatch =

    ''

      substituteInPlace CMakeLists.txt \

        --replace-fail GIT-hash-notfound "$version"

      # We want to use the Nix wrapper for the output check tool instead of running it through Python.

      substituteInPlace tests/query-files/lit.cfg \

        --replace-fail "pythonExec + ' ' +OutputCheckTool" "OutputCheckTool"

  postPatch = ''

    # Upstream fix for gcc-13 support:

    #   https://github.com/stp/stp/pull/462

    # Can't apply it as is as patch context changed in ither patches.

    # TODO: remove me on 2.4 release

    sed -e '1i #include <cstdint>' -i include/stp/AST/ASTNode.h

      # Results in duplication of Nix store paths and trouble finding the Python library at runtime

      substituteInPlace bindings/python/stp/library_path.py.in_install \

        --replace-fail "@CMAKE_INSTALL_PREFIX@/" ""

    ''

    + lib.optionalString useCadical ''

      # Fix up Cadical paths.

      substituteInPlace include/stp/Sat/Cadical.h \

        --replace-fail "src/cadical.hpp" "cadical.hpp"

      substituteInPlace CMakeLists.txt \

        --replace-fail "build/libcadical.a" "lib/libcadical.a" \

        --replace-fail 'include_directories(''${CADICAL_DIR}/)' 'include_directories(''${CADICAL_DIR}/include)'

    '';

  buildInputs = [

    boost

    zlib

    minisat

    cryptominisat

    python3

    gmp

    minisat

  ] ++ lib.optional (!useCadical) cryptominisat;

  nativeBuildInputs = [

    cmake

    bison

    flex

    perl

    pkg-config

  ];

  cmakeFlags =

    let

      # STP expects Cadical dependencies to all be in the same place.

      cadicalDependency = symlinkJoin {

        name = "stp-${finalAttrs.version}-cadical";

        paths = [

          cadical.lib

          cadical.dev

        ];

  nativeBuildInputs = [ cmake bison flex perl ];

  preConfigure = ''

      };

    in

    [

      (lib.cmakeBool "BUILD_SHARED_LIBS" true)

      (lib.cmakeBool "USE_CADICAL" useCadical)

      (lib.cmakeBool "NOCRYPTOMINISAT" useCadical)

      (lib.cmakeBool "FORCE_CMS" (!useCadical))

      (lib.cmakeBool "ENABLE_TESTING" finalAttrs.doCheck)

    ]

    ++ lib.optional finalAttrs.doCheck (lib.cmakeFeature "LIT_ARGS" "-v")

    ++ lib.optional useCadical (lib.cmakeFeature "CADICAL_DIR" (toString cadicalDependency));

  # Fixes the following warning in the aarch64 build on Linux:

  # lib/extlib-abc/aig/cnf/cnfData.c:4591:25: warning: result of comparison of

  # constant 255 with expression of type 'signed char' is always false [-Wtautological-constant-out-of-range-compare]

  # 4591 |         if ( pMemory[k] == (char)(-1) )

  #

  # This seems to cause an infinite loop in tests on aarch64-linux platforms.

  #

  # TODO: Remove these CFLAGS when they update to the version that pulls `abc` in with a submodule.

  # https://github.com/stp/stp/issues/498#issuecomment-2611251631

  CFLAGS = [ "-fsigned-char" ];

  outputs = [

    "dev"

    "out"

  ];

  preConfigure =

    ''

      python_install_dir=$out/${python3.sitePackages}

      mkdir -p $python_install_dir

    cmakeFlagsArray=(

      $cmakeFlagsArray

      "-DBUILD_SHARED_LIBS=ON"

      cmakeFlagsArray+=(

        "-DPYTHON_LIB_INSTALL_DIR=$python_install_dir"

      )

    ''

    + lib.optionalString finalAttrs.doCheck ''

      # Link in gtest and the output check utility.

      mkdir -p deps

      ln -s ${gtest.src} deps/gtest

      ln -s ${outputcheck} deps/OutputCheck

    '';

  meta = with lib; {

  nativeCheckInputs = [

    gtest

    lit

    outputcheck

  ];

  doCheck = true;

  postInstall = ''

    # Clean up installed gtest/gmock files that shouldn't be there.

    shopt -s globstar nocaseglob

    rm -rf $out/**/*g{test,mock}*

    # Some of the gtest/gmock files were in the pkgconfig folders, which may now be empty.

    find $out/ -name pkgconfig -type d -empty -delete

    # Python bindings are broken:

    substituteInPlace $python_install_dir/**/stp.py \

      --replace-fail "from library_path import PATHS" "from .library_path import PATHS"

  '';

  doInstallCheck = true;

  postInstallCheck = ''

    $out/bin/stp --version | tee /dev/stderr | grep -F "STP version $version"

    # Run the examples from the docs: https://stp.readthedocs.io/en/latest/#python-usage

    for binary in stp stp_simple; do

      echo "(set-logic QF_BV) (assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2))) (check-sat) (exit)" | tee /dev/stderr | $out/bin/$binary | grep "^sat$"

    done

    PYTHONPATH=$out/${python3.sitePackages} ${lib.getExe python3} -c \

      "import stp; s = stp.Solver(); a, b, c = s.bitvec('a', 32), s.bitvec('b', 32), s.bitvec('c', 32); s.add(a == 5); s.add(b == 6); s.add(a + b == c); assert s.check(); print(s.model())" >&2

  '';

  passthru = {

    updateScript = nix-update-script {

      extraArgs = [

        "--version-regex"

        "^v(2\\.3\\.[0-9]+)$"

      ];

    };

  };

  meta = {

    description = "Simple Theorem Prover";

    maintainers = with maintainers; [ McSinyx numinit ];

    platforms = platforms.linux;

    license = licenses.mit;

    homepage = "https://stp.github.io/";

    maintainers = with lib.maintainers; [

      McSinyx

      numinit

    ];

    platforms = with lib.platforms; linux ++ darwin;

    license = lib.licenses.mit;

  };

}

})

diff --git a/include/stp/AST/ASTNode.h b/include/stp/AST/ASTNode.h

index 91acd726182c..0a17db23ffbf 100644

--- a/include/stp/AST/ASTNode.h

+++ b/include/stp/AST/ASTNode.h

@@ -24,9 +24,10 @@ THE SOFTWARE.

 #ifndef ASTNODE_H

 #define ASTNODE_H

+#include "stp/AST/ASTInternal.h"

 #include "stp/AST/NodeFactory/HashingNodeFactory.h"

+#include "stp/AST/UsefulDefs.h"

 #include "stp/Util/Attributes.h"

-#include "ASTInternal.h"

 #include "stp/Globals/Globals.h"

 namespace stp

  stop-words = callPackage ../development/python-modules/stop-words { };

  stp = toPythonModule (pkgs.stp.override {

    python3 = self.python;

  });

  stransi = callPackage ../development/python-modules/stransi { };

  strategies = callPackage ../development/python-modules/strategies { };