aboutsummaryrefslogtreecommitdiffstats
path: root/scripts
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-13 04:09:24 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-03-13 04:09:24 +0100
commit0e423e645dba8a0f0a48e98a66aee9d53fb3a194 (patch)
tree1259511ef9da402a184d5858e0e23cb8e35dab8b /scripts
parent86aecfee139ed5cd76c38f82f03b7d7264583b79 (diff)
downloadcompcert-kvx-0e423e645dba8a0f0a48e98a66aee9d53fb3a194.tar.gz
compcert-kvx-0e423e645dba8a0f0a48e98a66aee9d53fb3a194.zip
scripts for using Gurobi and Cplex for ILP solving
Diffstat (limited to 'scripts')
-rwxr-xr-xscripts/cplex/ilp_solver4
-rwxr-xr-xscripts/gurobi/ilp_solver (renamed from scripts/ilp_solver)0
2 files changed, 2 insertions, 2 deletions
diff --git a/scripts/cplex/ilp_solver b/scripts/cplex/ilp_solver
index 9a6ff055..a449c203 100755
--- a/scripts/cplex/ilp_solver
+++ b/scripts/cplex/ilp_solver
@@ -1,7 +1,7 @@
#!/bin/sh
tmp=$2.tmp
-rm -f $tmp
+rm -f $tmp $2
cplex -c "read $1" "optimize" "write $tmp sol"
grep '<variable name="' $tmp | sed -e 's@ *<variable name="@@' -e 's@" index=.* value="@ @' -e 's@"/>@@' > $2
touch $2
-
+rm -f $tmp
diff --git a/scripts/ilp_solver b/scripts/gurobi/ilp_solver
index 7a67a942..7a67a942 100755
--- a/scripts/ilp_solver
+++ b/scripts/gurobi/ilp_solver