package org.batfish.z3;

import com.google.common.base.Throwables;
import com.microsoft.z3.BitVecExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Fixedpoint;
import com.microsoft.z3.Status;
import java.io.FileWriter;
import java.io.IOException;
import java.nio.file.Path;
import java.time.Instant;
import java.util.Map;
import java.util.SortedSet;
import javax.annotation.Nonnull;
import org.batfish.common.BatfishException;
import org.batfish.config.Settings;

public final class NodJob extends AbstractNodJob {

  private final Synthesizer _dataPlaneSynthesizer;

  private final boolean _optimize;

  private final QuerySynthesizer _querySynthesizer;

  public NodJob(
      Settings settings,
      Synthesizer dataPlaneSynthesizer,
      QuerySynthesizer querySynthesizer,
      SortedSet<IngressPoint> ingressPoints,
      String tag,
      boolean optimize) {
    super(settings, ingressPoints, tag);
    _dataPlaneSynthesizer = dataPlaneSynthesizer;
    _querySynthesizer = querySynthesizer;
    _optimize = optimize;
  }

  protected Status computeNodSat(long startTime, Context ctx) {
    NodProgram program = getNodProgram(ctx);
    Fixedpoint fix = mkFixedpoint(program, true);
    for (BoolExpr query : program.getQueries()) {
      Status status = fix.query(query);
      switch (status) {
        case SATISFIABLE:
          return status;
        case UNKNOWN:
          throw new BatfishException("Query satisfiability unknown");
        case UNSATISFIABLE:
          return status;
        default:
          throw new BatfishException("invalid status");
      }
    }
    throw new BatfishException("No queries");
  }

  @Override
  protected SmtInput computeSmtInput(long startTime, Context ctx) {
    NodProgram program = getNodProgram(ctx);
    if (_settings.debugFlagEnabled("saveNodProgram")) {
      saveNodProgram(program);
    }
    BoolExpr expr = computeSmtConstraintsViaNod(program, _querySynthesizer.getNegate());
    Map<String, BitVecExpr> variablesAsConsts = program.getNodContext().getVariablesAsConsts();
    return new SmtInput(expr, variablesAsConsts);
  }

  private void saveNodProgram(NodProgram program) {
    // synchronize to avoid z3 concurrency bugs
    synchronized (NodJob.class) {
      Path nodPath =
          _settings
              .getActiveTestrigSettings()
              .getBasePath()
              .resolve(
                  String.format(
                      "nodProgram-%s-%d.smt2", Instant.now(), Thread.currentThread().getId()));
      try (FileWriter writer = new FileWriter(nodPath.toFile())) {
        writer.write(program.toSmt2String());
      } catch (IOException e) {
        _logger.warnf("Error saving Nod program to file: %s", Throwables.getStackTraceAsString(e));
      }
    }
  }

  @Nonnull
  protected NodProgram getNodProgram(Context ctx) {
    ReachabilityProgram baseProgram =
        instrumentReachabilityProgram(_dataPlaneSynthesizer.synthesizeNodProgram());
    ReachabilityProgram queryProgram =
        instrumentReachabilityProgram(
            _querySynthesizer.getReachabilityProgram(_dataPlaneSynthesizer.getInput()));

    return _optimize
        ? optimizedProgram(ctx, baseProgram, queryProgram)
        : new NodProgram(ctx, baseProgram, queryProgram);
  }
}

@@ -167,76 +167,8 @@
 xt;%0A
-import com.microsoft.z3.Fixedpoint;%0Aimport com.microsoft.z3.Status;%0A
 impo
@@ -190,16 +190,16 @@
 Writer;%0A
+
 import j
@@ -358,52 +358,8 @@
 ll;%0A
-import org.batfish.common.BatfishException;%0A
 impo
@@ -925,24 +925,24 @@
 ynthesizer;%0A
+
     _optimiz
@@ -964,615 +964,8 @@
  %7D%0A%0A
-  protected Status computeNodSat(long startTime, Context ctx) %7B%0A    NodProgram program = getNodProgram(ctx);%0A    Fixedpoint fix = mkFixedpoint(program, true);%0A    for (BoolExpr query : program.getQueries()) %7B%0A      Status status = fix.query(query);%0A      switch (status) %7B%0A        case SATISFIABLE:%0A          return status;%0A        case UNKNOWN:%0A          throw new BatfishException(%22Query satisfiability unknown%22);%0A        case UNSATISFIABLE:%0A          return status;%0A        default:%0A          throw new BatfishException(%22invalid status%22);%0A      %7D%0A    %7D%0A    throw new BatfishException(%22No queries%22);%0A  %7D%0A%0A
   @O

remove unused function (#1410)