feat(util/scoped_vec): add operator[]
feat(realpaver/rp_constraint): implement 'used' field
feat(dsolver/icp_solver): support int type
feat(dsolver/icp_solver): implement simple build_explanation

For the literals in m_stack, we only choose the ones used by ICP solver
and return to NRA solver as an explanation for the conflict (UNSAT)