text: #!/usr/bin/env python3
  # -*- coding: utf-8 -*-
  
  # Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
  #
  # This program is free software; you can redistribute it and/or
  # modify it under the terms of the GNU General Public License
  # as published by the Free Software Foundation; version 2
  # of the License.
  #
  # This program is distributed in the hope that it will be useful,
  # but WITHOUT ANY WARRANTY; without even the implied warranty of
  # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  # GNU General Public License for more details.
  #
  # You should have received a copy of the GNU General Public License
  # along with this program; if not, write to the Free Software
  # Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
  
  from __future__ import with_statement  # Required in 2.5
  from __future__ import print_function
  import optparse
  import gzip
  import re
  import fnmatch
  from xor_to_cnf_class import *
  from debuglib import *
  import subprocess
  import os
  import stat
  import time
  import resource
  from functools import partial
  
  
  def unique_file(fname_begin, fname_end=".cnf"):
          counter = 1
          while 1:
              fname = "out/" + fname_begin + '_' + str(counter) + fname_end
              try:
                  fd = os.open(
                      fname, os.O_CREAT | os.O_EXCL, stat.S_IREAD | stat.S_IWRITE)
                  os.fdopen(fd).close()
                  return fname
              except OSError:
                  pass
  
              counter += 1
              if counter > 300:
                  print("Cannot create unique_file, last try was: %s" % fname)
                  exit(-1)
  
  
  def setlimits(maxtime):
      # sys.stdout.write("Setting resource limit in child (pid %d): %d s\n" %
      # (os.getpid(), maxtime))
      resource.setrlimit(resource.RLIMIT_CPU, (maxtime, maxtime))
  
  
  class solution_parser:
      def __init__(self, options):
          self.options = options
  
      @staticmethod
      def test_found_solution(solution, fname, debugLibPart=None):
          if debugLibPart is None:
              print("Verifying solution for CNF file %s" % fname)
          else:
              print("Verifying solution for CNF file %s, part %d" %
                    (fname, debugLibPart))
  
          if fnmatch.fnmatch(fname, '*.gz'):
              f = gzip.open(fname, "r")
          else:
              f = open(fname, "r")
          clauses = 0
          thisDebugLibPart = 0
  
          for line in f:
              line = line.rstrip()
  
              # skip empty lines
              if len(line) == 0:
                  continue
  
              # count debug lib parts
              if line[0] == 'c' and "Solver::solve" in line:
                  thisDebugLibPart += 1
  
              # if we are over debugLibPart, exit
              if debugLibPart is not None and thisDebugLibPart >= debugLibPart:
                  f.close()
                  return
  
              # check solution against clause
              try:
                  if line[0] != 'c' and line[0] != 'p':
                      if line[0] != 'x':
                          solution_parser._check_regular_clause(line, solution)
                      else:
                          assert line[0] == 'x', "Line must start with p, c, v or x"
                          solution_parser._check_xor_clause(line, solution)
  
                  clauses += 1
              except:
                  if debugLibPart is not None:
                      print("--> Error in part: %s. We are reading up to and including part: %s"
                            % (thisDebugLibPart, debugLibPart-1))
                  raise
  
          f.close()
          print("Verified %d original xor&regular clauses" % clauses)
  
      def sampling_vars_solution_check(self, fname, sampling_vars, solution):
          assert len(sampling_vars) > 0
          a = XorToCNF()
          tmpfname = unique_file("tmp_for_xor_to_cnf_convert")
          a.convert(fname, tmpfname, len(sampling_vars))
  
          with open(tmpfname, "a") as f:
              # NOTE: the "p cnf..." header will be wrong
              for i in sampling_vars:
                  if i not in solution:
                      print("ERROR: solution does not contain sampling var %d" % i)
                      print("Sampling vars were: %s" % sampling_vars)
                      exit(-1)
  
                  if solution[i]:
                      f.write("%d 0\n" % i)
                  else:
                      f.write("-%d 0\n" % i)
  
          print("-> added partial solution to temporary CNF file %s" % tmpfname)
  
          # execute with the other solver
          toexec = "../../build/utils/lingeling-ala/lingeling %s" % tmpfname
          print("sampling check -- solving with other solver: %s" % toexec)
          curr_time = time.time()
          try:
              p = subprocess.Popen(toexec.rsplit(),
                                   stdout=subprocess.PIPE,
                                   preexec_fn=partial(setlimits, self.options.maxtime),
                                   universal_newlines=True)
          except OSError:
              print("ERROR: Lingeing didn't run... did you install it? It should be in the path as `lingeling`")
              raise
  
          consoleOutput2 = p.communicate()[0]
          os.unlink(tmpfname)
  
          # if other solver was out of time, then we can't say anything
          diff_time = time.time() - curr_time
          if diff_time > self.options.maxtime - self.options.maxtimediff:
              print("Other solver: too much time to solve, aborted!")
              return None
  
          # extract output from the other solver
          print("Checking other solver output...")
          otherSolverUNSAT, _, _ = self.parse_solution_from_output(
              consoleOutput2.split("\n"))
  
          # check if the other solver finds a solution with the sampling vars
          # set as per partial solution returned
          if otherSolverUNSAT is True:
              print("ERROR; The other solver did NOT find a solution with the partial solution given")
              exit(-1)
              return False
  
          print("OK, other solver found a solution using the partial solution")
  
          return True
  
      def check_unsat(self, fname):
          a = XorToCNF()
          tmpfname = unique_file("tmp_for_xor_to_cnf_convert")
          a.convert(fname, tmpfname)
  
          # execute with the other solver
          toexec = "../../build/utils/lingeling-ala/lingeling %s" % tmpfname
          print("UNSAT check -- solving with other solver: %s" % toexec)
          curr_time = time.time()
          try:
              p = subprocess.Popen(toexec.rsplit(),
                                   stdout=subprocess.PIPE,
                                   preexec_fn=partial(setlimits, self.options.maxtime),
                                   universal_newlines=True)
          except OSError:
              print("ERROR: Lingeling didn't run... did you install it? It should be in the path as `lingeling`")
              raise
  
          consoleOutput2 = p.communicate()[0]
          os.unlink(tmpfname)
  
          # if other solver was out of time, then we can't say anything
          diff_time = time.time() - curr_time
          if diff_time > self.options.maxtime - self.options.maxtimediff:
              print("Other solver: too much time to solve, aborted!")
              return None
  
          # extract output from the other solver
          print("Checking other solver output...")
          otherSolverUNSAT, otherSolverSolution, _ = self.parse_solution_from_output(
              consoleOutput2.split("\n"))
  
          # check if the other solver agrees with us
          return otherSolverUNSAT
  
      def check_debug_lib(self, fname, must_check_unsat=True):
          largestPart = self._find_largest_debuglib_part(fname)
          for debugLibPart in range(1, largestPart + 1):
              fname_debug = "%s-debugLibPart%d.output" % (fname, debugLibPart)
              print("Checking debug lib part %s -- %s " % (debugLibPart, fname_debug))
  
              if (os.path.isfile(fname_debug) is False):
                  print("Error: Filename to be read '%s' is not a file!" % fname_debug)
                  exit(-1)
  
              # take file into mem
              f = open(fname_debug, "r")
              text = f.read()
              output_lines = text.splitlines()
              f.close()
  
              unsat, solution, conflict = self.parse_solution_from_output(output_lines)
              assumps = self._get_assumps(fname, debugLibPart)
              if unsat is False:
                  print("debugLib is SAT")
                  self._check_assumps_inside_solution(assumps, solution)
                  self.test_found_solution(solution, fname, debugLibPart)
              else:
                  print("debugLib is UNSAT")
                  if must_check_unsat:
                      assert conflict is not None, "debugLibPart must create a conflict in case of UNSAT"
                      self._check_assumps_inside_conflict(assumps, conflict)
                      tmpfname = unique_file("tmp_for_extract_libpart")
                      self._extract_lib_part(fname, debugLibPart, assumps, tmpfname)
  
                      # check with other solver
                      ret = self.check_unsat(tmpfname)
                      if ret is None:
                          print("Cannot check, other solver took too much time")
                      elif ret is True:
                          print("UNSAT verified by other solver")
                      else:
                          print("Grave bug: SAT-> UNSAT : Other solver found solution!!")
                          exit(-1)
                      os.unlink(tmpfname)
  
          self.remove_debuglib_files(fname)
  
      def remove_debuglib_files(self, fname):
          #removing debuglib files
          largestPart = self._find_largest_debuglib_part(fname)
          for debugLibPart in range(1, largestPart + 1):
              fname_debug = "%s-debugLibPart%d.output" % (fname, debugLibPart)
              os.unlink(fname_debug)
  
      @staticmethod
      def parse_solution_from_output(output_lines, ignoreNoSolution=False):
          if len(output_lines) == 0:
              print("Error! SAT solver output is empty!")
              print("output lines: %s" % output_lines)
              exit(-1)
  
          # solution will be put here
          satunsatfound = False
          vlinefound = False
          solution = {}
          conflict = None
  
          # parse in solution
          for line in output_lines:
              # skip comment
              if re.match('^conflict ', line):
                  line = line.strip().split()[1:]
                  conflict = [int(elem) for elem in line]
                  continue
  
              if (re.match('^c ', line)):
                  continue
  
              # solution
              if (re.match('^s ', line)):
                  if (satunsatfound):
                      print("ERROR: solution twice in solver output!")
                      exit(400)
  
                  if 'UNSAT' in line:
                      unsat = True
                      satunsatfound = True
                      continue
  
                  if 'SAT' in line:
                      unsat = False
                      satunsatfound = True
                      continue
  
                  print("ERROR: line starts with 's' but no SAT/UNSAT on line")
                  exit(400)
  
              # parse in solution
              if (re.match('^v ', line)):
                  vlinefound = True
                  myvars = line.split(' ')
                  for var in myvars:
                      var = var.strip()
                      if var == "" or var == 'v':
                          continue
                      if (int(var) == 0):
                          break
                      intvar = int(var)
                      solution[abs(intvar)] = (intvar >= 0)
                  continue
  
              if (line.strip() == ""):
                  continue
  
              print("Error! SAT solver output contains a line that is neither 'v' nor 'c' nor 's'!")
              print("Line is:", line.strip())
              exit(-1)
  
          # print("Parsed values:", solution)
  
          if (ignoreNoSolution is False and
                  (satunsatfound is False or (
                      unsat is False and vlinefound is False))):
              print("Error: Cannot find line starting with 's' or 'v' in output!")
              print(output_lines)
              print("Error code 500")
              exit(-1)
  
          if (ignoreNoSolution is True and
                  (satunsatfound is False or (
                      unsat is False and vlinefound is False))):
              print("Probably timeout, since no solution  printed. Could, of course, be segfault/assert fault, etc.")
              print("Making it look like an UNSAT, so no checks!")
              return (True, [])
  
          if (satunsatfound is False):
              print("Error: Cannot find if SAT or UNSAT. Maybe didn't finish running?")
              print(output_lines)
              print("Error code 500")
              exit(-1)
  
          if (unsat is False and vlinefound is False):
              print("Error: Solution is SAT, but no 'v' line")
              print (output_lines)
              print("Error code 500")
              exit(-1)
  
          return unsat, solution, conflict
  
      def _extract_lib_part(self, fname, debug_num, assumps, tofile):
          fromf = open(fname, "r")
          thisDebugLibPart = 0
          maxvar = 0
          numcls = 0
          for line in fromf:
              line = line.strip()
  
              # ignore empty strings and headers
              if not line or line[0] == "p":
                  continue
  
              # process (potentially special) comments
              if line[0] == "c":
                  if "Solver::solve" in line:
                      thisDebugLibPart += 1
  
                  continue
  
              # break out if we reached the debug lib part
              if thisDebugLibPart >= debug_num:
                  break
  
              # count clauses and get max var number
              numcls += 1
              maxvar = max(maxvar, get_max_var_from_clause(line))
  
          fromf.close()
  
          # now we can create the new CNF file
          fromf = open(fname, "r")
          tof = open(tofile, "w")
          tof.write("p cnf %d %d\n" % (maxvar, numcls + len(assumps)))
  
          thisDebugLibPart = 0
          for line in fromf:
              line = line.strip()
              # skip empty lines and headers
              if not line or line[0] == "p":
                  continue
  
              # parse up special header
              if line[0] == "c":
                  if "Solver::solve" in line:
                      thisDebugLibPart += 1
  
                  continue
  
              # break out if we reached the debug lib part
              if thisDebugLibPart >= debug_num:
                  break
  
              tof.write(line + '\n')
  
          # add assumptions
          for lit in assumps:
              tof.write("%d 0\n" % lit)
  
          fromf.close()
          tof.close()
  
      def _get_assumps(self, fname, debugLibPart):
          f = open(fname, "r")
  
          thispart = 0
          solveline = None
          for line in f:
              if "Solver::solve" in line:
                  thispart += 1
                  if thispart == debugLibPart:
                      solveline = line
                      break
          f.close()
  
          assert solveline is not None
          ret = re.match("c.*Solver::solve\((.*)\)", solveline)
          assert ret is not None
          assumps = ret.group(1).strip().split()
          assumps = [int(x) for x in assumps]
  
          print("Assumptions: ", assumps)
          return assumps
  
      def _check_assumps_inside_conflict(self, assumps, conflict):
          for lit in conflict:
              if -1 * lit not in assumps:
                  print("ERROR: Final conflict contains %s but assumps is %s" %(conflict, assumps))
                  print("ERROR: lit ", lit, " is in conflict but its inverse is not is assumps!")
                  exit(-100)
  
          print("OK, final conflict only contains elements from assumptions")
  
      def _check_assumps_inside_solution(self, assumps, solution):
          for lit in assumps:
              var = abs(lit)
              val = lit > 0
              if var in solution:
                  if solution[var] != val:
                      print("Solution pinted has literal %s but assumptions contained the inverse: '%s'" % (-1 * lit, assumps))
                      exit(-100)
  
          print("OK, all assumptions inside solution")
  
      def _find_largest_debuglib_part(self, fname):
          largestPart = 0
          dirList2 = os.listdir("out/.")
          fname_no_out = fname.replace("out/", "")
          for fname_debug in dirList2:
              if fnmatch.fnmatch(fname_debug, "%s-debugLibPart*.output" % fname_no_out):
                  largestPart += 1
  
          return largestPart
  
      @staticmethod
      def max_vars_in_file(fname):
          maxvar = 0
          with open(fname, "r") as f:
              for line in f:
                  line = line.strip()
  
                  # ignore comments
                  if not line or line[0] == "c" or line[0] == 'p':
                      continue
  
                  # calculate max variable
                  maxvar = max(maxvar, get_max_var_from_clause(line))
  
          return maxvar
  
      @staticmethod
      def _check_regular_clause(line, solution):
          lits = line.split()
          for lit in lits:
              numlit = int(lit)
              if numlit == 0:
                  break
  
              if abs(numlit) not in solution:
                  continue
  
              if solution[abs(numlit)] ^ (numlit < 0):
                  return True
  
          # print not set vars
          for lit in lits:
              numlit = int(lit)
              if numlit == 0:
                  break
  
              if abs(numlit) not in solution:
                  print("var %d in XOR clause not set" % abs(numlit))
  
          #print("Every other var set to FALSE")
          #print("Orig clause in DIMACS: ", lits)
          print("Error: clause '%s' not satisfied." % line.strip())
          raise NameError("Error: clause '%s' not satisfied." % line)
          return False
  
      @staticmethod
      def _check_xor_clause(line, solution):
          line = line.lstrip('x')
          lits = line.split()
          final = False
          for lit in lits:
              numlit = int(lit)
              if numlit != 0:
                  if abs(numlit) not in solution:
                      raise NameError("Error: var %d not solved, but referred to in a xor-clause of the CNF" % abs(numlit))
                  final ^= solution[abs(numlit)]
                  final ^= numlit < 0
          if final is False:
              print("Error: xor-clause '%s' not satisfied." % line.strip())
              raise NameError("Error: xor-clause '%s' not satisfied." % line)
  
          return final
  
  
  def parse_arguments():
      class PlainHelpFormatter(optparse.IndentedHelpFormatter):
  
          def format_description(self, description):
              if description:
                  return description + "\n"
              else:
                  return ""
  
      usage = """usage: %prog solution cnf
  
  For example:
  %prog my_solution_file.out my_problem.cnf.gz"""
      parser = optparse.OptionParser(usage=usage, formatter=PlainHelpFormatter())
      parser.add_option("--verbose", "-v", action="store_true",
                        default=False, dest="verbose", help="Be more verbose")
      parser.add_option("--tout", "-t", dest="maxtime", type=int, default=100,
                        help="Max time to run. Default: %default")
      parser.add_option("--textra", dest="maxtimediff", type=int, default=10,
                        help="Extra time on top of timeout for processing."
                        " Default: %default")
      # parse options
      options, args = parser.parse_args()
      return options, args
  
  if __name__ == "__main__":
      options, args = parse_arguments()
      print("Options are:", options)
      print("args are:", args)
      if len(args) != 2:
          print("ERROR: You must give exactly two parameters, "
                "one SOLUTION and one CNF")
          print("You gave {n} parameters".format(**{"n": len(args)}))
          exit(-1)
  
      sol_file = args[0]
      cnf_file = args[1]
      print("Verifying CNF file '{cnf}' against solution in file '{sol}'".format(
          **{"cnf": cnf_file, "sol": sol_file}))
  
      print("Checking debug libs...")
      sol_parser = solution_parser(options)
      sol_parser.check_debug_lib(cnf_file)
  
      print("Checking console output...")
      sol = {}
      with open(sol_file) as f:
          dat = f.read()
  
      dat = dat.split("\n")
      unsat, solution, _ = sol_parser.parse_solution_from_output(dat)
      if not unsat:
          sol_parser.test_found_solution(solution, cnf_file)
          exit(0)
  
      # check with other solver
      ret = sol_parser.check_unsat(cnf_file)
      if ret is None:
          print("Other solver time-outed, cannot check")
      elif ret is True:
          print("UNSAT verified by other solver")
      else:
          print("Grave bug: SAT-> UNSAT : Other solver found solution!!")
          exit(-1)
  