#!/usr/bin/env python3

# Boolector: Satisfiablity Modulo Theories (SMT) solver.
#
# Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
#
# This file is part of Boolector.
# See COPYING for more information on using this software.
#
import argparse
import os
import subprocess
import sys

def check(expected, out, err, output_dir):
    out = out.decode()
    err = err.decode()
    if err:
        try:
            pos = err.index('log/')
            err = err[pos:]
        except ValueError:
            pass
    cmp = '{}{}'.format(out, err)
    if expected.strip() != cmp.strip():
        print("Expected:\n{}".format(expected.encode()), file=sys.stderr)
        print('-' * 80, file=sys.stderr)
        outfile_name = os.path.join(output_dir, 'expected.log')
        print("see {}".format(outfile_name), file=sys.stderr)
        print('-' * 80, file=sys.stderr)
        outfile = open(outfile_name, 'w')
        outfile.write(expected)
        outfile.close()
        print('=' * 80, file=sys.stderr)
        print("Got:\n{}".format(cmp.encode()), file=sys.stderr)
        print('-' * 80, file=sys.stderr)
        outfile_name = os.path.join(output_dir, 'got.log')
        print("see {}".format(outfile_name), file=sys.stderr)
        print('-' * 80, file=sys.stderr)
        outfile = open(outfile_name, 'w')
        outfile.write(cmp)
        outfile.close()
        sys.exit(1)


def main():
    #print(sys.argv)
    ap = argparse.ArgumentParser()
    ap.add_argument('binary')
    ap.add_argument('testcase')
    ap.add_argument('output_dir')
    ap.add_argument('--check-sat', action='store_true', default=False)
    ap.add_argument('--check-unsat', action='store_true', default=False)
    ap.add_argument('--check-output', action='store_true', default=False)
    args = ap.parse_args()

    btor_args = args.testcase.split()
    cmd_args = [args.binary]
    cmd_args.extend(btor_args)

    testname, _ = os.path.splitext(btor_args[0])
    outfilename = '{}.out'.format(testname)
    #print(outfilename)
    #print(btor_args)

    print("Running test case '{}'".format(' '.join(cmd_args)))

    proc = subprocess.Popen(cmd_args,
                            stdin=subprocess.PIPE,
                            stdout=subprocess.PIPE,
                            stderr=subprocess.PIPE)

    out, err = proc.communicate()

    expected = None
    if args.check_sat:
        expected = 'sat'
    elif args.check_unsat:
        expected = 'unsat'
    else:
        assert args.check_output
        with open(outfilename, 'r') as outfile:
            expected = outfile.read()
    check(expected, out, err, args.output_dir)


if __name__ == '__main__':
    main()