<commit_before>/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     <NAME> <<EMAIL>>
 *
 *  Contributing authors:
 *     <NAME> <<EMAIL>>
 *
 *  Copyright:
 *     <NAME>, 2007
 *     <NAME>, 2009
 *
 *  Last modified:
 *     $Date: 2010-07-02 19:18:43 +1000 (Fri, 02 Jul 2010) $ by $Author: tack $
 *     $Revision: 11149 $
 *
 *  This file is part of Gecode, the generic constraint
 *  development environment:
 *     http://www.gecode.org
 *
 *  Permission is hereby granted, free of charge, to any person obtaining
 *  a copy of this software and associated documentation files (the
 *  "Software"), to deal in the Software without restriction, including
 *  without limitation the rights to use, copy, modify, merge, publish,
 *  distribute, sublicense, and/or sell copies of the Software, and to
 *  permit persons to whom the Software is furnished to do so, subject to
 *  the following conditions:
 *
 *  The above copyright notice and this permission notice shall be
 *  included in all copies or substantial portions of the Software.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 */

#include "base/commandlineflags.h"
#include "flatzinc/flatzinc.h"

DECLARE_bool(cp_trace_search);
DECLARE_bool(cp_trace_propagation);

namespace operations_research {
extern bool HasDomainAnnotation(AST::Node* const annotations);
namespace {
// Help

Constraint* MakeStrongScalProdEquality(Solver* const solver,
                                       std::vector<IntVar*>& variables,
                                       std::vector<int64>& coefficients,
                                       int64 rhs) {
  const bool trace = FLAGS_cp_trace_search;
  const bool propag = FLAGS_cp_trace_propagation;
  FLAGS_cp_trace_search = false;
  FLAGS_cp_trace_propagation = false;
  const int size = variables.size();
  IntTupleSet tuples(size);
  Solver s("build");
  std::vector<IntVar*> copy_vars(size);
  for (int i = 0; i < size; ++i) {
    copy_vars[i] = s.MakeIntVar(variables[i]->Min(), variables[i]->Max());
  }
  s.AddConstraint(s.MakeScalProdEquality(copy_vars, coefficients, rhs));
  s.NewSearch(s.MakePhase(copy_vars,
                          Solver::CHOOSE_FIRST_UNBOUND,
                          Solver::ASSIGN_MIN_VALUE));
  while (s.NextSolution()) {
    std::vector<int> one_tuple(size);
    for (int i = 0; i < size; ++i) {
      one_tuple[i] = copy_vars[i]->Value();
    }
    tuples.Insert(one_tuple);
  }
  s.EndSearch();
  FLAGS_cp_trace_search = trace;
  FLAGS_cp_trace_propagation = propag;
  return solver->MakeAllowedAssignments(variables, tuples);
}

/// Map from constraint identifier to constraint posting functions
class ModelBuilder {
 public:
  /// Type of constraint posting function
  typedef void (*Builder) (FlatZincModel* const model, CtSpec* const spec);
  /// Add posting function \a p with identifier \a id
  void Register(const std::string& id, Builder p);
  /// Post constraint specified by \a ce
  void Post(FlatZincModel* const model, CtSpec* const spec);

 private:
  /// The actual builders.
  std::map<std::string, Builder> r;
};

static ModelBuilder global_model_builder;

void ModelBuilder::Post(FlatZincModel* const model, CtSpec* const spec) {
  if (!spec->Nullified()) {
    const string& id = spec->Id();
    std::map<std::string, Builder>::iterator i = r.find(id);
    if (i == r.end()) {
      throw Error("ModelBuilder",
                  std::string("Constraint ") + spec->Id() + " not found");
    }
    i->second(model, spec);
  }
}

void ModelBuilder::Register(const std::string& id, Builder p) {
  r[id] = p;
}

void p_int_eq(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  if (spec->IsDefined(spec->Arg(0))) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
            << right->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(0));
    model->SetIntegerExpression(spec->Arg(0), right);
  } else if (spec->IsDefined(spec->Arg(1))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
            << left->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(1));
    model->SetIntegerExpression(spec->Arg(1), left);
  } else {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    Constraint* const ct = solver->MakeEquality(left, right);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ne(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeNonEquality(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_ge(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeGreaterOrEqual(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_gt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeGreater(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_le(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeLessOrEqual(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeLess(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

/* Comparisons */
void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsEqualCstVar(left, node_right->getInt()) :
        solver->MakeIsEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(node_right);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsDifferentCstVar(left, node_right->getInt()) :
        solver->MakeIsDifferentVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsDifferentCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsGreaterOrEqualCstVar(left, node_right->getInt()) :
        solver->MakeIsGreaterOrEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsGreaterOrEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  IntVar* const boolvar = model->GetIntExpr(spec->Arg(2))->Var();
  Constraint* const ct = solver->MakeIsGreaterCt(left, right, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_le_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar = node_right->isInt() ?
                            solver->MakeIsLessOrEqualCstVar(left, node_right->getInt()) :
                            solver->MakeIsLessOrEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsLessOrEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  IntVar* const boolvar = model->GetIntExpr(spec->Arg(2))->Var();
  Constraint* const ct = solver->MakeIsLessCt(left, right, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
  bool strong_propagation = HasDomainAnnotation(spec->annotations());
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  if (spec->DefinedArg() != NULL) {
    std::vector<int64> coefficients;
    std::vector<IntVar*> variables;
    int64 constant = 0;
    AST::Node* defined = NULL;
    for (int i = 0; i < size; ++i) {
      if (array_variables->a[i]->isInt()) {
        constant += array_coefficients->a[i]->getInt() *
                    array_variables->a[i]->getInt();
      } else if (spec->IsDefined(array_variables->a[i])) {
        CHECK(defined == NULL);
        defined = array_variables->a[i];
        if (array_coefficients->a[i]->getInt() != -1) {
          throw Error("ModelBuilder",
                      std::string("Constraint ") + spec->Id() +
                      " cannot define an integer variable with a coefficient"
                      " different from -1");
        }
      } else {
        coefficients.push_back(array_coefficients->a[i]->getInt());
        variables.push_back(model->GetIntExpr(array_variables->a[i])->Var());
      }
    }
    if (constant - rhs != 0) {
      coefficients.push_back(constant - rhs);
      variables.push_back(solver->MakeIntConst(1));
    }
    IntExpr* const target =
        solver->MakeScalProd(variables, coefficients);
    VLOG(1) << "  - creating " << defined->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(defined);
    model->SetIntegerExpression(defined, target);
  } else {
    std::vector<int64> coefficients(size);
    std::vector<IntVar*> variables(size);
    int ones = 0;
    for (int i = 0; i < size; ++i) {
      coefficients[i] = array_coefficients->a[i]->getInt();
      ones += coefficients[i] == 1;
      variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    }
    Constraint* const ct =
        strong_propagation ?
        MakeStrongScalProdEquality(solver, variables, coefficients, rhs) :
        (ones == size ?
         solver->MakeSumEquality(variables, rhs) :
         solver->MakeScalProdEquality(variables, coefficients, rhs));
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int> coefficients(size);
  std::vector<IntVar*> variables(size);

  int positive = 0;
  int negative = 0;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    if (coefficients[i] > 0) {
      positive++;
    } else if (coefficients[i] < 0) {
      negative++;
    }
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  if (negative > 0 && positive == 0) {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    rhs = -rhs;
    positive = negative;
    negative = 0;
  }
  const bool define = spec->IsDefined(node_boolvar);

  if (positive == 1) {
    IntVar* pos = NULL;
    std::vector<IntVar*> neg_vars;
    std::vector<int64> neg_coeffs;
    for (int i = 0; i < size; ++i) {
      const int64 coeff = coefficients[i];
      if (coeff > 0) {
        pos = solver->MakeProd(variables[i], coeff)->Var();
      } else if (coeff < 0) {
        neg_vars.push_back(variables[i]);
        neg_coeffs.push_back(-coeff);
      }
    }
    pos = solver->MakeSum(pos, -rhs)->Var();
    IntVar* const other = solver->MakeScalProd(neg_vars, neg_coeffs)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualVar(pos, other);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCt(pos, other, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  } else if (negative == 1) {
    IntVar* neg = NULL;
    std::vector<IntVar*> pos_vars;
    std::vector<int64> pos_coeffs;
    for (int i = 0; i < size; ++i) {
      const int64 coeff = coefficients[i];
      if (coeff < 0) {
        neg = solver->MakeProd(variables[i], -coeff)->Var();
      } else if (coeff > 0) {
        pos_vars.push_back(variables[i]);
        pos_coeffs.push_back(coeff);
      }
    }
    neg = solver->MakeSum(neg, rhs)->Var();
    IntVar* const other = solver->MakeScalProd(pos_vars, pos_coeffs)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualVar(neg, other);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCt(neg, other, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  } else {
    IntVar* const var = solver->MakeScalProd(variables, coefficients)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualCstVar(var, rhs);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCstCt(var, rhs, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  }
}

void p_int_lin_ne(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeNonEquality(
          solver->MakeScalProd(variables, coefficients)->Var(),
          rhs);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntVar* const var =
      solver->MakeScalProd(variables, coefficients)->Var();
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsDifferentCstCt(var, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_le(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  bool one_positive = false;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    if (coefficients[i] > 0) {
      one_positive = true;
    }
  }
  if (one_positive) {
    Constraint* const ct =
        solver->MakeScalProdLessOrEqual(variables, coefficients, rhs);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    Constraint* const ct =
        solver->MakeScalProdGreaterOrEqual(variables, coefficients, -rhs);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_le_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  bool one_positive = false;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    if (coefficients[i] > 0) {
      one_positive = true;
    }
  }
  if (one_positive) {
    IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsLessOrEqualCstCt(expr, rhs, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct =
        solver->MakeIsGreaterOrEqualCstCt(expr, -rhs, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_lt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdLessOrEqual(variables, coefficients, rhs - 1);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_lt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr =
      solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsLessCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ge(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdGreaterOrEqual(variables, coefficients, rhs);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsGreaterOrEqualCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_gt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdGreaterOrEqual(variables, coefficients, rhs + 1);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsGreaterCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

/* arithmetic constraints */

void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  if (spec->IsDefined(spec->Arg(0))) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    IntExpr* const left = solver->MakeDifference(target, right);
    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
            << left->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(0));
    model->SetIntegerExpression(spec->Arg(0), left);
  } else if (spec->IsDefined(spec->Arg(1))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    IntExpr* const right = solver->MakeDifference(target, left);
    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
            << right->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(1));
    model->SetIntegerExpression(spec->Arg(1), right);
  } else if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = solver->MakeSum(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeSum(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_minus(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeDifference(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeDifference(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeProd(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeProd(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_div(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const target = model->GetIntExpr(spec->Arg(2));
  if (spec->Arg(1)->isIntVar()) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeDiv(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    Constraint* const ct =
        solver->MakeEquality(
            solver->MakeDiv(left, spec->Arg(1)->getInt()), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_mod(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntVar* const left = model->GetIntExpr(spec->Arg(0))->Var();
  IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
  if (spec->Arg(1)->isIntVar()) {
    IntVar* const mod = model->GetIntExpr(spec->Arg(1))->Var();
    Constraint* const ct = solver->MakeModuloConstraint(left, mod, target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    const int64 mod = spec->Arg(1)->getInt();
    Constraint* const ct = solver->MakeModuloConstraint(left, mod, target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_min(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeMin(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeMin(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeMax(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeMax(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_negate(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const target = model->GetIntExpr(spec->Arg(2));
  Constraint* const ct =
      solver->MakeEquality(solver->MakeOpposite(left), target);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_array_bool_and(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_variables = spec->Arg(0)->getArray();
  AST::Node* const node_boolvar = spec->Arg(1);
  const int size = array_variables->a.size();
  std::vector<IntVar*> variables;
  hash_set<IntExpr*> added;
  for (int i = 0; i < size; ++i) {
    AST::Node* const a = array_variables->a[i];
    IntVar* const to_add = model->GetIntExpr(a)->Var();
    if (!ContainsKey(added, to_add)) {
      variables.push_back(to_add);
      added.insert(to_add);
    }
  }
  if (spec->IsDefined(node_boolvar)) {
    IntExpr* const boolvar = solver->MakeMin(variables);
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
  } else if (node_boolvar->isBool() && node_boolvar->getBool() == 1) {
    VLOG(1) << "  - forcing array_bool_and to 1";
    for (int i = 0; i < variables.size(); ++i) {
      variables[i]->SetValue(1);
    }
  } else {
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct =
        solver->MakeMinEquality(variables, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_array_bool_or(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_variables = spec->Arg(0)->getArray();
  AST::Node* const node_boolvar = spec->Arg(1);
  const int size = array_variables->a.size();
  std::vector<IntVar*> variables;
  hash_set<IntExpr*> added;
  for (int i = 0; i < size; ++i) {
    AST::Node* const a = array_variables->a[i];
    IntVar* const to_add = model->GetIntExpr(a)->Var();
    if (!ContainsKey(added, to_add) && to_add->Max() != 0) {
      variables.push_back(to_add);
      added.insert(to_add);
    }
  }
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar = solver->MakeMax(variables)->Var();
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
  } else if (node_boolvar->isBool() && node_boolvar->getBool() == 0) {
    VLOG(1) << "  - forcing array_bool_or to 0";
    for (int i = 0; i < variables.size(); ++i) {
      variables[i]->SetValue(0);
    }
  } else {
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeMaxEquality(variables, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_array_bool_clause(FlatZincModel* const model, CtSpec* const spec) {
  LOG(FATAL) << "array_bool_clause(" << (spec->Arg(0)->DebugString()) << ","
             << (spec->Arg(1)->DebugString())
             << ")::" << spec->annotations()->DebugString();
}

void p_array_bool_clause_reif(FlatZincModel* const model, CtSpec* const spec) {<commit_msg>array bool or and array bool and should always create a var<commit_after>/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
 *  Main authors:
 *     <NAME> <<EMAIL>>
 *
 *  Contributing authors:
 *     <NAME> <<EMAIL>>
 *
 *  Copyright:
 *     <NAME>, 2007
 *     <NAME>, 2009
 *
 *  Last modified:
 *     $Date: 2010-07-02 19:18:43 +1000 (Fri, 02 Jul 2010) $ by $Author: tack $
 *     $Revision: 11149 $
 *
 *  This file is part of Gecode, the generic constraint
 *  development environment:
 *     http://www.gecode.org
 *
 *  Permission is hereby granted, free of charge, to any person obtaining
 *  a copy of this software and associated documentation files (the
 *  "Software"), to deal in the Software without restriction, including
 *  without limitation the rights to use, copy, modify, merge, publish,
 *  distribute, sublicense, and/or sell copies of the Software, and to
 *  permit persons to whom the Software is furnished to do so, subject to
 *  the following conditions:
 *
 *  The above copyright notice and this permission notice shall be
 *  included in all copies or substantial portions of the Software.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 *
 */

#include "base/commandlineflags.h"
#include "flatzinc/flatzinc.h"

DECLARE_bool(cp_trace_search);
DECLARE_bool(cp_trace_propagation);

namespace operations_research {
extern bool HasDomainAnnotation(AST::Node* const annotations);
namespace {
// Help

Constraint* MakeStrongScalProdEquality(Solver* const solver,
                                       std::vector<IntVar*>& variables,
                                       std::vector<int64>& coefficients,
                                       int64 rhs) {
  const bool trace = FLAGS_cp_trace_search;
  const bool propag = FLAGS_cp_trace_propagation;
  FLAGS_cp_trace_search = false;
  FLAGS_cp_trace_propagation = false;
  const int size = variables.size();
  IntTupleSet tuples(size);
  Solver s("build");
  std::vector<IntVar*> copy_vars(size);
  for (int i = 0; i < size; ++i) {
    copy_vars[i] = s.MakeIntVar(variables[i]->Min(), variables[i]->Max());
  }
  s.AddConstraint(s.MakeScalProdEquality(copy_vars, coefficients, rhs));
  s.NewSearch(s.MakePhase(copy_vars,
                          Solver::CHOOSE_FIRST_UNBOUND,
                          Solver::ASSIGN_MIN_VALUE));
  while (s.NextSolution()) {
    std::vector<int> one_tuple(size);
    for (int i = 0; i < size; ++i) {
      one_tuple[i] = copy_vars[i]->Value();
    }
    tuples.Insert(one_tuple);
  }
  s.EndSearch();
  FLAGS_cp_trace_search = trace;
  FLAGS_cp_trace_propagation = propag;
  return solver->MakeAllowedAssignments(variables, tuples);
}

/// Map from constraint identifier to constraint posting functions
class ModelBuilder {
 public:
  /// Type of constraint posting function
  typedef void (*Builder) (FlatZincModel* const model, CtSpec* const spec);
  /// Add posting function \a p with identifier \a id
  void Register(const std::string& id, Builder p);
  /// Post constraint specified by \a ce
  void Post(FlatZincModel* const model, CtSpec* const spec);

 private:
  /// The actual builders.
  std::map<std::string, Builder> r;
};

static ModelBuilder global_model_builder;

void ModelBuilder::Post(FlatZincModel* const model, CtSpec* const spec) {
  if (!spec->Nullified()) {
    const string& id = spec->Id();
    std::map<std::string, Builder>::iterator i = r.find(id);
    if (i == r.end()) {
      throw Error("ModelBuilder",
                  std::string("Constraint ") + spec->Id() + " not found");
    }
    i->second(model, spec);
  }
}

void ModelBuilder::Register(const std::string& id, Builder p) {
  r[id] = p;
}

void p_int_eq(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  if (spec->IsDefined(spec->Arg(0))) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
            << right->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(0));
    model->SetIntegerExpression(spec->Arg(0), right);
  } else if (spec->IsDefined(spec->Arg(1))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
            << left->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(1));
    model->SetIntegerExpression(spec->Arg(1), left);
  } else {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    Constraint* const ct = solver->MakeEquality(left, right);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ne(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeNonEquality(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_ge(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeGreaterOrEqual(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_gt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeGreater(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_le(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeLessOrEqual(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  Constraint* const ct = solver->MakeLess(left, right);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

/* Comparisons */
void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsEqualCstVar(left, node_right->getInt()) :
        solver->MakeIsEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(node_right);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsDifferentCstVar(left, node_right->getInt()) :
        solver->MakeIsDifferentVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsDifferentCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar =
        node_right->isInt() ?
        solver->MakeIsGreaterOrEqualCstVar(left, node_right->getInt()) :
        solver->MakeIsGreaterOrEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsGreaterOrEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  IntVar* const boolvar = model->GetIntExpr(spec->Arg(2))->Var();
  Constraint* const ct = solver->MakeIsGreaterCt(left, right, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_le_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  AST::Node* const node_right = spec->Arg(1);
  AST::Node* const node_boolvar = spec->Arg(2);
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar = node_right->isInt() ?
                            solver->MakeIsLessOrEqualCstVar(left, node_right->getInt()) :
                            solver->MakeIsLessOrEqualVar(left, model->GetIntExpr(node_right));
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
    CHECK_NOTNULL(boolvar);
  } else {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsLessOrEqualCt(left, right, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  IntVar* const boolvar = model->GetIntExpr(spec->Arg(2))->Var();
  Constraint* const ct = solver->MakeIsLessCt(left, right, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
  bool strong_propagation = HasDomainAnnotation(spec->annotations());
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  if (spec->DefinedArg() != NULL) {
    std::vector<int64> coefficients;
    std::vector<IntVar*> variables;
    int64 constant = 0;
    AST::Node* defined = NULL;
    for (int i = 0; i < size; ++i) {
      if (array_variables->a[i]->isInt()) {
        constant += array_coefficients->a[i]->getInt() *
                    array_variables->a[i]->getInt();
      } else if (spec->IsDefined(array_variables->a[i])) {
        CHECK(defined == NULL);
        defined = array_variables->a[i];
        if (array_coefficients->a[i]->getInt() != -1) {
          throw Error("ModelBuilder",
                      std::string("Constraint ") + spec->Id() +
                      " cannot define an integer variable with a coefficient"
                      " different from -1");
        }
      } else {
        coefficients.push_back(array_coefficients->a[i]->getInt());
        variables.push_back(model->GetIntExpr(array_variables->a[i])->Var());
      }
    }
    if (constant - rhs != 0) {
      coefficients.push_back(constant - rhs);
      variables.push_back(solver->MakeIntConst(1));
    }
    IntExpr* const target =
        solver->MakeScalProd(variables, coefficients);
    VLOG(1) << "  - creating " << defined->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(defined);
    model->SetIntegerExpression(defined, target);
  } else {
    std::vector<int64> coefficients(size);
    std::vector<IntVar*> variables(size);
    int ones = 0;
    for (int i = 0; i < size; ++i) {
      coefficients[i] = array_coefficients->a[i]->getInt();
      ones += coefficients[i] == 1;
      variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    }
    Constraint* const ct =
        strong_propagation ?
        MakeStrongScalProdEquality(solver, variables, coefficients, rhs) :
        (ones == size ?
         solver->MakeSumEquality(variables, rhs) :
         solver->MakeScalProdEquality(variables, coefficients, rhs));
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int> coefficients(size);
  std::vector<IntVar*> variables(size);

  int positive = 0;
  int negative = 0;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    if (coefficients[i] > 0) {
      positive++;
    } else if (coefficients[i] < 0) {
      negative++;
    }
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  if (negative > 0 && positive == 0) {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    rhs = -rhs;
    positive = negative;
    negative = 0;
  }
  const bool define = spec->IsDefined(node_boolvar);

  if (positive == 1) {
    IntVar* pos = NULL;
    std::vector<IntVar*> neg_vars;
    std::vector<int64> neg_coeffs;
    for (int i = 0; i < size; ++i) {
      const int64 coeff = coefficients[i];
      if (coeff > 0) {
        pos = solver->MakeProd(variables[i], coeff)->Var();
      } else if (coeff < 0) {
        neg_vars.push_back(variables[i]);
        neg_coeffs.push_back(-coeff);
      }
    }
    pos = solver->MakeSum(pos, -rhs)->Var();
    IntVar* const other = solver->MakeScalProd(neg_vars, neg_coeffs)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualVar(pos, other);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCt(pos, other, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  } else if (negative == 1) {
    IntVar* neg = NULL;
    std::vector<IntVar*> pos_vars;
    std::vector<int64> pos_coeffs;
    for (int i = 0; i < size; ++i) {
      const int64 coeff = coefficients[i];
      if (coeff < 0) {
        neg = solver->MakeProd(variables[i], -coeff)->Var();
      } else if (coeff > 0) {
        pos_vars.push_back(variables[i]);
        pos_coeffs.push_back(coeff);
      }
    }
    neg = solver->MakeSum(neg, rhs)->Var();
    IntVar* const other = solver->MakeScalProd(pos_vars, pos_coeffs)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualVar(neg, other);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCt(neg, other, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  } else {
    IntVar* const var = solver->MakeScalProd(variables, coefficients)->Var();
    if (define) {
      IntVar* const boolvar = solver->MakeIsEqualCstVar(var, rhs);
      VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
              << boolvar->DebugString();
      model->CheckIntegerVariableIsNull(node_boolvar);
      model->SetIntegerExpression(node_boolvar, boolvar);
    } else {
      IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
      Constraint* const ct = solver->MakeIsEqualCstCt(var, rhs, boolvar);
      VLOG(1) << "  - posted " << ct->DebugString();
      solver->AddConstraint(ct);
    }
  }
}

void p_int_lin_ne(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeNonEquality(
          solver->MakeScalProd(variables, coefficients)->Var(),
          rhs);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntVar* const var =
      solver->MakeScalProd(variables, coefficients)->Var();
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsDifferentCstCt(var, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_le(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  bool one_positive = false;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    if (coefficients[i] > 0) {
      one_positive = true;
    }
  }
  if (one_positive) {
    Constraint* const ct =
        solver->MakeScalProdLessOrEqual(variables, coefficients, rhs);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    Constraint* const ct =
        solver->MakeScalProdGreaterOrEqual(variables, coefficients, -rhs);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_le_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  bool one_positive = false;
  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
    if (coefficients[i] > 0) {
      one_positive = true;
    }
  }
  if (one_positive) {
    IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeIsLessOrEqualCstCt(expr, rhs, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    for (int i = 0; i < size; ++i) {
      coefficients[i] *= -1;
    }
    IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct =
        solver->MakeIsGreaterOrEqualCstCt(expr, -rhs, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_lin_lt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdLessOrEqual(variables, coefficients, rhs - 1);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_lt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr =
      solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsLessCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ge(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdGreaterOrEqual(variables, coefficients, rhs);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_ge_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsGreaterOrEqualCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_gt(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  Constraint* const ct =
      solver->MakeScalProdGreaterOrEqual(variables, coefficients, rhs + 1);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_int_lin_gt_reif(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_coefficients = spec->Arg(0)->getArray();
  AST::Array* const array_variables = spec->Arg(1)->getArray();
  AST::Node* const node_rhs = spec->Arg(2);
  AST::Node* const node_boolvar = spec->Arg(3);
  const int64 rhs = node_rhs->getInt();
  const int size = array_coefficients->a.size();
  CHECK_EQ(size, array_variables->a.size());
  std::vector<int64> coefficients(size);
  std::vector<IntVar*> variables(size);

  for (int i = 0; i < size; ++i) {
    coefficients[i] = array_coefficients->a[i]->getInt();
    variables[i] = model->GetIntExpr(array_variables->a[i])->Var();
  }
  IntExpr* const expr = solver->MakeScalProd(variables, coefficients);
  IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
  Constraint* const ct = solver->MakeIsGreaterCstCt(expr, rhs, boolvar);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

/* arithmetic constraints */

void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  if (spec->IsDefined(spec->Arg(0))) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    IntExpr* const left = solver->MakeDifference(target, right);
    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
            << left->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(0));
    model->SetIntegerExpression(spec->Arg(0), left);
  } else if (spec->IsDefined(spec->Arg(1))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    IntExpr* const right = solver->MakeDifference(target, left);
    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
            << right->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(1));
    model->SetIntegerExpression(spec->Arg(1), right);
  } else if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = solver->MakeSum(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const left = model->GetIntExpr(spec->Arg(0));
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeSum(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_minus(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeDifference(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeDifference(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeProd(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeProd(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_div(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const target = model->GetIntExpr(spec->Arg(2));
  if (spec->Arg(1)->isIntVar()) {
    IntExpr* const right = model->GetIntExpr(spec->Arg(1));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeDiv(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    Constraint* const ct =
        solver->MakeEquality(
            solver->MakeDiv(left, spec->Arg(1)->getInt()), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_mod(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntVar* const left = model->GetIntExpr(spec->Arg(0))->Var();
  IntVar* const target = model->GetIntExpr(spec->Arg(2))->Var();
  if (spec->Arg(1)->isIntVar()) {
    IntVar* const mod = model->GetIntExpr(spec->Arg(1))->Var();
    Constraint* const ct = solver->MakeModuloConstraint(left, mod, target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  } else {
    const int64 mod = spec->Arg(1)->getInt();
    Constraint* const ct = solver->MakeModuloConstraint(left, mod, target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_min(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeMin(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeMin(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const right = model->GetIntExpr(spec->Arg(1));
  if (spec->IsDefined(spec->Arg(2))) {
    IntExpr* const target = solver->MakeMax(left, right);
    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
            << target->DebugString();
    model->CheckIntegerVariableIsNull(spec->Arg(2));
    model->SetIntegerExpression(spec->Arg(2), target);
  } else {
    IntExpr* const target = model->GetIntExpr(spec->Arg(2));
    Constraint* const ct =
        solver->MakeEquality(solver->MakeMax(left, right), target);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_int_negate(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  IntExpr* const left = model->GetIntExpr(spec->Arg(0));
  IntExpr* const target = model->GetIntExpr(spec->Arg(2));
  Constraint* const ct =
      solver->MakeEquality(solver->MakeOpposite(left), target);
  VLOG(1) << "  - posted " << ct->DebugString();
  solver->AddConstraint(ct);
}

void p_array_bool_and(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_variables = spec->Arg(0)->getArray();
  AST::Node* const node_boolvar = spec->Arg(1);
  const int size = array_variables->a.size();
  std::vector<IntVar*> variables;
  hash_set<IntExpr*> added;
  for (int i = 0; i < size; ++i) {
    AST::Node* const a = array_variables->a[i];
    IntVar* const to_add = model->GetIntExpr(a)->Var();
    if (!ContainsKey(added, to_add)) {
      variables.push_back(to_add);
      added.insert(to_add);
    }
  }
  if (spec->IsDefined(node_boolvar)) {
    IntExpr* const boolvar = solver->MakeMin(variables)->Var();
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
  } else if (node_boolvar->isBool() && node_boolvar->getBool() == 1) {
    VLOG(1) << "  - forcing array_bool_and to 1";
    for (int i = 0; i < variables.size(); ++i) {
      variables[i]->SetValue(1);
    }
  } else {
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct =
        solver->MakeMinEquality(variables, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_array_bool_or(FlatZincModel* const model, CtSpec* const spec) {
  Solver* const solver = model->solver();
  AST::Array* const array_variables = spec->Arg(0)->getArray();
  AST::Node* const node_boolvar = spec->Arg(1);
  const int size = array_variables->a.size();
  std::vector<IntVar*> variables;
  hash_set<IntExpr*> added;
  for (int i = 0; i < size; ++i) {
    AST::Node* const a = array_variables->a[i];
    IntVar* const to_add = model->GetIntExpr(a)->Var();
    if (!ContainsKey(added, to_add) && to_add->Max() != 0) {
      variables.push_back(to_add);
      added.insert(to_add);
    }
  }
  if (spec->IsDefined(node_boolvar)) {
    IntVar* const boolvar = solver->MakeMax(variables)->Var()->Var();
    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
            << boolvar->DebugString();
    model->CheckIntegerVariableIsNull(node_boolvar);
    model->SetIntegerExpression(node_boolvar, boolvar);
  } else if (node_boolvar->isBool() && node_boolvar->getBool() == 0) {
    VLOG(1) << "  - forcing array_bool_or to 0";
    for (int i = 0; i < variables.size(); ++i) {
      variables[i]->SetValue(0);
    }
  } else {
    IntVar* const boolvar = model->GetIntExpr(node_boolvar)->Var();
    Constraint* const ct = solver->MakeMaxEquality(variables, boolvar);
    VLOG(1) << "  - posted " << ct->DebugString();
    solver->AddConstraint(ct);
  }
}

void p_array_bool_clause(FlatZincModel* const model, CtSpec* const spec) {
  LOG(FATAL) << "array_bool_clause(" << (spec->Arg(0)->DebugString()) << ","
             << (spec->Arg(1)->DebugString())
             << ")::" << spec->annotations()->DebugString();
}

void p_array_bool_clause_reif(FlatZincModel* const model, CtSpec* const spec) {
{'fraction_non_alphanumeric': 0.16958249471022346, 'fraction_numerical': 0.009624812922537028, 'mean_word_length': 3.8316294726343347, 'pattern_counts': {'":': 0, '<': 809, '<?xml version=': 0, '>': 1571, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3067504', 'n_tokens_mistral': 26844, 'n_tokens_neox': 25975, 'n_words': 5321}