smtlib_solve.py

#!/usr/bin/env python2
from pysmt.shortcuts import Solver
from six.moves import cStringIO
from pysmt.smtlib.parser import SmtLibParser
from pysmt.smtlib.script import evaluate_command

from IPython import embed
import sys
import time

solvers_logic = {
        'bdd': [
        'QF_BOOL', 'BOOL'
        ],
        'msat': [
        'QF_ABV', 'QF_AUFBV*', 'QF_RDL', 'QF_AX', 'QF_UFIDL', 'QF_LRA',
        'QF_ALIA', 'QF_AUFBV', 'QF_BOOL', 'QF_UFLIRA', 'QF_UFLRA', 'QF_AX*',
        'QF_LIA', 'QF_AUFBVLIRA*', 'QF_ABV*', 'QF_BV', 'QF_IDL', 'QF_AUFBVLIRA',
        'QF_ALIA*', 'QF_UF', 'QF_UFBV', 'QF_AUFLIA*', 'QF_UFLIA', 'QF_AUFLIA'
        ],
        'yices': [
        'QF_LIA', 'QF_UFIDL', 'QF_LRA', 'QF_UFLRA', 'QF_UFBV', 'QF_BOOL',
        'QF_RDL', 'QF_BV', 'QF_IDL', 'QF_UFLIRA', 'QF_UF', 'QF_UFLIA'
        ],
        'cvc4': [
        'LIA', 'QF_AUFLIA', 'QF_RDL', 'QF_AX', 'QF_UFIDL', 'QF_LRA',
        'QF_ALIA', 'QF_AUFBV', 'QF_BOOL', 'QF_UFLIRA', 'QF_UF', 'QF_UFLIA',
        'QF_LIA', 'QF_BV', 'QF_IDL', 'QF_AUFBVLIRA', 'LRA', 'QF_UFLRA',
        'QF_UFBV', 'UFLRA', 'QF_ABV', 'BOOL', 'UFLIRA'
        ],
        'picosat': [
        'QF_BOOL'
        ],
        'btor': [
        'QF_BV', 'QF_UFBV', 'QF_ABV', 'QF_AUFBV', 'QF_AX'
        ],
        'z3': [
        'QF_LIA', 'LIA', 'QF_AUFBV*', 'QF_AUFLIA*', 'QF_AUFBVLIRA*',
        'QF_ABV*', 'QF_AUFLIA', 'QF_BV', 'QF_IDL', 'QF_RDL', 'QF_AX', 'QF_ALIA*',
        'LRA', 'QF_UFBV', 'QF_UFIDL', 'QF_LRA', 'QF_UF', 'QF_ALIA', 'QF_AX*',
        'QF_NIA', 'QF_NRA', 'UFLRA', 'QF_ABV', 'QF_AUFBV', 'QF_AUFBVLIRA',
        'QF_BOOL', 'BOOL', 'QF_UFLIRA', 'QF_UFLRA', 'QF_UFLIA', 'UFLIRA'
        ]
}

def main():
        if len(sys.argv) != 3:
                print 'Usage: python2 {} [file] [solver]'.format(sys.argv[0])
                exit()
        filename = sys.argv[1]
        solvername = sys.argv[2]
        prefix = '({} {}):'.format(filename, solvername)
        print prefix, 'Starting:', filename, ', with solver:', solvername

        f = open(filename, 'r')
        DEMO_SMTLIB = f.read()
        f.close()
        parser = SmtLibParser()
        start = time.time()
        script = parser.get_script(cStringIO(DEMO_SMTLIB))
        end = time.time()
        print prefix, 'Parsing file takes:', end-start, 'sec'

        logic = str(script.filter_by_command_name('set-logic').next().args[0])

        if logic not in solvers_logic[solvername]:
                print prefix, logic, 'not supported by', solvername, '\n'
                exit()

        try:
                push = script.filter_by_command_name('push').next()
        except:
                pass
        else:
                if solvername == 'btor':
                        print prefix, 'push/pop not supported by btor\n'
                        exit()

        print prefix, 'Using logic:', logic

        #t = 0
        #embed()
        start = time.time()
        with Solver(name=solvername, logic=logic) as solver:
                log = script.evaluate(solver)
                #embed()
                '''
                log = []
                start = time.time()
                for cmd in script.commands:
                        r = evaluate_command(cmd, solver)
                        if cmd.name == 'check-sat':
                                if r:
                                        #print '  sat:', time.time()-start
                                        pass
                                else:
                                        #print 'unsat:', time.time()-start
                                        pass
                                t += time.time()-start
                                start = time.time()
                                #embed()
                        log.append((cmd.name, r))
                '''
        end = time.time()

        print prefix, 'Solving takes:', end-start, 'sec\n'

if __name__ == '__main__':
        main()