#!/bin/bash
if [ "$EUID" -ne 0 ]
  then echo "Please run as root"
  exit
fi

export MYNAME=`id 1000 | awk '{print $1}' | sed 's/.*(\(.*\))/\1/'`
export MYHOME=/home/$MYNAME

runuser $MYNAME --preserve-environment -c '
cd /home/$MYNAME
mkdir hdl_tools
cd hdl_tools

git clone https://github.com/cliffordwolf/yosys.git
git clone https://github.com/YosysHQ/SymbiYosys.git sby
git clone https://github.com/SRI-CSL/yices2.git
git clone https://github.com/Z3Prover/z3.git
'
cd /home/$MYNAME/hdl_tools/yosys
make config-clang
make -j$(nproc)
make install

cd ../sby
make install

cd ../yices2
autoconf
./configure
make -j$(nproc)
make install

cd ../z3
python scripts/mk_make.py
cd build
make -j$(nproc)
make install

#cd ../../
#hg clone https://bitbucket.org/sterin/super_prove_build
#cd super_prove_build
#patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
#--- a/MetaSat/MiniSat2/System.cc	Thu Sep 14 01:44:08 2017 -0700
#+++ b/MetaSat/MiniSat2/System.cc	Thu May 14 20:10:24 2020 +0000
#@@ -20,6 +20,7 @@
# 
# #include <signal.h>
# #include <stdio.h>
#+#include <stdlib.h>
# 
# #include "System.hh"
# 
#@@ -27,7 +28,6 @@
# 
# #if defined(__linux__)
# 
#-#include <stdlib.h>
# 
# static inline int memReadStat(int field)
# {
#")
#patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
#--- a/Bip/Main_bip.cc	Thu Sep 14 01:44:08 2017 -0700
#+++ b/Bip/Main_bip.cc	Thu May 14 20:08:52 2020 +0000
#@@ -508,8 +508,8 @@
# void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
# {
#     Vec<Pair<int,GLit> > ffs, pis;
#-    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
#-    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
#+    For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w));
#+    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI  (w).number, w));
#     sort(ffs);
#     sort(pis);                             
# 
#")
#mkdir build && cd build
#cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
#ninja
#ninja package
#SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
#tar xvf $SPBIN -C /usr/local/bin/
#cat << "EOF" > /usr/local/bin/suprove
##!/bin/bash
#tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
#exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
#EOF
#chmod +x /usr/local/bin/suprove
#suprove