sat-encoder.cpp

/**
 * Encode link-grammar for solving with the SAT solver...
 */
#include <cstdlib>
#include <cstdio>
#include <iostream>
#include <vector>
#include <algorithm>
#include <iterator>
using std::cout;
using std::cerr;
using std::endl;
using std::vector;

extern "C" {
#include "sat-encoder.h"
}
#include "minisat/core/Solver.h"

#include "sat-encoder.hpp"
#include "variables.hpp"
#include "word-tag.hpp"
#include "matrix-ut.hpp"
#include "clock.hpp"
#include "fast-sprintf.hpp"

extern "C" {
#include "disjunct-utils.h"
#include "error.h"
#include "linkage/analyze-linkage.h" // for compute_link_names()
#include "linkage/linkage.h"
#include "linkage/sane.h"            // for sane_linkage_morphism()
#include "linkage/score.h"           // for linkage_score()
#include "parse/prune.h"             // for optional_gap_collapse()
#include "prepare/build-disjuncts.h" // for build_disjuncts_for_exp()
#include "post-process/post-process.h"
#include "post-process/pp-structures.h"
#include "tokenize/word-structures.h" // for Word_struct
#include "tokenize/tok-structures.h"  // got Gword internals
}

// Macro DEBUG_print is used to dump to stdout information while debugging
#ifdef SAT_DEBUG
#define DEBUG_print(x) (cout << x << endl)
#else
#define DEBUG_print(x)
#endif

#define D_SAT 5

// Convert a NULL C string pointer, for printing a possibly NULL string
#define N(s) ((s) ? (s) : "(null)")

/*-------------------------------------------------------------------------*
 *               C N F   C O N V E R S I O N                               *
 *-------------------------------------------------------------------------*/
void SATEncoder::generate_literal(Lit l) {
  vec<Lit> clause(1);
  clause[0] = l;
  add_clause(clause);
}

void SATEncoder::generate_and_definition(Lit lhs, vec<Lit>& rhs) {
  vec<Lit> clause(2);
  for (int i = 0; i < rhs.size(); i++) {
    clause[0] = ~lhs;
    clause[1] = rhs[i];
    add_clause(clause);
  }

  for (int i = 0; i < rhs.size(); i++) {
    clause[0] = ~rhs[i];
    clause[1] = lhs;
    add_clause(clause);
  }
}
void SATEncoder::generate_classical_and_definition(Lit lhs, vec<Lit>& rhs) {
  {
    vec<Lit> clause(2);
    for (int i = 0; i < rhs.size(); i++) {
      clause[0] = ~lhs;
      clause[1] = rhs[i];
      add_clause(clause);
    }
  }

  {
    vec<Lit> clause(rhs.size() + 1);
    for (int i = 0; i < rhs.size(); i++) {
      clause[i] = ~rhs[i];
    }
    clause[rhs.size()] = lhs;
    add_clause(clause);
  }
}

void SATEncoder::generate_or_definition(Lit lhs, vec<Lit>& rhs) {
  {
    vec<Lit> clause(2);
    for (int i = 0; i < rhs.size(); i++) {
      clause[0] = lhs;
      clause[1] = ~rhs[i];
      add_clause(clause);
    }
  }

  {
    vec<Lit> clause(rhs.size() + 1);
    for (int i = 0; i < rhs.size(); i++) {
      clause[i] = rhs[i];
    }
    clause[rhs.size()] = ~lhs;
    add_clause(clause);
  }
}

#if 0
void SATEncoder::generate_conditional_lr_implication_or_definition(Lit condition, Lit lhs, vec<Lit>& rhs) {
  {
    vec<Lit> clause(2);
    for (int i = 0; i < rhs.size(); i++) {
      clause[0] = lhs;
      clause[1] = ~rhs[i];
      add_clause(clause);
    }
  }

  {
    vec<Lit> clause(rhs.size() + 2);
    for (int i = 0; i < rhs.size(); i++) {
      clause[i] = rhs[i];
    }
    clause[rhs.size()] = ~lhs;
    clause[rhs.size()+1] = ~condition;
    add_clause(clause);
  }
}
#endif

#if 0
void SATEncoder::generate_conditional_lr_implication_or_definition(Lit condition1, Lit condition2, Lit lhs, vec<Lit>& rhs) {
  {
    vec<Lit> clause(2);
    for (int i = 0; i < rhs.size(); i++) {
      clause[0] = lhs;
      clause[1] = ~rhs[i];
      add_clause(clause);
    }
  }

  {
    vec<Lit> clause(rhs.size() + 3);
    for (int i = 0; i < rhs.size(); i++) {
      clause[i] = rhs[i];
    }
    clause[rhs.size()] = ~lhs;
    clause[rhs.size()+1] = ~condition1;
    clause[rhs.size()+2] = ~condition2;
    add_clause(clause);
  }
}
#endif

void SATEncoder::generate_xor_conditions(vec<Lit>& vect) {
  vec<Lit> clause(2);
  for (int i = 0; i < vect.size(); i++) {
    for (int j = i + 1; j < vect.size(); j++) {
      if (vect[i] == vect[j])
        continue;
      clause[0] = ~vect[i];
      clause[1] = ~vect[j];
      add_clause(clause);
    }
  }
}

void SATEncoder::generate_and(vec<Lit>& vect) {
  for (int i = 0; i < vect.size(); i++) {
    generate_literal(vect[i]);
  }
}


void SATEncoder::generate_or(vec<Lit>& vect) {
  add_clause(vect);
}

void SATEncoder::generate_equivalence_definition(Lit l1, Lit l2) {
  vec<Lit> clause(2);
  {
    clause[0] = ~l1;
    clause[1] = l2;
    add_clause(clause);
  }
  {
    clause[0] = l1;
    clause[1] = ~l2;
    add_clause(clause);
  }
}


/*-------------------------------------------------------------------------*
 *                          E N C O D I N G                                *
 *-------------------------------------------------------------------------*/
void SATEncoder::encode() {
    Clock clock;
    generate_satisfaction_conditions();
    clock.print_time(verbosity, "Generated satisfaction conditions");
    generate_linked_definitions();
    clock.print_time(verbosity, "Generated linked definitions");
    generate_planarity_conditions();
    clock.print_time(verbosity, "Generated planarity conditions");

#ifdef _CONNECTIVITY_
    generate_connectivity();
    clock.print_time(verbosity, "Generated connectivity");
#endif

    generate_encoding_specific_clauses();
    //clock.print_time(verbosity, "Generated encoding specific clauses");

    pp_prune();
    clock.print_time(verbosity, "PP pruned");
    power_prune();
    clock.print_time(verbosity, "Power pruned");

    _variables->setVariableParameters(_solver);
}



/*-------------------------------------------------------------------------*
 *                         W O R D - T A G S                               *
 *-------------------------------------------------------------------------*/
void SATEncoder::build_word_tags()
{
  char name[MAX_VARIABLE_NAME];
  name[0] = 'w';

  for (size_t w = 0; w < _sent->length; w++) {
    fast_sprintf(name+1, (int)w);
    // The SAT encoding word variables are set to be equal to the word numbers.
    Var var = _variables->string(name);
    assert((Var)w == var, "Word %zu: var %d", w, var);
  }

  for (size_t w = 0; w < _sent->length; w++) {
    _word_tags.push_back(WordTag(w, _variables, _sent, _opts));
    int dfs_position = 0;

    if (_sent->word[w].x == NULL) continue;

    bool join = _sent->word[w].x->next != NULL;
    Exp* exp = join ? join_alternatives(w) : _sent->word[w].x->exp;

#ifdef SAT_DEBUG
    cout << "Word ." << w << ".: " << N(_sent->word[w].unsplit_word) << endl;
    cout << lg_exp_stringify(exp);
    //prt_exp_mem(exp, 0);
    cout << endl;
#endif

    fast_sprintf(name+1, (int)w);
    bool leading_right = true;
    bool leading_left = true;
    std::vector<int> eps_right, eps_left;

    _word_tags[w].insert_connectors(exp, dfs_position, leading_right,
         leading_left, eps_right, eps_left, name, true, 0, NULL, _sent->word[w].x);
  }

  for (size_t wl = 0; wl < _sent->length - 1; wl++) {
    for (size_t wr = wl + 1; wr < _sent->length; wr++) {
      _word_tags[wl].add_matches_with_word(_word_tags[wr]);
    }
  }
}

#if 0
void SATEncoder::find_all_matches_between_words(size_t w1, size_t w2,
                                                std::vector<std::pair<const PositionConnector*, const PositionConnector*> >& matches) {
  const std::vector<PositionConnector>& w1_right = _word_tags[w1].get_right_connectors();
  std::vector<PositionConnector>::const_iterator i;
  for (i = w1_right.begin(); i != w1_right.end(); i++) {
    const std::vector<PositionConnector*>& w2_left_c = (*i).matches;
    std::vector<PositionConnector*>::const_iterator j;
    for (j = w2_left_c.begin(); j != w2_left_c.end(); j++) {
      if ((*j)->word == w2) {
        matches.push_back(std::pair<const PositionConnector*, const PositionConnector*>(&(*i), *j));
      }
    }
  }
}

bool SATEncoder::matches_in_interval(int wi, int pi, int l, int r) {
  for (int w = l; w < r; w++) {
    if (_word_tags[w].match_possible(wi, pi))
      return true;
  }
  return false;
}
#endif

/*-------------------------------------------------------------------------*
 *                     S A T I S F A C T I O N                             *
 *-------------------------------------------------------------------------*/

void SATEncoder::generate_satisfaction_conditions()
{
  char name[MAX_VARIABLE_NAME] = "w";

  for (size_t w = 0; w < _sent->length; w++) {

#ifdef SAT_DEBUG
    cout << "Word " << w << ": " << N(_sent->word[w].unsplit_word);
    if (_sent->word[w].optional) cout << " (optional)";
    cout << endl;
    cout << lg_exp_stringify(exp);
    cout << endl;
#endif

    fast_sprintf(name+1, w);

    if (_sent->word[w].optional)
      _variables->string(name);
    else
      determine_satisfaction(w, name);

    if (_sent->word[w].x == NULL) {
      if (!_sent->word[w].optional) {
        // Most probably everything got pruned. There will be no linkage.
        lgdebug(+D_SAT, "Word%zu '%s': Null X_node\n", w, _sent->word[w].unsplit_word);
        handle_null_expression(w);
      }
      continue; // No expression to handle.
    }

    bool join = _sent->word[w].x->next != NULL;
    Exp* exp = join ? join_alternatives(w) : _sent->word[w].x->exp;

    int dfs_position = 0;
    generate_satisfaction_for_expression(w, dfs_position, exp, name, 0);
  }
}


void SATEncoder::generate_satisfaction_for_expression(int w, int& dfs_position, Exp* e,
                                                      char* var, double parent_cost)
{
  Exp *opd;
  double total_cost = parent_cost + e->cost;

  if (e->type == CONNECTOR_type) {
    dfs_position++;

    generate_satisfaction_for_connector(w, dfs_position, e, var);

    if (total_cost > _cost_cutoff) {
      Lit lhs = Lit(_variables->string_cost(var, e->cost));
      generate_literal(~lhs);
    }
  } else {
    if (e->type == AND_type) {
      if (e->operand_first == NULL) {
        /* zeroary and */
        _variables->string_cost(var, e->cost);
        if (total_cost > _cost_cutoff) {
          generate_literal(~Lit(_variables->string_cost(var, e->cost)));
        }
      } else if (e->operand_first->operand_next == NULL) {
        /* unary and - skip */
        generate_satisfaction_for_expression(w, dfs_position, e->operand_first, var, total_cost);
      } else {
        /* n-ary and */
        int i;

        char new_var[MAX_VARIABLE_NAME];
        char* last_new_var = new_var;
        char* last_var = var;
        while((*last_new_var = *last_var)) {
          last_new_var++;
          last_var++;
        }

        vec<Lit> rhs;
        for (i = 0, opd=e->operand_first; opd!=NULL; opd=opd->operand_next, i++) {
          // sprintf(new_var, "%sc%d", var, i)
          char* s = last_new_var;
          *s++ = 'c';
          fast_sprintf(s, i);
          rhs.push(Lit(_variables->string(new_var)));
        }

        Lit lhs = Lit(_variables->string_cost(var, e->cost));
        generate_and_definition(lhs, rhs);

        /* Precedes */
        int dfs_position_tmp = dfs_position;
        for (opd = e->operand_first; opd->operand_next != NULL; opd = opd->operand_next) {
          Exp e_tmp, *e_rhs = &e_tmp;

          if (opd->operand_next->operand_next == NULL) {
            e_rhs = opd->operand_next;
          }
          else {
            // A workaround for issue #932:
            // Since the generated ordering conditions are not transitive
            // (see the example below), chains w/length > 2 miss needed
            // constrains.  So if the chain length > 2, refer to it as if
            // it is a 2-component chain (1st: l->e; 2nd: AND of the rest).
            //
            // Problem example:
            // Sentence: *I saw make some changes in the program
            // In word 2 we get here this subexpression (among many others):
            // e = (K+ & {[[@MV+]]} & (O*n+ or ())) // (& chain length = 3)
            // The generated constrains are only: (Decoding:
            // (word-number_connector-position_connector-string)_to-word-number)
            // Clause: -link_cw_(2_4_K)_6 -link_cw_(2_5_MV)_6
            // Clause: -link_cw_(2_5_MV)_6 -link_cw_(2_6_O*n)_4
            // (Reading: If MV connects from word 2 to word 6, then O*n
            // cannot connect from word 2 to word 4).
            // Clause: -link_cw_(2_5_MV)_6 -link_cw_(2_6_O*n)_5
            // However, the following, which are generated when the
            // chain length is limited to 2, are missing:
            // Clause: -link_cw_(2_4_K)_6 -link_cw_(2_6_O*n)_4
            // Clause: -link_cw_(2_4_K)_6 -link_cw_(2_6_O*n)_5
            // Clearly, they cannot be concluded transitively.
            e_rhs->type = AND_type;
            e_rhs->operand_first = opd->operand_next;
            e_rhs->cost = 0.0;
          };
          generate_conjunct_order_constraints(w, opd, e_rhs, dfs_position_tmp);
        }

        /* Recurse */
        for (i = 0, opd=e->operand_first; opd!=NULL; opd=opd->operand_next, i++) {
          // sprintf(new_var, "%sc%d", var, i)
          char* s = last_new_var;
          *s++ = 'c';
          fast_sprintf(s, i);

          /* if (i != 0) total_cost = 0; */ // This interferes with the cost cutoff
          generate_satisfaction_for_expression(w, dfs_position, opd, new_var, total_cost);
        }
      }
    } else if (e->type == OR_type) {
      if (e->operand_first == NULL) {
        /* zeroary or */
        cerr << "Zeroary OR" << endl;
        exit(EXIT_FAILURE);
      } else if (e->operand_first->operand_next == NULL) {
        /* unary or */
        generate_satisfaction_for_expression(w, dfs_position, e->operand_first, var, total_cost);
      } else {
        /* n-ary or */
        int i;

        char new_var[MAX_VARIABLE_NAME];
        char* last_new_var = new_var;
        char* last_var = var;
        while ((*last_new_var = *last_var)) {
          last_new_var++;
          last_var++;
        }

        vec<Lit> rhs;
        for (i = 0, opd=e->operand_first; opd!=NULL; opd=opd->operand_next, i++) {
          // sprintf(new_var, "%sc%d", var, i)
          char* s = last_new_var;
          *s++ = 'd';
          fast_sprintf(s, i);
          rhs.push(Lit(_variables->string(new_var)));
        }

        Lit lhs = Lit(_variables->string_cost(var, e->cost));
        generate_or_definition(lhs, rhs);
        generate_xor_conditions(rhs);

        /* Recurse */
        for (i = 0, opd=e->operand_first; opd!=NULL; opd=opd->operand_next, i++) {
          char* s = last_new_var;
          *s++ = 'd';
          fast_sprintf(s, i);

          generate_satisfaction_for_expression(w, dfs_position, opd, new_var, total_cost);
        }
      }
    }
  }
}

/**
 * Join all alternatives using an OR_type node.
 */
Exp* SATEncoder::join_alternatives(int w)
{
  Exp* exp = Exp_create(_sent->Exp_pool);
  exp->type = OR_type;
  exp->cost = 0.0;

  Exp** opdp = &exp->operand_first;

  for (X_node* x = _sent->word[w].x; x != NULL; x = x->next)
  {
    *opdp = Exp_create_dup(_sent->Exp_pool, x->exp);
    opdp = &(*opdp)->operand_next;
  }
  *opdp = NULL;

  return exp;
}

void SATEncoder::generate_link_cw_ordinary_definition(size_t wi, int pi,
                                                      Exp* e, size_t wj)
{
  const char* Ci = e->condesc->more->string;
  char dir = e->dir;
  double cost = e->cost;
  Lit lhs = Lit(_variables->link_cw(wj, wi, pi, Ci));
  vec<Lit> rhs;

  // Collect matches (wi, pi) with word wj
  std::vector<PositionConnector*>& matches = _word_tags[wi].get(pi)->matches;
  std::vector<PositionConnector*>::const_iterator i;
  for (i = matches.begin(); i != matches.end(); i++) {
    /* TODO: PositionConnector->matches[wj] */
    if ((*i)->word != wj)
      continue;

    if (dir == '+') {
      rhs.push(Lit(_variables->link_cost(wi, pi, Ci, e,
                                         (*i)->word, (*i)->position,
                                         connector_string(&(*i)->connector),
                                         (*i)->exp,
                                         cost + (*i)->cost)));
    } else if (dir == '-'){
      rhs.push(Lit(_variables->link((*i)->word, (*i)->position,
                                    connector_string(&(*i)->connector),
                                    (*i)->exp,
                                    wi, pi, Ci, e)));
    }
  }

  // Generate clauses
  DEBUG_print("--------- link_cw as ordinary down");
  generate_or_definition(lhs, rhs);
  generate_xor_conditions(rhs);
  DEBUG_print("--------- end link_cw as ordinary down");
}

/*--------------------------------------------------------------------------*
 *               C O N J U N C T    O R D E R I N G                         *
 *--------------------------------------------------------------------------*/
int SATEncoder::num_connectors(Exp* e)
{
  if (e->type == CONNECTOR_type)
    return 1;
  else {
    int num = 0;
    for (Exp* opd = e->operand_first; opd != NULL; opd = opd->operand_next) {
      num += num_connectors(opd);
    }
    return num;
  }
}

int SATEncoder::empty_connectors(Exp* e, char dir)
{
  if (e->type == CONNECTOR_type) {
    return e->dir != dir;
  } else if (e->type == OR_type) {
    for (Exp* opd = e->operand_first; opd != NULL; opd = opd->operand_next) {
      if (empty_connectors(opd, dir))
        return true;
    }
    return false;
  } else if (e->type == AND_type) {
    for (Exp* opd = e->operand_first; opd != NULL; opd = opd->operand_next) {
      if (!empty_connectors(opd, dir))
        return false;
    }
    return true;
  } else
    throw std::string("Unknown connector type");
}

#if 0
int SATEncoder::non_empty_connectors(Exp* e, char dir)
{
  if (e->type == CONNECTOR_type) {
    return e->dir == dir;
  } else if (e->type == OR_type) {
    for (E_list* l = e->operand_first; l != NULL; l = l->next) {
      if (non_empty_connectors(l->e, dir))
        return true;
    }
    return false;
  } else if (e->type == AND_type) {
    for (E_list* l = e->operand_first; l != NULL; l = l->next) {
      if (non_empty_connectors(l->e, dir))
        return true;
    }
    return false;
  } else
    throw std::string("Unknown connector type");
}
#endif

bool SATEncoder::trailing_connectors_and_aux(int w, Exp *opd, char dir, int& dfs_position,
                                             std::vector<PositionConnector*>& connectors)
{
  if (opd == NULL) {
    return true;
  } else {
    int dfs_position_in = dfs_position;
    dfs_position += num_connectors(opd);
    if (trailing_connectors_and_aux(w, opd->operand_next, dir, dfs_position, connectors)) {
      trailing_connectors(w, opd, dir, dfs_position_in, connectors);
    }
    return empty_connectors(opd, dir);
  }
}

void SATEncoder::trailing_connectors(int w, Exp* exp, char dir, int& dfs_position,
                                     std::vector<PositionConnector*>& connectors)
{
  if (exp->type == CONNECTOR_type) {
    dfs_position++;
    if (exp->dir == dir) {
      connectors.push_back(_word_tags[w].get(dfs_position));
    }
  } else if (exp->type == OR_type) {
    for (Exp* opd = exp->operand_first; opd != NULL; opd = opd->operand_next) {
      trailing_connectors(w, opd, dir, dfs_position, connectors);
    }
  } else if (exp->type == AND_type) {
    trailing_connectors_and_aux(w, exp->operand_first, dir, dfs_position, connectors);
  }
}

#if 0
void SATEncoder::certainly_non_trailing(int w, Exp* exp, char dir, int& dfs_position,
                                       std::vector<PositionConnector*>& connectors, bool has_right) {
  if (exp->type == CONNECTOR_type) {
    dfs_position++;
    if (exp->dir == dir && has_right) {
      connectors.push_back(_word_tags[w].get(dfs_position));
    }
  } else if (exp->type == OR_type) {
    for (E_list* l = exp->operand_first; l != NULL; l = l->next) {
      certainly_non_trailing(w, l->e, dir, dfs_position, connectors, has_right);
    }
  } else if (exp->type == AND_type) {
    if (has_right) {
      for (E_list* l = exp->operand_first; l != NULL; l = l->next) {
        certainly_non_trailing(w, l->e, dir, dfs_position, connectors, true);
      }
    } else {
      for (E_list* l = exp->operand_first; l != NULL; l = l->next) {
        has_right = false;
        for (E_list* m = l->next; m != NULL; m = m->next) {
          if (non_empty_connectors(m->e, dir) && !empty_connectors(m->e, dir)) {
            has_right = true;
            break;
          }
        }
        certainly_non_trailing(w, l->e, dir, dfs_position, connectors, has_right);
      }
    }
  }
}
#endif

void SATEncoder::leading_connectors(int w, Exp* exp, char dir, int& dfs_position, vector<PositionConnector*>& connectors) {
  if (exp->type == CONNECTOR_type) {
    dfs_position++;
    if (exp->dir == dir) {
      connectors.push_back(_word_tags[w].get(dfs_position));
    }
  } else if (exp->type == OR_type) {
    for (Exp* opd = exp->operand_first; opd != NULL; opd = opd->operand_next) {
      leading_connectors(w, opd, dir, dfs_position, connectors);
    }
  } else if (exp->type == AND_type) {
    Exp* opd;
    for (opd = exp->operand_first; opd != NULL; opd = opd->operand_next) {
      leading_connectors(w, opd, dir, dfs_position, connectors);
      if (!empty_connectors(opd, dir))
        break;
    }

    if (opd != NULL) {
      for (opd = opd->operand_next; opd != NULL; opd = opd->operand_next)
        dfs_position += num_connectors(opd);
    }
  }
}

void SATEncoder::generate_conjunct_order_constraints(int w, Exp *e1, Exp* e2, int& dfs_position) {
  DEBUG_print("----- conjunct order constraints");
  int dfs_position_e1 = dfs_position;
  std::vector<PositionConnector*> last_right_in_e1, first_right_in_e2;
  trailing_connectors(w, e1, '+', dfs_position_e1, last_right_in_e1);

  int dfs_position_e2 = dfs_position_e1;
  leading_connectors(w, e2, '+', dfs_position_e2, first_right_in_e2);

  vec<Lit> clause(2);

  if (!last_right_in_e1.empty() && !first_right_in_e2.empty()) {
    std::vector<PositionConnector*>::iterator i, j;
    for (i = last_right_in_e1.begin(); i != last_right_in_e1.end(); i++) {
      std::vector<PositionConnector*>& matches_e1 = (*i)->matches;

      for (j = first_right_in_e2.begin(); j != first_right_in_e2.end(); j++) {
        std::vector<PositionConnector*>& matches_e2 = (*j)->matches;
        std::vector<PositionConnector*>::const_iterator m1, m2;

        std::vector<int> mw1;
        for (m1 = matches_e1.begin(); m1 != matches_e1.end(); m1++) {
          if ((m1+1) == matches_e1.end() || (*m1)->word != (*(m1 + 1))->word)
            mw1.push_back((*m1)->word);
        }

        std::vector<int> mw2;
        for (m2 = matches_e2.begin(); m2 != matches_e2.end(); m2++) {
          if ((m2+1) == matches_e2.end() || (*m2)->word != (*(m2 + 1))->word)
            mw2.push_back((*m2)->word);
        }

        std::vector<int>::const_iterator mw1i, mw2i;
        for (mw1i = mw1.begin(); mw1i != mw1.end(); mw1i++) {
          for (mw2i = mw2.begin(); mw2i != mw2.end(); mw2i++) {
            if (*mw1i >= *mw2i) {
              clause[0] = ~Lit(_variables->link_cw(*mw1i, w, (*i)->position, connector_string(&(*i)->connector)));
              clause[1] = ~Lit(_variables->link_cw(*mw2i, w, (*j)->position, connector_string(&(*j)->connector)));
              add_clause(clause);
            }
          }
        }
      }
    }
  }

  DEBUG_print("----");
  dfs_position_e1 = dfs_position;
  std::vector<PositionConnector*> last_left_in_e1, first_left_in_e2;
  trailing_connectors(w, e1, '-', dfs_position_e1, last_left_in_e1);

  dfs_position_e2 = dfs_position_e1;
  leading_connectors(w, e2, '-', dfs_position_e2, first_left_in_e2);

  if (!last_left_in_e1.empty() && !first_left_in_e2.empty()) {
    std::vector<PositionConnector*>::iterator i, j;
    for (i = last_left_in_e1.begin(); i != last_left_in_e1.end(); i++) {
      std::vector<PositionConnector*>& matches_e1 = (*i)->matches;

      for (j = first_left_in_e2.begin(); j != first_left_in_e2.end(); j++) {
        std::vector<PositionConnector*>& matches_e2 = (*j)->matches;

        std::vector<PositionConnector*>::const_iterator m1, m2;


        std::vector<int> mw1;
        for (m1 = matches_e1.begin(); m1 != matches_e1.end(); m1++) {
          if ((m1+1) == matches_e1.end() || (*m1)->word != (*(m1 + 1))->word)
            mw1.push_back((*m1)->word);
        }

        std::vector<int> mw2;
        for (m2 = matches_e2.begin(); m2 != matches_e2.end(); m2++) {
          if ((m2+1) == matches_e2.end() || (*m2)->word != (*(m2 + 1))->word)
            mw2.push_back((*m2)->word);
        }

        std::vector<int>::const_iterator mw1i, mw2i;
        for (mw1i = mw1.begin(); mw1i != mw1.end(); mw1i++) {
          for (mw2i = mw2.begin(); mw2i != mw2.end(); mw2i++) {
            if (*mw1i <= *mw2i) {
              clause[0] = ~Lit(_variables->link_cw(*mw1i, w, (*i)->position, connector_string(&(*i)->connector)));
              clause[1] = ~Lit(_variables->link_cw(*mw2i, w, (*j)->position, connector_string(&(*j)->connector)));
              add_clause(clause);
            }
          }
        }
      }
    }
  }

  dfs_position = dfs_position_e1;

  DEBUG_print("---end conjunct order constraints");
}



/*--------------------------------------------------------------------------*
 *                       C O N N E C T I V I T Y                            *
 *--------------------------------------------------------------------------*/

#ifdef _CONNECTIVITY_
void SATEncoder::generate_connectivity() {
  for (int w = 1; w < _sent->length; w++) {
    if (!_linkage_possible(0, w)) {
      vec<Lit> clause;
      clause.push(~Lit(_variables->con(w, 1)));
      generate_and(clause);
    }
    else {
      generate_equivalence_definition(Lit(_variables->con(w, 1)),
                                      Lit(_variables->linked(0, w)));
    }
  }

  for (int d = 2; d < _sent->length; d++) {
    for (int w = 1; w < _sent->length; w++) {
      Lit lhs = Lit(_variables->con(w, d));

      vec<Lit> rhs;
      rhs.push(Lit(_variables->con(w, d-1)));
      for (int w1 = 1; w1 < _sent->length; w1++) {
        if (w == w1)
          continue;

        if (!_linkage_possible(std::min(w, w1), std::max(w, w1))) {
          continue;
        }
        rhs.push(Lit(_variables->l_con(w, w1, d-1)));
      }
      generate_or_definition(lhs, rhs);


      /* lc definitions*/
      for (int w1 = 1; w1 < _sent->length; w1++) {
        if (w == w1)
          continue;

        int mi = std::min(w, w1), ma = std::max(w, w1);
        if (!_linked_possible(mi, ma))
          continue;

        Lit lhs = Lit(_variables->l_con(w, w1, d-1));
        vec<Lit> rhs(2);
        rhs[0] = Lit(_variables->linked(mi, ma));
        rhs[1] = Lit(_variables->con(w1, d-1));
        generate_classical_and_definition(lhs, rhs);
      }
    }
  }


  for (int w = 1; w < _sent->length; w++) {
    generate_literal(Lit(_variables->con(w, _sent->length-1)));
  }
}
#endif

void SATEncoder::dfs(int node, const MatrixUpperTriangle<int>& graph, int component, std::vector<int>& components) {
  if (components[node] != -1)
    return;

  components[node] = component;
  for (size_t other_node = node + 1; other_node < components.size(); other_node++) {
    if (graph(node, other_node))
      dfs(other_node, graph, component, components);
  }
  for (int other_node = 0; other_node < node; other_node++) {
    if (graph(other_node, node))
      dfs(other_node, graph, component, components);
  }
}

/* Temporary debug (may be needed again for adding parsing with null-links).
 * This allows to do "CXXFLAGS=-DCONNECTIVITY_DEBUG configure" or
 * "make CXXFLAGS=-DCONNECTIVITY_DEBUG" . */
//#define CONNECTIVITY_DEBUG
#ifdef CONNECTIVITY_DEBUG
#undef CONNECTIVITY_DEBUG
#define CONNECTIVITY_DEBUG(x) x
static void debug_generate_disconnectivity_prohibiting(vector<int> components,
                                      std::vector<int> different_components) {

  printf("generate_disconnectivity_prohibiting: ");
  for (auto c: components) cout << c << " ";
  cout << endl;
  for (auto c: different_components) cout << c << " ";
  cout << endl;
}
#else
#define debug_generate_disconnectivity_prohibiting(x, y)
#define CONNECTIVITY_DEBUG(x)
#endif

/*
 * The idea here is to save issuing a priori a lot of clauses to enforce
 * linkage connectivity (i.e. no islands), and instead do it when
 * a solution finds a disconnected linkage. This works well for valid
 * sentences because their solutions tend to be connected or mostly connected.
 */

 /**
  * Find the connectivity vector of the linkage.
  * @param components (result) A connectivity vector whose components
  * correspond to the linkage words.
  * @return true iff the linkage is completely connected (ignoring
  * optional words).
  *
  * Each segment in the linkage is numbered by the ordinal number of its
  * start word. Each vector component is numbered according to the segment
  * in which the corresponding word resides.
  * For example, a linkage with 7 words, which consists of 3 segments
  * (islands) of 2,2,3 words, will be represented as: 0 0 1 1 2 2 2.
  *
  * In order to support optional words (words that are allowed to have
  * no connectivity), optional words which don't participate in the linkage
  * are marked with -1 instead of their segment number, and are disregarded
  * in the connectivity test.
  */
bool SATEncoder::connectivity_components(std::vector<int>& components) {
  // get satisfied linked(wi, wj) variables
  const std::vector<int>& linked_variables = _variables->linked_variables();
  std::vector<int> satisfied_linked_variables;
  for (std::vector<int>::const_iterator i = linked_variables.begin(); i != linked_variables.end(); i++) {
    int var = *i;
    if (_solver->model[var] == l_True) {
      satisfied_linked_variables.push_back(var);
    }
  }

  // Words that are not in the linkage don't need to be connected.
  // (For now these can be only be words marked as "optional").
  std::vector<bool> is_linked_word(_sent->length, false);
  for (size_t node = 0; node < _sent->length; node++) {
    is_linked_word[node] = _solver->model[node] == l_True;
  }

  // build the connectivity graph
  MatrixUpperTriangle<int> graph(_sent->length, 0);
  std::vector<int>::const_iterator i;
  CONNECTIVITY_DEBUG(printf("connectivity_components words:\n"));
  for (i = satisfied_linked_variables.begin(); i != satisfied_linked_variables.end(); i++) {
    const int lv_l = _variables->linked_variable(*i)->left_word;
    const int lv_r = _variables->linked_variable(*i)->right_word;

    if (!is_linked_word[lv_l] || !is_linked_word[lv_r]) continue;
    graph.set(lv_l, lv_r, 1);
    CONNECTIVITY_DEBUG(printf("L%d R%d\n", lv_l, lv_r));
  }

  // determine the connectivity components
  components.resize(_sent->length);
  std::fill(components.begin(), components.end(), -1);
  for (size_t node = 0; node < _sent->length; node++)
    dfs(node, graph, node, components);

  CONNECTIVITY_DEBUG(printf("connectivity_components: "));
  bool connected = true;
  for (size_t node = 0; node < _sent->length; node++) {
    CONNECTIVITY_DEBUG(
      if (is_linked_word[node]) printf("%d ", components[node]);
      else                      printf("[%d] ", components[node]);
    )
    if (is_linked_word[node]) {
      if (components[node] != 0) {
        connected = false;
      }
    } else {
       components[node] = -1;
    }
  }

  CONNECTIVITY_DEBUG(printf(" connected=%d\n", connected));
  return connected;
}

#ifdef SAT_DEBUG
#define MVALUE(s, v) (s->model[v] == l_True?'T':(s->model[v] == l_False?'f':'u'))
GNUC_UNUSED static void pmodel(Solver *solver, int var) {
  printf("%c\n", MVALUE(solver, var));
}

GNUC_UNUSED static void pmodel(Solver *solver, vec<Lit> &clause) {
  vector<int> t;
  for (int i = 0; i < clause.size(); i++) {
    int v = var(clause[i]);
    printf("%d:%c ", v, MVALUE(solver, v));
    if (solver->model[v] == l_True) t.push_back(v);
  }
  printf("\n");
  if (t.size()) {
    printf("l_True:");
    for (auto i: t) printf(" %d", i);
    printf("\n");
  }
}
#endif

/**
 * Generate clauses to enforce exactly the missing connectivity.
 * @param components A connectivity vector as computed by
 * connectivity_components().
 *
 * Iterate the list of possible links between words, and find links
 * between words that are found in different segments according to the
 * connectivity vector. For each two segments, issue a clause asserting
 * that at least one of the corresponding links must exist.
 *
 * In order to support optional words, optional words which don't have links
 * (marked as -1 in the connectivity vector) are ignored. A missing link
 * between words when one of them is optional (referred to as a
 * "conditional_link" below) is considered missing only if both words exist
 * in the linkage.
 */
void SATEncoder::generate_disconnectivity_prohibiting(std::vector<int> components) {
  // vector of unique components
  std::vector<int> different_components = components;
  std::sort(different_components.begin(), different_components.end());
  different_components.erase(std::unique(different_components.begin(), different_components.end()),
                             different_components.end());
  debug_generate_disconnectivity_prohibiting(components, different_components);
  // Each connected component must contain a branch going out of it
  std::vector<int>::const_iterator c;
  bool missing_word = false;
  if (*different_components.begin() == -1) {
    different_components.erase(different_components.begin());
    missing_word = true;
  }
  for (c = different_components.begin(); c != different_components.end(); c++) {
    vec<Lit> clause;
    const std::vector<int>& linked_variables = _variables->linked_variables();
    for (std::vector<int>::const_iterator i = linked_variables.begin(); i != linked_variables.end(); i++) {
      int var = *i;
      const Variables::LinkedVar* lv = _variables->linked_variable(var);
      if ((components[lv->left_word] == *c && components[lv->right_word] != *c) ||
          (components[lv->left_word] != *c && components[lv->right_word] == *c)) {

        CONNECTIVITY_DEBUG(printf(" %d(%d-%d)", var, lv->left_word, lv->right_word));
        bool optlw_exists = _sent->word[lv->left_word].optional &&
                            _solver->model[lv->left_word] == l_True;
        bool optrw_exists = _sent->word[lv->right_word].optional &&
                            _solver->model[lv->right_word] == l_True;
        if (optlw_exists || optrw_exists) {
          int conditional_link_var;
          bool conditional_link_var_exists;

          CONNECTIVITY_DEBUG(printf("R ")); // "replaced"
          char name[MAX_VARIABLE_NAME] = "0";
          sprintf(name+1, "%dw%dw%d", var, optlw_exists?lv->left_word:255,
                                           optrw_exists?lv->right_word:255);
          conditional_link_var_exists = _variables->var_exists(name);
          conditional_link_var = _variables->string(name);

          if (!conditional_link_var_exists) {
            Lit lhs = Lit(conditional_link_var);
            vec<Lit> rhs;
            rhs.push(Lit(var));
            if (optlw_exists) rhs.push(~Lit(lv->left_word));
            if (optrw_exists) rhs.push(~Lit(lv->right_word));
            generate_or_definition(lhs, rhs);
          }

          var = conditional_link_var; // Replace it by its conditional link var
        }
        clause.push(Lit(var)); // Implied link var is used if needed
      }
    }

    if (missing_word) {
      // The connectivity may be restored differently if a word reappears
      for (WordIdx w = 0; w < _sent->length; w++) {
        if (_solver->model[w] == l_False)
          clause.push(Lit(w));
      }
    }
    CONNECTIVITY_DEBUG(printf("\n"));
    _solver->addClause(clause);

    // Avoid issuing two identical clauses
    if (different_components.size() == 2)
      break;
  }
}

/*--------------------------------------------------------------------------*
 *                           P L A N A R I T Y                              *
 *--------------------------------------------------------------------------*/
void SATEncoder::generate_planarity_conditions()
{
  vec<Lit> clause(2);
  for (size_t wi1 = 0; wi1 < _sent->length; wi1++) {
    for (size_t wj1 = wi1+1; wj1 < _sent->length; wj1++) {
      for (size_t wi2 = wj1+1; wi2 < _sent->length; wi2++) {
        if (!_linked_possible(wi1, wi2))
          continue;
        for (size_t wj2 = wi2+1; wj2 < _sent->length; wj2++) {
          if (!_linked_possible(wj1, wj2))
            continue;
          clause[0] = ~Lit(_variables->linked(wi1, wi2));
          clause[1] = ~Lit(_variables->linked(wj1, wj2));
          add_clause(clause);
        }
      }
    }
  }
}

/*--------------------------------------------------------------------------*
 *               P O W E R     P R U N I N G                                *
 *--------------------------------------------------------------------------*/

void SATEncoder::generate_epsilon_definitions()
{
  for (size_t w = 0; w < _sent->length; w++) {
    if (_sent->word[w].x == NULL) {
      continue;
    }

    bool join = _sent->word[w].x->next != NULL;
    Exp* exp = join ? join_alternatives(w) : _sent->word[w].x->exp;

    char name[MAX_VARIABLE_NAME];
    // sprintf(name, "w%zu", w);
    name[0] = 'w';
    fast_sprintf(name+1, w);

    int dfs_position;

    dfs_position = 0;
    generate_epsilon_for_expression(w, dfs_position, exp, name, true, '+');

    dfs_position = 0;
    generate_epsilon_for_expression(w, dfs_position, exp, name, true, '-');
  }
}

bool SATEncoder::generate_epsilon_for_expression(int w, int& dfs_position, Exp* e,
                                                 char* var, bool root, char dir)
{
  if (e->type == CONNECTOR_type) {
    dfs_position++;
    if (var != NULL) {
      if (e->dir == dir) {
        // generate_literal(-_variables->epsilon(name, var, e->dir));
        return false;
      } else {
        generate_equivalence_definition(Lit(_variables->epsilon(var, dir)),
                                        Lit(_variables->string(var)));
        return true;
      }
    }
  } else if (e->type == AND_type) {
    if (e->operand_first == NULL) {
      /* zeroary and */
      generate_equivalence_definition(Lit(_variables->string(var)),
                                      Lit(_variables->epsilon(var, dir)));
      return true;
    } else
      if (e->operand_first != NULL && e->operand_first->operand_next == NULL) {
        /* unary and - skip */
        return generate_epsilon_for_expression(w, dfs_position, e->operand_first, var, root, dir);
      } else {
        /* Recurse */
        Exp* opd;
        int i;
        bool eps = true;

        char new_var[MAX_VARIABLE_NAME];
        char* last_new_var = new_var;
        char* last_var = var;
        while ((*last_new_var = *last_var)) {
          last_new_var++;
          last_var++;
        }


        for (i = 0, opd = e->operand_first; opd != NULL; opd = opd->operand_next, i++) {
          // sprintf(new_var, "%sc%d", var, i)
          char* s = last_new_var;
          *s++ = 'c';
          fast_sprintf(s, i);

          if (!generate_epsilon_for_expression(w, dfs_position, opd, new_var, false, dir)) {
            eps = false;
            break;
          }
        }

        if (opd != NULL) {
          for (opd = opd->operand_next; opd != NULL; opd = opd->operand_next)
            dfs_position += num_connectors(opd);
        }

        if (!root && eps) {
          Lit lhs = Lit(_variables->epsilon(var, dir));
          vec<Lit> rhs;
        for (i = 0, opd = e->operand_first; opd != NULL; opd = opd->operand_next, i++) {
            // sprintf(new_var, "%sc%d", var, i)
            char* s = last_new_var;
            *s++ = 'c';
            fast_sprintf(s, i);
            rhs.push(Lit(_variables->epsilon(new_var, dir)));
          }
          generate_classical_and_definition(lhs, rhs);
        }
        return eps;
      }
  } else if (e->type == OR_type) {
    if (e->operand_first != NULL && e->operand_first->operand_next == NULL) {
      /* unary or - skip */
      return generate_epsilon_for_expression(w, dfs_position, e->operand_first, var, root, dir);
    } else {
      /* Recurse */
      Exp* opd;
      int i;
      bool eps = false;

      char new_var[MAX_VARIABLE_NAME];
      char* last_new_var = new_var;
      char* last_var = var;
      while ((*last_new_var = *last_var)) {
        last_new_var++;
        last_var++;
      }

      vec<Lit> rhs;
        for (i = 0, opd = e->operand_first; opd != NULL; opd = opd->operand_next, i++) {
        // sprintf(new_var, "%sc%d", var, i)
        char* s = last_new_var;
        *s++ = 'd';
        fast_sprintf(s, i);

        if (generate_epsilon_for_expression(w, dfs_position, opd, new_var, false, dir) && !root) {
          rhs.push(Lit(_variables->epsilon(new_var, dir)));
          eps = true;
        }
      }

      if (!root && eps) {
        Lit lhs = Lit(_variables->epsilon(var, dir));
        generate_or_definition(lhs, rhs);
      }

      return eps;
    }
  }
  return false;
}

void SATEncoder::power_prune()
{
  generate_epsilon_definitions();

  // on two non-adjacent words, a pair of connectors can be used only
  // if not [both of them are the deepest].

  for (size_t wl = 0; wl < _sent->length - 2; wl++) {
    const std::vector<PositionConnector>& rc = _word_tags[wl].get_right_connectors();
    std::vector<PositionConnector>::const_iterator rci;
    for (rci = rc.begin(); rci != rc.end(); rci++) {
      if (!(*rci).leading_right || (*rci).connector.multi)
        continue;

      const std::vector<PositionConnector*>& matches = rci->matches;
      for (std::vector<PositionConnector*>::const_iterator lci = matches.begin(); lci != matches.end(); lci++) {
        if (!(*lci)->leading_left || (*lci)->connector.multi || (*lci)->word <= wl + 2)
          continue;
        if (_opts->min_null_count == 0)
          if (optional_gap_collapse(_sent, wl, (*lci)->word)) continue;

        //        printf("LR: .%zu. .%d. %s\n", wl, rci->position, rci->connector.desc->string);
        //        printf("LL: .%zu. .%d. %s\n", (*lci)->word, (*lci)->position, (*lci)->connector.desc->string);

        vec<Lit> clause;
        for (std::vector<int>::const_iterator i = rci->eps_right.begin(); i != rci->eps_right.end(); i++) {
          clause.push(~Lit(*i));
        }

        for (std::vector<int>::const_iterator i = (*lci)->eps_left.begin(); i != (*lci)->eps_left.end(); i++) {
          clause.push(~Lit(*i));
        }

        add_additional_power_pruning_conditions(clause, wl, (*lci)->word);

        clause.push(~Lit(_variables->link(
               wl, rci->position, connector_string(&rci->connector), rci->exp,
               (*lci)->word, (*lci)->position, connector_string(&(*lci)->connector), (*lci)->exp)));
        add_clause(clause);
      }
    }
  }

#if 0
  // on two adjacent words, a pair of connectors can be used only if
  // they're the deepest ones on their disjuncts
  for (size_t wl = 0; wl < _sent->length - 2; wl++) {
    const std::vector<PositionConnector>& rc = _word_tags[wl].get_right_connectors();
    std::vector<PositionConnector>::const_iterator rci;
    for (rci = rc.begin(); rci != rc.end(); rci++) {
      if (!(*rci).leading_right)
        continue;

      const std::vector<PositionConnector*>& matches = rci->matches;
      for (std::vector<PositionConnector*>::const_iterator lci = matches.begin(); lci != matches.end(); lci++) {
        if (!(*lci)->leading_left || (*lci)->word != wl + 1)
          continue;
        int link = _variables->link(wl, rci->position, rci->connector.desc->string, rci->exp,
                                    (*lci)->word, (*lci)->position, (*lci)->connector.desc->string, (*lci)->exp);
        vec<Lit> clause(2);
        clause.push(~Lit(link));

        for (std::vector<int>::const_iterator i = rci->eps_right.begin(); i != rci->eps_right.end(); i++) {
          clause.push(Lit(*i));
        }

        for (std::vector<int>::const_iterator i = (*lci)->eps_left.begin(); i != (*lci)->eps_left.end(); i++) {
          clause.push(Lit(*i));
        }

        add_clause(clause);
      }
    }
  }
#endif


#if 0
  // Two deep connectors cannot match (deep means notlast)
  std::vector<std::vector<PositionConnector*> > certainly_deep_left(_sent->length), certainly_deep_right(_sent->length);
  for (size_t w = 0; w < _sent->length - 2; w++) {
    if (_sent->word[w].x == NULL)
      continue;

    bool join = _sent->word[w].x->next != NULL;
    Exp* exp = join ? join_alternatives(w) : _sent->word[w].x->exp;

    int dfs_position = 0;
    certainly_non_trailing(w, exp, '+', dfs_position, certainly_deep_right[w], false);
    dfs_position = 0;
    certainly_non_trailing(w, exp, '-', dfs_position, certainly_deep_left[w], false);
  }

  for (size_t w = 0; w < _sent->length; w++) {
    std::vector<PositionConnector*>::const_iterator i;
    for (i = certainly_deep_right[w].begin(); i != certainly_deep_right[w].end(); i++) {
      const std::vector<PositionConnector*>& matches = (*i)->matches;
      std::vector<PositionConnector*>::const_iterator j;
      for (j = matches.begin(); j != matches.end(); j++) {
        if (std::find(certainly_deep_left[(*j)->word].begin(), certainly_deep_left[(*j)->word].end(),
                      *j) != certainly_deep_left[(*j)->word].end()) {
          generate_literal(~Lit(_variables->link((*i)->word, (*i)->position, (*i)->connector.desc->string, (*i)->exp,
                                             (*j)->word, (*j)->position, (*j)->connector.desc->string, (*j)->exp)));
        }
      }
    }
  }
#endif
}

/*--------------------------------------------------------------------------*
 *        P O S T P R O C E S S I N G   &  P P     P R U N I N G            *
 *--------------------------------------------------------------------------*/

#if 0 // Needed only for the additional PP pruning (pp_pruning_1)
/**
 * Returns false if the string s does not match anything in
 * the array. The array elements are post-processing symbols.
 */
static bool string_in_list(const char * s, const char * a[])
{
  for (size_t i = 0; a[i] != NULL; i++)
    if (post_process_match(a[i], s)) return true;
  return false;
}
#endif

/* For debugging. */
/*
GNUC_UNUSED static void print_link_array(const char **s)
{
  printf("|");
  do
  {
    printf("%s ", *s);
  } while (*++s);
  printf("|\n");
}
*/

void SATEncoder::pp_prune()
{
  const std::vector<int>& link_variables = _variables->link_variables();

  if (_sent->dict->base_knowledge == NULL)
    return;

  if (!_opts->perform_pp_prune)
    return;

  pp_knowledge * knowledge;
  knowledge = _sent->dict->base_knowledge;

  for (size_t i=0; i<knowledge->n_contains_one_rules; i++)
  {
    pp_rule rule = knowledge->contains_one_rules[i];
    // const char * selector = rule.selector;         /* selector string for this rule */
    pp_linkset * link_set = rule.link_set;            /* the set of criterion links */


    vec<Lit> triggers;
    for (size_t vi = 0; vi < link_variables.size(); vi++) {
      const Variables::LinkVar* var = _variables->link_variable(link_variables[vi]);
      if (post_process_match(rule.selector, var->label)) {
        triggers.push(Lit(link_variables[vi]));
      }
    }

    if (triggers.size() == 0)
      continue;

    vec<Lit> criterions;
    for (size_t j = 0; j < link_variables.size(); j++) {
      pp_linkset_node *p;
      for (size_t hashval = 0; hashval < link_set->hash_table_size; hashval++) {
        for (p = link_set->hash_table[hashval]; p!=NULL; p=p->next) {
          const Variables::LinkVar* var = _variables->link_variable(link_variables[j]);
          if (post_process_match(p->str, var->label)) {
            criterions.push(Lit(link_variables[j]));
          }
        }
      }
    }

    DEBUG_print("---pp_pruning--");
    for (int k = 0; k < triggers.size(); k++) {
      vec<Lit> clause(criterions.size() + 1);
      for (int ci = 0; ci < criterions.size(); ci++)
        clause[ci] = criterions[ci];
      clause[criterions.size()] = (~triggers[k]);
      add_clause(clause);
    }
    DEBUG_print("---end pp_pruning--");
  }

  /* The following code has a bug that causes it to be too restrictive.
   * Instead of fixing it, it is disabled here, as it is to be replaced
   * soon by the pp-pruning code of the classic parser. */
#if 0
  if (test_enabled("no-pp_pruning_1")) return; // For result comparison.
  /* Additional PP pruning.
   * Since the SAT parser defines constrains on links, it is possible
   * to encode all the postprocessing rules, in order to prune all the
   * solutions that violate the postprocessing rules.
   *
   * This may save much SAT-solver overhead, because solutions which are
   * not going to pass postprocessing will get eliminated, saving a very
   * high number of calls to the SAT-solver that are not yielding a valid
   * linkage.
   *
   * However, the encoding code has a non-negligible overhead, and also
   * it may add clauses that increase the overhead of the SAT-solver.
   *
   * FIXME:
   * A large part of the encoding overhead is because the need to
   * iterate a very large number of items in order to find the small
   * number of items that are needed. Hashing in advance can solve this
   * and similar problems.
   *
   * For now only a very limited pruning is tried.
   * For the CONTAINS_NONE_RULES, only the nearest link to the root-link
   * is checked.
   *
   * TODO:
   * BOUNDED_RULES pruning.
   * Domain encoding.
   */

  /*
   * CONTAINS_NONE_RULES
   * 1. Suppose no one of them refers to a URFL domain.
   * 2. Only the links of words accessible through a right link of
   * the root word are checked here. Even such a limited check saves CPU.
   *
   * Below, var_i and var_j are link variables, when var_i is the root link.
   * root_word---var_i---wr---var_j
   */

  //printf("n_contains_none_rules %zu\n", knowledge->n_contains_none_rules);
  //printf("link_variables.size() %zu\n", link_variables.size());
  for (size_t i=0; i<knowledge->n_contains_none_rules; i++)
  {
    pp_rule rule = knowledge->contains_none_rules[i];
    //printf("rule[%2zu]selector = %s; ", i, rule.selector);
    //print_link_array(rule.link_array);

    int root_link;
    int wr; // A word at the end of a right-link of the root word.
    for (size_t vi = 0; vi < link_variables.size(); vi++)
    {
      const Variables::LinkVar* var_i = _variables->link_variable(link_variables[vi]);
      if (!post_process_match(rule.selector, var_i->label)) continue;

      root_link = link_variables[vi];
      wr = var_i->right_word;

      //printf("Found rule[%zu].selector %s: %s %d\n", i, rule.selector, var_i->label, wr);

      vector<int> must_not_exist;
      for (size_t vj = 0; vj < link_variables.size(); vj++)
      {
        const Variables::LinkVar* var_j = _variables->link_variable(link_variables[vj]);
        if ((wr != var_j->left_word) && (wr != var_j->right_word)) continue;
        if (var_i == var_j) continue; // It points back to the root word.

        //printf("var_j->label %s %d %d\n", var_j->label, var_j->right_word, var_j->left_word);
        if (string_in_list(var_j->label, rule.link_array))
          must_not_exist.push_back(link_variables[vj]);
      }

      DEBUG_print("---pp_pruning 1--");
      for (auto c: must_not_exist)
      {
        vec<Lit> clause(2);
        clause[0] = ~Lit(root_link);
        clause[1] = ~Lit(c);
        add_clause(clause);
      }
      DEBUG_print("---end pp_pruning 1--");
    }
  }
#endif // 0
}

/*--------------------------------------------------------------------------*
 *                         D E C O D I N G                                  *
 *--------------------------------------------------------------------------*/

/**
 * Create the next linkage.
 * Return true iff the linkage can be created.
 */
bool SATEncoder::create_linkage(Linkage linkage)
{
  partial_init_linkage(_sent, linkage, _sent->length);
  if (!sat_extract_links(linkage)) return false;
  compute_link_names(linkage, _sent->string_set);
  return true;
}

void SATEncoder::generate_linkage_prohibiting()
{
  vec<Lit> clause;
  const std::vector<int>& link_variables = _variables->link_variables();
  for (std::vector<int>::const_iterator i = link_variables.begin(); i != link_variables.end(); i++) {
    int var = *i;
    if (_solver->model[var] == l_True) {
      clause.push(~Lit(var));
    } else if (_solver->model[var] == l_False) {
      clause.push(Lit(var));
    }
  }
  _solver->addClause(clause);
}

Linkage SATEncoder::get_next_linkage()
{
  Linkage_s linkage;
  bool connected;
  bool display_linkage_disconnected = false;


  /* Loop until a good linkage is found.
   * Insane (mixed alternatives) linkages are always ignored.
   * Disconnected linkages are normally ignored, unless
   * !test=linkage-disconnected is used (and they are sane) */
  bool linkage_ok;
  do {
    if (!_solver->solve()) return NULL;

    std::vector<int> components;
    connected = connectivity_components(components);

    // Prohibit this solution so the next ones can be found
    if (!connected) {
      _num_lkg_disconnected++;
      generate_disconnectivity_prohibiting(components);
      display_linkage_disconnected = test_enabled("linkage-disconnected");
    } else {
      generate_linkage_prohibiting();
    }

    linkage_ok = false;
    if (connected || display_linkage_disconnected) {
      memset(&linkage, 0, sizeof(struct Linkage_s));

      linkage_ok = create_linkage(&linkage);
      if (linkage_ok)
        linkage_ok = sane_linkage_morphism(_sent, &linkage, _opts);
      if (!linkage_ok) {
          /* We cannot elegantly add this linkage to sent->linkges[] -
           * to be freed in sentence_delete(), since insane linkages
           * must be there with index > num_linkages_post_processed - so
           * they remain hidden, but num_linkages_post_processed is an
           * arbitrary number.  So we must free it here. */
          free_linkage_connectors_and_disjuncts(&linkage);
          free_linkage(&linkage);
          continue; // skip this linkage
      }
      remove_empty_words(&linkage);  /* Discard optional words. */
    }

    if (!connected) {
      if (display_linkage_disconnected) {
        cout << "Linkage DISCONNECTED" << endl;
      } else {
        lgdebug(+D_SAT, "Linkage DISCONNECTED (skipped)\n");
      }
    }
  } while (!linkage_ok);

  /* We cannot expand the linkage array on demand, since the API uses
   * linkage pointers, and they would become invalid if realloc() changes
   * the address of the memory block. So it is allocated in advance. */
  if (NULL == _sent->lnkages)
  {
    _sent->num_linkages_alloced = _opts->linkage_limit;
    size_t nbytes = _sent->num_linkages_alloced * sizeof(struct Linkage_s);
    _sent->lnkages = (Linkage) malloc(nbytes);
    _next_linkage_index = 0;
  }
  assert(_next_linkage_index<_sent->num_linkages_alloced, "_sent->lnkages ovl");

  Linkage lkg = &_sent->lnkages[_next_linkage_index];
  _next_linkage_index++;
  *lkg = linkage;  /* copy en-mass */

  /* The link-parser code checks the next linkage for num_violations
   * (to save calls to linkage_create()). Allow for that practice. */
  if (_next_linkage_index < _sent->num_linkages_alloced)
    lkg[1].lifo.N_violations = 0;

  // Perform the rest of the post-processing
  if (NULL != _sent->postprocessor) {
    do_post_process(_sent->postprocessor, lkg, false);
    if (NULL != _sent->postprocessor->violation) {
      _num_pp_violations++;
      lkg->lifo.N_violations++;
      lkg->lifo.pp_violation_msg = _sent->postprocessor->violation;
      lgdebug(+D_SAT, "Postprocessing error: %s\n", lkg->lifo.pp_violation_msg);
    } else {
      // XXX We cannot maintain num_valid_linkages, because it starts from
      // a high number. If we start it from 0, then on value 1 link-parser
      // would report "Unique linkage".
      //_sent->num_valid_linkages++;
    }
    post_process_free_data(&_sent->postprocessor->pp_data);
  }
  linkage_score(lkg, _opts);

  // if (NULL == _sent->postprocessor->violation && verbosity > 1)
  //   _solver->printStats();
  return lkg;
}

/*******************************************************************************
 *        SAT encoding for sentences that do not contain conjunction.          *
 *******************************************************************************/

void SATEncoderConjunctionFreeSentences::generate_encoding_specific_clauses() {
}

void SATEncoderConjunctionFreeSentences::handle_null_expression(int w) {
  // Formula is unsatisfiable
  vec<Lit> clause;
  add_clause(clause);
}

void SATEncoderConjunctionFreeSentences::determine_satisfaction(int w, char* name)
{
  // All tags must be satisfied
  generate_literal(Lit(_variables->string(name)));
}

void SATEncoderConjunctionFreeSentences::generate_satisfaction_for_connector(
    int wi, int pi, Exp *e, char* var)
{
  const char* Ci = e->condesc->more->string;
  char dir = e->dir;
  bool multi = e->multi;
  double cost = e->cost;

  Lit lhs = Lit(_variables->string_cost(var, cost));

#ifdef SAT_DEBUG
  cout << "*** Connector: ." << wi << ". ." << pi << ". " << Ci << dir << endl;
#endif

  // words that can potentially match (wi, pi)
  int low = (dir == '-') ? 0 : wi + 1;
  int hi  = (dir == '-') ? wi : _sent->length;

  std::vector<int> _w_;
  for (int wj = low; wj < hi; wj++) {
    // Eliminate words that cannot be connected to (wi, pi)
    if (!_word_tags[wj].match_possible(wi, pi))
      continue;

    // Now we know that there is a potential link between the
    // connector (wi, pi) and the word wj
    _w_.push_back(wj);

    generate_link_cw_ordinary_definition(wi, pi, e, wj);
  }

  vec<Lit> _link_cw_;
  for (size_t i = 0; i < _w_.size(); i++)
    _link_cw_.push(Lit(_variables->link_cw(_w_[i], wi, pi, Ci)));
  generate_or_definition(lhs, _link_cw_);

  DEBUG_print("--------- multi");
  if (!multi) {
    generate_xor_conditions(_link_cw_);
  }
  DEBUG_print("--------- end multi");

#ifdef SAT_DEBUG
  cout << "*** End Connector: ." << wi << ". ." << pi << ". " <<  Ci << endl;
#endif
}

void SATEncoderConjunctionFreeSentences::generate_linked_definitions()
{
  _linked_possible.resize(_sent->length, 1);
  vector<vec<Lit>> linked_to_word(_sent->length);

  DEBUG_print("------- linked definitions");
  for (size_t w1 = 0; w1 < _sent->length; w1++) {
    vec<Lit> linked;
    for (size_t w2 = w1 + 1; w2 < _sent->length; w2++) {
      DEBUG_print("---------- ." << w1 << ". ." << w2 << ".");
      Lit lhs = Lit(_variables->linked(w1, w2));

      vec<Lit> rhs;
      const std::vector<PositionConnector>& w1_connectors = _word_tags[w1].get_right_connectors();
      std::vector<PositionConnector>::const_iterator c;
      for (c = w1_connectors.begin(); c != w1_connectors.end(); c++) {
        assert(c->word == w1, "Connector word must match");
        if (_word_tags[w2].match_possible(c->word, c->position)) {
          rhs.push(Lit(_variables->link_cw(w2, c->word, c->position, connector_string(&c->connector))));
        }
      }

      _linked_possible.set(w1, w2, rhs.size() > 0);
      generate_or_definition(lhs, rhs);

      /* Optional words that have no links should be "down", as a mark that
       * they are missing in the linkage.
       * Collect all possible word links, per word, to be used below. */
      if (rhs.size() > 0) {
        if (_sent->word[w1].optional) {
          linked_to_word[w1].push(Lit(_variables->linked(w1, w2)));
        }
        if (_sent->word[w2].optional) {
          linked_to_word[w2].push(Lit(_variables->linked(w1, w2)));
        }
      }
    }

    if (_sent->word[w1].optional) {
      /* The word should be connected to at least another word in order to be
       * in the linkage. */
      DEBUG_print("------------S not linked -> no word (w" << w1 << ")");
      generate_or_definition(Lit(w1), linked_to_word[w1]);
      DEBUG_print("------------E not linked -> no word");
    }
  }
  DEBUG_print("------- end linked definitions");
}

Exp* SATEncoderConjunctionFreeSentences::PositionConnector2exp(const PositionConnector* pc)
{
    Exp* e = Exp_create(_sent->Exp_pool);
    e->type = CONNECTOR_type;
    e->dir = pc->dir;
    e->multi = pc->connector.multi;
    e->condesc = (condesc_t *)pc->connector.desc; // FIXME - const
    e->cost = pc->cost;

    return e;
}

#define D_SEL 8
bool SATEncoderConjunctionFreeSentences::sat_extract_links(Linkage lkg)
{
  Disjunct *d;
  uint32_t current_link = 0;

  Exp **exp_word = (Exp **)alloca(_sent->length * sizeof(Exp *));
  memset(exp_word, 0, _sent->length * sizeof(Exp *));
  const X_node **xnode_word = (const X_node **)alloca(_sent->length * sizeof(X_node *));
  memset(xnode_word, 0, _sent->length * sizeof(X_node *));

  const std::vector<int>& link_variables = _variables->link_variables();
  std::vector<int>::const_iterator i;
  for (i = link_variables.begin(); i != link_variables.end(); i++) {
    if (_solver->model[*i] != l_True)
      continue;

    const Variables::LinkVar* var = _variables->link_variable(*i);
    if (_solver->model[_variables->linked(var->left_word, var->right_word)] != l_True)
      continue;

    assert(current_link < lkg->lasz, "Linkage array too small!");
    Link& clink = lkg->link_array[current_link];
    current_link++;
    clink.lw = var->left_word;
    clink.rw = var->right_word;

    PositionConnector* lpc = _word_tags[var->left_word].get(var->left_position);
    PositionConnector* rpc = _word_tags[var->right_word].get(var->right_position);

    const X_node *left_xnode = lpc->word_xnode;
    const X_node *right_xnode = rpc->word_xnode;

    // Allocate memory for the connectors, because they should persist
    // beyond the lifetime of the sat-solver data structures.
    clink.lc = connector_new(NULL, NULL);
    clink.rc = connector_new(NULL, NULL);

    *clink.lc = lpc->connector;
    *clink.rc = rpc->connector;

    Exp* lcexp = PositionConnector2exp(lpc);
    Exp* rcexp = PositionConnector2exp(rpc);
    add_anded_exp(_sent, exp_word[var->left_word], lcexp);
    add_anded_exp(_sent, exp_word[var->right_word], rcexp);

    if (verbosity_level(D_SAT)) {
      //cout<< "Lexp[" <<left_xnode->word->subword <<"]: " << lg_exp_stringify(var->left_exp);
      cout<< "w"<<var->left_word<<" LCexp[" <<left_xnode->word->subword <<"]: ", lg_exp_stringify(lcexp);
      //cout<< "Rexp[" <<right_xnode->word->subword <<"]: ", lg_exp_stringify(var->right_exp);
      cout<< "w"<<var->right_word<<" RCexp[" <<right_xnode->word->subword <<"]: ", lg_exp_stringify(rcexp);
      cout<< "L+L: ", lg_exp_stringify(exp_word[var->left_word]);
      cout<< "R+R: ", lg_exp_stringify(exp_word[var->right_word]);
    }

    if (xnode_word[var->left_word] && xnode_word[var->left_word] != left_xnode) {
      lgdebug(+0, "Warning: Inconsistent X_node for word %d (%s and %s)\n",
              var->left_word, xnode_word[var->left_word]->string,
              left_xnode->string);
    }
    if (xnode_word[var->right_word] && xnode_word[var->right_word] != right_xnode) {
      lgdebug(+0, "Warning: Inconsistent X_node for word %d (%s and %s)\n",
              var->right_word, xnode_word[var->right_word]->string,
              right_xnode->string);
    }

    xnode_word[var->left_word] = left_xnode;
    xnode_word[var->right_word] = right_xnode;
  }

  lkg->num_links = current_link;

  // Now build the disjuncts.
  // This is needed so that compute_chosen_word works correctly.
  // Just in case there is no expression for a disjunct, a null one is used.
  for (WordIdx wi = 0; wi < _sent->length; wi++) {
    Exp *de = exp_word[wi];

    // Skip optional words
    if (xnode_word[wi] == NULL)
    {
      if (!_sent->word[wi].optional)
      {
        de = null_exp();
        prt_error("Error: Internal error: Non-optional word %zu has no linkage\n", wi);
      }
      continue;
    }

    if (de == NULL) {
      de = null_exp();
      prt_error("Error: Internal error: No expression for word %zu\n", wi);
    }

    double cost_cutoff;
#if LIMIT_TOTAL_LINKAGE_COST // Undefined - incompatible to the classic parser.
    cost_cutoff = _opts->disjunct_cost;
#else
    cost_cutoff = 1000.0;
#endif // LIMIT_TOTAL_LINKAGE_COST
    d = build_disjuncts_for_exp(_sent, de, xnode_word[wi]->string,
                                &xnode_word[wi]->word->gword_set_head,
                                cost_cutoff, _opts);

    if (d == NULL)
    {
      lgdebug(+D_SEL, "Debug: Word %zu: Disjunct cost > cost_cutoff %.2f\n",
              wi, cost_cutoff);
#ifdef DEBUG
      if (!test_enabled("SAT-cost"))
#endif
      return false;
    }

    /* Recover cost of costly-nulls. */
    const vector<EmptyConnector>& ec = _word_tags[wi].get_empty_connectors();
    for (vector<EmptyConnector>::const_iterator j = ec.begin(); j < ec.end(); j++)
    {
      lgdebug(+D_SEL, "Debug: Word %zu: Costly-null var=%d, found=%d cost=%.2f\n",
              wi, j->ec_var, _solver->model[j->ec_var] == l_True, j->ec_cost);
      if (_solver->model[j->ec_var] == l_True)
        d->cost += j->ec_cost;
    }

    lkg->chosen_disjuncts[wi] = d;

#if LIMIT_TOTAL_LINKAGE_COST
    if (d->cost > cost_cutoff)
    {
      lgdebug(+D_SEL, "Word %zu: Disjunct cost  %.2f > cost_cutoff %.2f\n",
              wi, d->cost, cost_cutoff);
#ifdef DEBUG
      if (!test_enabled("SAT-cost"))
#endif
      return false;
    }
#endif // LIMIT_TOTAL_LINKAGE_COST
  }

  DEBUG_print("Total links: ." <<  lkg->num_links << "." << endl);
  return true;
}
#undef D_SEL

/**
 * Main entry point into the SAT parser.
 * A note about panic mode:
 * - The MiniSAT support for timeout is not yet used (FIXME).
 * - Parsing with null links is not supported (FIXME).
 * So nothing particularly useful happens in a panic mode, and it is
 * left for the user to disable it.
 */
extern "C" int sat_parse(Sentence sent, Parse_Options  opts)
{
  if (opts->min_null_count > 0) {
    // The sat solver doesn't support (yet) parsing with nulls.
    // For now, just avoid the delay of a useless re-parsing.
    if (opts->verbosity >= 1)
      prt_error("Info: use-sat: Cannot parse with null links (yet).\n"
                "              Set the \"null\" option to 0 to turn off "
                "parsing with null links.\n");
    sent->num_valid_linkages = 0;
    sent->num_linkages_post_processed = 0;
    return 0;
  }

  SATEncoder* encoder = (SATEncoder*) sent->hook;
  if (encoder) {
    sat_free_linkages(sent, encoder->_next_linkage_index);
    delete encoder;
  }

  encoder = new SATEncoderConjunctionFreeSentences(sent, opts);
  sent->hook = encoder;
  encoder->encode();

  LinkageIdx linkage_limit = opts->linkage_limit;
  LinkageIdx k;
  Linkage lkg = NULL;

  /* Due to the nature of SAT solving, we cannot know in advance the
   * number of linkages. But in order to process batch files, we must
   * know if there is at least one valid linkage. We check up to
   * linkage_limit number of linkages (settable by !limit).
   * Normally the following loop terminates after one or a few
   * iterations, when a valid linkage is found or when no more linkages
   * are found.
   *
   * Note that trying to find here the first valid linkage doesn't add
   * overhead to an interactive user. It also doesn't add overhead to
   * batch processing, which needs anyway to find out if there is a
   * valid linkage in order to be any useful. */
  for (k = 0; k < linkage_limit; k++)
  {
    lkg = encoder->get_next_linkage();
    if (lkg == NULL || lkg->lifo.N_violations == 0) break;
  }
  encoder->print_stats();

  if (lkg == NULL || k == linkage_limit) {
    // We don't have a valid linkages among the first linkage_limit ones
    sent->num_valid_linkages = 0;
    sent->num_linkages_found = k;
    sent->num_linkages_post_processed = k;
    if (opts->max_null_count > 0) {
      // The sat solver doesn't support (yet) parsing with nulls.
      if (opts->verbosity >= 1)
      prt_error("Info: use-sat: Cannot parse with null links (yet).\n"
                "              Set the \"null\" option to 0 to turn off "
                "parsing with null links.\n");
    }
  } else {
    /* We found a valid linkage. However, we actually don't know yet the
     * number of linkages, and if we set them too low, the command-line
     * client will fail to display all of the possible linkages.  Work
     * around this by lying... return the maximum number of linkages we
     * are going to produce.
     * A NULL linkage will be returned by linkage_create() after the last
     * linkage is produced to signify that there are no more linkages. */
    sent->num_valid_linkages = linkage_limit;
    sent->num_linkages_post_processed = linkage_limit;
  }

  return 0;
}

/**
 * Get a SAT linkage.
 * Validate that k is not too big.
 * If the k'th linkage already exists, return it.
 * Else k is the next linkage index - get the next SAT solution.
 */
extern "C" Linkage sat_create_linkage(LinkageIdx k, Sentence sent, Parse_Options  opts)
{
  SATEncoder* encoder = (SATEncoder*) sent->hook;
  if (!encoder) return NULL;

  if (k >= opts->linkage_limit)                  // > allocated memory
  {
    encoder->print_stats();
    return NULL;
  }

  if(k > encoder->_next_linkage_index)           // skips unproduced linkages
  {
    prt_error("Error: Linkage index %zu is greater than the "
              "maximum expected one %zu\n", k, encoder->_next_linkage_index);
    return NULL;
  }
  if (k < encoder->_next_linkage_index)          // already produced
    return &encoder->_sent->lnkages[k];

  return encoder->get_next_linkage();            // exactly next to produce
}

extern "C" void sat_sentence_delete(Sentence sent)
{
  SATEncoder* encoder = (SATEncoder*) sent->hook;
  if (!encoder) return;

  encoder->print_stats();

  sat_free_linkages(sent, encoder->_next_linkage_index);
  delete encoder;
}