Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

cannot obtain a working pbencoder executable #4

Open
leoliberti opened this issue Nov 6, 2024 · 0 comments
Open

cannot obtain a working pbencoder executable #4

leoliberti opened this issue Nov 6, 2024 · 0 comments

Comments

@leoliberti
Copy link

Hi,

I'm trying to compile PBLib on a MacOS Ventura 13.7.1 running on an Apple M1 Max processor, and failing in various ways. Here are the various steps I took, and their result.

  1. The first step, i.e. "cmake -H. -Bbuild" works (after having followed the advice in an earlier issue).

  2. The second step, i.e. "cmake --build build" fails with
    "fatal error: too many errors emitted, stopping now [-ferror-limit=] 20 errors generated.",
    many of them being
    "/usr/local/src/pblib/version:1:1: error: unknown type name 'PBLib' PBLib 1.2.1"
    "/usr/local/src/pblib/version:1:7: error: expected unqualified-id PBLib 1.2.1"
    (but not only -- there are also some
    "/Applications/Xcode.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX14.0.sdk/usr/include/c++/v1/__iterator/iterator_traits.h:429:13: error: reference to unresolved using declaration typedef ptrdiff_t difference_type;" and more besides)

  3. I have had better fortune using the GNU compiler: if the first step is "CC=gcc-14 CXX=g++-14 cmake -H. -Bbuild" then the second step "cmake --build build" fails much later, when it attempts to link its first executable pbo2maxsat: "ld: Assertion failed: (resultIndex < sectData.atoms.size()), function findAtom, file Relocations.cpp, line 1336." I could not solve this linking issue (I even tested lld from homebrew to no avail).

  4. I then moved to a virtual machine: an Ubuntu 20.04.2 ARM64 running on Parallels desktop. It links pbo2maxsat and pbencoder, then fails because minisat/minisat/mtl/Vec.h cites a "numeric_limits" which is not a member of the std namespace. This is probably just old code needing a brush-up.

  5. Then I run pbencode and pbo2maxsat on an .opb (pseudoboolean) instance: both fail on "PBParser.h:604: void SimpleParser::readMetaData() [with Callback = DefaultCallback]: Assertion `c=='*'' failed.", and then dump core.

  6. The same as 4-5 happens on Ubuntu on Intel.

Can anyone help me obtain a pbencoder that will encode an .opb file to a .sat file?

Thanks,
Leo Liberti

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant