summaryrefslogtreecommitdiffstats
path: root/scripts/dprove.sh
diff options
context:
space:
mode:
Diffstat (limited to 'scripts/dprove.sh')
-rw-r--r--scripts/dprove.sh15
1 files changed, 15 insertions, 0 deletions
diff --git a/scripts/dprove.sh b/scripts/dprove.sh
new file mode 100644
index 00000000..4289aad3
--- /dev/null
+++ b/scripts/dprove.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+abc_root()
+{
+ cwd="$(pwd)"
+ cd $(dirname "$1")
+ echo $(dirname "$(pwd)")
+ cd "${cwd}"
+}
+
+abc_dir=$(abc_root "$0")
+bin_dir="${abc_dir}"/bin
+aig_file="$1"
+
+exec ${bin_dir}/abc -c "/rf ${aig_file} ; /pushredirect ; /pushdtemp ; dprove ; /popdtemp ; /popredirect ; /print_aiger_result"