search

FlorentAvellaneda / EvalMaxSAT

State-of-the-art MaxSAT Solver & Library Based on Unsat Core Guided Techniques
GNU General Public License v3.0
14 stars 4 forks source link

Multicore Capabilities #6

Closed na3na3na closed 5 months ago

na3na3na commented 5 months ago

Hi,

You mentioned in your short description that a multicore version of EvalMaxSAT was already implemented although disabled. How do i go able re-enabling/ using the multicore version?

Side note: What does the first number in the output that follows the first o represent? Using the example you provided, it would be the 1844...1615. I know the 2 represents the cost of the solution (sum of weights of the unsat clauses)

> $ ./EvalMaxSAT_bin log.8.wcsp.log.wcnf 
> o 18446744073709551615
> o 2
> s OPTIMUM FOUND
> v 00100101010011111
> c Total time : 0.00165765s

Thanks!

FlorentAvellaneda commented 5 months ago

Hi,

The first versions of EvalMaxSAT did indeed support multi-threading. The latest version on GitHub with this functionality is the 440bf90edf88f6ab940934129e3c5b3b93764295. Or you can download the binary file from MSE2022 : https://maxsat-evaluations.github.io/2022/mse22-solver-src/complete/EvalMaxSAT.zip

You can then use the argument -p INT with the number of threads to be used to perform the core minimizations.

> $ ./EvalMaxSAT_bin -p 4 log.8.wcsp.log.wcnf

Site note: As admissible solutions are found, the cost of these solutions is displayed. When the optimal solution is found, then "OPTIMUM FOUND" and the solution are displayed. As the first solution is a naive solution, this explains the very high cost. In the current version on Github, this naive solution is no longer displayed because it is rarely useful.

na3na3na commented 5 months ago

Hi,

I tried running the binary from MSE2022 with the command u provided but i get an error saying multi thread not yet compatible with CadiCal.

Thanks again for your help.

FlorentAvellaneda commented 5 months ago

Hi,

Ah yes, sorry. I probably deactivate it directly in the source code for MSE2022... The easiest way would be to recompile from the sources on version 440bf90

> git clone https://github.com/FlorentAvellaneda/EvalMaxSAT.git
> cd EvalMaxSAT
> git checkout 440bf90
> mkdir build
> cd build
> cmake ..
> make
> ./EvalMaxSAT_bin -p 4 log.8.wcsp.log.wcnf
realharryhero commented 1 month ago

The given version still runs on 1 CPU, by checking top on my computer. I do also note there are quite a few warnings from that version; some warning information (an excerpt; it goes beyond my size of the bash terminal) is below:

Log

``` In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Sort.h:24, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:50: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::Option*]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:75:65: required from ‘void Glucose::vec::push(const T&) [with T = Glucose::Option*]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.h:76:29: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] 121 | ap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ^ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::Lit]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:75:65: required from ‘void Glucose::vec::push(const T&) [with T = Glucose::Lit]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/Solver.h:202:26: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = int]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:75:65: required from ‘void Glucose::vec::push(const T&) [with T = int]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/Solver.h:634:81: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = unsigned int]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:109:22: required from ‘void Glucose::vec::memCopyTo(Glucose::vec&) const [with T = unsigned int]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:133:28: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = char]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:109:22: required from ‘void Glucose::vec::memCopyTo(Glucose::vec&) const [with T = char]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:134:24: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::lbool]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:137:13: required from ‘void Glucose::vec::growTo(int) [with T = Glucose::lbool]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:664:37: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::vec]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:137:13: required from ‘void Glucose::vec::growTo(int) [with T = Glucose::vec]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/SolverTypes.h:390:18: required from ‘void Glucose::OccLists::copyTo(Glucose::OccLists&) const [with Idx = int; Vec = Glucose::vec; Deleted = Glucose::SimpSolver::ClauseDeleted]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:135:20: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:54: warning: ‘void* realloc(void*, size_t)’ moving an object of non-trivially copyable type ‘class Glucose::vec’; use ‘new’ and ‘delete’ instead [-Wclass-memaccess] 121 | if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Sort.h:24, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:50: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:39:7: note: ‘class Glucose::vec’ declared here 39 | class vec { | ^~~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Sort.h:24, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:50: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] 121 | ap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ^ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::Map, long unsigned int>::Pair]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:74:65: required from ‘void Glucose::vec::push() [with T = Glucose::Map, long unsigned int>::Pair]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Map.h:81:16: required from ‘void Glucose::Map::_insert(const K&, const D&) [with K = std::__cxx11::basic_string; D = long unsigned int; H = Glucose::Hash >; E = Glucose::Equal >]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Map.h:140:76: required from ‘void Glucose::Map::insert(const K&, const D&) [with K = std::__cxx11::basic_string; D = long unsigned int; H = Glucose::Hash >; E = Glucose::Equal >]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/SolverStats.h:74:23: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:54: warning: ‘void* realloc(void*, size_t)’ moving an object of non-trivially copyable type ‘struct Glucose::Map, long unsigned int>::Pair’; use ‘new’ and ‘delete’ instead [-Wclass-memaccess] 121 | if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/SolverTypes.h:61, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/core/Solver.h:56, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.h:54, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:51: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Map.h:62:12: note: ‘struct Glucose::Map, long unsigned int>::Pair’ declared here 62 | struct Pair { K key; D data; }; | ^~~~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Sort.h:24, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/simp/SimpSolver.cc:50: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] 121 | ap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ^ [ 50%] Building CXX object EvalMaxSAT/glucose/CMakeFiles/glucose.dir/src/glucose/utils/Options.cc.o In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.h:30, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:21: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/ParseUtils.h:99:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation] 99 | while (*in >= '0' && *in <= '9') | ^~~~~ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/ParseUtils.h:103:9: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the ‘while’ 103 | if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3); | ^~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:21: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.h: In member function ‘bool Glucose::Option::OptionLt::operator()(const Glucose::Option*, const Glucose::Option*)’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.h:63:44: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] 63 | return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; | ~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc: In function ‘void Glucose::parseOptions(int&, char**, bool)’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:45:16: warning: suggest explicit braces to avoid ambiguous ‘else’ [-Wdangling-else] 45 | if (!parsed_ok) | ^ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc: In function ‘void Glucose::printUsageAndExit(int, char**, bool)’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:62:5: warning: this ‘if’ clause does not guard... [-Wmisleading-indentation] 62 | if (usage != NULL) | ^~ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:65:9: note: ...this statement, but the latter is misleadingly indented as if it were guarded by the ‘if’ 65 | sort(Option::getOptionList(), Option::OptionLt()); | ^~~~ In file included from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Sort.h:24, from /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.cc:20: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h: In instantiation of ‘void Glucose::vec::capacity(int) [with T = Glucose::Option*]’: /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:75:65: required from ‘void Glucose::vec::push(const T&) [with T = Glucose::Option*]’ /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/utils/Options.h:76:29: required from here /home/mfan/EvalMaxSAT/lib/glucose/src/glucose/mtl/Vec.h:121:97: warning: suggest parentheses around ‘&&’ within ‘||’ [-Wparentheses] 121 | ap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) | ^ [ 54%] Building CXX object EvalMaxSAT/glucose/CMakeFiles/glucose.dir/src/glucose/utils/System.cc.o [ 58%] Linking CXX static library libglucose.a [ 58%] Built target glucose [ 62%] Building CXX object MaLib/CMakeFiles/MaLib.dir/src/main.cpp.o [ 66%] Linking CXX static library libMaLib.a [ 66%] Built target MaLib [ 70%] Building CXX object EvalMaxSAT/CMakeFiles/EvalMaxSAT.dir/src/card_oe.cpp.o In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp:3: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual VirtualSAT* VirtualSAT::clone()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:23:50: warning: no return statement in function returning non-void [-Wreturn-type] 23 | virtual VirtualSAT* clone() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nVars()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:27:51: warning: no return statement in function returning non-void [-Wreturn-type] 27 | virtual unsigned int nVars() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nSoftVar()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:29:54: warning: no return statement in function returning non-void [-Wreturn-type] 29 | virtual unsigned int nSoftVar() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nClauses()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:31:54: warning: no return statement in function returning non-void [-Wreturn-type] 31 | virtual unsigned int nClauses() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:33:43: warning: no return statement in function returning non-void [-Wreturn-type] 33 | virtual bool solve() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::propagate(const std::vector&, std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:37:102: warning: no return statement in function returning non-void [-Wreturn-type] 37 | pagate(const std::vector &assum, std::vector &result) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve(const std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:39:78: warning: no return statement in function returning non-void [-Wreturn-type] 39 | virtual bool solve(const std::vector &assumption) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::vector&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:41:114: warning: no return statement in function returning non-void [-Wreturn-type] 41 | st std::vector &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::__cxx11::list&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:43:112: warning: no return statement in function returning non-void [-Wreturn-type] 43 | onst std::list &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::set&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:45:111: warning: no return statement in function returning non-void [-Wreturn-type] 45 | const std::set &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::getValue(unsigned int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:47:63: warning: no return statement in function returning non-void [-Wreturn-type] 47 | virtual bool getValue(unsigned int var) {assert(!"TODO");} // TODO: unsigned int | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::newVar(bool)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:49:73: warning: no return statement in function returning non-void [-Wreturn-type] 49 | virtual unsigned int newVar(bool decisionVar=true) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::sizeConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:51:58: warning: no return statement in function returning non-void [-Wreturn-type] 51 | virtual unsigned int sizeConflict() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual std::vector VirtualSAT::getConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:53:62: warning: no return statement in function returning non-void [-Wreturn-type] 53 | virtual std::vector getConflict() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp: In member function ‘std::vector > Card_Lazy_OE::oe_4sel(const std::vector >&, unsigned int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp:32:17: warning: comparison of integer expressions of different signedness: ‘int’ and ‘unsigned int’ [-Wsign-compare] 32 | while(v <= k/6) { | ~~^~~~~~ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp:36:14: warning: comparison of integer expressions of different signedness: ‘int’ and ‘std::vector >::size_type’ {aka ‘long unsigned int’} [-Wsign-compare] 36 | if(v <= input.size()/4) { | ~~^~~~~~~~~~~~~~~~~ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp: In member function ‘std::vector > Card_Lazy_OE::select(std::vector >, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp:290:9: warning: control reaches end of non-void function [-Wreturn-type] 290 | default: { | ^~~~~~~ In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/lazyvariable.h:10, from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.h:5, from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/card_oe.cpp:1: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h: At global scope: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h:229:10: warning: ‘void MaLib::{anonymous}::_toString(std::ostringstream&)’ defined but not used [-Wunused-function] 229 | void _toString(std::ostringstream &oss){ | ^~~~~~~~~ [ 75%] Building CXX object EvalMaxSAT/CMakeFiles/EvalMaxSAT.dir/src/cardincremental.cpp.o In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/cardincremental.cpp:3: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual VirtualSAT* VirtualSAT::clone()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:23:50: warning: no return statement in function returning non-void [-Wreturn-type] 23 | virtual VirtualSAT* clone() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nVars()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:27:51: warning: no return statement in function returning non-void [-Wreturn-type] 27 | virtual unsigned int nVars() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nSoftVar()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:29:54: warning: no return statement in function returning non-void [-Wreturn-type] 29 | virtual unsigned int nSoftVar() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nClauses()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:31:54: warning: no return statement in function returning non-void [-Wreturn-type] 31 | virtual unsigned int nClauses() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:33:43: warning: no return statement in function returning non-void [-Wreturn-type] 33 | virtual bool solve() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::propagate(const std::vector&, std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:37:102: warning: no return statement in function returning non-void [-Wreturn-type] 37 | pagate(const std::vector &assum, std::vector &result) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve(const std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:39:78: warning: no return statement in function returning non-void [-Wreturn-type] 39 | virtual bool solve(const std::vector &assumption) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::vector&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:41:114: warning: no return statement in function returning non-void [-Wreturn-type] 41 | st std::vector &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::__cxx11::list&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:43:112: warning: no return statement in function returning non-void [-Wreturn-type] 43 | onst std::list &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::set&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:45:111: warning: no return statement in function returning non-void [-Wreturn-type] 45 | const std::set &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::getValue(unsigned int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:47:63: warning: no return statement in function returning non-void [-Wreturn-type] 47 | virtual bool getValue(unsigned int var) {assert(!"TODO");} // TODO: unsigned int | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::newVar(bool)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:49:73: warning: no return statement in function returning non-void [-Wreturn-type] 49 | virtual unsigned int newVar(bool decisionVar=true) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::sizeConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:51:58: warning: no return statement in function returning non-void [-Wreturn-type] 51 | virtual unsigned int sizeConflict() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual std::vector VirtualSAT::getConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:53:62: warning: no return statement in function returning non-void [-Wreturn-type] 53 | virtual std::vector getConflict() {assert(!"TODO");} | ^ In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/lazyvariable.h:10, from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/cardincremental.h:11, from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/cardincremental.cpp:1: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h: At global scope: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h:229:10: warning: ‘void MaLib::{anonymous}::_toString(std::ostringstream&)’ defined but not used [-Wunused-function] 229 | void _toString(std::ostringstream &oss){ | ^~~~~~~~~ [ 79%] Building CXX object EvalMaxSAT/CMakeFiles/EvalMaxSAT.dir/src/lazyvariable.cpp.o In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/lazyvariable.cpp:4: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual VirtualSAT* VirtualSAT::clone()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:23:50: warning: no return statement in function returning non-void [-Wreturn-type] 23 | virtual VirtualSAT* clone() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nVars()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:27:51: warning: no return statement in function returning non-void [-Wreturn-type] 27 | virtual unsigned int nVars() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nSoftVar()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:29:54: warning: no return statement in function returning non-void [-Wreturn-type] 29 | virtual unsigned int nSoftVar() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nClauses()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:31:54: warning: no return statement in function returning non-void [-Wreturn-type] 31 | virtual unsigned int nClauses() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:33:43: warning: no return statement in function returning non-void [-Wreturn-type] 33 | virtual bool solve() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::propagate(const std::vector&, std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:37:102: warning: no return statement in function returning non-void [-Wreturn-type] 37 | pagate(const std::vector &assum, std::vector &result) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve(const std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:39:78: warning: no return statement in function returning non-void [-Wreturn-type] 39 | virtual bool solve(const std::vector &assumption) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::vector&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:41:114: warning: no return statement in function returning non-void [-Wreturn-type] 41 | st std::vector &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::__cxx11::list&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:43:112: warning: no return statement in function returning non-void [-Wreturn-type] 43 | onst std::list &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::set&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:45:111: warning: no return statement in function returning non-void [-Wreturn-type] 45 | const std::set &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::getValue(unsigned int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:47:63: warning: no return statement in function returning non-void [-Wreturn-type] 47 | virtual bool getValue(unsigned int var) {assert(!"TODO");} // TODO: unsigned int | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::newVar(bool)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:49:73: warning: no return statement in function returning non-void [-Wreturn-type] 49 | virtual unsigned int newVar(bool decisionVar=true) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::sizeConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:51:58: warning: no return statement in function returning non-void [-Wreturn-type] 51 | virtual unsigned int sizeConflict() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual std::vector VirtualSAT::getConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:53:62: warning: no return statement in function returning non-void [-Wreturn-type] 53 | virtual std::vector getConflict() {assert(!"TODO");} | ^ In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/lazyvariable.h:10, from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/lazyvariable.cpp:1: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h: At global scope: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/../MaLib/src/coutUtil.h:229:10: warning: ‘void MaLib::{anonymous}::_toString(std::ostringstream&)’ defined but not used [-Wunused-function] 229 | void _toString(std::ostringstream &oss){ | ^~~~~~~~~ [ 83%] Building CXX object EvalMaxSAT/CMakeFiles/EvalMaxSAT.dir/src/virtualcard.cpp.o In file included from /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualcard.cpp:4: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual VirtualSAT* VirtualSAT::clone()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:23:50: warning: no return statement in function returning non-void [-Wreturn-type] 23 | virtual VirtualSAT* clone() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nVars()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:27:51: warning: no return statement in function returning non-void [-Wreturn-type] 27 | virtual unsigned int nVars() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nSoftVar()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:29:54: warning: no return statement in function returning non-void [-Wreturn-type] 29 | virtual unsigned int nSoftVar() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::nClauses()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:31:54: warning: no return statement in function returning non-void [-Wreturn-type] 31 | virtual unsigned int nClauses() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:33:43: warning: no return statement in function returning non-void [-Wreturn-type] 33 | virtual bool solve() {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::propagate(const std::vector&, std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:37:102: warning: no return statement in function returning non-void [-Wreturn-type] 37 | pagate(const std::vector &assum, std::vector &result) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::solve(const std::vector&)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:39:78: warning: no return statement in function returning non-void [-Wreturn-type] 39 | virtual bool solve(const std::vector &assumption) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::vector&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:41:114: warning: no return statement in function returning non-void [-Wreturn-type] 41 | st std::vector &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::__cxx11::list&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:43:112: warning: no return statement in function returning non-void [-Wreturn-type] 43 | onst std::list &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual int VirtualSAT::solveLimited(const std::set&, int, int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:45:111: warning: no return statement in function returning non-void [-Wreturn-type] 45 | const std::set &assumption, int confBudget, int except=0) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual bool VirtualSAT::getValue(unsigned int)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:47:63: warning: no return statement in function returning non-void [-Wreturn-type] 47 | virtual bool getValue(unsigned int var) {assert(!"TODO");} // TODO: unsigned int | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::newVar(bool)’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:49:73: warning: no return statement in function returning non-void [-Wreturn-type] 49 | virtual unsigned int newVar(bool decisionVar=true) {assert(!"TODO");} | ^ /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h: In member function ‘virtual unsigned int VirtualSAT::sizeConflict()’: /home/mfan/EvalMaxSAT/lib/EvalMaxSAT/src/virtualsat.h:51:58: warning: no return statement in function returning non-void [-Wreturn-type] ```