#!/bin/sh

#
#  This file is part of the Yices SMT Solver.
#  Copyright (C) 2017 SRI International.
# 
#  Yices is free software: you can redistribute it and/or modify
#  it under the terms of the GNU General Public License as published by
#  the Free Software Foundation, either version 3 of the License, or
#  (at your option) any later version.
# 
#  Yices is distributed in the hope that it will be useful,
#  but WITHOUT ANY WARRANTY; without even the implied warranty of
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
#  GNU General Public License for more details.
# 
#  You should have received a copy of the GNU General Public License
#  along with Yices.  If not, see <http://www.gnu.org/licenses/>.
#

#
# Script to get the GMP version used by yices
#
# Usage:
#   ./gmp-version <dist directory>
#
# - the argument must be the path to the binary or static dist
# - there should be a binary called yices or yices.ext in the bin directory
# - this script call yices --version then extract the GMP version from there
#
# NOTE: test -e xxx ;  is not supported by sh on Solaris
#

usage="Usage: $0 <distribution directory>

   For example

     $0 ./build/x86_64-unknown-linux-gnu-release/dist
"
  
if test $# != 1 ; then
   echo "$usage"
   exit 2
fi

dist=$1

if test ! -d $dist ; then
   echo "Error: $dist is not a directory"
   exit 2
fi

yices=$dist/bin/yices
test -x $yices || yices=$dist/bin/yices.exe

#
# NOTE: we use the awk command { printf "%s", $4 } instead of
# { print $4 } because the latter produces an extra '\n' on cygwin.
#
if test -x $yices ; then
  tmp=` $yices --version | awk '/GMP/ { printf "%s", $4 }'`
   case $tmp in
     *.*.* )
       echo $tmp
       ;;

     * )
       echo "Error: GMP version not found or badly formatted"
       echo $tmp
       exit 2
       ;;
   esac
else 
  echo "Error: can't run $dist/bin/yices"
  exit 2
fi