Incorrect `buildReason` leads to "Critical error: bad learnt clause."

[lucidliy]

Hello! I am implementing a new theory on top of MonoSAT, but MonoSAT sometimes crashes.

The exception is thrown by lbool Solver::search(int nof_conflicts) from Solver.cc.

if(value(learnt_clause[0]) == l_Undef){
    uncheckedEnqueue(learnt_clause[0], cr);
}else{
    assert(S);
    if(!S){
        throw std::runtime_error("Critical error: bad learnt clause.");
        //throw std::runtime_error("Critical error: bad learnt clause. Aborting\n");
    }
    //...
}

My understanding

It shows that the error occurs because learnt_clause[0] has been assigned to true or false. learnt_clause was generated by calling the analyze method.

learnt_clause.clear();
analyze(confl, learnt_clause, backtrack_level);

In the analyze method, the sat solver can interact with theory solvers through calling constructReason(p) and then the buildReason method of each theory solver will be called.

So according to my understanding, the crash happens because of the buildReason method of my theory solver. However, I have no idea of how to implement it.

void buildReason(Lit p, vec<Lit> &reason, CRef reason_marker) override {

}

My confusions

From my understanding, conflict has been constructed during propagation. The propagateTheory method already returns a conflict to the sat solver and it is added as a clause right after the propagation. So, why buildReason is needed? or how should I properly implement it?

Specifically, the following points confuse me:

1. What is difference between the confl returned by propagateTheory and the learnt_clause returned by analyze?
2. the buildReason method needs a Lit parameter p. What is the relation of the reason (what I need to return) and the literal p?
3. How the literal p is selected? I know the answer is in the analyze method but I can't understand the code.
4. How learnt_clause is generated? Why learnt_clause[0] should be l_Undef?

MonoSAT is an amazing piece of software. Looking forward to learning from you. Thank you!