sat-solver常见编译错误

2022-06-21 11:33:46 阅读：176 来源： 互联网

标签：LRB solver VSIDS fwrite unlocked 编译 drup buf sat

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()' collect2: error: ld returned 1 exit status
	改正：在main.c文件中mem_used的赋值将换为确定值，注释掉memUsedPeak()。 void printStats(Solver& solver) { double cpu_time = cpuTime(); double mem_used = 1; //memUsedPeak(); 。。。。。。 }

2	error: ‘fwrite_unlocked’ was not declared in this scope; did you mean ‘_fwrite_unlocked_r’? 375 \| fwrite_unlocked(drup_buf, sizeof(unsigned char), buf_len, drup_file);
	改正：在solver.h文件中将函数fwrite_unlocked做替换为fwrite. static inline void binDRUP_flush(FILE* drup_file) { fwrite(drup_buf, sizeof(unsigned char), buf_len, drup_file); //fwrite_unlocked(drup_buf, sizeof(unsigned char), buf_len, drup_file); buf_ptr = drup_buf; buf_len = 0; }

3	/MapleCOMSPS_LRB_VSIDS_no_drup/MapleCOMSPS_LRB_VSIDS/simp/SimpSolver.cc:24:10: fatal error: m4ri/m4ri.h: No such file or directory 24 \| #include <m4ri/m4ri.h>
	改正：该版本在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

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

1	/cygdrive/d/studySAT2022_06/MapleCOMSPS_LRB_VSIDS_no_drup/MapleCOMSPS_LRB_VSIDS/simp/Main.cc:43: undefined reference to `Minisat::memUsedPeak()' collect2: error: ld returned 1 exit status
	改正：在main.c文件中mem_used的赋值将换为确定值，注释掉memUsedPeak()。 void printStats(Solver& solver) { double cpu_time = cpuTime(); double mem_used = 1; //memUsedPeak(); 。。。。。。 }

2	error: ‘fwrite_unlocked’ was not declared in this scope; did you mean ‘_fwrite_unlocked_r’? 375 \| fwrite_unlocked(drup_buf, sizeof(unsigned char), buf_len, drup_file);
	改正：在solver.h文件中将函数fwrite_unlocked做替换为fwrite. static inline void binDRUP_flush(FILE* drup_file) { fwrite(drup_buf, sizeof(unsigned char), buf_len, drup_file); //fwrite_unlocked(drup_buf, sizeof(unsigned char), buf_len, drup_file); buf_ptr = drup_buf; buf_len = 0; }

3	/MapleCOMSPS_LRB_VSIDS_no_drup/MapleCOMSPS_LRB_VSIDS/simp/SimpSolver.cc:24:10: fatal error: m4ri/m4ri.h: No such file or directory 24 \| #include <m4ri/m4ri.h>
	改正：该版本在SimpSolver.cc中用到头文件定义了以下函数： bool SimpSolver::gaussElim()； bool SimpSolver::performGaussElim(vec<XorScc>& xor_sccs)；可以将这两个函数在.h的声明和在.cc的定义代码注释掉，同时将其被调用的两处也注释掉。也可以用2019年之后拓展版本的simp文件夹整体将早期版本simp文件夹做替换*。

ICode9

sat-solver常见编译错误