#!/bin/sh
#
# Script to use paradox/equinox
#
# Stéphane Lens
# Janvier 2010
# Logiques pour l'intelligence artificielle
# Université de Liège
# Institut Montefiore
#
###############################################################################
#
# Copyright (C) 2010 Stéphane Lens.
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License, version 2, as
# published by the Free Software Foundation.
#
# This program 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.
#
###############################################################################

# Equinox timeout
timeout=10


# dirname
dir=$(dirname $0)



# TODO line change work only with sat !!! (find smth else)
# Function to check if there was errors when running paradox or equinox
# $1 = output of paradox/equinox
# $2 = input file of paradox/equinox
# $3 = paradox / equinox
function check_errors()
{
  if grep -q ERROR $1
  then
    if grep -q PARSE $1
    then
      echo -e "\n*** Parse error !\n"

      # Print the parse error
      # (Modif line number according to the real file provided by user)

      # temporary removed
      #cat $1 | sed -e '/version/d;/PROBLEM/d;/PARSE/d;s/line:/line: LINE/g' \
      #       | perl -pe 's/LINE.*(\d+)/$1 - 1/eg'

      sed -e '/version/d;/PROBLEM/d;/PARSE/d;/line:/d' $1

      echo ""
    else
      echo -e "\n*** Unknown error !\n"
      echo "----------------------------------------"
      echo "'$2' :"
      echo "----------------------------------------"
      cat $2
      echo -e "\n----------------------------------------"
      echo "'$dir/$3 --model $2' :"
      echo "----------------------------------------"
      cat $1
      echo -e "\n----------------------------------------\n"
    fi
    return 1
  fi
  return 0
}



# Find a negative model for the rule
# $1 = input file
function find_neg_model()
{
  # Find a negative model
  $dir/paradox --model $1 > modtmp

  # Check for errors
  check_errors modtmp $1 paradox
  if [ $? == 1 ] # test return value
  then
    rm -Rf modtmp
    return 1
  fi

  # Print the negative model
  if grep -q CounterSatisfiable modtmp
  then
    echo -e "Negative model :\n"
    sed -e '/+++ BEGIN MODEL/,/+++ END MODEL/!d;
            /+++ BEGIN MODEL/d;/+++ END MODEL/d' modtmp
    echo ""
  fi

  rm -Rf modtmp
  return 0
}



# Test satisfaisability of the input formula
# $1 = file for input formula
function test_sat()
{
  echo -e "\nTest satisfaisability of the input formula"

  # Create the file for paradox
  # Replace ',' by '&' for set of formulas
  echo "fof(formula, axiom, (" > tmp.tptp
  sed -e 's/,[ |\t]*$/)\&(/g' $1 >> tmp.tptp
  echo "))." >> tmp.tptp

  # Test formula
  $dir/paradox --model tmp.tptp > tmp1

  # Check for errors
  check_errors tmp1 tmp.tptp paradox
  if [ $? == 1 ] # test return value
  then
    rm -Rf tmp.tptp tmp1
    exit 1
  fi

  # If unsatisfiable print result and exit
  # otherwise we should test the oposite
  if grep -q Unsatisfiable tmp1
  then
    echo -e "\n--> Unsatisfiable\n"
    rm -Rf tmp.tptp tmp1
    exit 0
  fi


  # Create the file for paradox with the oposite formula
  # Replace ',' by '&' for set of formulas
  echo "fof(formula, axiom, ~(" > tmp.tptp
  sed -e 's/,[ |\t]*$/)\&(/g' $1 >> tmp.tptp
  echo "))." >> tmp.tptp

  # Test oposite formula
  $dir/paradox --model tmp.tptp > tmp2

  # Check for errors
  check_errors tmp2 tmp.tptp paradox
  if [ $? == 1 ] # test return value
  then
    rm -Rf tmp.tptp tmp1 tmp2
    exit 1
  fi

  # If the oposite is unsatisfiable the formula is valid
  # otherwise the formula is just satisfiable
  if grep -q Satisfiable tmp1
  then
    if grep -q Satisfiable tmp2
    then
      echo -e "\n--> Satisfiable\n"
      echo "----------------------------------------"
      echo -e "Model :\n"
      sed -e '/+++ BEGIN MODEL/,/+++ END MODEL/!d;
              /+++ BEGIN MODEL/d;/+++ END MODEL/d' tmp1
      echo -e "\n----------------------------------------"
      echo -e "Negative model :\n"
      sed -e '/+++ BEGIN MODEL/,/+++ END MODEL/!d;
              /+++ BEGIN MODEL/d;/+++ END MODEL/d' tmp2
      echo -e "\n----------------------------------------\n"
    elif grep -q Unsatisfiable tmp2
    then
      echo -e "\n--> Valid\n"
    fi
  fi

  rm -Rf tmp.tptp tmp1 tmp2
  return 0
}



# Test the correctness of the input inference rule
# $1 = file for input rule
function test_rule()
{
  echo -e "\nTest if the conclusion is a logical consequence of the premises"

  # Create the file for equinox
  sed -e 's/premise[ |\t]*{/fof(premise, axiom, (/g;
          s/conclusion[ |\t]*{/fof(conclusion, conjecture, (/g;s/}/))./g' $1 \
          > tmp.tptp

  # Test the rule
  $dir/equinox --time $timeout tmp.tptp > tmp

  # Check for errors
  check_errors tmp tmp.tptp equinox
  if [ $? == 1 ] # test return value
  then
    rm -Rf tmp.tptp tmp
    exit 1
  fi

  # If theorem print result and exit
  # otherwise we should test with paradox to have a negative model
  if grep -q Theorem tmp
  then
    echo -e "\n--> Correct\n"
    rm -Rf tmp.tptp tmp
    exit 0
  elif grep -q GaveUp tmp
  then
    echo -e "\n--> Incorrect\n"
  elif grep -q Timeout tmp
  then
    echo -e "\n--> Equinox timeout ($timeout sec)\n"
  fi


  # Find a negative model
  echo "----------------------------------------"
  find_neg_model tmp.tptp
  echo -e "----------------------------------------\n"

  rm -Rf tmp.tptp tmp
}



# Compare set of formulas
# $1 = file for input formulas
function cmp_formulas()
{
  echo -e "\nCompare set of formulas\n"

  # Get hypothesis
  sed -e 's/}/\n}/' $1 |
  sed -e '/hyp[ |\t]*{/,/}/!d' |
  sed -e 's/hyp[ |\t]*{/fof(hyp, axiom, (/g;s/}/))./g' |
  sed -e 's/|=/=>/g;s/=|/<=/g;s/<->/<=>/g' > tmp_hyp.tptp

  # Get the number of formulas
  nb_form=$(grep -c '^formula\[' $1)

  # Put names and formulas to a tab
  for i in `seq 1 $nb_form`;
  do
    name[$i]=$(grep '^formula\[' $1 |
               sed -e "$i!d;s/[ |\t]*\].*//;s/[ |\t]*formula\[[ |\t]*//")

    form[$i]=$(sed -e 's/}/\n}/' $1 |
               sed -e "/formula\[[ |\t]*${name[$i]}[ |\t]*\][ |\t]*{/,/}/!d" |
               sed -e "/}/d;
                     s/.*formula\[[ |\t]*${name[$i]}[ |\t]*\][ |\t]*{[ |\t]*//")
  done

  # Compare formulas 2 by 2
  for i in `seq 1 $nb_form`;
  do
    for j in `seq $(( i + 1 )) $nb_form`;
    do

      cat tmp_hyp.tptp > tmp1.tptp
      echo "fof(premise, axiom, (" >> tmp1.tptp
      echo ${form[$i]} >> tmp1.tptp
      echo "))." >> tmp1.tptp
      echo "" >> tmp1.tptp
      echo "fof(conclusion, conjecture, (" >> tmp1.tptp
      echo ${form[$j]} >> tmp1.tptp
      echo "))." >> tmp1.tptp


      cat tmp_hyp.tptp > tmp2.tptp
      echo "fof(premise, axiom, (" >> tmp2.tptp
      echo ${form[$j]} >> tmp2.tptp
      echo "))." >> tmp2.tptp
      echo "" >> tmp2.tptp
      echo "fof(conclusion, conjecture, (" >> tmp2.tptp
      echo ${form[$i]} >> tmp2.tptp
      echo "))." >> tmp2.tptp

      # Test the rules
      $dir/equinox --time $timeout tmp1.tptp > tmp1
      if grep -q Timeout tmp1
      then
        echo -e "\n--> Equinox timeout ($timeout sec)\n"
        sed -e "s/Timeout/GaveUp/g;" tmp1
      fi
      $dir/equinox --time $timeout tmp2.tptp > tmp2
      if grep -q Timeout tmp2
      then
        echo -e "\n--> Equinox timeout ($timeout sec)\n"
        sed -e "s/Timeout/GaveUp/g;" tmp2
      fi

      # Check for errors
      check_errors tmp1 tmp1.tptp equinox
      if [ $? == 1 ] # test return value
      then
        rm -Rf tmp_hyp.tptp tmp1.tptp tmp1 tmp2.tptp tmp2
        exit 1
      fi
      check_errors tmp2 tmp2.tptp equinox
      if [ $? == 1 ] # test return value
      then
        rm -Rf tmp_hyp.tptp tmp1.tptp tmp1 tmp2.tptp tmp2
        exit 1
      fi


      if grep -q Theorem tmp1
      then
        # If the 2 rules are correct -> formulas are equivalent
        if grep -q Theorem tmp2
        then
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$i]} <-> ${name[$j]}\n"
        elif grep -q GaveUp tmp2
        then
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$i]} |= ${name[$j]}\n"
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$j]} |/= ${name[$i]}\n"
          find_neg_model tmp2.tptp
        fi
      elif grep -q GaveUp tmp1
      then
        if grep -q Theorem tmp2
        then
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$i]} |/= ${name[$j]}\n"
          find_neg_model tmp1.tptp
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$j]} |= ${name[$i]}\n"
        elif grep -q GaveUp tmp2
        then
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$i]} |/= ${name[$j]}\n"
          find_neg_model tmp1.tptp
          echo -e "----------------------------------------\n"
          echo -e "* ${name[$j]} |/= ${name[$i]}\n"
          find_neg_model tmp2.tptp
        fi
      fi
    done
  done

  echo -e "----------------------------------------\n"

  rm -Rf tmp_hyp.tptp tmp1.tptp tmp1 tmp2.tptp tmp2
}



# Main
# $1 = mode
# $2 = input file
if [ $# == 2 ]
then
  if [ -f $2 ]
  then
    if [ $1 == '-sat' ]
    then
      test_sat $2
    elif [ $1 == '-csq' ]
    then
      test_rule $2
    elif [ $1 == '-cmp' ]
    then
      cmp_formulas $2
    else
      echo "$1: Unknown parameter"
    fi
  else
    echo "$2: No such file or directory"
  fi
else
  echo -e "Usage: $0 mode fileName\n"
  echo "mode :"
  echo -e "\t-sat (Test satisfaisability of the input formula)"
  echo -e "\t-csq (Test if conclusion is a logical consequence of the premises)"
  echo -e "\t-cmp (Compare set of formulas)\n"
fi

