#if ! defined _pres_conj_h
#define _pres_conj_h 1

#include <limits.h>
#include <omega/pres_decl.h>
#include <omega/pres_logic.h>
#include <omega/pres_cnstr.h>

namespace omega {

//
// Conjunct
//
// About variables in Conjunct:
// All varaibles appear in exactly one declaration.
// All variables used in Conjunct are referenced in mappedVars.
// Wildcard variables are referenced both in mappedVars and in myLocals, 
//   since they are declared in the conjunct.
// All other variables are declared at the levels above.
// Column number is: 
//   in forwardingAddress in Problem if variablesInitialized is set, 
//   equal to position of Variable_ID in mappedVars list otherwise.
//

class Conjunct : public F_Declaration {
public:
  Constraint_Iterator constraints();
  Variable_ID_Tuple  *variables();
  EQ_Iterator         EQs();
  GEQ_Iterator        GEQs();
  inline int          n_EQs() { return problem->nEQs; }
  inline int          n_GEQs() { return problem->nGEQs; }

  void promise_that_ub_solutions_exist(Relation &R);

  inline Node_Type node_type() {return Op_Conjunct;}

  inline int is_true() {return problem->nEQs==0 && problem->nGEQs==0 
      && exact;}

  void query_difference(Variable_ID v1, Variable_ID v2,
                        coef_t &lowerBound, coef_t &upperBound, bool &guaranteed);
  void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound);
  coef_t query_variable_mod(Variable_ID v, coef_t factor);
  bool query_variable_used(Variable_ID v);

  int countNonzeros() const {
    int numberNZs;
    coef_t maxCoef, SumAbsCoef;
    problem->difficulty(numberNZs,maxCoef,SumAbsCoef);
    return numberNZs;
  }

  void difficulty(int &numberNZs, coef_t &maxCoef, coef_t &SumAbsCoef) const {
    problem->difficulty(numberNZs,maxCoef,SumAbsCoef);
  }

  int query_guaranteed_leading_0s() {
    count_leading_0s();
    return guaranteed_leading_0s;
  }

  int query_possible_leading_0s() {
    count_leading_0s();
    return possible_leading_0s;
  }

  int query_leading_dir() {
    count_leading_0s();
    return leading_dir;
  }

  void calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain);
  int max_ufs_arity_of_set();
  int max_ufs_arity_of_in();
  int max_ufs_arity_of_out();

  int rank();

  ~Conjunct();

  bool is_unknown() const;
  inline bool is_exact() const { return exact;}
  inline bool is_inexact() const { return !exact;}
  inline void make_inexact()   { exact=false;}
   

#if ! defined NDEBUG
  void     assert_leading_info();
#else
  void     assert_leading_info() {}
#endif


  // PRINTING FUNCTIONS
  void print(FILE *output_file);
  void prefix_print(FILE *output_file, int debug = 1);
  std::string print_to_string(int true_printed);
  std::string print_EQ_to_string(eqn *e) { return problem->print_EQ_to_string(e); }
  std::string print_GEQ_to_string(eqn *e) { return problem->print_GEQ_to_string(e); }
  std::string print_EQ_to_string(int e) 
  { return problem->print_EQ_to_string(&(problem->EQs[e])); }
  std::string print_GEQ_to_string(int e) 
  { return problem->print_GEQ_to_string(&(problem->GEQs[e])); }
  std::string print_term_to_string(eqn *e) { return problem->print_term_to_string(e,1); }
  std::string print_EQ_term_to_string(int e) 
  { return problem->print_term_to_string(&(problem->EQs[e]),1); }
  std::string print_GEQ_term_to_string(int e) 
  { return problem->print_term_to_string(&(problem->GEQs[e]),1); }
  std::string print_sub_to_string(int col) { return problem->print_sub_to_string(col); }

private:

  inline void interpret_unknown_as_true()   { exact=true;}

  friend Relation approx_closure(NOT_CONST Relation &r, int n);

  virtual Conjunct *really_conjunct();


  // create new constraints with all co-efficients 0
  // These are public in F_And, use them from there.
  EQ_Handle   add_stride(int step, int preserves_level = 0);
  EQ_Handle   add_EQ(int preserves_level = 0);
  GEQ_Handle  add_GEQ(int preserves_level = 0);
  EQ_Handle   add_EQ(const Constraint_Handle &c, int preserves_level = 0);
  GEQ_Handle  add_GEQ(const Constraint_Handle &c, int preserves_level = 0);

  friend class GEQ_Handle;
  friend class  EQ_Handle;
  friend class Sub_Handle;
  friend class Constraint_Handle;
  friend class Constraint_Iterator;
  friend class GEQ_Iterator;
  friend class  EQ_Iterator;
  friend class Sub_Iterator;
  friend class Constr_Vars_Iter;


  // FUNCTIONS HAVING TO DO WITH BUILDING FORMULAS/DNFs 
  bool     can_add_child();
  void remap();
  void beautify();
  DNF* DNFize();
  int priority();
  virtual Conjunct *find_available_conjunct();
  void finalize();

  friend class DNF;



  // CREATING CONJUNCTS
  Conjunct();
  Conjunct(Conjunct &);
  Conjunct(Formula *, Rel_Body *);

  friend class Formula; // add_conjunct (a private function) creates Conjuncts
  friend class F_Not;
  friend class F_Or;
  //   class F_And; is a friend below
  

  // VARIOUS FUNCTIONS TO CREATE / WORK WITH VARIABLES
  Variable_ID declare(Const_String s);
  Variable_ID declare();
  Variable_ID declare(Variable_ID v);  
  
  friend const char *get_var_name(unsigned int, void *);
  void push_exists(Variable_ID_Tuple &S);
  int  get_column(Variable_ID);
  int  find_column(Variable_ID);
  int  map_to_column(Variable_ID);
  void combine_columns();
  void reorder();
  void reorder_for_print(bool reverseOrder=false,
                         int first_pass_input=0,
                         int first_pass_output=0,
                         bool sort=false);

  friend void      remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel);

  void localize_var(Variable_ID D);


  // this creates variables in conjuncts for us:
  friend int       new_WC(Conjunct *nc, Problem *np);


  // UFS/LEADING ZEROS STUFF

  void move_UFS_to_input();

  void count_leading_0s();
  void invalidate_leading_info(int changed = -1);
  void enforce_leading_info(int guaranteed, int possible, int dir);

  void reverse_leading_dir_info();

 

  // CONJUNCT SPECIFIC STUFF

  void      rm_color_constrs();
  inline int N_protected() { return problem->safeVars; }


  void ordered_elimination(int symLen) { problem->ordered_elimination(symLen);}
  void convertEQstoGEQs(bool excludeStrides);

  int cost();
  
  inline Formula*  copy(Formula *parent, Rel_Body *reln)
  { return copy_conj_diff_relation(parent,reln); }
  Conjunct* copy_conj_diff_relation(Formula *parent, Rel_Body *reln);
  inline Conjunct* copy_conj_same_relation()
  { return copy_conj_diff_relation(&(parent()), relation()); }
  friend void internal_copy_conjunct(Conjunct* to, Conjunct* fr);
  friend void copy_constraint(Constraint_Handle H,
                              const Constraint_Handle initial);

#if defined STUDY_EVACUATIONS
  // The core function of "evac.c" does lots of work with conjuncts:
  friend bool check_subseq_n(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity, int n, bool allow_offset);
  friend void assert_subbed_syms(Conjunct *c);
  friend bool check_affine(Conjunct *d, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity);
  friend evac study(Conjunct *C, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity);
#endif

  // The relational ops tend to do lots of demented things to Conjuncts:
  friend class Rel_Body;
  friend_rel_ops;

  // F_And sometimes absorbs conjuncts
  friend class F_And;

  // Various DNFize functions also get a the problem:

  friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak);
  friend class F_Exists;

  // Substitutions are a wrapper around a low-level Problem operation
  friend class Substitutions;

  // private functions to call problem functions 
  int simplifyProblem();
  int simplifyProblem(int verify, int subs, int redundantElimination);
  int redSimplifyProblem(int effort, int computeGist);

  friend int       simplify_conj(Conjunct* conj, int ver_sim, int elim_red, int color);
  friend DNF*      negate_conj(Conjunct* conj);
  friend Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2,
                               Merge_Action action, Rel_Body *body = 0);
  friend void      copy_conj_header(Conjunct* to, Conjunct* fr);


  // === at last, the data ===

  Variable_ID_Tuple mappedVars;

  int              n_open_constraints;
  bool             cols_ordered;
  bool             simplified;
  bool             verified;

  int     guaranteed_leading_0s;  // -1 if unknown
  int     possible_leading_0s;  // -1 if unknown
  int     leading_dir; // 0 if unknown, else +/- 1
  int     leading_dir_valid_and_known();

  bool             exact;

  short     r_constrs; // are redundant constraints eliminated?
  Problem         *problem;

  bool is_compressed();
  void compress();
  void uncompress();

  friend class Comp_Problem;
  Comp_Problem    *comp_problem;
};


/* === Misc. problem manipulation utilities === */

const int CantBeNegated = INT_MAX-10;
const int AvoidNegating = INT_MAX-11;

void copy_column(Problem *tp,  int to_col,
                 Problem *fp,  int fr_col,
                 int start_EQ, int start_GEQ);
void zero_column(Problem *tp,  int to_col,
                 int start_EQ, int start_GEQ,
                 int no_EQs,   int no_GEQs);

} // namespace

#endif