How to use the claripy.Not function in claripy

if s_stmt is not None:
            state.history.extend_actions(s_stmt.actions)

        # for the exits, put *not* taking the exit on the list of constraints so
        # that we can continue on. Otherwise, add the constraints
        if type(stmt) == pyvex.IRStmt.Exit:
            l.debug("%s adding conditional exit", self)

            # Produce our successor state!
            # Let SimSuccessors.add_successor handle the nitty gritty details
            exit_state = state.copy()
            successors.add_successor(exit_state, s_stmt.target, s_stmt.guard, s_stmt.jumpkind,
                                     exit_stmt_idx=state.scratch.stmt_idx, exit_ins_addr=state.scratch.ins_addr)

            # Do our bookkeeping on the continuing state
            cont_condition = claripy.Not(s_stmt.guard)
            state.add_constraints(cont_condition)
            state.scratch.guard = claripy.And(state.scratch.guard, cont_condition)

if type(src_block) is GraphRegion:
            return claripy.true

        last_stmt = self._get_last_statement(src_block)

        if last_stmt is None:
            return claripy.true
        if type(last_stmt) is ailment.Stmt.Jump:
            return claripy.true
        if type(last_stmt) is ailment.Stmt.ConditionalJump:
            bool_var = self._bool_variable_from_ail_condition(last_stmt.condition)
            if last_stmt.true_target.value == dst_block.addr:
                return bool_var
            else:
                return claripy.Not(bool_var)

        return claripy.true

            'Not': lambda expr, conv: claripy.Not(conv(expr.operand)),
            'Xor': lambda expr, conv: conv(expr.operands[0]) ^ conv(expr.operands[1]),

while True:
            for node_0 in seq.nodes:
                if not type(node_0) is CodeNode:
                    continue
                rcond_0 = node_0.reaching_condition
                if rcond_0 is None:
                    continue
                for node_1 in seq.nodes:
                    if not type(node_1) is CodeNode:
                        continue
                    if node_0 is node_1:
                        continue
                    rcond_1 = node_1.reaching_condition
                    if rcond_1 is None:
                        continue
                    cond_ = claripy.simplify(claripy.Not(rcond_0) == rcond_1)
                    if claripy.is_true(cond_):
                        # node_0 and node_1 should be structured using an if-then-else
                        self._make_ite(seq, node_0, node_1)
                        break
            else:
                break

        # make all conditionally-reachable nodes ConditionNodes
        for i in range(len(seq.nodes)):
            node = seq.nodes[i]
            if node.reaching_condition is not None and not claripy.is_true(node.reaching_condition):
                if isinstance(node.node, ConditionalBreakNode):
                    # Put conditions together and simplify them
                    cond = claripy.And(node.reaching_condition, self._bool_variable_from_ail_condition(node.node.condition))
                    new_node = CodeNode(ConditionalBreakNode(node.node.addr, cond, node.node.target), None)
                else:

else:
                    exit_state = state.copy()
                    cont_state = state
            else:
                exit_state = state.copy()
                cont_state = state

            if exit_state is not None:
                successors.add_successor(exit_state, target, guard, jumpkind,
                                         exit_stmt_idx=state.scratch.stmt_idx, exit_ins_addr=state.scratch.ins_addr)

            if cont_state is None:
                return False

            # Do our bookkeeping on the continuing state
            cont_condition = claripy.Not(guard)
            cont_state.add_constraints(cont_condition)
            cont_state.scratch.guard = claripy.And(cont_state.scratch.guard, cont_condition)

        return True

cont_state = None
            exit_state = None

            if o.COPY_STATES not in state.options:
                # very special logic to try to minimize copies
                # first, check if this branch is impossible
                if guard.is_false():
                    cont_state = state
                elif o.LAZY_SOLVES not in state.options and not state.solver.satisfiable(extra_constraints=(guard,)):
                    cont_state = state

                # then, check if it's impossible to continue from this branch
                elif guard.is_true():
                    exit_state = state
                elif o.LAZY_SOLVES not in state.options and not state.solver.satisfiable(extra_constraints=(claripy.Not(guard),)):
                    exit_state = state
                else:
                    exit_state = state.copy()
                    cont_state = state
            else:
                exit_state = state.copy()
                cont_state = state

            if exit_state is not None:
                successors.add_successor(exit_state, target, guard, jumpkind,
                                         exit_stmt_idx=state.scratch.stmt_idx, exit_ins_addr=state.scratch.ins_addr)

            if cont_state is None:
                return False

            # Do our bookkeeping on the continuing state

def excavate_if(f):
    if not isinstance(f,claripy.ast.Base):
        return [([],f)]
    fs = [([],f)]
    prev = 0
    while len(fs) > prev:
        prev = len(fs)
        new = []
        for e in fs:
            ee = e[1].ite_excavated
            if ee.op == 'If':
                if is_state_merge_condition(ee.args[0]):
                    new += [(e[0]+[ee.args[0]],ee.args[1]),(e[0]+[claripy.Not(ee.args[0])],ee.args[2])]
                else:
                    #TODO: What can we do here? Maybe a deeper excavation..
                    new.append(e)
            else:
                new.append(e)
        fs = new
    return fs

if not_a.variables == or_arg1.args[0].variables:
            solver.add(not_a == or_arg1.args[0])
            not_b = or_arg1.args[1]
        elif not_a.variables == or_arg1.args[1].variables:
            solver.add(not_a == or_arg1.args[1])
            not_b = or_arg1.args[0]
        else:
            return cond

        if not solver.satisfiable():
            # found it!
            b = claripy.Not(not_b)
            a = claripy.Not(not_a)
            if len(cond.args) <= 2:
                return claripy.Not(claripy.And(a, b))
            else:
                return claripy.Or(claripy.Not(claripy.And(a, b)), *cond.args[2:])
        else:
            return cond