sat-solver常见编译错误

/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();

    。。。。。。

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;
}

/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

改正：

该版本在SimpSolver.cc中用到头文件定义了以下函数：

    bool SimpSolver::gaussElim()；

    bool SimpSolver::performGaussElim(vec& xor_sccs)；

可以将这两个函数在.h的声明和在.cc的定义代码注释掉，同时将其被调用的两处也注释掉。

也可以用2019年之后拓展版本的simp文件夹整体将早期版本simp文件夹做替换。

error: friend declaration of ‘Minisat::Lit Minisat::mkLit(Minisat::Var, bool)’ specifies default arguments and isn’t the only declaration [-fpermissive]
60 | inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }

struct Lit {
    int x;

    // Use this as a constructor:
    friend Lit mkLit(Var var, bool sign = false);  //更正：将红色代码去掉

    bool operator == (Lit p) const { return x == p.x; }
    bool operator != (Lit p) const { return x != p.x; }
    bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
};

inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } //更正：红色代码添加

Linking: minisat ( /cygdrive/d/studySAT2022_06/MapleCOMSPS_CHB_VSIDS_no_drup/MapleCOMSPS_CHB_VSIDS/simp/Main.o /cygdrive/d/studySAT2022_06/MapleCOMSPS_CHB_VSIDS_no_drup/MapleCOMSPS_CHB_VSIDS/simp/SimpSolver.o utils/Options.o utils/System.o core/Solver.o )
/usr/lib/gcc/x86_64-pc-cygwin/11/../../../../x86_64-pc-cygwin/bin/ld: cannot find -lm4ri
collect2: error: ld returned 1 exit status
make: *** [..//mtl/template.mk:77: minisat] Error 1