/*
 This file is part of DepQBF.

 DepQBF, a solver for quantified boolean formulae (QBF).	
 Copyright 2010 Florian Lonsing, Johannes Kepler University, Linz, Austria.

 See also http://fmv.jku.at/depqbf for further information.

 DepQBF is free software: you can redistribute it and/or modify
 it under the terms of the GNU General Public License as published by
 the Free Software Foundation, either version 3 of the License, or (at
 your option) any later version.

 DepQBF is distributed in the hope that it will be useful, but
 WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 General Public License for more details.

 You should have received a copy of the GNU General Public License
 along with DepQBF.  If not, see <http://www.gnu.org/licenses/>.
*/

#ifndef QDPLL_PCNF_H_INCLUDED
#define QDPLL_PCNF_H_INCLUDED

#include <limits.h>
#include "qdpll.h"
#include "qdpll_stack.h"
#include "qdpll_dep_man_qdag_types.h"
#include "qdpll_config.h"

typedef struct QDPLLPCNF QDPLLPCNF;
typedef struct Scope Scope;
typedef struct Var Var;
typedef struct Constraint Constraint;

#define QDPLL_DECLARE_DLIST(name, type)					\
  struct name ## List {type * first; type * last; unsigned int cnt;};	\
  typedef struct name ## List name ## List				\

#define QDPLL_DECLARE_DLINK(name, type)			\
  struct name ## Link {type * prev; type * next;};	\
  typedef struct name ## Link name ## Link		\

QDPLL_DECLARE_DLINK (Scope, Scope);
QDPLL_DECLARE_DLIST (Scope, Scope);
QDPLL_DECLARE_DLINK (Constraint, Constraint);
QDPLL_DECLARE_DLIST (Constraint, Constraint);

struct OccLink
{
  Constraint *prev;
  unsigned int poffset;
  Constraint *next;
  unsigned int noffset;
};

typedef struct OccLink OccLink;

struct OccList
{
  Constraint *first;
  unsigned int foffset;
  Constraint *last;
  unsigned int loffset;
  unsigned int cnt;
};

typedef struct OccList OccList;

/* Iterator for traversing occurrence lists. */

struct OccListIterator
{
  Constraint *cur;
  unsigned int offset;
  OccLink *occ_link;
};

typedef struct OccListIterator OccListIterator;

#define OLITER_INIT(it, c, o, lit)					\
  do {									\
    (it).cur = (c);							\
    (it).offset = (o);							\
    if ((it).cur)							\
      {									\
	assert (o < c->num_lits);					\
	assert (c->lits[o] == lit);					\
	(it).occ_link = &((it).cur->occ_link[(it).offset]);		\
      }									\
    else								\
      (it).occ_link = 0;						\
  } while (0)

#define OLITER_NEXT(it, lit)					\
  do {								\
    assert ((it).cur);						\
    assert ((it).occ_link);					\
    assert ((it).offset < (it).cur->num_lits);			\
    assert ((it).offset < (it).cur->num_lits);			\
    (it).cur = (it).occ_link->next;				\
    (it).offset = (it).occ_link->noffset;			\
    if ((it).cur)						\
      {									\
	assert((it).offset < (it).cur->num_lits);			\
	assert((it).cur->lits[(it).offset] == lit);		\
	(it).occ_link = &((it).cur->occ_link[(it).offset]);	\
      }								\
    else							\
      (it).occ_link = 0;					\
  } while (0)							\

#define OLITER_CUR(it) ((it).cur)


QDPLL_DECLARE_STACK (ConstraintPtr, Constraint *);
QDPLL_DECLARE_STACK (VarPtr, Var *);
QDPLL_DECLARE_STACK (VarID, VarID);
QDPLL_DECLARE_STACK (LitID, LitID);

typedef unsigned int QDPLLVarMode;
#define QDPLL_VARMODE_UNDEF 0
#define QDPLL_VARMODE_UNIT 1
#define QDPLL_VARMODE_PURE 2
#define QDPLL_VARMODE_LBRANCH 3
#define QDPLL_VARMODE_RBRANCH 4

struct QDPLLPCNF
{
  ScopeList scopes;
  VarID max_declared_var_id;
  VarID size_vars;
  VarID used_vars;
  Var *vars;
  ConstraintList clauses;
  ConstraintList learnt_clauses;
  ConstraintList learnt_cubes;
};

struct Scope
{
  QDPLLQuantifierType type;
  unsigned int nesting;
  VarIDStack vars;
  ScopeLink link;
  /* Data for representing QDAG. List of equivalence classes. */
  QDAGVarList classes[2];
};

struct Var
{
  VarID id;
  unsigned int decision_level;
  unsigned int trail_pos;
  QDPLLAssignment assignment:2;
  QDPLLVarMode mode:3;
  unsigned int mark0:1;
  unsigned int mark1:1;
  unsigned int mark_propagated:1;
  unsigned int mark_is_candidate:1;
  unsigned int mark_is_neg_watching_cube:1;
  unsigned int mark_is_pos_watching_cube:1;
  unsigned int mark_reduce_cover:1;

  unsigned int mark_learn0:1;
  unsigned int mark_learn1:1;
  unsigned int mark_res_cand:1;
#ifndef NDEBUG
  unsigned int mark_clauses_disabled:1;
#endif
  unsigned int choose_var_class_collected:1;

  VarPtrStack type_red_members;

  Constraint *antecedent;

  OccList neg_occ_cubes;
  OccList pos_occ_cubes;
  OccList neg_occ_clauses;
  OccList pos_occ_clauses;

  /* Clause watching for pure literal detection.  The watcher (if any)
     is always the first clause on occurrence stack.  Signed IDs of
     variables which must find new pos./neg. watcher after assignment.
     Entries must be deleted if a variable has found a new watched
     clause.  */
  LitIDStack pos_notify_clause_watchers;
  LitIDStack neg_notify_clause_watchers;

  /* For each literal 'l' in a clause watched by e.g. 'x', the
     position of x's entry in l's notify-list is maintained. Two lists
     of positions are needed, since there are two watched clauses: one
     positive and one negative. */
  VarIDStack pos_offset_in_notify_list;
  VarIDStack neg_offset_in_notify_list;

  /* For each entry 'l' in a notify-list of e.g. 'x', the position of
     'x' in the clause (containing both x and l) watched by 'l' is
     maintained. */
  VarIDStack pos_offset_in_watched_clause;
  VarIDStack neg_offset_in_watched_clause;

  /* Literal watching for unit literal detection.  Two literals
     watched in each clause: EE or AE.  Notification lists contain
     pointers to clauses where one of the two watchers needs update
     after assignment of variable.  */
  ConstraintPtrStack pos_notify_lit_watchers;
  ConstraintPtrStack neg_notify_lit_watchers;

  Scope *scope;
  unsigned int priority_pos;
  double priority;
  QDPLLAssignment cached_assignment:2;

  /* Data for representing QDAG. */
  QDAG qdag;
};


struct Constraint
{
#ifndef NDEBUG
  unsigned int size_lits;
#endif
  unsigned int num_lits:(sizeof (unsigned int) * 8 - 4);
  unsigned int is_cube:1;
  unsigned int learnt:1;
  unsigned int disabled:1;	/* Marks clauses to be ignored by dep-man. */
  unsigned int is_reason:1;
  /* Counting the number of times a constraint is watched by a
     variable. */
  unsigned int is_watched:(sizeof (unsigned int) * 8 - 1);
  unsigned int covered:1;
  unsigned int counted:1;
  unsigned int unit_cnt;
  unsigned int res_cnt;

  unsigned int dep_init_level;

  /* Link to next/prev constraint in list. */
  ConstraintLink link;

  /* For O(1)-notify list maintenance during literal watcher update,
     we store the position of a constraint in the notify lists of the watched
     literals. pos_in_notify_list[0] and [1] are the
     positions for the left and right watcher, respectively. */
  unsigned int offset_in_notify_list[2];
  unsigned int rwatcher_pos;	/* Position of right watched literal. */
  unsigned int lwatcher_pos;	/* Position of left watched literal. */
  /* List of ConstraintLinks that link occurrences of a literal. */
  OccLink *occ_link;
  LitID lits[];
};


#define QDPLL_LIT_NEG(lit) ((lit) < 0)
#define QDPLL_LIT_POS(lit) (!QDPLL_LIT_NEG((lit)))

#define LIT2VARID(lit) ((lit) < 0 ? -(lit) : (lit))
#define LIT2VARPTR(vars, lit) ((vars) + LIT2VARID(lit))
#define LIT2VAR(vars, lit) ((vars)[LIT2VARID(lit)])

#define VARID2VARPTR(vars, id) ((vars) + (id))
#define VARID2VAR(vars, lit) ((vars)[(id)])

#define QDPLL_DEFAULT_SCOPE_NESTING 0
#define QDPLL_SCOPE_EXISTS(s) ((s)->type == QDPLL_QTYPE_EXISTS)
#define QDPLL_SCOPE_FORALL(s) ((s)->type == QDPLL_QTYPE_FORALL)
#define QDPLL_VAR_EXISTS(v) (QDPLL_SCOPE_EXISTS((v)->scope))
#define QDPLL_VAR_FORALL(v) (QDPLL_SCOPE_FORALL((v)->scope))

#define QDPLL_VAR_POS_MARK(v) ((v)->mark0 = 1)
#define QDPLL_VAR_NEG_MARK(v) ((v)->mark1 = 1)
#define QDPLL_VAR_UNMARK(v) ((v)->mark0 = (v)->mark1 = 0)
#define QDPLL_VAR_POS_UNMARK(v) ((v)->mark0 = 0)
#define QDPLL_VAR_NEG_UNMARK(v) ((v)->mark1 = 0)
#define QDPLL_VAR_POS_MARKED(v) ((v)->mark0)
#define QDPLL_VAR_NEG_MARKED(v) ((v)->mark1)
#define QDPLL_VAR_MARKED(v) ((v)->mark0 || (v)->mark1)

#define QDPLL_VAR_ASSIGNED(v) ((v)->assignment)
#define QDPLL_VAR_ASSIGNED_TRUE(v) ((v)->assignment == QDPLL_ASSIGNMENT_TRUE)
#define QDPLL_VAR_ASSIGNED_FALSE(v) ((v)->assignment == QDPLL_ASSIGNMENT_FALSE)
#define QDPLL_VAR_ASSIGN_TRUE(v) ((v)->assignment = QDPLL_ASSIGNMENT_TRUE)
#define QDPLL_VAR_ASSIGN_FALSE(v) ((v)->assignment = QDPLL_ASSIGNMENT_FALSE)

#define QDPLL_INVALID_TRAIL_POS UINT_MAX
#define QDPLL_INVALID_PQUEUE_POS UINT_MAX
#define QDPLL_INVALID_WATCHER_POS UINT_MAX
#define QDPLL_WATCHER_SAT (UINT_MAX - 1)

#define QDPLL_VAR_HAS_NEG_OCC_CLAUSES(v) ((v)->neg_occ_clauses.first)
#define QDPLL_VAR_HAS_POS_OCC_CLAUSES(v) ((v)->pos_occ_clauses.first)
#define QDPLL_VAR_HAS_OCC_CLAUSES(v) (QDPLL_VAR_HAS_NEG_OCC_CLAUSES(v) || \
			       QDPLL_VAR_HAS_POS_OCC_CLAUSES(v))
#define QDPLL_VAR_HAS_NEG_OCC_CUBES(v) ((v)->neg_occ_cubes.first)
#define QDPLL_VAR_HAS_POS_OCC_CUBES(v) ((v)->pos_occ_cubes.first)
#define QDPLL_VAR_HAS_OCC_CUBES(v) (QDPLL_VAR_HAS_NEG_OCC_CUBES(v) || \
			       QDPLL_VAR_HAS_POS_OCC_CUBES(v))
#define QDPLL_VAR_HAS_NEG_OCCS(v) (QDPLL_VAR_HAS_NEG_OCC_CLAUSES(v) || \
			       QDPLL_VAR_HAS_NEG_OCC_CUBES(v))
#define QDPLL_VAR_HAS_POS_OCCS(v) (QDPLL_VAR_HAS_POS_OCC_CLAUSES(v) || \
			       QDPLL_VAR_HAS_POS_OCC_CUBES(v))
#define QDPLL_VAR_HAS_OCCS(v) (QDPLL_VAR_HAS_OCC_CLAUSES(v) || \
			       QDPLL_VAR_HAS_OCC_CUBES(v))
#define QDPLL_VAR_MARK_EXPORTED(v) ((v)->mark_exported = 1)
#define QDPLL_VAR_UNMARK_EXPORTED(v) ((v)->mark_exported = 0)
#define QDPLL_VAR_MARKED_EXPORTED(v) ((v)->mark_exported)
#define QDPLL_VAR_MARK_PROPAGATED(v) ((v)->mark_propagated = 1)
#define QDPLL_VAR_UNMARK_PROPAGATED(v) ((v)->mark_propagated = 0)
#define QDPLL_VAR_MARKED_PROPAGATED(v) ((v)->mark_propagated)

#endif