--- /dev/null
+diff -Nur stp/CMakeLists.txt r446port/CMakeLists.txt\r
+--- stp/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,139 @@\r
++cmake_minimum_required(VERSION 2.6)\r
++\r
++# base common definitions\r
++set(TargetName "stp")\r
++set(ProjectName "stp")\r
++\r
++##########################################################################\r
++project(${ProjectName})\r
++\r
++#set(CMAKE_BUILD_TYPE Release)\r
++\r
++# static build settings for MSVC/gcc\r
++include("../cmakemods/staticrt.cmake")\r
++\r
++set(PHINTS "")\r
++set(STP_DEFS_COMM -DCRYPTOMINISAT)\r
++set(STP_INCL_COMM src/sat/mtl src/AST)\r
++\r
++option(BUILD_SHARED_LIB "Whether to Build shared libstp or not" ON)\r
++\r
++set(OPTIMIZITION_FLAGS "-O3")\r
++\r
++# bison and flex is needed for buiding\r
++if(WIN32)\r
++ # build shared lib on windows is not prepared at source level\r
++ set(BUILD_SHARED_LIB OFF)\r
++ set(FLEX_PATH_HINT "e:/cygwin/bin" CACHE STRING "Flex path hints, can be null if on your path")\r
++ set(FLEX_PATH_HINT "e:/cygwin/bin" CACHE STRING "Bison path hints, can be null if on your path")\r
++ set(FLEX_PATH_HINT "C:/Perl/bin" CACHE STRING "Perl path hints, can be null if on your pat")\r
++\r
++ set(PHINTS ${PERL_PATH_HINT} ${FLEX_PATH_HINT} ${BISON_PATH_HINT})\r
++\r
++ if(MSVC)\r
++ set(OPTIMIZITION_FLAGS "/GL /Ox /Oi /Ot /Oy")\r
++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -D_CRT_SECURE_NO_WARNINGS)\r
++ set(STP_INCL_COMM ../winports ../winports/msc99hdr ${STP_INCL_COMM})\r
++\r
++ # stack size of MSVC must be specified\r
++ string(REGEX REPLACE "/STACK:[0-9]+" "" CMAKE_EXE_LINKER_FLAGS ${CMAKE_EXE_LINKER_FLAGS})\r
++ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} /STACK:256000000")\r
++ else(MSVC)\r
++ # mingw \r
++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -DEXT_HASH_MAP)\r
++ endif(MSVC)\r
++elseif(UNIX)\r
++ set(STP_DEFS_COMM ${STP_DEFS_COMM} -DEXT_HASH_MAP)\r
++endif(WIN32)\r
++\r
++find_program(PERLP perl)\r
++find_program(FLEXP flex HINTS ${PHINTS})\r
++find_program(BISONP bison HINTS ${PHINTS})\r
++\r
++#message(${PERLP})\r
++#message(${FLEXP})\r
++#message(${BISONP})\r
++\r
++\r
++if(NOT FLEXP OR NOT BISONP OR NOT PERLP)\r
++message(FATAL_ERROR "Flex/Bison/Perl is not found and is required, Abort!")\r
++endif(NOT FLEXP OR NOT BISONP OR NOT PERLP)\r
++\r
++##\r
++## add rules generate the custom files in AST\r
++##\r
++set(ASTD_PREFIX ${CMAKE_CURRENT_SOURCE_DIR}/src/AST)\r
++\r
++set(OUTFILES ${ASTD_PREFIX}/ASTKind.h ${ASTD_PREFIX}/ASTKind.cpp)\r
++set(GenKindsScript ${ASTD_PREFIX}/genkinds.pl)\r
++add_custom_command(OUTPUT ${OUTFILES}\r
++ COMMAND ${PERLP} ${GenKindsScript}\r
++ DEPENDS ${GenKindsScript}\r
++ WORKING_DIRECTORY ${ASTD_PREFIX}\r
++ )\r
++\r
++##\r
++## add rules generate the custom files in parser\r
++##\r
++set(PARSERD_PREFIX ${CMAKE_CURRENT_SOURCE_DIR}/src/parser)\r
++set(OUTFILES ${PARSERD_PREFIX}/lexCVC.cpp ${PARSERD_PREFIX}/lexSMT.cpp \r
++ ${PARSERD_PREFIX}/parseCVC.cpp ${PARSERD_PREFIX}/parseCVC_defs.h\r
++ ${PARSERD_PREFIX}/parseSMT.cpp ${PARSERD_PREFIX}/parseSMT_defs.h)\r
++add_custom_command(OUTPUT ${OUTFILES}\r
++ COMMAND ${FLEXP} -olexCVC.cpp -Pcvc CVC.lex\r
++ COMMAND ${FLEXP} -olexSMT.cpp -Psmt smtlib.lex\r
++ COMMAND ${BISONP} -y -v --defines=parseCVC_defs.h -oparseCVC.cpp -pcvc CVC.y\r
++ COMMAND ${BISONP} -y -v --defines=parseSMT_defs.h -oparseSMT.cpp -psmt smtlib.y\r
++ DEPENDS ${PARSERD_PREFIX}/CVC.lex ${PARSERD_PREFIX}/smtlib.lex ${PARSERD_PREFIX}/CVC.y ${PARSERD_PREFIX}/smtlib.y\r
++ WORKING_DIRECTORY ${PARSERD_PREFIX}\r
++ )\r
++\r
++#\r
++add_definitions(${STP_DEFS_COMM})\r
++include_directories(${STP_INCL_COMM})\r
++\r
++macro(add_stp_library lib_name, filelist)\r
++ source_group(${lib_name} FILES ${filelist})\r
++ set(LIBSTP_SRCLIST ${LIBSTP_SRCLIST} ${${filelist}} PARENT_SCOPE)\r
++endmacro(add_stp_library)\r
++\r
++\r
++set(SDIRLIST \r
++ sat \r
++ AST\r
++ STPManager\r
++ parser\r
++ absrefine_counterexample\r
++ to-sat\r
++ simplifier\r
++ printer\r
++ c_interface\r
++ extlib-constbv\r
++ )\r
++\r
++foreach(cdir ${SDIRLIST})\r
++ add_subdirectory(src/${cdir})\r
++endforeach(cdir ${SDIRLIST})\r
++\r
++# the stp library\r
++add_library(${TargetName}_lib ${STP_LIBTYPE} ${LIBSTP_SRCLIST})\r
++set_target_properties(${TargetName}_lib \r
++ PROPERTIES OUTPUT_NAME ${TargetName}\r
++ COMPILE_DEFINITIONS_RELEASE ${OPTIMIZITION_FLAGS}\r
++ COMPILE_DEFINITIONS_RELWITHDEBINFO ${OPTIMIZITION_FLAGS}\r
++ )\r
++\r
++set(DEPLIBS ${TargetName}_lib)\r
++\r
++# generate the stp main program\r
++file(GLOB SRC_LIST ${PROJECT_SOURCE_DIR}/src/main/*.c* ${PROJECT_SOURCE_DIR}/src/main/*.h)\r
++add_executable(${TargetName} ${SRC_LIST})\r
++set_target_properties(${TargetName} \r
++ PROPERTIES\r
++ COMPILE_DEFINITIONS_RELEASE ${OPTIMIZITION_FLAGS}\r
++ COMPILE_DEFINITIONS_RELWITHDEBINFO ${OPTIMIZITION_FLAGS}\r
++ )\r
++\r
++add_dependencies(${TargetName} ${DEPLIBS})\r
++target_link_libraries(${TargetName} ${DEPLIBS})\r
++\r
+diff -Nur stp/scripts/dotest.py r446port/scripts/dotest.py\r
+--- stp/scripts/dotest.py 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/scripts/dotest.py 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,316 @@\r
++#! /usr/bin/python\r
++# -*- coding: iso-8859-1 -*-\r
++\r
++# Run STP regression tests of a given level (default: 0, meaning\r
++# minimum amount of tests). The higher the regression level, the more\r
++# tests to run, and the harder they get.\r
++# Each test may contain information about its regression level,\r
++# expected outcome, expected runtime, whether it produces a proof,\r
++# etc. in the format given below. This script will scan the first 100\r
++# lines of each test and try to collect this information.\r
++# If some info is not found, defaults are assumed. Default regression\r
++# level is 0, expected runtime is unbounded, outcome is undefined\r
++# (whatever it returns is OK), proof should be produced if outcome is\r
++# Valid, and if it is produced, it'll be verified.\r
++# Test info is given in the comments; here are examples\r
++# \r
++# %%% Regression level = 2\r
++# %%% Result = Valid %% or Invalid, or Unknown\r
++# %%% Runtime = 10 %% in seconds\r
++# %%% Proof = yes %% or 'no', if it doesn't produce a proof\r
++# %%% Language = presentation %% or 'internal'\r
++\r
++# The number of '%' and following spaces can vary, case is not\r
++# important. Any text after the value is ignored. Any comments that\r
++# are not recognized are also ignored.\r
++\r
++import os, sys, subprocess, glob, re\r
++import logging, optparse\r
++from os import path\r
++from mtimeit import *\r
++\r
++gprofiler = profiler()\r
++line_len = 75\r
++\r
++class test_context:\r
++ def __init__ (self):\r
++ self.num_total = 0\r
++ self.time_total = 0\r
++ self.proofs_checked = 0\r
++ self.num_problems = 0\r
++ self.test_problems = {}\r
++ \r
++ def add_keyval (self, k, v):\r
++ if not k in self.test_problems:\r
++ self.test_problems[k] = [v]\r
++ else:\r
++ self.test_problems[k].append(v)\r
++ \r
++ def get_key (self, k):\r
++ if k in self.test_problems:\r
++ return self.test_problems[k]\r
++ return []\r
++\r
++ def add_problems (self, catig, dat):\r
++ self.add_keyval(catig, dat)\r
++ self.num_problems += 1\r
++\r
++ def add_errors (self, fn, expect_res, act_res):\r
++ self.add_problems("errors", (fn, expect_res, act_res))\r
++ \r
++ def print_errors (self):\r
++ logging.info("Total tested %d and found %d problems", self.num_total, self.num_problems)\r
++ if self.num_problems:\r
++ for k, v in self.test_problems.iteritems():\r
++ logging.info("%s test total %d", k, len(v))\r
++ for i in v:\r
++ logging.info("\t%s", i[0])\r
++ \r
++class expected_test_args:\r
++ def __init__ (self):\r
++ self.level = None\r
++ self.result = None\r
++ self.runtime = None\r
++ self.proof = None\r
++ self.sat_mode = None\r
++ self.lang = None\r
++ self.stp_opts = ""\r
++ \r
++ def set_default(self, opts):\r
++ pass\r
++\r
++def parse_cmdline(permit_null_args=True):\r
++ the_usage = "usage: %prog [options] [test path] [test path]..."\r
++ the_version = "version 0.1"\r
++ parser = optparse.OptionParser(usage = the_usage, version = the_version)\r
++\r
++ # logging options\r
++ parser.add_option("-v", "--verbose", action="store_const", const=logging.INFO, dest="log_level", default=logging.INFO)\r
++ parser.add_option("-q", "--quiet", action="store_const", const=logging.ERROR, dest="log_level")\r
++ parser.add_option("--log-format", dest="log_format", metavar="FMT", default="%(asctime)s %(levelname)s %(message)s")\r
++ parser.add_option("--log-file", dest="log_file", metavar="FILE")\r
++ parser.add_option("--log-syslog", dest="log_syslog", metavar="HOST")\r
++\r
++ # timeouts\r
++ parser.add_option("-t", "--timeout", dest="timeout", action="store_const", default=0, \r
++ help = "Timeouts in seconds 0 = no limit (default: %default)")\r
++ parser.add_option("-l", "--testlevel", dest="level", action="store_const", default=4, \r
++ help = "Max regression test level (default: %default)") \r
++ parser.add_option("--lang", dest="lang", action="store", default="all", \r
++ help = "Language: presentation/internal/smt-lib (default: %default)")\r
++ parser.add_option("-p", "--stppath", dest="stppath", action="store", default="", \r
++ help = "Stp path (default: %default)") \r
++ parser.add_option("--stpopt", dest="stpopt", action="store", default="-d", \r
++ help = "Options passed to stp command line (default: %default)") \r
++ parser.add_option("--vc", dest="vc", action="store", default="bin/stp", \r
++ help = "Verification program (default: %default)") \r
++ parser.add_option("--rt", dest="checkruntime", action="store_true", default=True,\r
++ help = "Check that each test finishes within the specified runtime (default: %default)") \r
++ parser.add_option("--no-rt", dest="checkruntime", action="store_false",\r
++ help = "Don't check that each test finishes within the specified runtime")\r
++ parser.add_option("--max-info-lines", dest="maxinfolines", action="store_const", default=4,\r
++ help = "Max info lines to check per testcase file (default: %default)") \r
++ parser.add_option("--proofs", dest="proofs", action="store_true",\r
++ help = "Produce and verify proofs, None means depends on testcase(default: %default)") \r
++ parser.add_option("--no-proofs", dest="proofs", action="store_false",\r
++ help = "Do not produce / verify proofs ")\r
++ parser.add_option("-f", "--list-file", dest="listfile", action="store",\r
++ help = "Check test case listed in file")\r
++ parser.add_option("-r", "--recursive", dest="recursive", action="store_true", default=False,\r
++ help = "Do test recursively (default: %default)")\r
++\r
++ opts, args = parser.parse_args()\r
++ if len(args) == 0 and not permit_null_args:\r
++ parser.print_help()\r
++ parser.exit()\r
++ return (opts, args)\r
++\r
++def parse_cmdline_and_logging(permit_null_args=True):\r
++ opts, args = parse_cmdline(permit_null_args)\r
++ # process logging support\r
++ logging.basicConfig(level=opts.log_level, format=opts.log_format, filename=opts.log_file, stream=sys.stdout)\r
++ if opts.log_syslog:\r
++ from logging.handlers import SysLogHandler\r
++ logging.info("redirect log to syslogd at %s", opts.log_syslog)\r
++ logging.getLogger().addHandler(SysLogHandler((opts.log_syslog, 514), SysLogHandler.LOG_LOCAL0))\r
++ return (opts, args)\r
++\r
++def log_basic_test_info(opts):\r
++ logging.info("Base Test Options:")\r
++ logging.info("*"*line_len)\r
++ logging.info("Regression level: %d"%opts.level)\r
++ logging.info("Language: %s"%opts.lang)\r
++ if None == opts.proofs: s = "depends on testcase"\r
++ elif opts.proofs: s = "yes"\r
++ else: s = "no"\r
++ logging.info("Whether to produce / check proofs: %s"%s)\r
++ \r
++ if opts.timeout == 0: s = "no limit"\r
++ else: s = "%d seconds"%opts.timeout\r
++ logging.info("Time limit per test: %s"%s)\r
++ logging.info("*"*line_len)\r
++ logging.info("\n\n")\r
++\r
++def get_test_opt(opts, test_fn):\r
++ targs = expected_test_args()\r
++ with open(test_fn, "rt") as f:\r
++ for idx, ln in enumerate(f):\r
++ if idx > opts.maxinfolines:\r
++ break\r
++ so = re.search(r"^(\s|%|\#)*Regression level\s*=\s*(\d+)", ln, re.I)\r
++ if so:\r
++ targs.level = int(so.group(2))\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*Result\s*=\s*(Invalid|Valid|Unknown)", ln, re.I)\r
++ if so:\r
++ targs.result = so.group(2)\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*Runtime\s*=\s*(\d+)", ln, re.I)\r
++ if so:\r
++ targs.runtime = int(so.group(2))\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*Proof\s*=\s*(yes|no)", ln, re.I)\r
++ if so:\r
++ targs.proofs = so.group(2)\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*SAT mode\s*=\s*(on|off)", ln, re.I)\r
++ if so:\r
++ targs.sat_mode = so.group(2)\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*Language\s*=\s*((\w|\d|\_)+)", ln, re.I)\r
++ if so:\r
++ targs.lang = so.group(2)\r
++ continue\r
++ so = re.search(r"^(\s|%|\#)*STP Options\s*=\s*(.*)$", ln, re.I)\r
++ if so:\r
++ targs.stp_opts = so.group(2)\r
++ continue\r
++ # guess the level and lang\r
++ if targs.level == None: targs.level = 3\r
++ if targs.lang == None: \r
++ if re.search(r"\.(stp|svc)$", test_fn, re.I): targs.lang = "presentation"\r
++ if re.search(r"\.(li?sp)$", test_fn, re.I): targs.lang = "internal"\r
++ if re.search(r"\.(smt)$", test_fn, re.I): targs.lang = "smt-lib"\r
++ if targs.result == None:\r
++ targs.result = "Unknown"\r
++ return targs\r
++\r
++def do_test (opts, tfn):\r
++ if path.exists(tfn): tfn = path.abspath(tfn) \r
++ targs = get_test_opt(opts, tfn)\r
++\r
++ # test only levels that below current or no level hints\r
++ if targs.level and targs.level > opts.level:\r
++ logging.warn("Skip test case %s at level %d", tfn, targs.level);\r
++ return \r
++ if opts.lang != "all" and targs.lang and targs.lang != opts.lang:\r
++ logging.warn("Skip test case %s with lang %d", tfn, targs.lang);\r
++ return \r
++\r
++ cmd = [opts.stppath]\r
++ if opts.stpopt: cmd.append(opts.stpopt)\r
++\r
++ logging.info("\n")\r
++ logging.info("="*line_len)\r
++ logging.info("checking %s"%tfn)\r
++ logging.info("Language: %s", targs.lang)\r
++ logging.info("Checking proofs: %s", "yes" if opts.proofs else "no")\r
++ if targs.runtime:\r
++ logging.info("Expected runtime: %d sec", targs.runtime)\r
++ if targs.result:\r
++ logging.info("Expected result: %s", targs.result)\r
++ if targs.stp_opts:\r
++ logging.info("STP options: ", targs.stp_opts)\r
++ cmd.append(targs.stp_opts)\r
++ cmd.append(tfn)\r
++\r
++ opts.text_ctx.num_total += 1\r
++ test_tim = accum_time()\r
++ try:\r
++ with mtimeit_ctxmgr(test_tim):\r
++ subp = subprocess.Popen(cmd, stdout = subprocess.PIPE, stderr = subprocess.PIPE)\r
++ sout, serr = subp.communicate()\r
++ if opts.timeout:\r
++ test_runtime = opts.timeout\r
++ if targs.runtime and targs.runtime > opts.timeout:\r
++ test_runtime = targs.runtime\r
++ while True:\r
++ if subp.poll():\r
++ break\r
++ if test_tim() > test_runtime:\r
++ subp.terminate()\r
++ opts.text_ctx.add_problems("timedout->killed", (tfn, test_runtime))\r
++ time.sleep(0.05)\r
++ else: \r
++ subp.wait()\r
++ \r
++ if targs.result:\r
++ so = re.search(targs.result, sout, re.M|re.I)\r
++ if not so:\r
++ logging.error("%s result not conform!"%tfn)\r
++ s = (sout+serr)\r
++ if s: s.strip("\r\n ") \r
++ opts.text_ctx.add_problems("Result error", (tfn, targs.result, s))\r
++ else:\r
++ logging.info("test passed")\r
++\r
++ except:\r
++ logging.error("Exception when testing: %s", tfn)\r
++ raise\r
++ opts.text_ctx.add_problems("Failed tests", (tfn, targs.runtime))\r
++\r
++ if targs.runtime:\r
++ if test_tim() > targs.runtime:\r
++ opts.text_ctx.add_problems("Longer tests", (tfn, targs.runtime))\r
++ if targs.runtime > 5 and test_tim() < targs.runtime/2:\r
++ opts.text_ctx.add_problems("Faster tests", (tfn, targs.runtime))\r
++\r
++ logging.info("-"*(line_len/2))\r
++ logging.info("Runtime is: %d", test_tim())\r
++ logging.info("="*line_len+"\n")\r
++ \r
++@fun_profile("Time Total", gprofiler)\r
++def do_task_test (opts, args):\r
++ for arg in args:\r
++ if os.path.isfile(arg): do_test(opts, arg)\r
++ elif os.path.isdir(arg):\r
++ fns = os.path.join(arg, "*.*")\r
++ testcases = glob.glob(fns)\r
++ for fn in testcases:\r
++ do_test(opts, fn)\r
++\r
++ if opts.listfile:\r
++ with open(opts.listfile, "rt") as f:\r
++ for ln in f:\r
++ ln = ln.strip("\r\n ")\r
++ if ln:\r
++ do_test(opts, ln) \r
++\r
++if __name__=='__main__':\r
++ opts, args = parse_cmdline_and_logging()\r
++ \r
++ # guess some predefined paths\r
++ defp1 = path.join("..", "bin", "stp.exe")\r
++ defp2 = path.join("..", "bin", "stp")\r
++ if not opts.stppath:\r
++ if path.exists(defp1): opts.stppath = defp1\r
++ elif path.exists(defp2): opts.stppath = defp2\r
++ else: opts.stppath = path.join("bin", "stp")\r
++\r
++ log_basic_test_info(opts)\r
++ opts.text_ctx = test_context()\r
++ try:\r
++ do_task_test(opts, args)\r
++ except KeyboardInterrupt:\r
++ logging.error("="*line_len)\r
++ logging.error("!!! User aborted by keyboard interrupt!")\r
++ logging.error("="*line_len)\r
++ finally:\r
++ logging.getLogger('').setLevel(logging.INFO)\r
++ logging.info("\n\n")\r
++ logging.info("Statistics:")\r
++ logging.info("="*line_len)\r
++ opts.text_ctx.print_errors()\r
++ gprofiler.print_percent()\r
++ logging.info("="*line_len)\r
++ logging.info("\n\n")\r
+diff -Nur stp/scripts/mtimeit.py r446port/scripts/mtimeit.py\r
+--- stp/scripts/mtimeit.py 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/scripts/mtimeit.py 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,136 @@\r
++#! /usr/bin/python\r
++# -*- coding: iso-8859-1 -*-\r
++# assuming python 2.6+ we use with statement without\r
++import os, sys, time\r
++import logging\r
++\r
++class mtimeit:\r
++ def __init__ (self):\r
++ # to make sure that these should not be un-initialized\r
++ self.stt = None\r
++ self.edt = None\r
++\r
++ def start (self):\r
++ self.stt = time.time() #time.clock() #time.time()\r
++\r
++ def end_and_get_length(self):\r
++ self.end()\r
++ return self.length()\r
++ \r
++ def end (self):\r
++ self.edt = time.time() #time.clock() #time.time()\r
++\r
++ def length (self):\r
++ return self.edt - self.stt\r
++\r
++ def get_srepr (self):\r
++ tstr = ""\r
++ ttim = self.length()\r
++ if ttim >= 3110400000.0:\r
++ tstr = "%f centuries"%(ttim/3110400000.0)\r
++ elif ttim >= 31104000:\r
++ tstr = "%f years"%(ttim/31104000.0)\r
++ elif ttim >= 2592000:\r
++ tstr = "%f months"%(ttim/2592000.0)\r
++ elif ttim >= 86400:\r
++ tstr = "%f days"%(ttim/86400.0)\r
++ elif ttim >= 3600:\r
++ tstr = "%f hours"%(ttim/3600.0)\r
++ elif ttim >= 60:\r
++ tstr = "%f minutes"%(ttim/60)\r
++ else:\r
++ tstr = "%f seconds"%ttim\r
++ return tstr\r
++ \r
++ def print_srepr(self):\r
++ print(self.get_srepr())\r
++ return True\r
++\r
++ show_time = print_srepr\r
++\r
++class accum_time:\r
++ def __init__(self, val=0):\r
++ self.val = val\r
++\r
++ def __iadd__( self, n):\r
++ self.val += n\r
++\r
++ def __add__( self, n):\r
++ self.val += n\r
++\r
++ def __call__( self):\r
++ return self.val\r
++\r
++\r
++class mtimeit_ctxmgr():\r
++ def __init__(self, tacc):\r
++ self.val = tacc\r
++\r
++ def __enter__(self):\r
++ self.tobj = mtimeit()\r
++ self.tobj.start()\r
++ return self.tobj\r
++\r
++ def __exit__(self, exc_type, exc_value, traceback):\r
++ self.val += self.tobj.end_and_get_length()\r
++ return False\r
++\r
++class profiler():\r
++ def __init__(self):\r
++ self.tot_tim = 0\r
++ self.profd = {}\r
++ \r
++ def __getitem__( self, key):\r
++ if self.profd.has_key(key):\r
++ return self.profd[key] \r
++ names = [name for name in self.profd.keys() if name.startswith(key + '.')] \r
++ if names:\r
++ return accum_time(sum([self.profd[name]() for name in names]))\r
++ else:\r
++ return self.profd.setdefault(key, accum_time())\r
++ \r
++ def __setitem__( self, key, value):\r
++ self.profd[key] = value\r
++ \r
++ def print_percent(self, tval = None):\r
++ self.tot_tim = tval\r
++ tt = 0\r
++ if not self.tot_tim:\r
++ self.tot_tim = 0\r
++ for k, v in self.profd.iteritems():\r
++ self.tot_tim += v()\r
++ for k, v in self.profd.iteritems():\r
++ tt += v()\r
++ logging.info("%-20s: time: %5.2f seconds percent: %2.2f%%"%(k, v(), self.get_percent(v())))\r
++ logging.info("%-20s: time: %5.2f seconds percent: %2.2f%%"%("All monitored events", tt, self.get_percent(tt)))\r
++ \r
++ def get_percent(self, v):\r
++ rv = 0.0 \r
++ if self.tot_tim:\r
++ rv = v*100 / self.tot_tim\r
++ return rv\r
++ \r
++def class_profile(name): \r
++ def wrapper(func):\r
++ def newf(self, *args, **kwds):\r
++ if not hasattr(self, "profiler"): self.profiler = profiler() \r
++ with mtimeit_ctxmgr(self.profiler[name]):\r
++ return func(self, *args, **kwds)\r
++ return newf\r
++ return wrapper\r
++\r
++def fun_profile(name, the_profiler):\r
++ def wrapper(func):\r
++ def newf(self, *args, **kwds):\r
++ with mtimeit_ctxmgr(the_profiler[name]):\r
++ return func(self, *args, **kwds)\r
++ return newf\r
++ return wrapper\r
++\r
++\r
++if __name__=='__main__':\r
++ tim = mtimeit()\r
++ tim.start()\r
++ time.sleep(2.5)\r
++ tim.end()\r
++ tim.print_srepr()\r
+diff -Nur stp/src/absrefine_counterexample/CMakeLists.txt r446port/src/absrefine_counterexample/CMakeLists.txt\r
+--- stp/src/absrefine_counterexample/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/absrefine_counterexample/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(absrefine_counterexample, SRCS)\r
+diff -Nur stp/src/AST/CMakeLists.txt r446port/src/AST/CMakeLists.txt\r
+--- stp/src/AST/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/AST/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,9 @@\r
++set(OUTFILES ${CMAKE_CURRENT_SOURCE_DIR}/ASTKind.h ${CMAKE_CURRENT_SOURCE_DIR}/ASTKind.cpp)\r
++\r
++file(GLOB SRCS *.h *.c*)\r
++string(REGEX MATCH HasAstKindFile "ASTKind.(h|cpp)" ${SRCS})\r
++if(NOT HasAstKindFile)\r
++ set(SRCS ${SRCS} ${OUTFILES})\r
++endif(NOT HasAstKindFile)\r
++\r
++add_stp_library(ast, SRCS)\r
+diff -Nur stp/src/AST/UsefulDefs.h r446port/src/AST/UsefulDefs.h\r
+--- stp/src/AST/UsefulDefs.h 2009-11-27 14:47:14.484375000 +0800\r
++++ r446port/src/AST/UsefulDefs.h 2009-12-07 12:51:46.000000000 +0800\r
+@@ -29,12 +29,19 @@\r
+ #ifdef EXT_HASH_MAP\r
+ #include <ext/hash_set>\r
+ #include <ext/hash_map>\r
+-#elif defined(TR1_UNORDERED_MAP)\r
++#elif defined(TR1_UNORDERED_MAP) || defined(_GLIBCXX_UNORDERED_MAP)\r
+ #include <tr1/unordered_map>\r
+ #include <tr1/unordered_set>\r
+ #define hash_map tr1::unordered_map\r
+ #define hash_set tr1::unordered_set\r
+ #define hash_multiset tr1::unordered_multiset\r
++#elif defined(_MSC_VER) && defined(_HAS_TR1)\r
++#include <unordered_map>\r
++#include <unordered_set>\r
++#define hash_map tr1::unordered_map\r
++#define hash_set tr1::unordered_set\r
++#define hash_multiset tr1::unordered_multiset\r
++#define TR1_UNORDERED_MAP 1\r
+ #else\r
+ #include <hash_set>\r
+ #include <hash_map>\r
+diff -Nur stp/src/c_interface/CMakeLists.txt r446port/src/c_interface/CMakeLists.txt\r
+--- stp/src/c_interface/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/c_interface/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(c_interface, SRCS)\r
+diff -Nur stp/src/extlib-constbv/CMakeLists.txt r446port/src/extlib-constbv/CMakeLists.txt\r
+--- stp/src/extlib-constbv/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/extlib-constbv/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(constantbv, SRCS)\r
+diff -Nur stp/src/main/main.cpp r446port/src/main/main.cpp\r
+--- stp/src/main/main.cpp 2009-11-13 11:49:35.859375000 +0800\r
++++ r446port/src/main/main.cpp 2009-12-07 12:51:46.000000000 +0800\r
+@@ -26,6 +26,11 @@\r
+ exit(0);\r
+ }\r
+ \r
++#if 1 \r
++namespace BEEV{\r
++ const std::string version = "1.00";\r
++}\r
++#endif\r
+ \r
+ // Amount of memory to ask for at beginning of main.\r
+ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000;\r
+@@ -44,12 +49,16 @@\r
+ extern FILE *cvcin;\r
+ extern FILE *smtin;\r
+ \r
+- // Grab some memory from the OS upfront to reduce system time when\r
+- // individual hash tables are being allocated\r
+- if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1))\r
+- {\r
+- FatalError("Initial allocation of memory failed.");\r
+- }\r
++\r
++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
++ // Grab some memory from the OS upfront to reduce system time when\r
++ // individual hash tables are being allocated\r
++ if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1))\r
++ {\r
++ FatalError("Initial allocation of memory failed.");\r
++ }\r
++#endif // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
++\r
+ \r
+ \r
+ STPMgr * bm = new STPMgr();\r
+@@ -59,7 +68,9 @@\r
+ ToSAT * tosat = new ToSAT(bm, simp);\r
+ AbsRefine_CounterExample * Ctr_Example = \r
+ new AbsRefine_CounterExample(bm, simp, arrayTransformer, tosat); \r
+- itimerval timeout; \r
++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
++ itimerval timeout; \r
++#endif // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
+ \r
+ ParserBM = bm;\r
+ GlobalSTP = \r
+@@ -145,12 +156,14 @@\r
+ bm->UserFlags.num_absrefine = atoi(argv[++i]);\r
+ break; \r
+ case 'g':\r
+- signal(SIGVTALRM, handle_time_out);\r
+- timeout.it_interval.tv_usec = 0;\r
+- timeout.it_interval.tv_sec = 0;\r
+- timeout.it_value.tv_usec = 0;\r
+- timeout.it_value.tv_sec = atoi(argv[++i]);\r
+- setitimer(ITIMER_VIRTUAL, &timeout, NULL);\r
++#if !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
++ signal(SIGVTALRM, handle_time_out);\r
++ timeout.it_interval.tv_usec = 0;\r
++ timeout.it_interval.tv_sec = 0;\r
++ timeout.it_value.tv_usec = 0;\r
++ timeout.it_value.tv_sec = atoi(argv[++i]);\r
++ setitimer(ITIMER_VIRTUAL, &timeout, NULL);\r
++#endif // !defined(_MSC_VER) && !defined(__MINGW32__) && !defined(__MINGW64__)\r
+ break; \r
+ case 'h':\r
+ fprintf(stderr,usage,prog);\r
+Files stp/src/parser/.parsePL.cpp.swp and r446port/src/parser/.parsePL.cpp.swp differ\r
+Files stp/src/parser/.PL.y.swp and r446port/src/parser/.PL.y.swp differ\r
+diff -Nur stp/src/parser/CMakeLists.txt r446port/src/parser/CMakeLists.txt\r
+--- stp/src/parser/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/parser/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,11 @@\r
++set(OUTFILES ${CMAKE_CURRENT_SOURCE_DIR}/lexCVC.cpp ${CMAKE_CURRENT_SOURCE_DIR}/lexSMT.cpp \r
++ ${CMAKE_CURRENT_SOURCE_DIR}/parseCVC.cpp ${CMAKE_CURRENT_SOURCE_DIR}/parseCVC_defs.h \r
++ ${CMAKE_CURRENT_SOURCE_DIR}/parseSMT.cpp ${CMAKE_CURRENT_SOURCE_DIR}/parseSMT_defs.h)\r
++\r
++file(GLOB SRCS *.h *.c *.cpp)\r
++string(REGEX MATCH HasAstKindFile "lexCVC.(h|cpp)" ${SRCS})\r
++if(NOT HasAstKindFile)\r
++ set(SRCS ${SRCS} ${OUTFILES})\r
++endif(NOT HasAstKindFile)\r
++\r
++add_stp_library(parser, SRCS)\r
+diff -Nur stp/src/parser/CVC.lex r446port/src/parser/CVC.lex\r
+--- stp/src/parser/CVC.lex 2009-11-17 09:20:17.484375000 +0800\r
++++ r446port/src/parser/CVC.lex 2009-12-07 12:51:46.000000000 +0800\r
+@@ -15,6 +15,9 @@\r
+ using namespace BEEV; \r
+ extern char *yytext;\r
+ extern int cvcerror (const char *msg);\r
++#ifdef _MSC_VER\r
++ #include <io.h>\r
++#endif\r
+ %}\r
+ \r
+ %option noyywrap\r
+diff -Nur stp/src/parser/smtlib.lex r446port/src/parser/smtlib.lex\r
+--- stp/src/parser/smtlib.lex 2009-10-21 13:36:04.937500000 +0800\r
++++ r446port/src/parser/smtlib.lex 2009-12-07 12:51:46.000000000 +0800\r
+@@ -36,7 +36,9 @@\r
+ #include <iostream>\r
+ #include "parser.h"\r
+ #include "parseSMT_defs.h"\r
+-\r
++#ifdef _MSC_VER\r
++ #include <io.h>\r
++#endif\r
+ using namespace std;\r
+ using namespace BEEV;\r
+ \r
+diff -Nur stp/src/printer/CMakeLists.txt r446port/src/printer/CMakeLists.txt\r
+--- stp/src/printer/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/printer/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(printer, SRCS)\r
+diff -Nur stp/src/sat/CMakeLists.txt r446port/src/sat/CMakeLists.txt\r
+--- stp/src/sat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/sat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++add_subdirectory(cryptominisat)\r
++add_stp_library(the_sat, SRCS)\r
+diff -Nur stp/src/sat/cryptominisat/clause.cpp r446port/src/sat/cryptominisat/clause.cpp\r
+--- stp/src/sat/cryptominisat/clause.cpp 2009-10-30 09:23:32.671875000 +0800\r
++++ r446port/src/sat/cryptominisat/clause.cpp 2009-12-07 12:51:46.000000000 +0800\r
+@@ -24,14 +24,16 @@\r
+ \r
+ Clause* Clause_new(const vec<Lit>& ps, const uint group, const bool learnt)\r
+ {\r
+- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));\r
++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0);\r
++ void* mem = malloc(msiz);\r
+ Clause* real= new (mem) Clause(ps, group, learnt);\r
+ return real;\r
+ }\r
+ \r
+ Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt)\r
+ {\r
+- void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));\r
++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0);\r
++ void* mem = malloc(msiz);\r
+ Clause* real= new (mem) Clause(ps, group, learnt);\r
+ return real;\r
+ }\r
+@@ -39,6 +41,8 @@\r
+ #ifdef USE_GAUSS\r
+ Clause* Clause_new(const mpz_class& ps, const vec<lbool>& assigns, const vector<uint>& col_to_var_original, const uint group, const bool learnt)\r
+ {\r
++ size_t msiz = sizeof(Clause) + sizeof(Lit)* (ps.size() ? (ps.size() - 1) : 0);\r
++ void* mem = malloc(msiz);\r
+ void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size()));\r
+ Clause* real= new (mem) Clause(ps, assigns, col_to_var_original, group, learnt);\r
+ return real;\r
+diff -Nur stp/src/sat/cryptominisat/clause.h r446port/src/sat/cryptominisat/clause.h\r
+--- stp/src/sat/cryptominisat/clause.h 2009-11-11 15:22:26.619365500 +0800\r
++++ r446port/src/sat/cryptominisat/clause.h 2009-12-07 12:51:46.000000000 +0800\r
+@@ -49,7 +49,7 @@\r
+ protected:\r
+ uint32_t size_etc;\r
+ float act;\r
+- Lit data[0];\r
++ Lit data[1];\r
+ \r
+ public:\r
+ Clause(const vec<Lit>& ps, const uint _group, const bool learnt) :\r
+diff -Nur stp/src/sat/cryptominisat/CMakeLists.txt r446port/src/sat/cryptominisat/CMakeLists.txt\r
+--- stp/src/sat/cryptominisat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/sat/cryptominisat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,3 @@\r
++file(GLOB SRCS *.h *.c*)\r
++#add_library(minisat STATIC ${SRCS})\r
++add_stp_library(minisat, SRCS)\r
+diff -Nur stp/src/sat/cryptominisat/Solver.h r446port/src/sat/cryptominisat/Solver.h\r
+--- stp/src/sat/cryptominisat/Solver.h 2009-10-30 09:23:32.656250000 +0800\r
++++ r446port/src/sat/cryptominisat/Solver.h 2009-12-07 12:51:46.000000000 +0800\r
+@@ -31,7 +31,7 @@\r
+ #include "clause.h"\r
+ #include <string.h>\r
+ \r
+-#ifdef _MSC_VER\r
++#if defined(_MSC_VER) || defined(__MINGW32__) || defined(__MINGW64__)\r
+ #include <ctime>\r
+ #else\r
+ #include <sys/time.h>\r
+diff -Nur stp/src/sat/mtl/Sort.h r446port/src/sat/mtl/Sort.h\r
+--- stp/src/sat/mtl/Sort.h 2009-10-30 09:23:32.937500000 +0800\r
++++ r446port/src/sat/mtl/Sort.h 2009-12-07 12:51:46.000000000 +0800\r
+@@ -86,7 +86,7 @@\r
+ \r
+ \r
+ template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {\r
+- sort((T*)v, v.size(), lt); }\r
++ sort(v.getData(), v.size(), lt); }\r
+ template <class T> void sort(vec<T>& v) {\r
+ sort(v, LessThan_default<T>()); }\r
+ \r
+diff -Nur stp/src/simplifier/CMakeLists.txt r446port/src/simplifier/CMakeLists.txt\r
+--- stp/src/simplifier/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/simplifier/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(simplifier, SRCS)\r
+diff -Nur stp/src/STPManager/CMakeLists.txt r446port/src/STPManager/CMakeLists.txt\r
+--- stp/src/STPManager/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/STPManager/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(STPManager, SRCS)\r
+diff -Nur stp/src/STPManager/STPManager.h r446port/src/STPManager/STPManager.h\r
+--- stp/src/STPManager/STPManager.h 2009-11-18 10:56:12.484375000 +0800\r
++++ r446port/src/STPManager/STPManager.h 2009-12-07 12:51:46.000000000 +0800\r
+@@ -13,6 +13,9 @@\r
+ #include "UserDefinedFlags.h"\r
+ #include "../AST/AST.h"\r
+ #include "../parser/let-funcs.h"\r
++#if defined(_MSC_VER)\r
++ #include <compdep.h>\r
++#endif\r
+ \r
+ namespace BEEV\r
+ {\r
+diff -Nur stp/src/to-sat/BitBlast.cpp r446port/src/to-sat/BitBlast.cpp\r
+--- stp/src/to-sat/BitBlast.cpp 2009-11-11 15:22:27.213107900 +0800\r
++++ r446port/src/to-sat/BitBlast.cpp 2009-12-07 12:51:46.000000000 +0800\r
+@@ -1019,14 +1019,12 @@\r
+ // left shift x (destructively) within width. loop backwards so\r
+ // that copy to self works correctly. (DON'T use STL insert!)\r
+ ASTVec::iterator xbeg = x.begin();\r
+- ASTVec::iterator xit = x.end() - 1;\r
+- for (; xit >= xbeg; xit--)\r
+- {\r
+- if (xit - shift >= xbeg)\r
+- *xit = *(xit - shift);\r
+- else\r
+- *xit = ASTFalse; // new LSB is zero.\r
+- }\r
++ ASTVec::iterator xend = x.end();\r
++ ASTVec::iterator semi_end = xbeg + shift;\r
++ if ( semi_end < xend ) {\r
++ copy_backward(xbeg, xend - shift, x.end());\r
++ }\r
++ fill(xbeg, min(semi_end, x.end()), ASTFalse);\r
+ }\r
+ \r
+ // Right shift within fixed field inserting zeros at MSB.\r
+diff -Nur stp/src/to-sat/CMakeLists.txt r446port/src/to-sat/CMakeLists.txt\r
+--- stp/src/to-sat/CMakeLists.txt 1970-01-01 08:00:00.000000000 +0800\r
++++ r446port/src/to-sat/CMakeLists.txt 2009-12-07 12:51:46.000000000 +0800\r
+@@ -0,0 +1,2 @@\r
++file(GLOB SRCS *.h *.c*)\r
++add_stp_library(to-sat, SRCS)\r
--- /dev/null
+// ISO C9x compliant stdint.h for Microsoft Visual Studio
+// Based on ISO/IEC 9899:TC2 Committee draft (May 6, 2005) WG14/N1124
+//
+// Copyright (c) 2006-2008 Alexander Chemeris
+//
+// Redistribution and use in source and binary forms, with or without
+// modification, are permitted provided that the following conditions are met:
+//
+// 1. Redistributions of source code must retain the above copyright notice,
+// this list of conditions and the following disclaimer.
+//
+// 2. Redistributions in binary form must reproduce the above copyright
+// notice, this list of conditions and the following disclaimer in the
+// documentation and/or other materials provided with the distribution.
+//
+// 3. The name of the author may be used to endorse or promote products
+// derived from this software without specific prior written permission.
+//
+// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED
+// WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+// MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO
+// EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
+// OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
+// WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
+// OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
+// ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+//
+///////////////////////////////////////////////////////////////////////////////
+
+#ifndef _MSC_VER // [
+#error "Use this header only with Microsoft Visual C++ compilers!"
+#endif // _MSC_VER ]
+
+#ifndef _MSC_STDINT_H_ // [
+#define _MSC_STDINT_H_
+
+#if _MSC_VER > 1000
+#pragma once
+#endif
+
+#include <limits.h>
+
+// For Visual Studio 6 in C++ mode and for many Visual Studio versions when
+// compiling for ARM we should wrap <wchar.h> include with 'extern "C++" {}'
+// or compiler give many errors like this:
+// error C2733: second C linkage of overloaded function 'wmemchr' not allowed
+#ifdef __cplusplus
+extern "C" {
+#endif
+# include <wchar.h>
+#ifdef __cplusplus
+}
+#endif
+
+// Define _W64 macros to mark types changing their size, like intptr_t.
+#ifndef _W64
+# if !defined(__midl) && (defined(_X86_) || defined(_M_IX86)) && _MSC_VER >= 1300
+# define _W64 __w64
+# else
+# define _W64
+# endif
+#endif
+
+
+// 7.18.1 Integer types
+
+// 7.18.1.1 Exact-width integer types
+
+// Visual Studio 6 and Embedded Visual C++ 4 doesn't
+// realize that, e.g. char has the same size as __int8
+// so we give up on __intX for them.
+#if (_MSC_VER < 1300)
+ typedef signed char int8_t;
+ typedef signed short int16_t;
+ typedef signed int int32_t;
+ typedef unsigned char uint8_t;
+ typedef unsigned short uint16_t;
+ typedef unsigned int uint32_t;
+#else
+ typedef signed __int8 int8_t;
+ typedef signed __int16 int16_t;
+ typedef signed __int32 int32_t;
+ typedef unsigned __int8 uint8_t;
+ typedef unsigned __int16 uint16_t;
+ typedef unsigned __int32 uint32_t;
+#endif
+typedef signed __int64 int64_t;
+typedef unsigned __int64 uint64_t;
+
+
+// 7.18.1.2 Minimum-width integer types
+typedef int8_t int_least8_t;
+typedef int16_t int_least16_t;
+typedef int32_t int_least32_t;
+typedef int64_t int_least64_t;
+typedef uint8_t uint_least8_t;
+typedef uint16_t uint_least16_t;
+typedef uint32_t uint_least32_t;
+typedef uint64_t uint_least64_t;
+
+// 7.18.1.3 Fastest minimum-width integer types
+typedef int8_t int_fast8_t;
+typedef int16_t int_fast16_t;
+typedef int32_t int_fast32_t;
+typedef int64_t int_fast64_t;
+typedef uint8_t uint_fast8_t;
+typedef uint16_t uint_fast16_t;
+typedef uint32_t uint_fast32_t;
+typedef uint64_t uint_fast64_t;
+
+// 7.18.1.4 Integer types capable of holding object pointers
+#ifdef _WIN64 // [
+ typedef signed __int64 intptr_t;
+ typedef unsigned __int64 uintptr_t;
+#else // _WIN64 ][
+ typedef _W64 signed int intptr_t;
+ typedef _W64 unsigned int uintptr_t;
+#endif // _WIN64 ]
+
+// 7.18.1.5 Greatest-width integer types
+typedef int64_t intmax_t;
+typedef uint64_t uintmax_t;
+
+
+// 7.18.2 Limits of specified-width integer types
+
+#if !defined(__cplusplus) || defined(__STDC_LIMIT_MACROS) // [ See footnote 220 at page 257 and footnote 221 at page 259
+
+// 7.18.2.1 Limits of exact-width integer types
+#define INT8_MIN ((int8_t)_I8_MIN)
+#define INT8_MAX _I8_MAX
+#define INT16_MIN ((int16_t)_I16_MIN)
+#define INT16_MAX _I16_MAX
+#define INT32_MIN ((int32_t)_I32_MIN)
+#define INT32_MAX _I32_MAX
+#define INT64_MIN ((int64_t)_I64_MIN)
+#define INT64_MAX _I64_MAX
+#define UINT8_MAX _UI8_MAX
+#define UINT16_MAX _UI16_MAX
+#define UINT32_MAX _UI32_MAX
+#define UINT64_MAX _UI64_MAX
+
+// 7.18.2.2 Limits of minimum-width integer types
+#define INT_LEAST8_MIN INT8_MIN
+#define INT_LEAST8_MAX INT8_MAX
+#define INT_LEAST16_MIN INT16_MIN
+#define INT_LEAST16_MAX INT16_MAX
+#define INT_LEAST32_MIN INT32_MIN
+#define INT_LEAST32_MAX INT32_MAX
+#define INT_LEAST64_MIN INT64_MIN
+#define INT_LEAST64_MAX INT64_MAX
+#define UINT_LEAST8_MAX UINT8_MAX
+#define UINT_LEAST16_MAX UINT16_MAX
+#define UINT_LEAST32_MAX UINT32_MAX
+#define UINT_LEAST64_MAX UINT64_MAX
+
+// 7.18.2.3 Limits of fastest minimum-width integer types
+#define INT_FAST8_MIN INT8_MIN
+#define INT_FAST8_MAX INT8_MAX
+#define INT_FAST16_MIN INT16_MIN
+#define INT_FAST16_MAX INT16_MAX
+#define INT_FAST32_MIN INT32_MIN
+#define INT_FAST32_MAX INT32_MAX
+#define INT_FAST64_MIN INT64_MIN
+#define INT_FAST64_MAX INT64_MAX
+#define UINT_FAST8_MAX UINT8_MAX
+#define UINT_FAST16_MAX UINT16_MAX
+#define UINT_FAST32_MAX UINT32_MAX
+#define UINT_FAST64_MAX UINT64_MAX
+
+// 7.18.2.4 Limits of integer types capable of holding object pointers
+#ifdef _WIN64 // [
+# define INTPTR_MIN INT64_MIN
+# define INTPTR_MAX INT64_MAX
+# define UINTPTR_MAX UINT64_MAX
+#else // _WIN64 ][
+# define INTPTR_MIN INT32_MIN
+# define INTPTR_MAX INT32_MAX
+# define UINTPTR_MAX UINT32_MAX
+#endif // _WIN64 ]
+
+// 7.18.2.5 Limits of greatest-width integer types
+#define INTMAX_MIN INT64_MIN
+#define INTMAX_MAX INT64_MAX
+#define UINTMAX_MAX UINT64_MAX
+
+// 7.18.3 Limits of other integer types
+
+#ifdef _WIN64 // [
+# define PTRDIFF_MIN _I64_MIN
+# define PTRDIFF_MAX _I64_MAX
+#else // _WIN64 ][
+# define PTRDIFF_MIN _I32_MIN
+# define PTRDIFF_MAX _I32_MAX
+#endif // _WIN64 ]
+
+#define SIG_ATOMIC_MIN INT_MIN
+#define SIG_ATOMIC_MAX INT_MAX
+
+#ifndef SIZE_MAX // [
+# ifdef _WIN64 // [
+# define SIZE_MAX _UI64_MAX
+# else // _WIN64 ][
+# define SIZE_MAX _UI32_MAX
+# endif // _WIN64 ]
+#endif // SIZE_MAX ]
+
+// WCHAR_MIN and WCHAR_MAX are also defined in <wchar.h>
+#ifndef WCHAR_MIN // [
+# define WCHAR_MIN 0
+#endif // WCHAR_MIN ]
+#ifndef WCHAR_MAX // [
+# define WCHAR_MAX _UI16_MAX
+#endif // WCHAR_MAX ]
+
+#define WINT_MIN 0
+#define WINT_MAX _UI16_MAX
+
+#endif // __STDC_LIMIT_MACROS ]
+
+
+// 7.18.4 Limits of other integer types
+
+#if !defined(__cplusplus) || defined(__STDC_CONSTANT_MACROS) // [ See footnote 224 at page 260
+
+// 7.18.4.1 Macros for minimum-width integer constants
+
+#define INT8_C(val) val##i8
+#define INT16_C(val) val##i16
+#define INT32_C(val) val##i32
+#define INT64_C(val) val##i64
+
+#define UINT8_C(val) val##ui8
+#define UINT16_C(val) val##ui16
+#define UINT32_C(val) val##ui32
+#define UINT64_C(val) val##ui64
+
+// 7.18.4.2 Macros for greatest-width integer constants
+#define INTMAX_C INT64_C
+#define UINTMAX_C UINT64_C
+
+#endif // __STDC_CONSTANT_MACROS ]
+
+
+#endif // _MSC_STDINT_H_ ]
projects / francis / stp.git / commitdiff