// Copyright 2010-2025 Google LLC
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

#include "ortools/sat/cp_model_solver.h"

#include <cstdint>
#include <string>
#include <vector>

#include "absl/container/flat_hash_set.h"
#include "absl/log/log.h"
#include "absl/strings/str_join.h"
#include "gtest/gtest.h"
#include "ortools/base/gmock.h"
#include "ortools/base/parse_test_proto.h"
#include "ortools/linear_solver/linear_solver.pb.h"
#include "ortools/port/os.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_checker.h"
#include "ortools/sat/cp_model_test_utils.h"
#include "ortools/sat/lp_utils.h"
#include "ortools/sat/model.h"
#include "ortools/sat/sat_parameters.pb.h"
#include "ortools/util/logging.h"

namespace operations_research {
namespace sat {
namespace {

using ::google::protobuf::contrib::parse_proto::ParseTestProto;
using ::testing::AnyOf;
using ::testing::Eq;
using ::testing::UnorderedElementsAre;

int AddVariable(int64_t lb, int64_t ub, CpModelProto* model) {
  const int index = model->variables_size();
  sat::IntegerVariableProto* var = model->add_variables();
  var->add_domain(lb);
  var->add_domain(ub);
  return index;
}

int AddInterval(int64_t start, int64_t size, int64_t end, CpModelProto* model) {
  const int index = model->constraints_size();
  IntervalConstraintProto* interval =
      model->add_constraints()->mutable_interval();
  interval->mutable_start()->add_vars(AddVariable(start, end - size, model));
  interval->mutable_start()->add_coeffs(1);
  interval->mutable_size()->set_offset(size);
  *interval->mutable_end() = interval->start();
  interval->mutable_end()->set_offset(size);
  return index;
}

int AddOptionalInterval(int64_t start, int64_t size, int64_t end,
                        int existing_enforcement_variable,
                        CpModelProto* model) {
  const int index = model->constraints_size();
  ConstraintProto* constraint = model->add_constraints();
  constraint->add_enforcement_literal(existing_enforcement_variable);
  IntervalConstraintProto* interval = constraint->mutable_interval();
  interval->mutable_start()->add_vars(AddVariable(start, end - size, model));
  interval->mutable_start()->add_coeffs(1);
  interval->mutable_size()->set_offset(size);
  *interval->mutable_end() = interval->start();
  interval->mutable_end()->set_offset(size);
  return index;
}

TEST(LoadCpModelTest, PureSatProblem) {
  const CpModelProto model_proto = Random3SatProblem(100, 3);
  LOG(INFO) << CpModelStats(model_proto);
  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  LOG(INFO) << CpSolverResponseStats(response);
}

TEST(LoadCpModelTest, PureSatProblemWithLimit) {
  const CpModelProto model_proto = Random3SatProblem(500);
  LOG(INFO) << CpModelStats(model_proto);
  SatParameters params;
  params.set_max_deterministic_time(0.00001);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::UNKNOWN);
  LOG(INFO) << CpSolverResponseStats(response);
}

TEST(LoadCpModelTest, BooleanLinearOptimizationProblem) {
  const CpModelProto model_proto = RandomLinearProblem(20, 5);
  LOG(INFO) << CpModelStats(model_proto);
  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  LOG(INFO) << CpSolverResponseStats(response);
}

TEST(StopAfterFirstSolutionTest, BooleanLinearOptimizationProblem) {
  const CpModelProto model_proto = RandomLinearProblem(100, 100);
  LOG(INFO) << CpModelStats(model_proto);

  Model model;
  SatParameters params;
  params.set_num_workers(8);
  params.set_stop_after_first_solution(true);

  int num_solutions = 0;
  model.Add(NewFeasibleSolutionObserver(
      [&num_solutions](const CpSolverResponse& /*r*/) { num_solutions++; }));
  model.Add(NewSatParameters(params));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::FEASIBLE);
  EXPECT_GE(num_solutions, 1);

  // Because we have 8 threads and we currently report all solution as we found
  // them, we might report more than one the time every subsolver is
  // terminated. This happens 8% of the time as of March 2020.
  EXPECT_LE(num_solutions, 2);
  LOG(INFO) << CpSolverResponseStats(response);
}

TEST(RelativeGapLimitTest, BooleanLinearOptimizationProblem) {
  const CpModelProto model_proto = RandomLinearProblem(100, 100);
  LOG(INFO) << CpModelStats(model_proto);

  Model model;
  SatParameters params;
  params.set_num_workers(1);
  params.set_relative_gap_limit(1e10);  // Should stop at the first solution!

  int num_solutions = 0;
  model.Add(NewFeasibleSolutionObserver(
      [&num_solutions](const CpSolverResponse& /*r*/) { num_solutions++; }));
  model.Add(NewSatParameters(params));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);

  // We reported OPTIMAL, but there is indeed a gap.
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_LT(response.best_objective_bound() + 1e-6, response.objective_value());
  EXPECT_EQ(1, num_solutions);
  LOG(INFO) << CpSolverResponseStats(response);
}

TEST(LoadCpModelTest, InvalidProblem) {
  CpModelProto model_proto;
  model_proto.add_variables();  // No domain.
  Model model;
  EXPECT_EQ(SolveCpModel(model_proto, &model).status(),
            CpSolverStatus::MODEL_INVALID);
}

TEST(LoadCpModelTest, UnsatProblem) {
  CpModelProto model_proto;
  for (int i = 0; i < 2; ++i) {
    AddVariable(i, i, &model_proto);
  }
  auto* ct = model_proto.add_constraints()->mutable_linear();
  ct->add_domain(0);
  ct->add_domain(0);
  ct->add_vars(0);
  ct->add_coeffs(1);
  ct->add_vars(1);
  ct->add_coeffs(1);
  Model model;
  EXPECT_EQ(SolveCpModel(model_proto, &model).status(),
            CpSolverStatus::INFEASIBLE);
}

TEST(LoadCpModelTest, SimpleCumulative) {
  CpModelProto model_proto;
  AddInterval(0, 2, 4, &model_proto);
  AddInterval(1, 2, 4, &model_proto);
  ConstraintProto* ct = model_proto.add_constraints();
  ct->mutable_cumulative()->add_intervals(0);
  ct->mutable_cumulative()->add_demands()->set_offset(3);
  ct->mutable_cumulative()->add_intervals(1);
  ct->mutable_cumulative()->add_demands()->set_offset(4);
  ct->mutable_cumulative()->mutable_capacity()->set_offset(6);

  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 0);  // start_1
  EXPECT_EQ(response.solution(1), 2);  // start_2
}

TEST(SolverCpModelTest, EmptyModel) {
  CpModelProto cp_model;
  cp_model.mutable_solution_hint();

  SatParameters params;
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, SimpleInterval) {
  CpModelProto model_proto;
  const int deadline = 6;
  const int i1 = AddInterval(0, 3, deadline, &model_proto);
  const int i3 = AddInterval(3, 3, deadline, &model_proto);
  NoOverlapConstraintProto* no_overlap =
      model_proto.add_constraints()->mutable_no_overlap();
  no_overlap->add_intervals(i1);
  no_overlap->add_intervals(i3);
  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, SimpleOptionalIntervalFeasible) {
  CpModelProto model_proto;
  const int deadline = 6;
  const int i1_enforcement = AddVariable(0, 1, &model_proto);
  const int i1 =
      AddOptionalInterval(0, 3, deadline, i1_enforcement, &model_proto);

  const int i2_enforcement = AddVariable(0, 1, &model_proto);
  const int i2 =
      AddOptionalInterval(2, 2, deadline, i2_enforcement, &model_proto);

  const int i3 = AddInterval(3, 3, deadline, &model_proto);

  NoOverlapConstraintProto* no_overlap =
      model_proto.add_constraints()->mutable_no_overlap();
  no_overlap->add_intervals(i1);
  no_overlap->add_intervals(i2);
  no_overlap->add_intervals(i3);

  BoolArgumentProto* one_of_intervals_on =
      model_proto.add_constraints()->mutable_bool_xor();
  one_of_intervals_on->add_literals(i1_enforcement);
  one_of_intervals_on->add_literals(i2_enforcement);

  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, SimpleOptionalIntervalInfeasible) {
  CpModelProto model_proto;
  const int deadline = 6;
  const int i1_enforcement = AddVariable(0, 1, &model_proto);
  const int i1 =
      AddOptionalInterval(0, 3, deadline, i1_enforcement, &model_proto);

  const int i2_enforcement = AddVariable(0, 1, &model_proto);
  const int i2 =
      AddOptionalInterval(2, 2, deadline, i2_enforcement, &model_proto);

  const int i3 = AddInterval(3, 3, deadline, &model_proto);

  NoOverlapConstraintProto* no_overlap =
      model_proto.add_constraints()->mutable_no_overlap();
  no_overlap->add_intervals(i1);
  no_overlap->add_intervals(i2);
  no_overlap->add_intervals(i3);

  BoolArgumentProto* one_of_intervals_on =
      model_proto.add_constraints()->mutable_bool_and();
  one_of_intervals_on->add_literals(i1_enforcement);
  one_of_intervals_on->add_literals(i2_enforcement);

  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(SolveCpModelTest, NoOverlapWithEnforcementLiteral) {
  CpModelProto model_proto;
  const int enforcement = AddVariable(0, 1, &model_proto);
  const int i1 = AddInterval(0, 3, 5, &model_proto);
  const int i2 = AddInterval(0, 2, 5, &model_proto);

  ConstraintProto* no_overlap = model_proto.add_constraints();
  no_overlap->add_enforcement_literal(enforcement);
  no_overlap->mutable_no_overlap()->add_intervals(i1);
  no_overlap->mutable_no_overlap()->add_intervals(i2);

  Model model;
  SatParameters params;
  params.set_enumerate_all_solutions(true);
  model.Add(NewSatParameters(params));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // Two solutions when the constraint is enforced (i1 before i2, or i2 before
  // i1, tightly packed), and 3 * 4 otherwise -- 3 possible starts for i1, 4 for
  // i2).
  EXPECT_EQ(count, 2 + 3 * 4);
}

TEST(SolveCpModelTest, NoOverlap2DWithEnforcementLiteral) {
  CpModelProto model_proto;
  const int enforcement = AddVariable(0, 1, &model_proto);
  const int i1 = AddInterval(0, 3, 5, &model_proto);
  const int i2 = AddInterval(0, 2, 5, &model_proto);
  const int i3 = AddInterval(0, 4, 5, &model_proto);
  const int i4 = AddInterval(0, 1, 2, &model_proto);
  const int i5 = AddInterval(0, 1, 2, &model_proto);
  const int i6 = AddInterval(0, 1, 2, &model_proto);

  ConstraintProto* no_overlap_2d = model_proto.add_constraints();
  no_overlap_2d->add_enforcement_literal(enforcement);
  no_overlap_2d->mutable_no_overlap_2d()->add_x_intervals(i1);
  no_overlap_2d->mutable_no_overlap_2d()->add_x_intervals(i2);
  no_overlap_2d->mutable_no_overlap_2d()->add_x_intervals(i3);
  no_overlap_2d->mutable_no_overlap_2d()->add_y_intervals(i4);
  no_overlap_2d->mutable_no_overlap_2d()->add_y_intervals(i5);
  no_overlap_2d->mutable_no_overlap_2d()->add_y_intervals(i6);

  Model model;
  SatParameters params;
  params.set_enumerate_all_solutions(true);
  model.Add(NewSatParameters(params));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // Eight solutions when the constraint is enforced (i1 before i2 on x, or i2
  // before i1 on x, tightly packed, each with 2 possible x starts for i3, and
  // two vertical placements -- i1 and i2 above or below i4), and 3 * 4 * 2^4
  // otherwise -- 3 possible starts for i1, 4 for i2, 2 for i3, i4, i5, and i6).
  EXPECT_EQ(count, 8 + 3 * 4 * 2 * 2 * 2 * 2);
}

TEST(SolveCpModelTest, CumulativeWithEnforcementLiteral) {
  CpModelProto model_proto;
  const int enforcement = AddVariable(0, 1, &model_proto);
  const int i1 = AddInterval(0, 3, 5, &model_proto);
  const int i2 = AddInterval(0, 2, 5, &model_proto);
  const int i3 = AddInterval(0, 4, 5, &model_proto);

  ConstraintProto* cumulative = model_proto.add_constraints();
  cumulative->add_enforcement_literal(enforcement);
  cumulative->mutable_cumulative()->add_intervals(i1);
  cumulative->mutable_cumulative()->add_intervals(i2);
  cumulative->mutable_cumulative()->add_intervals(i3);
  cumulative->mutable_cumulative()->add_demands()->set_offset(1);
  cumulative->mutable_cumulative()->add_demands()->set_offset(1);
  cumulative->mutable_cumulative()->add_demands()->set_offset(1);
  cumulative->mutable_cumulative()->mutable_capacity()->set_offset(2);

  Model model;
  SatParameters params;
  params.set_enumerate_all_solutions(true);
  model.Add(NewSatParameters(params));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // Four solutions when the constraint is enforced (i1 before i2, or i2 before
  // i1, tightly packed, each with 2 possible starts for i3), and 3 * 4 * 2
  // otherwise -- 3 possible starts for i1, 4 for i2, 2 for i3).
  EXPECT_EQ(count, 4 + 3 * 4 * 2);
}

TEST(SolveCpModelTest, NonInstantiatedVariables) {
  CpModelProto model_proto;
  const int a = AddVariable(0, 10, &model_proto);
  const int b = AddVariable(0, 10, &model_proto);
  auto* linear_constraint = model_proto.add_constraints()->mutable_linear();
  linear_constraint->add_vars(a);
  linear_constraint->add_vars(b);
  linear_constraint->add_coeffs(1);
  linear_constraint->add_coeffs(1);
  linear_constraint->add_domain(4);
  linear_constraint->add_domain(5);

  // We need to fix the first one, otherwise the lower bound will not be
  // enough for the second.
  model_proto.add_search_strategy()->add_variables(0);

  Model model;
  SatParameters params;
  params.set_instantiate_all_variables(false);
  params.set_search_branching(SatParameters::FIXED_SEARCH);
  params.set_cp_model_presolve(false);
  params.set_num_workers(1);
  model.Add(NewSatParameters(params));

  const CpSolverResponse response = SolveCpModel(model_proto, &model);

  // Because we didn't try to instantiate the variables, we just did one round
  // of propagation. Note that this allows to use the solve as a simple
  // propagation engine with no search decision (modulo the binary variable that
  // will be instantiated anyway)!
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  ASSERT_EQ(2, response.solution_size());
  EXPECT_EQ(response.solution(0), 0);

  // Note that this one was not instantiated, but we used its lower bound.
  EXPECT_EQ(response.solution(1), 4);
}

// When there is nothing to do, we had a bug that didn't copy the solution
// with the core based solver, this simply test this corner case.
TEST(SolveCpModelTest, TrivialModelWithCore) {
  CpModelProto model_proto;
  const int a = AddVariable(1, 1, &model_proto);
  model_proto.mutable_objective()->add_vars(a);
  model_proto.mutable_objective()->add_coeffs(1);
  Model model;
  SatParameters params;
  params.set_optimize_with_core(true);
  params.set_cp_model_presolve(false);
  model.Add(NewSatParameters(params));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_TRUE(SolutionIsFeasible(
      model_proto, std::vector<int64_t>(response.solution().begin(),
                                        response.solution().end())));
}

#if ORTOOLS_TARGET_OS_SUPPORTS_THREADS

TEST(SolveCpModelTest, IntervalsWithSeveralEnforcementLiterals) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      enforcement_literal: [ 0, 1 ]
      interval {
        start { offset: 0 }
        end { offset: 1 }
        size { offset: 1 }
      }
    }
    constraints {
      enforcement_literal: [ 1, 2 ]
      interval {
        start { offset: 0 }
        end { offset: 1 }
        size { offset: 1 }
      }
    }
    constraints {
      enforcement_literal: [ 2, 0 ]
      interval {
        start { offset: 0 }
        end { offset: 1 }
        size { offset: 1 }
      }
    }
    constraints { no_overlap { intervals: [ 0, 1, 2 ] } }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // All combinations except (1, 1, 1) are feasible.
  EXPECT_EQ(count, 7);
}

TEST(SolveCpModelTest, TrivialLinearTranslatedModel) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: -10 domain: 10 }
    variables { domain: -10 domain: 10 }
    variables { domain: -461168601842738790 domain: 461168601842738790 }
    constraints {
      linear {
        vars: 0
        vars: 1
        coeffs: 1
        coeffs: 1
        domain: -4611686018427387903
        domain: 4611686018427387903
      }
    }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 2
        coeffs: -1
        domain: 0
        domain: 0
      }
    }
    objective { vars: 2 coeffs: -1 scaling_factor: -1 }
  )pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_TRUE(SolutionIsFeasible(
      model_proto, std::vector<int64_t>(response.solution().begin(),
                                        response.solution().end())));
}

TEST(ConvertMPModelProtoToCpModelProtoTest, SimpleLinearExampleWithMaximize) {
  const MPModelProto mp_model = ParseTestProto(R"pb(
    maximize: true
    objective_offset: 0
    variable {
      lower_bound: -10
      upper_bound: 10
      objective_coefficient: 1
      is_integer: true
    }
    variable {
      lower_bound: -10
      upper_bound: 10
      objective_coefficient: 2
      is_integer: true
    }
    constraint {
      lower_bound: -100
      upper_bound: 100
      var_index: 0
      var_index: 1
      coefficient: 1
      coefficient: 1
    }
  )pb");
  CpModelProto cp_model;
  SolverLogger logger;
  ConvertMPModelProtoToCpModelProto(SatParameters(), mp_model, &cp_model,
                                    &logger);
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(cp_model, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_TRUE(SolutionIsFeasible(
      cp_model, std::vector<int64_t>(response.solution().begin(),
                                     response.solution().end())));
}

TEST(SolveCpModelTest, SmallDualConnectedComponentsModel) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 1 coeffs: 2 domain: 0 domain: 8 }
    }
    constraints {
      linear { vars: 2 vars: 3 coeffs: 1 coeffs: 2 domain: 0 domain: 6 }
    }
    objective {
      vars: 0
      vars: 1
      vars: 2
      vars: 3
      coeffs: -1
      coeffs: -2
      coeffs: -3
      coeffs: -4
      scaling_factor: -1
    }
  )pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_TRUE(SolutionIsFeasible(
      model_proto, std::vector<int64_t>(response.solution().begin(),
                                        response.solution().end())));
}

TEST(SolveCpModelTest, DualConnectedComponentsModel) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 1 coeffs: 2 domain: 0 domain: 8 }
    }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 1 coeffs: 1 domain: 2 domain: 20 }
    }
    constraints {
      linear { vars: 2 vars: 3 coeffs: 1 coeffs: 2 domain: 0 domain: 6 }
    }
    constraints {
      linear { vars: 2 vars: 3 coeffs: 1 coeffs: 1 domain: 2 domain: 20 }
    }
    objective {
      vars: 0
      vars: 1
      vars: 2
      vars: 3
      coeffs: -1
      coeffs: -2
      coeffs: -3
      coeffs: -4
      scaling_factor: -1
    }
  )pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_TRUE(SolutionIsFeasible(
      model_proto, std::vector<int64_t>(response.solution().begin(),
                                        response.solution().end())));
}

TEST(SolveCpModelTest, EnumerateAllSolutions) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    constraints {
      all_diff {
        exprs { vars: 0 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
        exprs { vars: 2 coeffs: 1 }
        exprs { vars: 3 coeffs: 1 }
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 24);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsBis) {
  const std::string model_str = R"pb(
    variables { domain: 0 domain: 5 }
    variables { domain: 0 domain: 5 }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 1 coeffs: 1 domain: 6 domain: 6 }
    }
  )pb";
  const CpModelProto model_proto = ParseTestProto(model_str);

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
        // Test the response was correctly filled.
        EXPECT_NE(0, response.num_branches());
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 5);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsDomainsWithHoleInVar) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 1 domain: 2 domain: 4 domain: 5 }
    constraints {
      enforcement_literal: 0
      enforcement_literal: 1
      linear { vars: 2 coeffs: 1 domain: 2 domain: 2 }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 3 * 4 + 1);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsDomainsWithHoleInEnforcedLinear1) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 1 domain: 5 }
    constraints {
      enforcement_literal: 0
      enforcement_literal: 1
      linear {
        vars: 2
        coeffs: 1
        domain: [ 1, 2, 4, 4 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 5 * 3 + 3);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsDomainsWithHoleInEnforcedLinear2) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 2 }
    variables { domain: 0 domain: 2 }
    constraints {
      enforcement_literal: 0
      enforcement_literal: 1
      linear {
        vars: 2
        coeffs: 1
        vars: 3
        coeffs: 1
        domain: [ 0, 1, 3, 4 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 9 * 3 + (9 - 3));
}

TEST(SolveCpModelTest, EnumerateAllSolutionsDomainsWithHoleInLinear2) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 2 }
    variables { domain: 0 domain: 2 }
    constraints {
      linear {
        vars: 0
        coeffs: 1
        vars: 1
        coeffs: 1
        domain: [ 0, 1, 3, 4 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 9 - 3);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsAndCopyToResponse) {
  const std::string model_str = R"pb(
    variables { domain: 0 domain: 5 }
    variables { domain: 0 domain: 5 }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 1 coeffs: 1 domain: 6 domain: 6 }
    }
  )pb";
  const CpModelProto model_proto = ParseTestProto(model_str);

  SatParameters params;
  params.set_enumerate_all_solutions(true);
  params.set_fill_additional_solutions_in_response(true);
  params.set_solution_pool_size(1000);  // A big enough value.

  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  std::vector<std::vector<int64_t>> additional_solutions;
  for (const auto& solution : response.additional_solutions()) {
    additional_solutions.push_back(std::vector<int64_t>(
        solution.values().begin(), solution.values().end()));
  }
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_THAT(additional_solutions,
              UnorderedElementsAre(
                  UnorderedElementsAre(1, 5), UnorderedElementsAre(2, 4),
                  UnorderedElementsAre(3, 3), UnorderedElementsAre(4, 2),
                  UnorderedElementsAre(5, 1)));

  // Not setting the solution_pool_size high enough gives partial result.
  // Because we randomize variable order, we don't know which solution will be
  // in the pool deterministically.
  params.set_solution_pool_size(3);
  const CpSolverResponse response2 = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response2.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response2.additional_solutions().size(), 3);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsOfEmptyModel) {
  const std::string model_str = R"pb(
    variables { domain: 0 domain: 2 }
    variables { domain: 0 domain: 2 }
    variables { domain: 0 domain: 2 }
  )pb";
  const CpModelProto model_proto = ParseTestProto(model_str);

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 27);
}

TEST(SolveCpModelTest, SolutionsAreCorrectlyPostsolvedInTheObserver) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 1 }
    variables { domain: 3 domain: 3 }
    variables { domain: 1 domain: 4 }
  )pb");
  Model model;
  model.Add(NewFeasibleSolutionObserver([](const CpSolverResponse& response) {
    EXPECT_EQ(response.solution_size(), 4);
    LOG(INFO) << absl::StrJoin(response.solution(), " ");
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, ObjectiveDomainLowerBound) {
  // y = 10 - 2x.
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 10 }
    variables { domain: 1 domain: 10 }
    constraints {
      linear { vars: 0 vars: 1 coeffs: 2 coeffs: 1 domain: 10 domain: 10 }
    }
    objective { vars: 1 coeffs: 1 domain: 1 domain: 10 }
  )pb");
  for (int lb = 1; lb <= 8; ++lb) {
    model_proto.mutable_objective()->set_domain(0, lb);
    Model model;
    model.Add(NewSatParameters("cp_model_presolve:false"));
    const CpSolverResponse response = SolveCpModel(model_proto, &model);
    EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
    EXPECT_EQ(response.objective_value(), lb % 2 ? lb + 1 : lb);
  }
}

TEST(SolveCpModelTest, AtMostAndExactlyOneWithEnforcementLiteral) {
  // a => at_most_one(a, a)
  // not(b) => exactly_one(not(b), not(b))
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      enforcement_literal: 0
      at_most_one { literals: [ 0, 0 ] }
    }
    constraints {
      enforcement_literal: -2
      exactly_one { literals: [ -2, -2 ] }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_THAT(response.solution(), ::testing::ElementsAre(0, 1));
}

TEST(SolveCpModelTest, BoolXorWithEnforcementLiteral) {
  // a => a xor b
  // not(a) => a xor a
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      enforcement_literal: 0
      bool_xor { literals: [ 0, 1 ] }
    }
    constraints {
      enforcement_literal: -1
      bool_xor { literals: [ 0, 0 ] }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_THAT(response.solution(), ::testing::ElementsAre(1, 0));
}

TEST(SolveCpModelTest, BoolXorWithEnforcementLiteralPresolved) {
  // a => a xor b
  // not(a) => a xor a
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      enforcement_literal: 0
      bool_xor { literals: [ 0, 1 ] }
    }
    constraints {
      enforcement_literal: -1
      bool_xor { literals: [ 0, 0 ] }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:true"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_THAT(response.solution(), ::testing::ElementsAre(1, 0));
}

TEST(SolveCpModelTest, IntDivWithEnforcementLiteral) {
  // not(b) => 7x / 3y = 17, x in [0, 10], y in [1, 2]
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 10 ] }
    variables { domain: [ 1, 2 ] }
    constraints {
      enforcement_literal: -1
      int_prod {
        target { offset: 17 }
        exprs { vars: 1 coeffs: 7 }
        exprs { vars: 2 coeffs: 3 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, IntModWithEnforcementLiteral) {
  // not(b) => x % 10 = y, x in [8, 11], y in [2, 7]
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 2, 7 ] }
    variables { domain: [ 8, 11 ] }
    constraints {
      enforcement_literal: -1
      int_prod {
        target { vars: 1 coeffs: 1 }
        exprs { vars: 2 coeffs: 1 }
        exprs { offset: 10 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, IntProdWithEnforcementLiteral) {
  // not(b) => x.y.z = 17
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 2, 20 ] }
    variables { domain: [ 2, 20 ] }
    variables { domain: [ 2, 20 ] }
    constraints {
      enforcement_literal: -1
      int_prod {
        target { offset: 17 }
        exprs { vars: 1 coeffs: 1 }
        exprs { vars: 2 coeffs: 1 }
        exprs { vars: 3 coeffs: 1 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, SquareIntProdWithEnforcementLiteral) {
  // not(b) => x^2 = 17
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 2, 20 ] }
    constraints {
      enforcement_literal: -1
      int_prod {
        target { offset: 17 }
        exprs { vars: 1 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, IntProdWithEnforcementLiteralButNoTerms) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 0
      int_prod { target { vars: 0 coeffs: -4096 offset: 4096 } }
    }
  )pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, LinMaxObjectiveDomainLowerBoundInfeasible) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 3 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 0, 1 ]
      }
    }
    constraints {
      linear {
        vars: [ 2 ]
        coeffs: [ 1 ]
        domain: [ 2, 9223372036854775807 ]
      }
    }
    constraints {
      lin_max {
        target { vars: 2 coeffs: 1 }
        exprs { vars: 0 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
      }
    }
    objective { vars: 2 coeffs: 1 }
  )pb");

  Model model;
  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(SolveCpModelTest, LinMaxUniqueTargetLowerBoundInfeasible) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 3 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 0, 1 ]
      }
    }
    constraints {
      linear {
        vars: [ 2 ]
        coeffs: [ 1 ]
        domain: [ 2, 9223372036854775807 ]
      }
    }
    constraints {
      lin_max {
        target { vars: 2 coeffs: 1 }
        exprs { vars: 0 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
      }
    }
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(SolveCpModelTest, LinMaxUniqueTarget) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 4 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 0, 1 ]
      }
    }
    constraints {
      linear {
        vars: [ 2 ]
        coeffs: [ 1 ]
        domain: [ 0, 4 ]
      }
    }
    constraints {
      lin_max {
        target { vars: 2 coeffs: 1 }
        exprs { vars: 0 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
      }
    }
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, LinMaxWithEnforcementLiteral) {
  // not(b) => z = max(x, y), x in [2, 5], y in [0, 4], z in [6, 9].
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 2, 5 ] }
    variables { domain: [ 0, 4 ] }
    variables { domain: [ 6, 9 ] }
    constraints {
      enforcement_literal: -1
      lin_max {
        target { vars: 3 coeffs: 1 }
        exprs { vars: 1 coeffs: 1 }
        exprs { vars: 2 coeffs: 1 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, AllDifferentWithEnforcementLiteral) {
  // not(b) => all_diff(x, y+1, 2-z), x,y+1,3-z in [1, 2].
  CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 1, 2 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 1, 2 ] }
    constraints {
      enforcement_literal: -1
      all_diff {
        exprs { vars: 1 coeffs: 1 }
        exprs { vars: 2 coeffs: 1 offset: 1 }
        exprs { vars: 3 coeffs: -1 offset: 3 }
      }
    })pb");
  Model model;
  model.Add(NewSatParameters("cp_model_presolve:false"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.solution(0), 1);
}

TEST(SolveCpModelTest, FeasibleCircuitWithEnforcementLiteral) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 3
      circuit {
        tails: [ 0, 1, 2, 3, 0, 2, 1 ]
        heads: [ 1, 2, 3, 0, 2, 1, 3 ]
        literals: [ 0, 1, 2, 3, 4, 5, 6 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) {
    LOG(INFO) << absl::StrJoin(response.solution(), " ");
    EXPECT_TRUE(SolutionIsFeasible(
        model_proto, std::vector<int64_t>(response.solution().begin(),
                                          response.solution().end())));
    ++count;
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // Two feasible circuits (0, 1, 2, 3) and (0, 2, 1, 3), plus 2^6 solutions
  // when the circuit constraint is not enforced.
  EXPECT_EQ(count, 2 + 2 * 2 * 2 * 2 * 2 * 2);
}

TEST(SolveCpModelTest, InfeasibleCircuitDueToMultiArcsWithEnforcementLiteral) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 2
      circuit {
        tails: [ 0, 0, 1 ]
        heads: [ 1, 1, 0 ]
        literals: [ 0, 0, 1 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) {
    LOG(INFO) << absl::StrJoin(response.solution(), " ");
    EXPECT_TRUE(SolutionIsFeasible(
        model_proto, std::vector<int64_t>(response.solution().begin(),
                                          response.solution().end())));
    ++count;
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // No feasible circuit, but 2 solutions with a false enforcement literal.
  EXPECT_EQ(count, 2);
}

TEST(SolveCpModelTest,
     InfeasibleCircuitDueToMissingArcsWithEnforcementLiteral) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 4
      circuit {
        tails: [ 0, 1, 0, 2 ]
        heads: [ 1, 1, 2, 2 ]
        literals: [ 0, 1, 2, 3 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) {
    LOG(INFO) << absl::StrJoin(response.solution(), " ");
    EXPECT_TRUE(SolutionIsFeasible(
        model_proto, std::vector<int64_t>(response.solution().begin(),
                                          response.solution().end())));
    ++count;
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // No feasible circuit, but 2^4 solutions with a false enforcement literal.
  EXPECT_EQ(count, 2 * 2 * 2 * 2);
}

// The graph look like this with a self-loop at 2. If 2 is not selected
// (self-loop) then there is one solution (0,1,3,0) and (0,3,5,0). Otherwise,
// there is 2 more solutions with 2 inserted in one of the two routes.
//
//   0  ---> 1 ---> 4 -------------
//   |       |      ^             |
//   |       -----> 2* --> 5 ---> 0
//   |              ^      ^
//   |              |      |
//   -------------> 3 ------
//
TEST(CircuitConstraintTest, RouteConstraintWithEnforcementLiteral) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 11
      routes {
        tails: [ 0, 0, 1, 1, 2, 2, 2, 3, 3, 4, 5 ]
        heads: [ 1, 3, 2, 4, 2, 4, 5, 2, 5, 0, 0 ]
        literals: [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(NewFeasibleSolutionObserver([&](const CpSolverResponse& response) {
    LOG(INFO) << absl::StrJoin(response.solution(), " ");
    EXPECT_TRUE(SolutionIsFeasible(
        model_proto, std::vector<int64_t>(response.solution().begin(),
                                          response.solution().end())));
    ++count;
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  // 3 solutions when the constraint is enforced, 2^11 otherwise.
  EXPECT_EQ(count, 3 + 2048);
}

TEST(SolveCpModelTest, HintWithCore) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 5 ] }
    variables { domain: [ 0, 5 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 2, 8 ]
      }
    }
    objective {
      vars: [ 0, 1 ]
      coeffs: [ 1, 1 ]
      scaling_factor: 1
    }
    solution_hint {
      vars: [ 0, 1 ]
      values: [ 2, 3 ]
    }
  )pb");
  Model model;
  model.Add(NewSatParameters("optimize_with_core:true, linearization_level:0"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(2.0, response.objective_value());
}

TEST(SolveCpModelTest, BadHintWithCore) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 5 }
    variables { domain: 0 domain: 5 }
    variables { domain: 2 domain: 8 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 1
        coeffs: -1
        domain: 0
        domain: 0
      }
    }
    objective { vars: 2 scaling_factor: 1 coeffs: 1 }
    solution_hint { vars: 0 vars: 1 values: 4 values: 5 }
  )pb");
  Model model;
  model.Add(NewSatParameters("optimize_with_core:true, linearization_level:0"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(2.0, response.objective_value());
}

TEST(SolveCpModelTest, ForcedBadHint) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 5 }
    variables { domain: 0 domain: 5 }
    variables { domain: 2 domain: 8 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 1
        coeffs: -1
        domain: 0
        domain: 0
      }
    }
    objective { vars: 2 scaling_factor: 1 coeffs: 1 }
    solution_hint { vars: 0 vars: 1 values: 4 values: 5 }
  )pb");
  Model model;
  model.Add(NewSatParameters(
      "fix_variables_to_their_hinted_value:true, linearization_level:0"));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(SolveCpModelTest, UnforcedBadHint) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 5 }
    variables { domain: 0 domain: 5 }
    variables { domain: 2 domain: 8 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 1
        coeffs: -1
        domain: 0
        domain: 0
      }
    }
    objective { vars: 2 scaling_factor: 1 coeffs: 1 }
    solution_hint { vars: 0 vars: 1 values: 4 values: 5 }
  )pb");
  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, HintWithNegativeRef) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    solution_hint { vars: -1 values: 1 }
  )pb");
  Model model;
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(SolveCpModelTest, SolutionHintBasicTest) {
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_num_workers(1);
  for (int loop = 0; loop < 50; ++loop) {
    CpModelProto model_proto;

    // Because the random problem might be UNSAT, we loop a few times until we
    // have a SAT one.
    for (;;) {
      model_proto = Random3SatProblem(200, 3);

      // Find a solution.
      Model model;
      model.Add(NewSatParameters(params));
      const CpSolverResponse response = SolveCpModel(model_proto, &model);
      if (response.status() != CpSolverStatus::OPTIMAL) continue;
      if (response.num_conflicts() == 0) continue;

      // Copy the solution to the hint.
      for (int i = 0; i < response.solution_size(); ++i) {
        model_proto.mutable_solution_hint()->add_vars(i);
        model_proto.mutable_solution_hint()->add_values(response.solution(i));
      }
      break;
    }

    // Now solve again, we should have no conflict!
    {
      Model model;
      int num_solution = 0;
      model.Add(NewSatParameters(params));
      model.Add(NewFeasibleSolutionObserver(
          [&num_solution](const CpSolverResponse& /*r*/) { num_solution++; }));
      const CpSolverResponse response = SolveCpModel(model_proto, &model);
      EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
      EXPECT_EQ(response.num_conflicts(), 0);
      EXPECT_EQ(num_solution, 1);
    }
  }
}

TEST(SolveCpModelTest, SolutionHintRepairTest) {
  SatParameters params;
  params.set_num_workers(1);
  params.set_cp_model_presolve(false);

  // NOTE(user): This test doesn't ensure that the hint is repaired. It only
  // makes sure that the solver doesn't crash if the hint is perturbed.
  CpModelProto model_proto;

  // Because the random problem might be UNSAT, we loop a few times until we
  // have a SAT one.
  for (;;) {
    model_proto = Random3SatProblem(200, 3);

    // Find a solution.
    Model model;
    model.Add(NewSatParameters(params));

    const CpSolverResponse response = SolveCpModel(model_proto, &model);
    if (response.status() != CpSolverStatus::OPTIMAL) continue;
    if (response.num_conflicts() == 0) continue;

    // Copy the solution to the hint with small perturbation.
    model_proto.mutable_solution_hint()->add_vars(0);
    model_proto.mutable_solution_hint()->add_values(response.solution(0) ^ 1);
    for (int i = 1; i < response.solution_size(); ++i) {
      model_proto.mutable_solution_hint()->add_vars(i);
      model_proto.mutable_solution_hint()->add_values(response.solution(i));
    }
    break;
  }

  // Now solve again.
  {
    Model model;
    params.set_repair_hint(true);
    model.Add(NewSatParameters(params));
    int num_solution = 0;
    model.Add(NewFeasibleSolutionObserver(
        [&num_solution](const CpSolverResponse& /*r*/) { num_solution++; }));
    const CpSolverResponse response = SolveCpModel(model_proto, &model);
    EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
    EXPECT_EQ(num_solution, 1);
  }
}

TEST(SolveCpModelTest, SolutionHintMinimizeL1DistanceTest) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      linear {
        vars: [ 0, 1, 2, 3 ]
        coeffs: [ 1, 1, 1, 1 ]
        domain: [ 1, 1 ]
      }
    }
    objective {
      vars: [ 0, 1, 2, 3 ]
      coeffs: [ 1, 2, 4, 8 ]
    }
    solution_hint {
      vars: [ 0, 1, 2, 3 ]
      values: [ 0, 1, 0, 1 ]
    }
  )pb");

  // TODO(user): Instead, we might change the presolve to always try to keep the
  // given hint feasible.
  Model model;
  SatParameters params;
  params.set_repair_hint(true);
  params.set_stop_after_first_solution(true);
  params.set_keep_all_feasible_solutions_in_presolve(true);
  params.set_num_workers(1);
  model.Add(NewSatParameters(params));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_THAT(response.status(),
              AnyOf(Eq(CpSolverStatus::OPTIMAL), Eq(CpSolverStatus::FEASIBLE)));
  EXPECT_THAT(response.objective_value(), AnyOf(Eq(1), Eq(2), Eq(4), Eq(8)));
}

TEST(SolveCpModelTest, SolutionHintObjectiveTest) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    objective {
      vars: [ 0, 1, 2, 3 ]
      coeffs: [ 1, 2, 3, 4 ]
    }
    solution_hint {
      vars: [ 0, 1, 2, 3 ]
      values: [ 1, 0, 0, 1 ]
    }
  )pb");
  Model model;
  std::vector<double> solutions;
  SatParameters* parameters = model.GetOrCreate<SatParameters>();
  parameters->set_cp_model_presolve(false);
  parameters->set_log_search_progress(true);
  model.Add(
      NewFeasibleSolutionObserver([&solutions](const CpSolverResponse& r) {
        solutions.push_back(r.objective_value());
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  ASSERT_GE(solutions.size(), 2);
  EXPECT_EQ(solutions[0], 5.0);
  EXPECT_EQ(solutions.back(), 0.0);
}

TEST(SolveCpModelTest, SolutionHintOptimalObjectiveTest) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    objective {
      vars: [ 0, 1, 2, 3 ]
      coeffs: [ -1, 2, 3, -4 ]
    }
    solution_hint {
      vars: [ 0, 1, 2, 3 ]
      values: [ 1, 0, 0, 1 ]
    }
  )pb");
  Model model;
  std::vector<double> solutions;
  model.Add(
      NewFeasibleSolutionObserver([&solutions](const CpSolverResponse& r) {
        solutions.push_back(r.objective_value());
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  ASSERT_EQ(solutions.size(), 1);
  EXPECT_EQ(solutions[0], -5.0);
}

TEST(SolveCpModelTest, SolutionHintEnumerateTest) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { name: "x" domain: 0 domain: 10 }
    variables { name: "y" domain: 0 domain: 10 }
    constraints {
      linear { vars: 1 vars: 0 coeffs: 1 coeffs: 1 domain: 10 domain: 10 }
    }
    solution_hint { vars: 0 values: -1 }
  )pb");
  Model model;
  SatParameters parameters;
  parameters.set_cp_model_presolve(false);
  parameters.set_enumerate_all_solutions(true);
  model.Add(NewSatParameters(parameters));
  int num_solutions = 0;
  model.Add(NewFeasibleSolutionObserver(
      [&num_solutions](const CpSolverResponse& /*r*/) { num_solutions++; }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(num_solutions, 11);
}

TEST(SolveCpModelTest, SolutionHintAndAffineRelation) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 4, 4, 8, 8, 12, 12 ] }
    variables { domain: [ 2, 2, 4, 4, 6, 6 ] }
    solution_hint {
      vars: [ 0, 1 ]
      values: [ 8, 4 ]
    }
  )pb");
  SatParameters params;
  params.set_enumerate_all_solutions(true);
  params.set_stop_after_first_solution(true);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::FEASIBLE);
  EXPECT_EQ(response.solution(0), 8);
  EXPECT_EQ(response.solution(1), 4);
  EXPECT_EQ(response.num_conflicts(), 0);
}

TEST(SolveCpModelTest, MultipleEnforcementLiteral) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 0, 4 ] }
    variables { domain: [ 0, 4 ] }
    constraints {
      enforcement_literal: [ 0, 1 ]
      linear {
        vars: [ 2, 3 ]
        coeffs: [ 1, -1 ]
        domain: [ 0, 0 ]
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 25 + 25 + 25 + /*when enforced*/ 5);
}

TEST(SolveCpModelTest, IntProdWithNonAffineExpressions) {
  // z = (x-2y-1)^2 = (3-x)(1+x)
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables {
      name: "x"
      domain: [ -5, 5 ]
    }
    variables {
      name: "y"
      domain: [ -5, 5 ]
    }
    variables {
      name: "z"
      domain: [ -5, 5 ]
    }
    constraints {
      int_prod {
        target { vars: 2 coeffs: 1 }
        exprs {
          vars: [ 0, 1 ]
          coeffs: [ 1, -2 ]
          offset: -1
        }
        exprs {
          vars: [ 0, 1 ]
          coeffs: [ 1, -2 ]
          offset: -1
        }
      }
    }
    constraints {
      int_prod {
        target { vars: 2 coeffs: 1 }
        exprs { vars: 0 coeffs: -1 offset: 3 }
        exprs { vars: 0 coeffs: 1 offset: 1 }
      }
    }
  )pb");

  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  absl::flat_hash_set<std::vector<int>> solutions;
  model.Add(NewFeasibleSolutionObserver([&solutions](
                                            const CpSolverResponse& response) {
    solutions.insert({response.solution().begin(), response.solution().end()});
  }));
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_THAT(solutions,
              testing::UnorderedElementsAre(testing::ElementsAre(-1, -1, 0),
                                            testing::ElementsAre(1, -1, 4),
                                            testing::ElementsAre(1, 1, 4),
                                            testing::ElementsAre(3, 1, 0)));
}

TEST(SolveCpModelTest, TightenedDomains) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 0 domain: 10 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 2
        coeffs: 3
        domain: 0
        domain: 7
      }
    }
  )pb");
  SatParameters params;
  params.set_fill_tightened_domains_in_response(true);
  params.set_keep_all_feasible_solutions_in_presolve(true);

  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  CpSolverResponse response_with_domains_only;
  *response_with_domains_only.mutable_tightened_variables() =
      response.tightened_variables();

  const CpSolverResponse expected_domains = ParseTestProto(R"pb(
    tightened_variables { domain: 0 domain: 5 }
    tightened_variables { domain: 1 domain: 3 }
    tightened_variables { domain: 0 domain: 1 }
  )pb");
  EXPECT_THAT(expected_domains,
              testing::EqualsProto(response_with_domains_only));
}

TEST(SolveCpModelTest, TightenedDomainsAfterPresolve) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 0 domain: 10 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 2
        coeffs: 3
        domain: 0
        domain: 7
      }
    }
  )pb");
  SatParameters params;
  params.set_fill_tightened_domains_in_response(true);
  params.set_keep_all_feasible_solutions_in_presolve(true);
  params.set_stop_after_presolve(true);

  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  CpSolverResponse response_with_domains_only;
  *response_with_domains_only.mutable_tightened_variables() =
      response.tightened_variables();

  const CpSolverResponse expected_domains = ParseTestProto(R"pb(
    tightened_variables { domain: 0 domain: 5 }
    tightened_variables { domain: 1 domain: 3 }
    tightened_variables { domain: 0 domain: 1 }
  )pb");
  EXPECT_THAT(expected_domains,
              testing::EqualsProto(response_with_domains_only));
}

TEST(SolveCpModelTest, TightenedDomains2) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 100 }
    constraints {
      enforcement_literal: 0
      linear { vars: 1 coeffs: 1 domain: 90 domain: 100 }
    }
    constraints {
      enforcement_literal: -1
      linear { vars: 1 coeffs: 1 domain: 0 domain: 10 }
    }
  )pb");
  SatParameters params;
  params.set_fill_tightened_domains_in_response(true);
  params.set_keep_all_feasible_solutions_in_presolve(true);

  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  CpSolverResponse response_with_domains_only;
  *response_with_domains_only.mutable_tightened_variables() =
      response.tightened_variables();

  const CpSolverResponse expected_domains = ParseTestProto(R"pb(
    tightened_variables { domain: 0 domain: 1 }
    tightened_variables { domain: 0 domain: 10 domain: 90 domain: 100 }
  )pb");
  EXPECT_THAT(expected_domains,
              testing::EqualsProto(response_with_domains_only));
}

TEST(SolveCpModelTest, TightenedDomainsIfInfeasible) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 10 }
    variables { domain: 1 domain: 10 }
    variables { domain: 0 domain: 10 }
    constraints {
      linear {
        vars: 0
        vars: 1
        vars: 2
        coeffs: 1
        coeffs: 2
        coeffs: 3
        domain: 80
        domain: 87
      }
    }
  )pb");
  SatParameters params;
  params.set_fill_tightened_domains_in_response(true);

  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(CpSolverStatus::INFEASIBLE, response.status());
  EXPECT_TRUE(response.tightened_variables().empty());
}

TEST(SolveCpModelTest, PermutedObjectiveNoPresolve) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 7 domain: 10 }
    variables { domain: 4 domain: 10 }
    variables { domain: 5 domain: 10 }
    objective {
      vars: [ 2, 1, 0 ]
      coeffs: [ 1, 2, 3 ]
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(CpSolverStatus::OPTIMAL, response.status());
}

TEST(SolveCpModelTest, TriviallyInfeasibleAssumptions) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 0 }
    assumptions: [ 0, 1 ]
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  EXPECT_THAT(response.sufficient_assumptions_for_infeasibility(),
              testing::ElementsAre(1));
}

TEST(SolveCpModelTest, TriviallyInfeasibleNegatedAssumptions) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 1 domain: 1 }
    assumptions: [ 0, -2 ]
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  EXPECT_THAT(response.sufficient_assumptions_for_infeasibility(),
              testing::ElementsAre(-2));
}

TEST(SolveCpModelTest, AssumptionsAndInfeasibility) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 3 }
    constraints {
      enforcement_literal: 0
      linear {
        vars: [ 1 ]
        coeffs: [ 1 ]
        domain: [ 4, 4 ]
      }
    }
    assumptions: [ 0 ]
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  EXPECT_THAT(response.sufficient_assumptions_for_infeasibility(),
              testing::ElementsAre(0));
}

TEST(SolveCpModelTest, AssumptionsAndInfeasibility2) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 3 }
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: 0
      linear {
        vars: [ 1 ]
        coeffs: [ 1 ]
        domain: [ 4, 4 ]
      }
    }
    assumptions: [ 3, 0, 2 ]
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  EXPECT_THAT(response.sufficient_assumptions_for_infeasibility(),
              testing::ElementsAre(0));
}

TEST(SolveCpModelTest, AssumptionsAndInfeasibility3) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables {
      name: "a"
      domain: [ 0, 1 ]
    }
    variables {
      name: "b"
      domain: [ 0, 1 ]
    }
    variables {
      name: "i1"
      domain: [ 0, 1 ]
    }
    variables {
      name: "i2"
      domain: [ 0, 1 ]
    }
    variables {
      name: "i3"
      domain: [ 0, 1 ]
    }
    variables {
      name: "i4"
      domain: [ 0, 1 ]
    }
    constraints {
      enforcement_literal: 2
      bool_or { literals: [ -1, 1 ] }
    }
    constraints {
      enforcement_literal: 3
      bool_or { literals: [ 0, 1 ] }
    }
    constraints {
      enforcement_literal: 4
      bool_or { literals: [ -2, -1 ] }
    }
    constraints {
      enforcement_literal: 5
      bool_or { literals: [ -2 ] }
    }
    assumptions: [ 2, 3, 4, 5 ]
  )pb");

  SatParameters params;
  params.set_log_search_progress(true);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  EXPECT_THAT(response.sufficient_assumptions_for_infeasibility(),
              testing::ElementsAre(2, 3, 5));
}

TEST(SolveCpModelTest, RegressionTest) {
  // This used to wrongly return UNSAT.
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 1 }
    variables { domain: 0 domain: 1 }
    constraints {
      enforcement_literal: -2
      bool_or { literals: -1 }
    }
  )pb");
  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

// This used to crash because of how nodes with no arc were handled.
TEST(SolveCpModelTest, RouteConstraintRegressionTest) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 1, 1 ] }
    variables { domain: [ 1, 1 ] }
    variables { domain: [ 0, 1 ] }
    constraints {
      routes {
        tails: [ 0, 1, 3 ]
        heads: [ 1, 3, 0 ]
        literals: [ 0, 2, 1 ]
      }
    }
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(SolveCpModelTest, ObjectiveInnerObjectiveBasic) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 2, 10 ] }
    variables { domain: [ 2, 10 ] }
    objective {
      vars: [ 0, 1 ]
      coeffs: [ 1, 2 ]
      scaling_factor: 10
      offset: 5
    }
  )pb");

  const CpSolverResponse response = Solve(model_proto);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.objective_value(), 10 * (6 + 5));
  EXPECT_EQ(response.best_objective_bound(), 10 * (6 + 5));
  EXPECT_EQ(response.inner_objective_lower_bound(), 6);
}

TEST(SolveCpModelTest, ObjectiveDomainWithCore) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 10 ] }
    variables { domain: [ 0, 10 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 6, 100 ]
      }
    }
    objective {
      vars: [ 0, 1 ]
      coeffs: [ 1, 1 ]
      scaling_factor: 1
      domain: [ 3, 4, 8, 10 ]
    }
  )pb");
  Model model;
  SatParameters params;
  params.set_optimize_with_core(true);
  params.set_linearization_level(0);
  params.set_log_search_progress(true);
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(8.0, response.objective_value());
}

TEST(SolveCpModelTest, ObjectiveDomainWithCore2) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: [ 0, 10 ] }
    variables { domain: [ 0, 10 ] }
    constraints {
      linear {
        vars: [ 0, 1 ]
        coeffs: [ 1, 1 ]
        domain: [ 6, 8 ]
      }
    }
    objective {
      vars: [ 0, 1 ]
      coeffs: [ 1, 1 ]
      scaling_factor: 1
      domain: [ 3, 4, 9, 10 ]
    }
  )pb");
  Model model;
  SatParameters params;
  params.set_optimize_with_core(true);
  params.set_linearization_level(0);
  params.set_log_search_progress(true);
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(SolveCpModelTest, EnumerateAllSolutionsReservoir) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    variables { domain: 1 domain: 4 }
    constraints {
      reservoir {
        time_exprs { vars: 0 coeffs: 1 }
        time_exprs { vars: 1 coeffs: 1 }
        time_exprs { vars: 2 coeffs: 1 }
        time_exprs { vars: 3 coeffs: 1 }
        level_changes: { offset: 1 }
        level_changes: { offset: -1 }
        level_changes: { offset: 3 }
        level_changes: { offset: -3 }
        min_level: 0
        max_level: 3
      }
    }
  )pb");

  // We can have (var0 <= var1) <= (var2 <= var3) or the other way.
  for (const bool encode : {true, false}) {
    SatParameters params;
    params.set_enumerate_all_solutions(true);
    params.set_expand_reservoir_constraints(encode);
    Model model;
    model.Add(NewSatParameters(params));
    int count = 0;
    model.Add(
        NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
          LOG(INFO) << absl::StrJoin(response.solution(), " ");
          ++count;
        }));
    const CpSolverResponse response = SolveCpModel(model_proto, &model);
    EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
    EXPECT_EQ(count, 89);
  }
}

TEST(SolveCpModelTest, EmptyModel) {
  const CpModelProto model_proto = ParseTestProto(R"pb()pb");
  SatParameters params;
  params.set_log_search_progress(true);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, EmptyOptimizationModel) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    objective { offset: 0 }
  )pb");
  SatParameters params;
  params.set_log_search_progress(true);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, EmptyOptimizationModelBuggy) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    objective { offset: 0 }
  )pb");
  SatParameters params;
  params.set_num_workers(1);
  params.set_log_search_progress(true);

  // This causes the inner solver to abort before finding the empty solution!
  params.set_max_number_of_conflicts(0);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::UNKNOWN);
}

TEST(SolveCpModelTest, EmptyOptimizationModelMultiThread) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    objective { offset: 0 }
  )pb");
  SatParameters params;
  params.set_log_search_progress(true);

  // This causes the inner solver to abort before finding the empty solution!
  // In non-interleave mode, everyone aborts and we finish with UNKNOWN.
  params.set_max_number_of_conflicts(0);
  params.set_num_workers(8);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(SolveCpModelTest, EmptyOptimizationModelBuggyInterleave) {
  const CpModelProto model_proto = ParseTestProto(R"pb(
    objective { offset: 0 }
  )pb");
  SatParameters params;
  params.set_log_search_progress(true);

  // This cause each chunk to abort right away with UNKNOWN. But because we are
  // in chunked mode, we always reschedule full solver and we never finish if
  // there is no time limit.
  //
  // TODO(user): Fix this behavior by not rescheduling in this case?
  params.set_max_number_of_conflicts(0);
  params.set_num_workers(8);
  params.set_interleave_search(true);
  params.set_use_feasibility_jump(false);
  params.set_interleave_batch_size(10);
  params.set_max_time_in_seconds(1);
  const CpSolverResponse response = SolveWithParameters(model_proto, params);

  // The feasibility jump solver does not care about max_number_of_conflicts(),
  // so it finds the empty solution. But it is disabled in interleaved search.
  EXPECT_THAT(response.status(), testing::Eq(CpSolverStatus::UNKNOWN));
}

TEST(PresolveCpModelTest, Issue4068) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    variables { domain: [ 1, 2 ] }
    variables { domain: [ 1, 2 ] }
    constraints {
      no_overlap_2d {
        x_intervals: [ 1, 2 ]
        y_intervals: [ 3, 4 ]
      }
    }
    constraints {
      interval {
        start {}
        end {
          vars: [ 1 ]
          coeffs: [ 1 ]
        }
        size {
          vars: [ 1 ]
          coeffs: [ 1 ]
        }
      }
    }
    constraints {
      interval {
        start {}
        end { offset: 1 }
        size { offset: 1 }
      }
    }
    constraints {
      interval {
        start {
          vars: [ 2 ]
          coeffs: [ 1 ]
        }
        end {
          vars: [ 2 ]
          coeffs: [ 1 ]
          offset: 2
        }
        size { offset: 2 }
      }
    }
    constraints {
      interval {
        start { offset: 2 }
        end {
          vars: [ 0 ]
          coeffs: [ 1 ]
          offset: 2
        }
        size {
          vars: [ 0 ]
          coeffs: [ 1 ]
        }
      }
    }
  )pb");
  SatParameters params;
  params.set_keep_all_feasible_solutions_in_presolve(true);
  Model model;
  model.Add(NewSatParameters("enumerate_all_solutions:true"));
  int count = 0;
  model.Add(
      NewFeasibleSolutionObserver([&count](const CpSolverResponse& response) {
        LOG(INFO) << absl::StrJoin(response.solution(), " ");
        ++count;
      }));
  const CpSolverResponse response = SolveCpModel(cp_model, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(count, 2);
}

TEST(PresolveCpModelTest, EmptyExactlyOne) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: [ 0, 1 ] }
    constraints { exactly_one {} }
  )pb");
  Model model;
  const CpSolverResponse response = SolveCpModel(cp_model, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, EmptyConstantProduct) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints { int_prod { target { offset: 2 } } })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, EmptyElement) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints { element {} })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, EmptyCumulativeNegativeCapacity) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints { cumulative { capacity { offset: -1 } } })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, BadAutomaton) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints {
      automaton {
        transition_tail: -2
        transition_head: -1
        transition_label: 1
        exprs { coeffs: 1 }
      }
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, ConstantEnforcementLiteral) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 0 domain: 0 }
    constraints {
      enforcement_literal: -1
      bool_xor {}
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, EmptySearchStrategyExpr) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints {}
    search_strategy {
      domain_reduction_strategy: SELECT_UPPER_HALF
      exprs {}
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, ConstantSearchStrategyExpr) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    constraints {}
    search_strategy {
      domain_reduction_strategy: SELECT_UPPER_HALF
      exprs { offset: 1 }
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NegativeElement) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 0 domain: 10 }
    variables { domain: 0 domain: 10 }
    constraints { element { target: -1 vars: -1 } }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, NegativeAutomaton) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 0 domain: 10 }
    constraints {
      automaton {
        final_states: 3
        transition_tail: 0
        transition_head: 0
        transition_label: 0
        vars: [ -1 ]
      }
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, ImpossibleInterval) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 1 domain: 10 }
    constraints {
      interval {
        start { vars: 0 coeffs: 1 }
        end {}
        size {}
      }
    })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, BadCumulative) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 1 domain: 10 }
    constraints { cumulative { capacity { vars: 0 coeffs: -1 } } })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, NegatedStrategy) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 1 domain: 4617263143898057573 }
    variables { domain: 1 domain: 1 }
    search_strategy { variables: -1 }
    assumptions: 1)pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, CumulativeWithOverflow) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables { domain: 0 domain: 1 }
    variables { domain: 0 domain: 6 }
    variables { domain: 3 domain: 3 }
    variables { domain: 0 domain: 6 }
    constraints {
      enforcement_literal: 0
      interval {
        start { vars: 1 coeffs: 1 }
        end { vars: 3 coeffs: 1 }
        size { vars: 2 coeffs: 1 }
      }
    }
    constraints {
      cumulative {
        intervals: 0
        demands { offset: 4402971607593202523 }
      }
    }
  )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, CumulativeWithOverflow2) {
  const CpModelProto cp_model =
      ParseTestProto(
          R"pb(
            variables { domain: 1 domain: 10 }
            variables { domain: 1 domain: 10 }
            constraints {
              cumulative { capacity { vars: 0 coeffs: 0 offset: -1 } }
            })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  const CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, NoOverlap2dCornerCase) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        constraints {
          enforcement_literal: 2
          interval {
            start { vars: 0 coeffs: 1 }
            end { vars: 1 coeffs: 1 }
            size { offset: 3 }
          }
        }
        constraints {
          enforcement_literal: 2
          interval {
            start { vars: 3 coeffs: 1 }
            end { vars: 2 coeffs: 1 }
            size { offset: 2 }
          }
        }
        constraints { no_overlap_2d { x_intervals: 0 y_intervals: 1 } }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, BadDivision) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 1 domain: 4 }
        variables { domain: 1 domain: 4 }
        constraints {
          int_div {
            target { vars: 1 coeffs: 0 }
            exprs { offset: 1 }
            exprs { vars: 1 coeffs: 0 offset: 1 }
          }
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, CumulativeWithNegativeCapacity) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        variables { domain: 2 domain: 2 }
        variables { domain: 2 domain: 6 }
        constraints {
          enforcement_literal: 1
          interval {
            start { vars: 2 coeffs: 1 }
            end { vars: 4 coeffs: 1 }
            size { vars: 3 coeffs: 1 }
          }
        }
        constraints {
          cumulative {
            capacity { offset: -1 }
            intervals: 0
            demands { vars: 0 coeffs: -1 offset: 1 }
          }
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, TrivialTableNegated) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        constraints {
          table {
            values: [ 0, 1 ]
            negated: true
            exprs { offset: 1 }
            exprs { vars: 0 coeffs: 1 }
          }
        })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, TrivialTable) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        constraints {
          table {
            values: [ 0, 1 ]
            exprs { offset: 1 }
            exprs { vars: 0 coeffs: 1 }
          }
        })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(NoOverlap2dCpModelTest, RequiresLns) {
  const CpModelProto cp_model = ParseTestProto(R"pb(
    variables: {
      name: "x_0"
      domain: [ 0, 80 ]
    }
    variables: {
      name: "y_0"
      domain: [ 0, 40 ]
    }
    variables: {
      name: "x_1"
      domain: [ 0, 80 ]
    }
    variables: {
      name: "y_1"
      domain: [ 0, 60 ]
    }
    variables: {
      name: "x_2"
      domain: [ 0, 90 ]
    }
    variables: {
      name: "y_2"
      domain: [ 0, 50 ]
    }
    variables: { domain: [ 1, 1 ] }
    variables: { domain: [ 0, 200 ] }
    variables: { domain: [ 0, 200 ] }
    variables: { domain: [ 0, 200 ] }
    variables: { domain: [ 0, 200 ] }
    variables: { domain: [ 0, 200 ] }
    variables: { domain: [ 0, 200 ] }
    constraints: {
      no_overlap_2d: {
        x_intervals: [ 1, 3, 5 ]
        y_intervals: [ 2, 4, 6 ]
      }
    }
    constraints: {
      name: "x_interval_0"
      enforcement_literal: 6
      interval: {
        start: { vars: 0 coeffs: 1 }
        end: { vars: 0 coeffs: 1 offset: 20 }
        size: { offset: 20 }
      }
    }
    constraints: {
      name: "y_interval_0"
      enforcement_literal: 6
      interval: {
        start: { vars: 1 coeffs: 1 }
        end: { vars: 1 coeffs: 1 offset: 60 }
        size: { offset: 60 }
      }
    }
    constraints: {
      name: "x_interval_1"
      enforcement_literal: 6
      interval: {
        start: { vars: 2 coeffs: 1 }
        end: { vars: 2 coeffs: 1 offset: 20 }
        size: { offset: 20 }
      }
    }
    constraints: {
      name: "y_interval_1"
      enforcement_literal: 6
      interval: {
        start: { vars: 3 coeffs: 1 }
        end: { vars: 3 coeffs: 1 offset: 40 }
        size: { offset: 40 }
      }
    }
    constraints: {
      name: "x_interval_2"
      enforcement_literal: 6
      interval: {
        start: { vars: 4 coeffs: 1 }
        end: { vars: 4 coeffs: 1 offset: 10 }
        size: { offset: 10 }
      }
    }
    constraints: {
      name: "y_interval_2"
      enforcement_literal: 6
      interval: {
        start: { vars: 5 coeffs: 1 }
        end: { vars: 5 coeffs: 1 offset: 50 }
        size: { offset: 50 }
      }
    }
    constraints: {
      linear: {
        vars: [ 7, 0, 2 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ 0, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 7, 0, 2 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ 0, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 8, 0, 4 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ 10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 8, 0, 4 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ -10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 9, 2, 4 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ 10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 9, 2, 4 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ -10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 10, 1, 3 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ 20, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 10, 1, 3 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ -20, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 11, 1, 5 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ 10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 11, 1, 5 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ -10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 12, 3, 5 ]
        coeffs: [ 1, -2, 2 ]
        domain: [ -10, 9223372036854775807 ]
      }
    }
    constraints: {
      linear: {
        vars: [ 12, 3, 5 ]
        coeffs: [ 1, 2, -2 ]
        domain: [ 10, 9223372036854775807 ]
      }
    }
    objective: {
      vars: [ 7, 8, 9, 10, 11, 12 ]
      coeffs: [ 1, 1, 1, 1, 1, 1 ]
    }
  )pb");
  SatParameters params;
  params.set_num_workers(16);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.objective_value(), 120);
}
TEST(PresolveCpModelTest, TableWithOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -6055696632510658248 domain: 10 }
        variables { domain: 0 domain: 10 }
        constraints {
          table { vars: 1 vars: 0 values: 2 values: 0 negated: true }
        })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, ProdOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 5 }
        variables { domain: 0 domain: 5 }
        constraints {
          int_prod {
            target { offset: -3652538342751591977 }
            exprs { offset: -3 }
            exprs { vars: 0 coeffs: 0 offset: -3243792610144686519 }
            exprs {}
            exprs { offset: -1 }
          }
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, ModuloNotCanonical) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 10 }
        variables { domain: -4299172082820395165 domain: 10 }
        variables { domain: 0 domain: 10 }
        constraints {
          int_mod {
            target { vars: 1 coeffs: 1 offset: -4 }
            exprs { vars: 0 coeffs: 0 }
            exprs { offset: 3 }
          }
        }
        search_strategy { variables: 0 variables: 1 })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, CumulativeWithOverflow3) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 4 }
        variables { domain: 2 domain: 2 }
        variables { domain: 0 domain: 4 }
        variables { domain: 1 domain: 4 }
        variables { domain: 2 domain: 33554434 }
        variables { domain: 0 domain: 4 }
        variables { domain: 3 domain: 3 }
        variables { domain: 4 domain: 4 }
        variables { domain: 6 domain: 18014398509481990 }
        constraints {
          interval {
            start {}
            end { vars: 2 coeffs: 1 }
            size { vars: 4 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 3 coeffs: 1 }
            end { vars: 5 coeffs: 1 }
            size { vars: 4 coeffs: 1 }
          }
        }
        constraints {
          cumulative {
            capacity { vars: 8 coeffs: 129 }
            intervals: 0
            intervals: 1
            demands { vars: 2 coeffs: 1 offset: 1 }
            demands { vars: 7 coeffs: 1 }
          }
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, CumulativeWithOverflow4) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 4 }
        variables { domain: 2 domain: 2 }
        variables { domain: 0 domain: 4 }
        variables { domain: 1 domain: 4 }
        variables { domain: 2 domain: 33554434 }
        variables { domain: 0 domain: 4 }
        variables { domain: 3 domain: 3 }
        variables { domain: 4 domain: 32772 }
        variables { domain: 6 domain: 3848116990577877790 }
        constraints {
          interval {
            start {}
            end { vars: 2 coeffs: 1 }
            size { vars: 4 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 3 coeffs: 1 }
            end { vars: 5 coeffs: 1 }
            size { vars: 4 coeffs: 1 }
          }
        }
        constraints {
          cumulative {
            capacity { vars: 8 coeffs: 1 }
            intervals: 0
            intervals: 1
            demands { vars: 6 coeffs: 1 offset: 1 }
            demands { vars: 7 coeffs: 1 offset: 1 }
          }
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, FoundByFuzzing) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1024 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 1, 4 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 1, 4 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 1, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 4 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 512 ] }
        variables { domain: [ 0, 512 ] }
        variables { domain: [ 0, 2048 ] }
        variables { domain: [ 0, 512 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        constraints {
          linear {
            vars: [ 2, 1 ]
            coeffs: [ 1, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          linear {
            vars: [ 3, 1 ]
            coeffs: [ 1, -1 ]
            domain: [ 1, 9223372036854775807 ]
          }
        }
        constraints {
          linear {
            vars: [ 5, 4 ]
            coeffs: [ 1, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          linear {
            vars: [ 6, 4 ]
            coeffs: [ 1, -1 ]
            domain: [ 1, 9223372036854775807 ]
          }
        }
        constraints {}
        constraints {
          linear {
            vars: [ 9, 7 ]
            coeffs: [ 1, -1 ]
            domain: [ 1, 9223372036854775807 ]
          }
        }
        constraints {
          linear {
            vars: [ 3, 1, 10 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 1 ]
              coeffs: [ 1 ]
              offset: 1
            }
            end {
              vars: [ 3 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 10 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          linear {
            vars: [ 1, 2, 11 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 2 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 1 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 11 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          linear {
            vars: [ 6, 4, 12 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 4 ]
              coeffs: [ 1 ]
              offset: 1
            }
            end {
              vars: [ 6 ]
              coeffs: [ 1 ]
              offset: 1
            }
            size {
              vars: [ 12 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          linear {
            vars: [ 4, 5, 13 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 5 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 4 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 13 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          linear {
            vars: [ 9, 7, 14 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 7 ]
              coeffs: [ 1 ]
              offset: 1
            }
            end {
              vars: [ 9 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 14 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          linear {
            vars: [ 7, 8, 15 ]
            coeffs: [ -1, 1, 1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          interval {
            start {
              vars: [ 8 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 7 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 15 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {}
        constraints {
          linear {
            vars: [ 6, 1 ]
            coeffs: [ 1, -1 ]
            domain: [ 1, 9223372036854775807 ]
          }
        }
        constraints {
          enforcement_literal: [ -17 ]
          linear {
            vars: [ 4, 1 ]
            coeffs: [ 1, -1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          enforcement_literal: [ 16 ]
          interval {
            start {
              vars: [ 1 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 1 ]
              coeffs: [ 1 ]
              offset: 1
            }
            size { offset: 1 }
          }
        }
        constraints {
          interval {
            start {
              vars: [ 4 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 4 ]
              coeffs: [ 1 ]
              offset: 1
            }
            size { offset: 1 }
          }
        }
        constraints {
          linear {
            vars: [ 8, 4 ]
            coeffs: [ 1, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          linear {
            vars: [ 9, 4 ]
            coeffs: [ 1, -1 ]
            domain: [ 1, 9223372036854775807 ]
          }
        }
        constraints {
          enforcement_literal: [ -18 ]
          linear {
            vars: [ 7, 4 ]
            coeffs: [ 1, -1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          enforcement_literal: [ 17 ]
          interval {
            start {
              vars: [ 4 ]
              coeffs: [ 1 ]
            }
            end {
              vars: [ 4 ]
              coeffs: [ 1 ]
              offset: 1
            }
            size { offset: 1 }
          }
        }
        constraints {
          linear {
            vars: [ 7 ]
            coeffs: [ 1 ]
            domain: [ 0, 0 ]
          }
        }
        constraints {
          linear {
            vars: [ 1 ]
            coeffs: [ 1 ]
            domain: [ 1, 1 ]
          }
        }
        constraints {
          linear {
            vars: [ 18, 0 ]
            coeffs: [ 2, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          cumulative {
            capacity {
              vars: [ 18 ]
              coeffs: [ 1 ]
            }
            intervals: [ 7, 11, 15 ]
            demands { offset: 1 }
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          linear {
            vars: [ 19, 0 ]
            coeffs: [ 2, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          cumulative {
            capacity {
              vars: [ 19 ]
              coeffs: [ 1 ]
            }
            intervals: [ 9, 13, 17 ]
            demands { offset: 1 }
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          cumulative {
            capacity {
              vars: [ 20 ]
              coeffs: [ 1 ]
            }
            intervals: [ 21, 26 ]
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          linear {
            vars: [ 21, 0 ]
            coeffs: [ 2, -1 ]
            domain: [ -9223372036854775808, 0 ]
          }
        }
        constraints {
          cumulative {
            capacity {
              vars: [ 21 ]
              coeffs: [ 1 ]
            }
            intervals: [ 22 ]
            demands { offset: 1 }
          }
        }
        constraints {
          enforcement_literal: [ 22 ]
          linear {
            vars: [ 2, 3 ]
            coeffs: [ 1, -1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          enforcement_literal: [ 23 ]
          linear {
            vars: [ 5, 6 ]
            coeffs: [ 1, -1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          enforcement_literal: [ 24 ]
          linear {
            vars: [ 8, 9 ]
            coeffs: [ 1, -1 ]
            domain: [ -1, -1 ]
          }
        }
        objective {
          vars: [ 0 ]
          coeffs: [ 1 ]
        }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, AllDifferentNotCanonical) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 1, 4294967306 ] }
        variables { domain: [ 1, 6 ] }
        variables { domain: [ 0, 10 ] }
        variables { domain: [ 1, 10000000 ] }
        constraints {
          all_diff {
            exprs { vars: 1 coeffs: 0 }
            exprs {}
            exprs { vars: 1 coeffs: 2 }
            exprs { vars: 0 coeffs: -1 }
          }
        })pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, HintGetBrokenByPresolve) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        constraints {
          enforcement_literal: [ -1 ]
          table { vars: 1 }
        }
        constraints {
          enforcement_literal: [ -1 ]
          table {
            values: [ 9223372036854775807, 1 ]
            exprs {
              vars: [ 0 ]
              coeffs: [ 1 ]
              offset: 3562345932446661909
            }
            exprs {
              vars: [ 1 ]
              coeffs: [ 1 ]
            }
          }
        }
        objective {
          vars: [ 0, 1 ]
          coeffs: [ 1, 2 ]
        }
        solution_hint {
          vars: [ 0, 1 ]
          values: [ 1, 0 ]
        })pb");
  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, DisjunctiveFromFuzzing) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 6 ] }
        variables { domain: [ 3, 140737488355331 ] }
        variables { domain: [ 0, 6 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 2, 6 ] }
        variables { domain: [ 2, 2 ] }
        variables { domain: [ 2, 6 ] }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 offset: -1 }
            size { vars: 2 coeffs: -1 offset: 2199023255554 }
          }
        }
        constraints {
          interval {
            start { vars: 5 coeffs: 1 }
            end { vars: 7 coeffs: 1 }
            size { vars: 6 coeffs: 1 }
          }
        }
        constraints { no_overlap { intervals: [ 0, 0, 1, 1 ] } }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, PresolveChangesFeasibility) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 0 ] }
        variables { domain: [ 1, 1 ] }
        constraints { cumulative { capacity { vars: 1 coeffs: -1 } } }
        solution_hint { vars: 1 values: 6277701416517650879 }
      )pb");
  SatParameters params;
  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, PresolveChangesFeasibility2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        constraints {
          enforcement_literal: -1
          bool_and { literals: 0 }
        }
        objective {
          vars: [ 0, 1, 2, 3 ]
          coeffs: [ -1, 2, 3, -4 ]
        }
        solution_hint {
          vars: [ 0, 1, 2, 3 ]
          values: [ 1, 0, 0, 1 ]
        }
        assumptions: -1
      )pb");
  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, HintContradictsAssumptions) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { name: "x" domain: 0 domain: 1 }
        variables { name: "y" domain: 0 domain: 1 }
        constraints { bool_or { literals: 0 } }
        constraints { bool_or { literals: -1 literals: -2 } }
        solution_hint { vars: 1 values: 1 }
        assumptions: 1
      )pb");
  CpSolverResponse response = SolveWithParameters(cp_model, SatParameters());
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, CumulativeOutOfBoundsRead) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 10 }
        variables { domain: 0 domain: 10 }
        constraints { cumulative { capacity { vars: 0 coeffs: -1 } } }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, InverseCrash) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 0 }
        variables { domain: 1 domain: 1 }
        constraints { inverse { f_direct: 1 f_inverse: 1 } }
        solution_hint { vars: 1 values: -1 })pb");
  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, CumulativeOutOfBoundsReadFixedDemand) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 4 }
        variables { domain: 2 domain: 2 }
        variables { domain: 0 domain: 4 }
        variables { domain: 1 domain: 4 }
        variables { domain: 2 domain: 2 }
        variables { domain: 0 domain: 4 }
        variables { domain: 3 domain: 3 }
        variables { domain: 4 domain: 4 }
        variables { domain: 6 domain: 6 }
        constraints {
          interval {
            start {}
            end { vars: 2 coeffs: 1 offset: 1 }
            size { vars: 2 coeffs: 1 offset: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 3 coeffs: 1 }
            end { vars: 5 coeffs: 1 }
            size { vars: 4 coeffs: 1 }
          }
        }
        constraints {
          cumulative {
            capacity { vars: 8 coeffs: 36028797018963969 }
            intervals: 0
            intervals: 1
            demands { vars: 6 coeffs: 1 offset: -3 }
            demands { vars: 8 coeffs: 1 }
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, PresolveChangesFeasibilityMultiplication) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 2327064070896255483, 2327067369431138070 ] }
        variables { domain: [ 257, 1099511627786 ] }
        constraints {
          int_prod {
            target { vars: 0 coeffs: 1 offset: -6 }
            exprs { vars: 1 coeffs: 3 offset: 2327064070896254706 }
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, BadNoOverlap2d) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 2 }
        variables { domain: 2 domain: 6 }
        constraints {
          enforcement_literal: 0
          bool_or {}
        }
        constraints {
          enforcement_literal: 1
          interval {
            start { vars: 0 coeffs: 1 }
            end { vars: 3 coeffs: 1 offset: -4607772983994847345 }
            size { vars: 2 coeffs: 1 }
          }
        }
        constraints { no_overlap_2d { x_intervals: 1 y_intervals: 1 } }
      )pb");
  SatParameters params;

  params.set_use_timetabling_in_no_overlap_2d(true);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NoOverlapLinearizationOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        variables { domain: -3659321530269907407 domain: 3496689482055784131 }
        variables { domain: 2 domain: 7 }
        constraints {
          enforcement_literal: 0
          linear {
            vars: [ 1, 2, 3 ]
            coeffs: [ 1, 1, -1 ]
            domain: [ 0, 0 ]
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, TableHintBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 576460752303423489 }
        variables { domain: 0 domain: 268435457 }
        variables { domain: 0 domain: 576460752303423489 }
        constraints {
          table { vars: 1 values: 17179869184 values: 1 negated: true }
        }
        solution_hint {
          vars: 0
          vars: 1
          vars: 2
          vars: 3
          values: 1
          values: 0
          values: 0
          values: 1
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, LinearizationBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -4040617518406929344 domain: 10 }
        variables { domain: 6 domain: 10 }
        variables { domain: 0 domain: 10 }
        variables { domain: 1 domain: 10000000 }
        constraints {
          all_diff {
            exprs {
              vars: 1
              coeffs: 18014398509481986
              offset: -1252623043085079047
            }
            exprs { vars: 0 coeffs: -1 }
            exprs { vars: 0 coeffs: -1 offset: -7 }
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, DetectDuplicateColumnsOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -4611686018427387903 domain: 0 }
        variables { domain: 0 domain: 5 }
        variables { domain: 0 domain: 5 }
        objective {
          vars: 0
          vars: 1
          coeffs: 1
          coeffs: 1
          domain: 1
          domain: 7666432986417144262
        })pb");
  SatParameters params;

  params.set_log_search_progress(true);
  params.set_cp_model_presolve(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, TableExpandPreservesSolutionHint) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 18014398509481985 }
        variables { domain: 0 domain: 1 }
        constraints {
          enforcement_literal: -1
          table {
            values: 9223372036854775807
            values: 1
            values: 0
            exprs { vars: 1 coeffs: 1 }
          }
        }
        solution_hint {
          vars: [ 0, 1, 2, 3 ]
          values: [ 1, 0, 0, 1 ]
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, TableExpandPreservesSolutionHint2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: [ 0, 1, 18014398509481985, 18014398509481985 ] }
        variables { domain: [ 0, 18014398509481985 ] }
        variables { domain: [ 0, 18014398509481985 ] }
        constraints {
          enforcement_literal: -1
          table {
            values: [ 9223372036854775807, 1, 0 ]
            exprs { vars: 1 coeffs: 1 }
          }
        }
        constraints {
          enforcement_literal: 0
          table {
            values: [ 9223372036854775807, 1, 0 ]
            exprs { vars: 1 coeffs: 1 }
          }
        }
        solution_hint {
          vars: [ 0, 1, 2, 3 ]
          values: [ 1, 0, 0, 1 ]
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, PresolveOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 4611686018427387903 }
        variables { domain: 0 domain: 1 }
        variables {
          domain: 8
          domain: 12
          domain: 2986687222969572620
          domain: 2986687222969572620
        }
        variables { domain: 2 domain: 2 }
        constraints {
          int_prod {
            target { vars: 2 coeffs: 1 }
            exprs { vars: 1 coeffs: 1 offset: 1 }
            exprs { vars: 0 coeffs: 1 }
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, InverseBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -3744721377111001386 domain: 0 }
        variables { domain: 0 domain: 3 }
        variables {
          domain: -1
          domain: 0
          domain: 4611686018427387903
          domain: 4611686018427387903
        }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        constraints {
          inverse {
            f_direct: 0
            f_direct: 2
            f_direct: 4
            f_direct: 6
            f_inverse: 1
            f_inverse: 3
            f_inverse: 5
            f_inverse: 7
          }
        }
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(true);
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, FuzzerCrash3) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1024 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 1 domain: 4 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 1 domain: 4 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 1 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 4 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 512 }
        variables { domain: 0 domain: 512 }
        variables { domain: 0 domain: 2048 }
        variables { domain: 0 domain: 512 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints {
          linear {
            vars: 2
            vars: 1
            coeffs: 1
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          linear {
            vars: 3
            vars: 1
            coeffs: 1
            coeffs: -1
            domain: 1
            domain: 9223372036854775807
          }
        }
        constraints {}
        constraints {}
        constraints {
          linear {
            vars: 8
            vars: 7
            coeffs: 1
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          linear {
            vars: 9
            vars: 7
            coeffs: 1
            coeffs: -1
            domain: 1
            domain: 9223372036854775807
          }
        }
        constraints {}
        constraints {
          interval {
            start { vars: 1 coeffs: 1 offset: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 10 coeffs: 1 }
          }
        }
        constraints {
          linear {
            vars: 1
            vars: 2
            vars: 11
            coeffs: -1
            coeffs: 1
            coeffs: 1
            domain: 0
            domain: 0
          }
        }
        constraints {
          interval {
            start { vars: 2 coeffs: 1 }
            end { vars: 1 coeffs: 1 }
            size { vars: 11 coeffs: 1 }
          }
        }
        constraints {
          linear {
            vars: 6
            vars: 4
            vars: 12
            coeffs: -1
            coeffs: 1
            coeffs: 1
            domain: -1
            domain: -1
          }
        }
        constraints {
          interval {
            start { vars: 4 coeffs: 1 offset: 1 }
            end { vars: 6 coeffs: 1 }
            size { vars: 12 coeffs: 1 }
          }
        }
        constraints {
          linear {
            vars: 4
            vars: 5
            vars: 13
            coeffs: -1
            coeffs: 1
            coeffs: 1
            domain: 0
            domain: 0
          }
        }
        constraints {
          interval {
            start { vars: 5 coeffs: 1 }
            end { vars: 4 coeffs: 1 }
            size { vars: 13 coeffs: 1 }
          }
        }
        constraints {}
        constraints {
          interval {
            start { vars: 7 coeffs: 1 offset: 1 }
            end { vars: 9 coeffs: 1 }
            size { vars: 14 coeffs: 1 }
          }
        }
        constraints {
          linear {
            vars: 7
            vars: 8
            vars: 15
            coeffs: -1
            coeffs: 1
            coeffs: 1
            domain: 0
            domain: 0
          }
        }
        constraints {
          interval {
            start { vars: 8 coeffs: 1 }
            end { vars: 7 coeffs: 1 }
            size { vars: 15 coeffs: 1 }
          }
        }
        constraints {
          linear {
            vars: 5
            vars: 1
            coeffs: 1
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          linear {
            vars: 6
            vars: 1
            coeffs: 1
            coeffs: -1
            domain: 1
            domain: 9223372036854775807
          }
        }
        constraints {
          enforcement_literal: -17
          linear { vars: 4 vars: 1 coeffs: 1 coeffs: -1 domain: 0 domain: 0 }
        }
        constraints {
          enforcement_literal: 16
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 1 coeffs: 1 offset: 1 }
            size { offset: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 4 coeffs: 1 }
            end { vars: 4 coeffs: 1 offset: 1 }
            size { offset: 1 }
          }
        }
        constraints {
          linear {
            vars: 8
            vars: 4
            coeffs: 1
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          linear {
            vars: 9
            vars: 4
            coeffs: 1
            coeffs: -1
            domain: 1
            domain: 9223372036854775807
          }
        }
        constraints {
          enforcement_literal: -18
          linear { vars: 7 vars: 4 coeffs: 1 coeffs: -1 domain: 0 domain: 0 }
        }
        constraints {
          enforcement_literal: 17
          interval {
            start { vars: 4 coeffs: 1 }
            end { vars: 4 coeffs: 1 offset: 4175356038966811637 }
            size { offset: 1 }
          }
        }
        constraints { linear { vars: 7 coeffs: 1 domain: 0 domain: 0 } }
        constraints {}
        constraints {
          linear {
            vars: 18
            vars: 0
            coeffs: 2
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          cumulative {
            capacity { vars: 18 coeffs: 1 }
            intervals: 7
            intervals: 11
            intervals: 15
            demands { offset: 1 }
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          linear {
            vars: 19
            vars: 0
            coeffs: 2
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          cumulative {
            capacity { vars: 19 coeffs: 1 }
            intervals: 9
            intervals: 13
            intervals: 17
            demands { offset: 1 }
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          linear {
            vars: 20
            vars: 0
            coeffs: 1
            coeffs: -2
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          cumulative {
            capacity { vars: 20 coeffs: 1 }
            intervals: 21
            intervals: 26
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        constraints {
          linear {
            vars: 21
            vars: 0
            coeffs: 2
            coeffs: -1
            domain: -9223372036854775808
            domain: 0
          }
        }
        constraints {
          cumulative {
            capacity { vars: 21 coeffs: 1 }
            intervals: 22
            demands { offset: 1 }
          }
        }
        constraints {
          enforcement_literal: 22
          linear { vars: 2 vars: 3 coeffs: 1 coeffs: -1 domain: -1 domain: -1 }
        }
        constraints {
          enforcement_literal: 23
          linear { vars: 5 vars: 6 coeffs: 1 coeffs: -1 domain: -1 domain: -1 }
        }
        constraints {
          enforcement_literal: 24
          linear { vars: 8 vars: 9 coeffs: 1 coeffs: -1 domain: -1 domain: -1 }
        }
        objective { vars: 0 coeffs: 1 }
      )pb");
  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, PotentialOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables {
          domain: 2
          domain: 2447234766972268842
          domain: 3535826881723299506
          domain: 4050838349900690071
        }
        variables {
          domain: -2798048574462918627
          domain: 2251799813685248
          domain: 357364299240879354
          domain: 1499017952464168848
        }
        variables { domain: 1 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints {
          reservoir {
            max_level: 2
            time_exprs { vars: 0 coeffs: 1 }
            time_exprs { vars: 1 coeffs: 1 }
            active_literals: 2
            active_literals: 3
            level_changes { offset: -1 }
            level_changes { offset: 1 }
          }
        }
      )pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, LinearizationOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables {
          domain: 0
          domain: 6
          domain: 1495197974356070066
          domain: 1495197974356070067
        }
        variables { domain: 0 domain: 50 }
        constraints {
          linear {
            vars: 0
            vars: 2
            vars: 3
            coeffs: 2
            coeffs: 4
            coeffs: -1
            domain: -896813501530156794
            domain: 6343756879353628413
            domain: 9223372036854775807
            domain: 9223372036854775807
          }
        }
      )pb");
  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, LinearizationOverflow2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -1 domain: 0 }
        variables { domain: 0 domain: 5 }
        variables { domain: 0 domain: 5 }
        variables { domain: 2 domain: 8 }
        constraints {
          linear {
            vars: 1
            vars: 2
            coeffs: 1
            coeffs: -1
            domain: 3
            domain: 1387315275818938588
            domain: 9223372036854775807
            domain: 9223372036854775807
          }
        }
      )pb");
  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, IntervalThatCanOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables {
          domain: -2700435943562583052
          domain: 122393683034791
          domain: 1153604922529384902
          domain: 1153604922529384903
        }
        variables { domain: 2 domain: 2 }
        variables {
          domain: 5
          domain: 8198
          domain: 502515202656425278
          domain: 3082664781292582538
        }
        variables { domain: 3 domain: 6 }
        variables { domain: 3 domain: 3 }
        variables { domain: 3 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 }
          }
        }
        assumptions: -1
      )pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::MODEL_INVALID);
}

TEST(PresolveCpModelTest, ProdPotentialOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: -4611686018427387903 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 2 }
        variables { domain: 0 domain: 100 }
        constraints {
          int_prod {
            target { vars: 2 coeffs: 1 }
            exprs { vars: 1 coeffs: 1 }
            exprs { vars: 0 coeffs: 1 }
          }
        }
        assumptions: 0
      )pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, CumulativeCornerCase) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints { cumulative { capacity { vars: 1 coeffs: -1 } } }
        objective { vars: 1 offset: 1 coeffs: 1 }
        solution_hint {}
        assumptions: 1
        assumptions: -1)pb");
  SatParameters params;

  params.set_linearization_level(2);

  params.set_cp_model_presolve(false);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, ProdPotentialOverflow2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -2547768298502951547 domain: 0 }
        variables { domain: 2 domain: 2 }
        variables { domain: -4611686018427387903 domain: 1 }
        constraints {
          int_prod {
            target { vars: 2 coeffs: 1 }
            exprs { vars: 1 coeffs: 1 }
            exprs { vars: 0 coeffs: 1 }
          }
        }
        solution_hint {})pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NoOverlap2dBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 6 }
        variables { domain: -2 domain: 19 domain: 2185 domain: 2185 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 808 }
        variables { domain: 3 domain: 6 }
        variables { domain: 3 domain: 3 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 4 coeffs: 1 }
            end { vars: 6 coeffs: 1 }
            size { vars: 5 coeffs: 1 }
          }
        }
        constraints { no_overlap_2d { x_intervals: 0 y_intervals: 1 } }
        assumptions: 0
      )pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NoOverlap2dBug2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 6 }
        variables { domain: -58 domain: 11 domain: 3523 domain: 3524 }
        variables { domain: 0 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 }
          }
        }
        constraints { no_overlap_2d { x_intervals: 0 y_intervals: 0 } }
        assumptions: 0)pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, LinMaxBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 4096 }
        variables { domain: -3013 domain: 516 domain: 680 domain: 681 }
        variables { domain: 1 domain: 4 }
        variables { domain: 1 domain: 4 }
        variables { domain: 1 domain: 4 }
        constraints {
          lin_max {
            exprs { vars: 0 vars: 0 coeffs: 1 coeffs: -1 offset: -4032 }
          }
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, InverseBug2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        variables { domain: 0 domain: 3 }
        constraints {
          lin_max {
            target { vars: 0 coeffs: -1 }
            exprs { vars: 1 coeffs: 1 offset: -1 }
          }
        }
        constraints {
          inverse {
            f_direct: 0
            f_direct: 2
            f_direct: 4
            f_direct: 6
            f_inverse: 1
            f_inverse: 3
            f_inverse: 5
            f_inverse: 7
          }
        })pb");

  SatParameters params;

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, ElementBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 5 }
        variables { domain: -1298 domain: -1 domain: 4095 domain: 4095 }
        constraints {
          element {
            linear_index { vars: 0 coeffs: 1 }
            linear_target { vars: 1 coeffs: -3 }
            exprs { offset: 1 }
            exprs { offset: 2 }
            exprs { offset: 3 }
            exprs { offset: 4 }
            exprs { offset: 5 }
            exprs { offset: 6 }
          }
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, AutomatonBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: -1 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints {
          automaton {
            final_states: 3
            transition_tail: [ 0, 0, 1, 2, 1, 2 ]
            transition_head: [ 1, 2, 1, 2, 3, 3 ]
            transition_label: [ 0, 1, 0, 1, 1, 0 ]
            exprs { vars: 0 coeffs: 1 }
            exprs { vars: 1 coeffs: 1 }
            exprs { vars: 1 coeffs: -1 }
            exprs { vars: 2 coeffs: 1 }
            exprs { vars: 3 coeffs: 1 }
          }
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NoOverlapBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 0 }
        variables { domain: 0 domain: 0 }
        variables { domain: 0 domain: 0 }
        variables { domain: 0 domain: 0 }
        variables { domain: 0 domain: 0 }
        variables { domain: 0 domain: 0 domain: 2 domain: 2 }
        constraints {
          enforcement_literal: 0
          interval {
            start {}
            end { vars: 0 coeffs: 1 }
            size { offset: 1 }
          }
        }
        constraints {
          enforcement_literal: 0
          interval {
            start {}
            end {}
            size { vars: 6 coeffs: 1 }
          }
        }
        constraints {
          no_overlap { intervals: 1 intervals: 0 intervals: 1 intervals: 0 }
        })pb");

  SatParameters params;

  params.set_debug_crash_if_presolve_breaks_hint(true);

  // Enable all fancy heuristics.
  params.set_linearization_level(2);
  params.set_use_try_edge_reasoning_in_no_overlap_2d(true);
  params.set_exploit_all_precedences(true);
  params.set_use_hard_precedences_in_cumulative(true);
  params.set_max_num_intervals_for_timetable_edge_finding(1000);
  params.set_use_overload_checker_in_cumulative(true);
  params.set_use_strong_propagation_in_disjunctive(true);
  params.set_use_timetable_edge_finding_in_cumulative(true);
  params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000);
  params.set_use_timetabling_in_no_overlap_2d(true);
  params.set_use_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_conservative_scale_overload_checker(true);
  params.set_use_dual_scheduling_heuristics(true);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, NoOverlapBug2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: -1558 domain: 2 domain: 2476 domain: 3080 }
        variables { domain: -3998 domain: 5 domain: 3175 domain: 3527 }
        variables { domain: 3 domain: 38 domain: 2329 domain: 2922 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        variables { domain: 5 domain: 18 domain: 402 domain: 1493 }
        variables { domain: 258 domain: 1534 domain: 2025 domain: 2026 }
        variables { domain: -4096 domain: 1962 domain: 2394 domain: 3458 }
        variables { domain: 3 domain: 3 }
        variables { domain: 3 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 offset: 2 }
          }
        }
        constraints {
          enforcement_literal: 4
          interval {
            start { vars: 5 coeffs: 1 }
            end { vars: 7 coeffs: 1 }
            size { vars: 6 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 8 coeffs: 1 }
            end { vars: 10 coeffs: 1 }
            size { vars: 9 coeffs: 1 }
          }
        }
        constraints {
          no_overlap { intervals: 1 intervals: 0 intervals: 1 intervals: 2 }
        }
        constraints { bool_xor { literals: 0 literals: 4 } }
        floating_point_objective { vars: 1 coeffs: 1 offset: 2 }
      )pb");

  SatParameters params;

  params.set_debug_crash_if_presolve_breaks_hint(true);

  // Enable all fancy heuristics.
  params.set_linearization_level(2);
  params.set_use_try_edge_reasoning_in_no_overlap_2d(true);
  params.set_exploit_all_precedences(true);
  params.set_use_hard_precedences_in_cumulative(true);
  params.set_max_num_intervals_for_timetable_edge_finding(1000);
  params.set_use_overload_checker_in_cumulative(true);
  params.set_use_strong_propagation_in_disjunctive(true);
  params.set_use_timetable_edge_finding_in_cumulative(true);
  params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000);
  params.set_use_timetabling_in_no_overlap_2d(true);
  params.set_use_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_conservative_scale_overload_checker(true);
  params.set_use_dual_scheduling_heuristics(true);

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, LinMaxBug2) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 2 }
        constraints {
          lin_max {
            target { vars: 0 coeffs: -1 }
            exprs { vars: 0 coeffs: -1 offset: -1 }
          }
        })pb");

  SatParameters params;
  params.set_cp_model_presolve(false);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, NoOverlap2dBug3) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 6 }
        variables { domain: 3 domain: 3 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        variables { domain: -3 domain: 3 domain: 3033 domain: 3033 }
        variables { domain: 2 domain: 6 }
        variables { domain: 3 domain: 6 }
        variables { domain: 0 domain: 0 }
        variables { domain: 3 domain: 3 }
        variables { domain: 3 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 offset: 2 }
          }
        }
        constraints {
          enforcement_literal: 4
          interval {
            start { vars: 5 coeffs: 1 }
            end { vars: 7 coeffs: 1 }
            size { vars: 6 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 8 coeffs: 1 }
            end { vars: 10 coeffs: 1 }
            size { vars: 9 coeffs: 1 }
          }
        }
        constraints {
          no_overlap_2d {
            x_intervals: 1
            x_intervals: 1
            y_intervals: 1
            y_intervals: 1
          }
        }
        constraints { bool_xor { literals: 0 literals: 4 } })pb");

  SatParameters params;
  params.set_max_time_in_seconds(4.0);
  params.set_debug_crash_if_presolve_breaks_hint(true);

  // Enable all fancy heuristics.
  params.set_linearization_level(2);
  params.set_use_try_edge_reasoning_in_no_overlap_2d(true);
  params.set_exploit_all_precedences(true);
  params.set_use_hard_precedences_in_cumulative(true);
  params.set_max_num_intervals_for_timetable_edge_finding(1000);
  params.set_use_overload_checker_in_cumulative(true);
  params.set_use_strong_propagation_in_disjunctive(true);
  params.set_use_timetable_edge_finding_in_cumulative(true);
  params.set_max_pairs_pairwise_reasoning_in_no_overlap_2d(50000);
  params.set_use_timetabling_in_no_overlap_2d(true);
  params.set_use_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_area_energetic_reasoning_in_no_overlap_2d(true);
  params.set_use_conservative_scale_overload_checker(true);
  params.set_use_dual_scheduling_heuristics(true);
  params.set_maximum_regions_to_split_in_disconnected_no_overlap_2d(100);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, ObjectiveOverflow) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints {
          exactly_one {
            literals: 0
            literals: 1
            literals: 2
            literals: 3
            literals: 4
          }
        }
        objective {
          vars: 1
          vars: 0
          coeffs: 4611686018427387903
          coeffs: -1771410674732262910
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_log_search_progress(true);
  params.set_linearization_level(2);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(StopSolveTest, StopBeforeStart) {
  CpModelProto model_proto;
  AddInterval(0, 2, 4, &model_proto);
  AddInterval(1, 2, 4, &model_proto);
  ConstraintProto* ct = model_proto.add_constraints();
  ct->mutable_cumulative()->add_intervals(0);
  ct->mutable_cumulative()->add_demands()->set_offset(3);
  ct->mutable_cumulative()->add_intervals(1);
  ct->mutable_cumulative()->add_demands()->set_offset(4);
  ct->mutable_cumulative()->mutable_capacity()->set_offset(6);

  Model model;
  StopSearch(&model);
  const CpSolverResponse response = SolveCpModel(model_proto, &model);
  EXPECT_EQ(response.status(), CpSolverStatus::UNKNOWN);
}

TEST(PresolveCpModelTest, NoOverlap2DCumulativeRelaxationBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: -1353 domain: 1143 domain: 3041 domain: 3042 }
        variables { domain: -2 domain: 5 domain: 1207 domain: 1207 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 1 }
        variables { domain: 2 domain: 6 }
        variables { domain: 2 domain: 2 }
        variables { domain: 1 domain: 4096 }
        variables { domain: 1 domain: 4096 }
        variables { domain: 2 domain: 6 }
        variables { domain: 1 domain: 4096 }
        variables { domain: 3 domain: 3 }
        variables { domain: 3 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 offset: 2 }
          }
        }
        constraints {
          enforcement_literal: 4
          interval {
            start { vars: 5 coeffs: 1 }
            end { vars: 7 coeffs: 1 }
            size { vars: 6 coeffs: 1 }
          }
        }
        constraints {
          interval {
            start { vars: 8 coeffs: 1 }
            end { vars: 10 coeffs: 1 }
            size { vars: 9 coeffs: 1 }
          }
        }
        constraints { no_overlap { intervals: 0 intervals: 1 intervals: 2 } }
        constraints { no_overlap_2d {} }
        constraints { no_overlap_2d { x_intervals: 0 y_intervals: 0 } }
        objective { vars: 0 vars: 1 coeffs: -1 coeffs: -3237 }
        search_strategy {
          variables: 1
          domain_reduction_strategy: SELECT_UPPER_HALF
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  params.set_use_timetabling_in_no_overlap_2d(true);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.inner_objective_lower_bound(), -9846954);
}

TEST(PresolveCpModelTest, ReservoirBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 3 domain: 2805 domain: 2923 domain: 2923 }
        variables { domain: 0 domain: 0 }
        variables { domain: 1 domain: 1 }
        variables { domain: 0 domain: 1 }
        constraints {
          reservoir {
            max_level: 2
            time_exprs { vars: 0 coeffs: 1 }
            time_exprs { vars: 1 coeffs: 1 }
            active_literals: 2
            active_literals: 3
            level_changes { offset: -1 }
            level_changes { offset: 1 }
          }
        }
        search_strategy { variables: 0 }
        search_strategy {
          variable_selection_strategy: CHOOSE_MIN_DOMAIN_SIZE
          domain_reduction_strategy: SELECT_MAX_VALUE
          exprs { offset: -1 }
        }
        solution_hint {})pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, IntModBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: -1264 domain: -1 domain: 4095 domain: 4096 }
        constraints {
          int_mod {
            target { offset: 1 }
            exprs { vars: 0 coeffs: 1 offset: -2607 }
            exprs { offset: 2780 }
          }
        })pb");

  SatParameters params;

  params.set_cp_model_presolve(false);
  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(PresolveCpModelTest, CumulativeBugWithEmptyInterval) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 37 ] }
        variables { domain: [ 1, 1 ] }
        variables { domain: [ 2, 2 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 0 ] }
        variables { domain: [ 1, 4 ] }
        variables { domain: [ 1, 4 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 0, 0 ] }
        variables { domain: [ 0, 3 ] }
        variables { domain: [ 1, 1 ] }
        constraints {
          interval {
            start { offset: 2 }
            end { offset: 2 }
            size {}
          }
        }
        constraints {
          interval {
            start {
              vars: [ 3 ]
              coeffs: [ 1 ]
              offset: 1
            }
            end {
              vars: [ 5 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 7 ]
              coeffs: [ 1 ]
            }
          }
        }
        constraints {
          interval {
            start { offset: 1 }
            end {
              vars: [ 6 ]
              coeffs: [ 1 ]
            }
            size {
              vars: [ 6 ]
              coeffs: [ 1 ]
              offset: -1
            }
          }
        }
        constraints {
          linear {
            vars: [ 3, 5 ]
            coeffs: [ -1, 1 ]
            domain: [ 1, 4 ]
          }
        }
        constraints {
          linear {
            vars: [ 3, 5, 7 ]
            coeffs: [ 1, -1, 1 ]
            domain: [ -1, -1 ]
          }
        }
        constraints {
          linear {
            vars: [ 10, 5 ]
            coeffs: [ -1, 1 ]
            domain: [ 1, 4 ]
          }
        }
        constraints {
          linear {
            vars: [ 3, 6 ]
            coeffs: [ -1, 1 ]
            domain: [ 1, 4 ]
          }
        }
        constraints {
          linear {
            vars: [ 0, 9 ]
            coeffs: [ -1, 2 ]
            domain: [ -37, 0 ]
          }
        }
        constraints {
          cumulative {
            capacity {
              vars: [ 9 ]
              coeffs: [ 1 ]
            }
            intervals: [ 0, 1, 2 ]
            demands { offset: 1 }
            demands { offset: 1 }
            demands { offset: 2 }
          }
        }
        objective {
          vars: [ 0, 6 ]
          scaling_factor: 1
          coeffs: [ 1, -1 ]
          domain: [ -4, 37 ]
        }
      )pb");

  SatParameters params;
  params.set_max_time_in_seconds(4.0);
  params.set_debug_crash_if_presolve_breaks_hint(true);

  params.set_log_search_progress(true);
  params.set_linearization_level(2);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.inner_objective_lower_bound(), 0);

  params.set_cp_model_presolve(false);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.inner_objective_lower_bound(), 0);
}

TEST(PresolveCpModelTest, CumulativeBug3) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 1 domain: 1 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 6 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: -1 offset: 2 }
          }
        }
        constraints {
          cumulative {
            capacity { offset: 1 }
            intervals: 0
            demands { vars: 1 coeffs: 1 offset: 1 }
          }
        }
        objective { vars: 1 coeffs: -1 }
      )pb");

  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.inner_objective_lower_bound(), -6);

  params.set_cp_model_presolve(false);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
  EXPECT_EQ(response.inner_objective_lower_bound(), -6);
}

TEST(PresolveCpModelTest, CumulativeBug4) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 1 }
        variables { domain: 0 domain: 6 }
        variables { domain: -920 domain: -15 domain: 1540 domain: 1692 }
        variables { domain: 0 domain: 6 }
        variables { domain: 0 domain: 1 }
        variables { domain: -1 domain: 0 domain: 4096 domain: 4096 }
        variables { domain: 0 domain: 17 }
        constraints {
          enforcement_literal: 0
          interval {
            start { vars: 1 coeffs: 1 }
            end { vars: 3 coeffs: 1 }
            size { vars: 2 coeffs: 1 offset: 2 }
          }
        }
        constraints {
          enforcement_literal: 4
          interval {
            start { offset: 2 }
            end { vars: 6 coeffs: 1 }
            size { vars: 5 coeffs: 1 }
          }
        }
        constraints {
          cumulative {
            capacity { offset: 1 }
            intervals: 1
            demands { vars: 6 coeffs: 1 }
          }
        }
        constraints { bool_xor { literals: 0 literals: 4 } }
      )pb");

  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_cp_model_presolve(false);
  params.set_cp_model_probing_level(0);
  params.set_symmetry_level(0);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);

  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, AutomatonNonCanonical) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        variables { domain: [ 0, 1 ] }
        constraints {
          automaton {
            final_states: [ 3 ]
            transition_tail: [ 0, 0, 1, 2, 1, 2 ]
            transition_head: [ 1, 2, 1, 2, 3, 3 ]
            transition_label: [ 0, 1, 0, 1, 1, 0 ]
            exprs {
              vars: [ 0 ]
              coeffs: [ 1 ]
            }
            exprs {
              vars: [ 1 ]
              coeffs: [ 0 ]
            }
            exprs {
              vars: [ 2 ]
              coeffs: [ 1 ]
            }
            exprs {
              vars: [ 3 ]
              coeffs: [ 1 ]
            }
          }
        })pb");

  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_cp_model_presolve(false);
  params.set_cp_model_probing_level(0);
  params.set_symmetry_level(0);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);

  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::OPTIMAL);
}

TEST(PresolveCpModelTest, SolutionCrushBug) {
  const CpModelProto cp_model = ParseTestProto(
      R"pb(
        variables { domain: 0 domain: 2 }
        variables { domain: 0 domain: 2 }
        constraints {
          int_mod {
            target {}
            exprs { offset: -1 }
            exprs { vars: 1 coeffs: 1 offset: 2647 }
          }
        }
        constraints { at_most_one {} }
        floating_point_objective { vars: 0 coeffs: 1 offset: 5.12549424074614 }
      )pb");

  SatParameters params;
  params.set_log_search_progress(true);
  params.set_debug_crash_if_presolve_breaks_hint(true);
  params.set_cp_model_presolve(false);
  params.set_cp_model_probing_level(0);
  params.set_symmetry_level(0);

  CpSolverResponse response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);

  params.set_cp_model_presolve(true);
  response = SolveWithParameters(cp_model, params);
  EXPECT_EQ(response.status(), CpSolverStatus::INFEASIBLE);
}

TEST(CpModelSolverTest, DratProofIsValidForRandom3Sat) {
  SatParameters params;
  params.set_num_workers(1);
  params.set_cp_model_presolve(false);
  params.set_inprocessing_use_sat_sweeping(false);
  params.set_symmetry_level(1);
  params.set_linearization_level(1);
  params.set_check_drat_proof(true);
  params.set_max_drat_time_in_seconds(60);
  params.set_debug_crash_if_lrat_check_fails(true);

  int num_infeasible = 0;
  for (int i = 0; i < 100; ++i) {
    const int kNumVariables = 100;
    CpModelProto model_proto = Random3SatProblem(kNumVariables);

    CpSolverResponse response = SolveWithParameters(model_proto, params);
    if (response.status() == CpSolverStatus::INFEASIBLE) {
      ++num_infeasible;
    }
  }
  LOG(INFO) << "num_infeasible: " << num_infeasible;
  EXPECT_GT(num_infeasible, 0);
}

TEST(CpModelSolverTest, LratProofIsValidForRandom3Sat) {
  SatParameters params;
  params.set_num_workers(8);
  params.set_cp_model_presolve(false);
  params.set_inprocessing_use_sat_sweeping(false);
  params.set_symmetry_level(1);
  params.set_linearization_level(1);
  params.set_check_lrat_proof(true);
  params.set_debug_crash_if_lrat_check_fails(true);

  int num_infeasible = 0;
  for (int i = 0; i < 100; ++i) {
    const int kNumVariables = 100;
    CpModelProto model_proto = Random3SatProblem(kNumVariables);

    CpSolverResponse response = SolveWithParameters(model_proto, params);
    if (response.status() == CpSolverStatus::INFEASIBLE) {
      ++num_infeasible;
    }
  }
  LOG(INFO) << "num_infeasible: " << num_infeasible;
  EXPECT_GT(num_infeasible, 0);
}

#endif  // ORTOOLS_TARGET_OS_SUPPORTS_THREADS

}  // namespace
}  // namespace sat
}  // namespace operations_research