sat-solver常见编译错误
作者:互联网
1.MapleCOMSPS_LRB_VSIDS
1 |
/cygdrive/d/studySAT2022_06/MapleCOMSPS_LRB_VSIDS_no_drup/MapleCOMSPS_LRB_VSIDS/simp/Main.cc:43: undefined reference to `Minisat::memUsedPeak()' |
改正: 在main.c文件中mem_used的赋值将换为确定值,注释掉memUsedPeak()。 void printStats(Solver& solver) 。。。。。。 } |
|
2 |
error: ‘fwrite_unlocked’ was not declared in this scope; did you mean ‘_fwrite_unlocked_r’? |
改正: 在solver.h文件中将函数fwrite_unlocked做替换为fwrite. static inline void binDRUP_flush(FILE* drup_file) { |
|
3 |
/MapleCOMSPS_LRB_VSIDS_no_drup/MapleCOMSPS_LRB_VSIDS/simp/SimpSolver.cc:24:10: fatal error: m4ri/m4ri.h: No such file or directory |
改正: 该版本在SimpSolver.cc中用到头文件定义了以下函数: bool SimpSolver::gaussElim(); bool SimpSolver::performGaussElim(vec<XorScc*>& xor_sccs); 可以将这两个函数在.h的声明和在.cc的定义代码注释掉,同时将其被调用的两处也注释掉。
也可以用2019年之后拓展版本的simp文件夹整体将早期版本simp文件夹做替换。 |
|
标签:LRB,solver,VSIDS,fwrite,unlocked,编译,drup,buf,sat 来源: https://www.cnblogs.com/yuweng1689/p/16396225.html