# Snippet from ortools/sat/samples/assumptions_sample_sat.py
from ortools.sat.python import cp_model


def main() -> None:
  """Showcases assumptions."""
  # Creates the model.
  model = cp_model.CpModel()

  # Creates the variables.
  x = model.new_int_var(0, 10, 'x')
  y = model.new_int_var(0, 10, 'y')
  z = model.new_int_var(0, 10, 'z')
  a = model.new_bool_var('a')
  b = model.new_bool_var('b')
  c = model.new_bool_var('c')

  # Creates the constraints.
  model.add(x > y).only_enforce_if(a)
  model.add(y > z).only_enforce_if(b)
  model.add(z > x).only_enforce_if(c)

  # Add assumptions
  model.add_assumptions([a, b, c])

  # Creates a solver and solves.
  solver = cp_model.CpSolver()
  status = solver.solve(model)

  # Print solution.
  print(f'Status = {solver.status_name(status)}')
  if status == cp_model.INFEASIBLE:
    print(
        'sufficient_assumptions_for_infeasibility = '
        f'{solver.sufficient_assumptions_for_infeasibility()}'
    )


if __name__ == '__main__':
  main()

// Snippet from ortools/sat/samples/assumptions_sample_sat.cc
#include <stdlib.h>

#include "ortools/base/init_google.h"
#include "ortools/base/logging.h"
#include "absl/base/log_severity.h"
#include "absl/log/globals.h"
#include "absl/types/span.h"
#include "ortools/sat/cp_model.h"
#include "ortools/sat/cp_model.pb.h"
#include "ortools/sat/cp_model_solver.h"
#include "ortools/util/sorted_interval_list.h"

namespace operations_research {
namespace sat {

void AssumptionsSampleSat() {
  CpModelBuilder cp_model;

  const Domain domain(0, 10);
  const IntVar x = cp_model.NewIntVar(domain).WithName("x");
  const IntVar y = cp_model.NewIntVar(domain).WithName("y");
  const IntVar z = cp_model.NewIntVar(domain).WithName("z");
  const BoolVar a = cp_model.NewBoolVar().WithName("a");
  const BoolVar b = cp_model.NewBoolVar().WithName("b");
  const BoolVar c = cp_model.NewBoolVar().WithName("c");

  cp_model.AddGreaterThan(x, y).OnlyEnforceIf(a);
  cp_model.AddGreaterThan(y, z).OnlyEnforceIf(b);
  cp_model.AddGreaterThan(z, x).OnlyEnforceIf(c);

  // Add assumptions
  cp_model.AddAssumptions({a, b, c});

  // Solving part.
  const CpSolverResponse response = Solve(cp_model.Build());

  // Print solution.
  LOG(INFO) << CpSolverResponseStats(response);
  if (response.status() == CpSolverStatus::INFEASIBLE) {
    for (const int index :
         response.sufficient_assumptions_for_infeasibility()) {
      LOG(INFO) << index;
    }
  }
}
}  // namespace sat
}  // namespace operations_research

int main(int argc, char* argv[]) {
  InitGoogle(argv[0], &argc, &argv, true);
  absl::SetStderrThreshold(absl::LogSeverityAtLeast::kInfo);
  operations_research::sat::AssumptionsSampleSat();
  return EXIT_SUCCESS;
}

// Snippet from ortools/sat/samples/AssumptionsSampleSat.java
package com.google.ortools.sat.samples;
import com.google.ortools.Loader;
import com.google.ortools.sat.CpSolverStatus;
import com.google.ortools.sat.CpModel;
import com.google.ortools.sat.CpSolver;
import com.google.ortools.sat.IntVar;
import com.google.ortools.sat.Literal;

/** Minimal CP-SAT example to showcase assumptions. */
public class AssumptionsSampleSat {
  public static void main(String[] args) {
    Loader.loadNativeLibraries();
    // Create the model.
    CpModel model = new CpModel();

    // Create the variables.
    IntVar x = model.newIntVar(0, 10, "x");
    IntVar y = model.newIntVar(0, 10, "y");
    IntVar z = model.newIntVar(0, 10, "z");
    Literal a = model.newBoolVar("a");
    Literal b = model.newBoolVar("b");
    Literal c = model.newBoolVar("c");

    // Creates the constraints.
    model.addGreaterThan(x, y).onlyEnforceIf(a);
    model.addGreaterThan(y, z).onlyEnforceIf(b);
    model.addGreaterThan(z, x).onlyEnforceIf(c);

    // Add assumptions
    model.addAssumptions(new Literal[] {a, b, c});

    // Create a solver and solve the model.
    CpSolver solver = new CpSolver();
    CpSolverStatus status = solver.solve(model);

    // Print solution.
    // Check that the problem is infeasible.
    if (status == CpSolverStatus.INFEASIBLE) {
      System.out.println(solver.sufficientAssumptionsForInfeasibility());
    }
  }

  private AssumptionsSampleSat() {}
}

// Snippet from ortools/sat/samples/AssumptionsSampleSat.cs
using System;
using Google.OrTools.Sat;

public class AssumptionsSampleSat
{
    static void Main()
    {
        // Creates the model.
        CpModel model = new CpModel();

        // Creates the variables.
        IntVar x = model.NewIntVar(0, 10, "x");
        IntVar y = model.NewIntVar(0, 10, "y");
        IntVar z = model.NewIntVar(0, 10, "z");
        ILiteral a = model.NewBoolVar("a");
        ILiteral b = model.NewBoolVar("b");
        ILiteral c = model.NewBoolVar("c");

        // Creates the constraints.
        model.Add(x > y).OnlyEnforceIf(a);
        model.Add(y > z).OnlyEnforceIf(b);
        model.Add(z > x).OnlyEnforceIf(c);

        // Add assumptions
        model.AddAssumptions(new ILiteral[] { a, b, c });

        // Creates a solver and solves the model.
        CpSolver solver = new CpSolver();
        CpSolverStatus status = solver.Solve(model);
        Console.WriteLine(solver.SufficientAssumptionsForInfeasibility());
    }
}