vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157

#!/usr/bin/python
"""
Will run two vampires in parallel and compare their output.
Attempts to change the memory alignment of the second vampire by
creating a lot of environment variables (this should make stack 
start from a different place in memory).

Command line:
[-p] [-a alternative_executable] executable arg1 ...

default alternative_executable is the same as executable

Runs in parallel
executable arg1 ...
alternative_executable arg1 ...
and prints out a message when their outputs start to differ.

"-p" will cause the outputs to be printed out even if they do not 
differ.

This script is particularly useful in combination with the "-tr"
options of Vampire which enable tracing outputs. For example,
"-tr sa" prints out details of all newly generated, processed, 
activated and simplified clauses. List of all possible arguments
to the "-tr" option can be obtained by running "-tr help".

"""

import sys
import platform
import subprocess
import re
import time
import tempfile
import os
import math

vampCmdLine = None
printTraces = False
altExecutable = None
errFollowUpLines = 5

def readArgs(args):
    global vampCmdLine
    global printTraces
    global altExecutable
    
    while True:
        if args[0]=="-p":
            printTraces = True
            args = args[1:]
        if args[0]=="-a":
            altExecutable = args[1]
            args = args[2:]
        else:
            break
    vampCmdLine = args
    
class Finished(Exception):
    def __init__(self, msg):
        self.msg = msg

readArgs(sys.argv[1:])

def createVampProc(isSecond):
    global vampCmdLine
    global altExecutable
    
    childEnv = os.environ
    cmdLine = list(vampCmdLine)
    if isSecond:
        #we try to make the second Vampire behave differently, so we put some large stuff 
        #into the system environment, which could change the memory alignment a bit
        childEnv = dict(childEnv)
        s = "a"
        for i in range(0,12):
            s = s+s
        childEnv["abcd"] = s
        #we also use the alternative executable if it was supplied
        if altExecutable:
            cmdLine[0] = altExecutable
    try:
        return subprocess.Popen(cmdLine, bufsize=1, stderr=subprocess.PIPE, env=childEnv)
    except OSError:
        print "Command line giving error:"
        print cmdLine
        raise 

def trimEOL(str):
    if str[-1]=="\n":
        return str[:-1]
    else:
        return str

def printFollowUp(hdr, firstLine, proc):
    global errFollowUpLines
    
    print "%s: %s" % (hdr, trimEOL(firstLine))
    for i in range(0,errFollowUpLines):
        ln = proc.stderr.readline()
        if not ln:
            print "%s terminated" % hdr
            break
        print "%s: %s" % (hdr, trimEOL(ln))


vp1 = createVampProc(False)
vp2 = createVampProc(True)

try:
    while True:
        ln1 = vp1.stderr.readline()
        ln2 = vp2.stderr.readline()
        
        if ln1==ln2:
            if not ln1:
                raise Finished("Both vampires terminated")

            if printTraces:
                print trimEOL(ln1)

            continue
        if not ln1:
            raise Finished("First vampire terminated")
        if not ln2:
            raise Finished("Second vampire terminated")
        
        if ln2[0:len(ln1)]==ln1 and vp1.poll():
            print "v1: %s" % trimEOL(ln1)
            print "v2: %s" % trimEOL(ln2)
            raise Finished("First vampire terminated in the middle of a line")
        if ln1[0:len(ln2)]==ln2 and vp2.poll():
            print "v1: %s" % trimEOL(ln1)
            print "v2: %s" % trimEOL(ln2)
            raise Finished("Second vampire terminated in the middle of a line")

        
        print "Vampire outputs differ:"
        print
        print "v1: %s" % trimEOL(ln1)
        print "v2: %s" % trimEOL(ln2)
        
        if errFollowUpLines:
            print
            printFollowUp("v1", ln1, vp1)
            print
            printFollowUp("v2", ln2, vp2)
        print
        raise Finished("Non-determinism detected")
except Finished as e:
    print e.msg
finally:
    if vp1.poll()==None:
        vp1.kill()
    if vp2.poll()==None:
        vp2.kill()