nick8325 / equinox

Paradox model finder and equinox theorem prover for first-order logic.
MIT License
19 stars 4 forks source link

error building minisat with clang #9

Open jessealama opened 11 years ago

jessealama commented 11 years ago

Building equinox/paradox/etc. using the clang C++ compiler on Mac OS X 10.8 results in an error:

$ make
make Solver.or -C minisat/current-base
Compiling: Solver.or ( Solver.C )
clang: warning: argument unused during compilation: '-ffloat-store'
In file included from Solver.C:20:
In file included from ./Solver.h:65:
./VarOrder.h:88:1: warning: 'VarFilter' defined as a struct here but previously declared as a class [-Wmismatched-tags]
struct VarFilter {
^
./VarOrder.h:70:12: note: did you mean struct here?
    friend class VarFilter;
           ^~~~~
           struct
In file included from Solver.C:20:
./Solver.h:265:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpbin   = Clause_new(dummy);
                                     ^
./Solver.h:266:38: error: use of undeclared identifier 'Clause_new'
                analyze_tmpbin     = Clause_new(dummy);
                                     ^
./Solver.h:268:38: error: use of undeclared identifier 'Clause_new'
                bwdsub_tmpunit     = Clause_new(dummy);
                                     ^
./Solver.h:270:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpempty = Clause_new(dummy);
                                     ^
Solver.C:89:23: error: use of undeclared identifier 'Clause_new'
        Clause* c   = Clause_new(ps, learnt);
                      ^
Solver.C:879:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
Solver.C:910:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
3 warnings and 5 errors generated.
make[1]: *** [Solver.or] Error 1
make: *** [mk-minisat] Error 2

A solution it to use g++:

CXX=g++ make
[proceeds as expected]
nick8325 commented 11 years ago

Fixed! Thanks for the report.

jessealama commented 9 years ago

This problem still remains -- if one doesn't have access to GNU g++, then the build fails.

$ g++ --version
Configured with: --prefix=/Library/Developer/CommandLineTools/usr --with-gxx-include-dir=/usr/include/c++/4.2.1
Apple LLVM version 6.0 (clang-600.0.54) (based on LLVM 3.5svn)
Target: x86_64-apple-darwin14.0.0
Thread model: posix

The error is precisely as before, but just for the sake of completeness:

$ make
make Solver.or -C minisat/current-base
make[1]: Entering directory '/Users/alama/sources/equinox/minisat/current-base'
Compiling: Solver.or ( Solver.C )
In file included from Solver.C:20:
In file included from ./Solver.h:65:
./VarOrder.h:88:1: warning: 'VarFilter' defined as a struct here but previously declared
      as a class [-Wmismatched-tags]
struct VarFilter {
^
./VarOrder.h:70:12: note: did you mean struct here?
    friend class VarFilter;
           ^~~~~
           struct
In file included from Solver.C:20:
./Solver.h:265:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpbin   = Clause_new(dummy);
                                     ^
./Solver.h:266:38: error: use of undeclared identifier 'Clause_new'
                analyze_tmpbin     = Clause_new(dummy);
                                     ^
./Solver.h:268:38: error: use of undeclared identifier 'Clause_new'
                bwdsub_tmpunit     = Clause_new(dummy);
                                     ^
./Solver.h:270:38: error: use of undeclared identifier 'Clause_new'
                propagate_tmpempty = Clause_new(dummy);
                                     ^
Solver.C:89:23: error: use of undeclared identifier 'Clause_new'
        Clause* c   = Clause_new(ps, learnt);
                      ^
Solver.C:879:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
Solver.C:910:21: warning: add explicit braces to avoid dangling else [-Wdangling-else]
                    else
                    ^
In file included from Solver.C:20:
In file included from ./Solver.h:65:
./VarOrder.h:50:25: warning: private field 'activity' is not used
      [-Wunused-private-field]
    const vec<double>&  activity;    // var->act. Pointer to external activity table.
                        ^
4 warnings and 5 errors generated.
../mtl/template.mk:61: recipe for target 'Solver.or' failed
make[1]: *** [Solver.or] Error 1
make[1]: Leaving directory '/Users/alama/sources/equinox/minisat/current-base'
Makefile:18: recipe for target 'mk-minisat' failed
make: *** [mk-minisat] Error 2
brunoczim commented 7 years ago

I am compiling in GNU and the error is also happening with me

Solver.h: In constructor ‘Solver::Solver(char*)’:
Solver.h:265:54: error: ‘Clause_new’ was not declared in this scope
                 propagate_tmpbin   = Clause_new(dummy);
                                                      ^
Solver.h:265:54: note: suggested alternative:
In file included from Solver.h:64:0,
                 from Solver.C:20:
SolverTypes.h:108:20: note:   ‘Clause_new’
     friend Clause* Clause_new(const V& ps, bool learnt = false) {
                    ^
Solver.C: In member function ‘bool Solver::newClause(const vec<Lit>&, bool, bool)’:
Solver.C:89:44: error: ‘Clause_new’ was not declared in this scope
         Clause* c   = Clause_new(ps, learnt);
                                            ^
Solver.C:89:44: note: suggested alternative:
In file included from Solver.h:64:0,
                 from Solver.C:20:
SolverTypes.h:108:20: note:   ‘Clause_new’
     friend Clause* Clause_new(const V& ps, bool learnt = false) {
                    ^
Solver.C: In member function ‘bool Solver::merge(const Clause&, const Clause&, Var, vec<Lit>&)’:
Solver.C:876:20: warning: suggest explicit braces to avoid ambiguous ‘else’ [-Wparentheses]
                 if (var(ps[j]) == var(qs[i]))
                    ^
Solver.C: In member function ‘bool Solver::merge(const Clause&, const Clause&, Var)’:
Solver.C:907:20: warning: suggest explicit braces to avoid ambiguous ‘else’ [-Wparentheses]
                 if (var(__ps[j]) == var(__qs[i]))
                    ^
../mtl/template.mk:61: recipe for target 'Solver.or' failed
make[1]: *** [Solver.or] Error 1
make[1]: Leaving directory '/home/ubuntu/Downloads/paradox-master/minisat/current-base'
Makefile:18: recipe for target 'mk-minisat' failed
make: *** [mk-minisat] Error 2
nick8325 commented 7 years ago

I can't reproduce this on my machine, but patches welcome!

brunoczim commented 7 years ago

Sorry, I've downloaded this from the paradox repository and it wasn't up-to-date