text: /*++
  Copyright (c) 2020 Microsoft Corporation
  
  Module Name:
  
      q_clause.h
  
  Abstract:
  
      Literals, clauses, justifications for quantifier instantiation
  
  Author:
  
      Nikolaj Bjorner (nbjorner) 2021-01-24
  
  --*/
  #pragma once
  
  #include "util/dlist.h"
  #include "ast/ast.h"
  #include "ast/quantifier_stat.h"
  #include "ast/euf/euf_enode.h"
  #include "sat/smt/euf_solver.h"
  
  namespace q {
  
      struct lit {
          expr_ref lhs;
          expr_ref rhs;
          bool     sign;
          lit(expr_ref const& lhs, expr_ref const& rhs, bool sign):
              lhs(lhs), rhs(rhs), sign(sign) {
              SASSERT(!rhs.m().is_false(rhs) || !sign);
          }
          std::ostream& display(std::ostream& out) const;
      };
  
      struct binding : public dll_base<binding> {
          app*               m_pattern;
          unsigned           m_max_generation;
          unsigned           m_min_top_generation;
          unsigned           m_max_top_generation;
          euf::enode*        m_nodes[0];
  
          binding(app* pat, unsigned max_generation, unsigned min_top, unsigned max_top):
              m_pattern(pat),
              m_max_generation(max_generation),
              m_min_top_generation(min_top),
              m_max_top_generation(max_top) {}
  
          euf::enode* const* nodes() { return m_nodes; }
  
          euf::enode* operator[](unsigned i) const { return m_nodes[i]; }
  
          std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const;
      };
  
      struct clause {
          unsigned            m_index;
          vector<lit>         m_lits;
          quantifier_ref      m_q;
          unsigned            m_watch = 0;
          sat::literal        m_literal = sat::null_literal;
          q::quantifier_stat* m_stat = nullptr;
          binding*            m_bindings = nullptr;
  
  
          clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
  
          std::ostream& display(euf::solver& ctx, std::ostream& out) const;
          lit const& operator[](unsigned i) const { return m_lits[i]; }
          lit& operator[](unsigned i) { return m_lits[i]; }
          unsigned size() const { return m_lits.size(); }
          unsigned num_decls() const { return m_q->get_num_decls(); }
          unsigned index() const { return m_index; }
          quantifier* q() const { return m_q; }
      };
  
      struct justification {
          expr*     m_lhs, *m_rhs;
          bool      m_sign;
          unsigned  m_num_ev;
          euf::enode_pair* m_evidence;
          clause&   m_clause;
          euf::enode* const* m_binding;
          justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev):
              m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {}
          sat::ext_constraint_idx to_index() const { 
              return sat::constraint_base::mem2base(this); 
          }
          static justification& from_index(size_t idx) {
              return *reinterpret_cast<justification*>(sat::constraint_base::from_index(idx)->mem());
          }
          static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); }
      };
  
  }
  