void context::display_literal_info(std::ostream & out, literal l) const {
     l.display_compact(out, m_bool_var2expr.c_ptr());
     if (l.sign())
         out << "  (not " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << ") ";
     else
         out << "  " << mk_bounded_pp(bool_var2expr(l.var()), m_manager, 10) << " ";
     out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
 }

 bool context::check_watch_list(literal l) const {
     watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]);
     l.neg();
     watch_list::clause_iterator it  = wl.begin_clause();
     watch_list::clause_iterator end = wl.end_clause();
     for (; it != end; ++it) {
         clause * cls = *it;
         TRACE("watch_list", tout << "l: "; display_literal(tout, l); tout << "\n";
               display_clause(tout, cls); tout << "\n";);
         SASSERT(l == cls->get_literal(0) || l == cls->get_literal(1));
     }

 void context::display_watch_list(std::ostream & out, literal l) const {
     display_literal(out, l); out << " watch_list:\n";
     watch_list & wl = const_cast<watch_list &>(m_watches[l.index()]);
     watch_list::clause_iterator it  = wl.begin_clause();
     watch_list::clause_iterator end = wl.end_clause();
     for (; it != end; ++it) {
         display_clause(out, *it); out << "\n";
     }
 }

 void superposition::insert_p(clause * cls, literal & l, unsigned i) {
     l.set_p_indexed(true);
     expr * atom = l.atom();
     if (!m_manager.is_eq(atom))
         return;
     if (l.is_oriented())
         insert_p(cls, l.is_left() ? l.lhs() : l.rhs(), i);
     else {
         insert_p(cls, l.lhs(), i);
         insert_p(cls, l.rhs(), i);
     }
 }

 /**
    \brief Return true if l is a maximal selected literal in the clause, given a substitution s.
    
    s(l) is considered maximal selected literal if there is no
    selected literal l' in the clause such s(l') is greater than s(l).
 */
 bool clause::is_sel_maximal(order & o, literal const & l, unsigned offset, substitution * s) const {
     if (!l.is_selected())
         return false;
     unsigned num_lits = get_num_literals();
     for (unsigned i = 0; i < num_lits; i++) {
         literal const & l_prime = m_lits[i];
         if (l != l_prime && l_prime.is_selected() && greater(o, l_prime, l, offset, s))
             return false;
     }
     return true;
 }

 void superposition::insert_r(clause * cls, literal & l, unsigned i) {
     l.set_r_indexed(true);
     expr * atom = l.atom();
     if (m_manager.is_eq(atom)) {
         expr * lhs = l.lhs();
         expr * rhs = l.rhs();
         if (l.is_oriented()) {
             bool left = true;
             if (!l.is_left()) {
                 left  = false;
                 std::swap(lhs, rhs);
             }
             insert_r(cls, lhs, i, left);
         }
         else {
             insert_r(cls, lhs, i, true);
             insert_r(cls, rhs, i, false);
         }
     }
     else {
         insert_r(cls, atom, i, false);
     }
     m_subst.reserve_vars(m_r.get_approx_num_regs());
 }

 inline literal norm(literal_vector const & roots, literal l) {
     if (l.sign())
         return ~roots[l.var()];
     else
         return roots[l.var()];
 }

 literal(literal<U, Domain> const &u)
   : base_type(terminal_type::make(u.get()))
 {}

void repr_printer::operator()(const literal &n) {
    print_name("Literal", n.id());
}

 bool operator()(literal const & l1, literal const & l2) const {
     if (l1.is_ground() > l2.is_ground())
         return true;
     if (l1.is_ground() != l2.is_ground())
         return false;
     if (l1.get_approx_depth() > l2.get_approx_depth())
         return true;
     if (l1.get_approx_depth() != l2.get_approx_depth())
         return false;
     if (l1.get_approx_sym_count() > l2.get_approx_sym_count())
         return true;
     if (l1.get_approx_sym_count() != l2.get_approx_sym_count())
         return false;
     if (l1.get_approx_const_count() > l2.get_approx_const_count())
         return true;
     if (l1.get_approx_const_count() != l2.get_approx_const_count())
         return false;
     return l1.get_id() < l2.get_id();
 }