def _simple_add_learned_clause(self, cls):
        cls_num = len(self.clauses)
        self.clauses.append(cls)

        for lit in cls:
            self.occurrence_count[lit] += 1

        self.sentinels[cls[0]].add(cls_num)
        self.sentinels[cls[-1]].add(cls_num)

        self.heur_clause_added(cls)
Add a new clause to the theory.
dataset/ETHPy150Open sympy/sympy/sympy/logic/algorithms/dpll2.py/SATSolver._simple_add_learned_clause