Commit 077fb951 authored by Julien Girard-Satabin's avatar Julien Girard-Satabin
Browse files

added QF LRA substitution

parent ffcb1947
......@@ -80,9 +80,12 @@ at the root of the project.
Output will be saved under `/path/to/file.smt2`.
Change the target theory with option `-theory`.
For instance, to target
QF_LRA theory, type
QF_NRA theory, type
`dune exec -- bin/converter.exe /path/to/file.onnx -theory QF_NRA`.
Supported theories are QF_NRA, QF_LRA and QF_FP.
For QF_LRA, you will need to pass an additional script on the resulting
SMTLIB2 file `substition_QF_LRA.py`; else the solvers will not be able
to parse correctly the resulting files.
### Tests:
* To run unit tests, type `dune runtest` at root of project.
......
import sys
def substitution(smt):
fp = open(smt, 'r')
to_subst = {}
lines = []
to_write = []
for line in fp:
lines.append(line)
if '/' in line:
if not ('(<' or '(>') in line:
k = line.split(' ')[2]
if line.split(' ')[-3] == '(-':
v = line.split(' ')[-4:]
else:
v = line.split(' ')[-3:]
if k=='0':
pass # print("line=", line)
else:
to_subst[k] = v
keys = to_subst.keys()
for elt in lines:
split = elt.split(' ')
if 'assert' and len(split) == 4:
k = split[2]
v = split[3]
if v.rstrip()[:-2] in keys:
to_subst[k] = to_subst[v.rstrip()[:-2]]
for key in keys:
if key and 'assert' in elt:
elt = elt.replace(key, ' '.join(to_subst[key]).rstrip()[:-2])
to_write.append(elt)
of = open(smt, 'w')
for x in to_write:
of.write(x)
if __name__ == '__main__':
substitution(sys.argv[1])
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment