#!/bin/bash

# This program links main problem in $1 with its propagator in $2 as
# well as the propagator's reason generator in $3. To do so, the names
# of predicate symbols in the main program are matched against the
# names of propagator's symbols and reason generator's symbols. The
# propagator's defining line is then generated according to such info.
# Finally, the propagator's defining line plus its CNF representation
# is added to the CNF representation of the main problem.

function extract_symbols {
	grep $1 $3 | sed "s/^c \([0-9][0-9]*\) $1\(.*\)/$2\2 \1/" | LC_ALL=C sort >$4
}

function generate_translation_table {
	tmp1=`mktemp`
	tmp2=`mktemp`
	extract_symbols $1 $1 $3 $tmp1
	extract_symbols $2 $1 $4 $tmp2

	LC_ALL=C join $tmp1 $tmp2 | sed "s/.* \([0-9][0-9]*\) \([0-9][0-9]*\)/\1 \2/"
	rm $tmp1 $tmp2
}

function populate_translation_table {
	for (( pop_ctr=0; pop_ctr < ${#table[@]}; pop_ctr+=2 ))
	do
		next=$(( pop_ctr + 1 ))
		key=${table[$pop_ctr]}
		value=${table[$next]}
		tr_table[$key]=$value
	done
}

function print_translated_literal {
	if [ $1 -lt 0 ]; then
		key=$(( 0 - $1))
		printf "%s" "-${tr_table[$key]}"
	else
		printf "%s" "${tr_table[$1]}"
	fi
}

function usage {
	>&2 echo "link.sh: links a propagator's CNF representation to a problem's CNF."
	>&2 echo "Usage: ./link.sh <M-cnf> <P-cnf> <R-cnf> <sym-tr> [--incomplete]"
	>&2 echo "    <M-cnf>      : main problem's CNF representation"
	>&2 echo "    <P-cnf>      : propagator's CNF representation"
	>&2 echo "    <R-cnf>      : reason's CNF representation (links propagator to the main"
	>&2 echo "                   problem). can be an empty file in case of automatic reason"
	>&2 echo "                    generation"
	>&2 echo "    <sym-tr>     : list of symbol translations between CNFs as below"
	>&2 echo "      -u <sym1> <sym2> : propagator's symbol <sym2> takes the upperbound value of"
	>&2 echo "                         main problem's symbol <sym1>"
	>&2 echo "      -l <sym1> <sym2> : propagator's symbol <sym2> takes the lowerbound value of"
	>&2 echo "                         main problem's symbol <sym1>"
	>&2 echo "      -rm <sym>        : the reason shares symbol <sym> with the main problem"
	>&2 echo "      -rp <sym>        : the reason shares symbol <sym> with the propagator"
	>&2 echo "    --incomplete : indicate that P-cnf is not a complete representation of the"
	>&2 echo "                   propagator. default is being complete."

	exit -1
}

if [[ $# -lt 3 ]]; then
	usage
fi

upperboundSymPs=( )
upperboundSymMs=( )
lowerboundSymPs=( )
lowerboundSymMs=( )
reasonSymPs=( )
reasonSymMs=( )

main_file=$1
prop_file=$2
reason_file=$3
complete_prop_cnf=1

shift 3

while [[ $# -gt 0 ]]
do
	case $1 in
		"-u")
			if [[ $# -lt 3 ]]; then
				usage
			fi
			upperboundSymMs=( ${upperboundSymMs[@]} $2 )
			upperboundSymPs=( ${upperboundSymPs[@]} $3 )
			shift 2
			;;
		"-l")
			if [[ $# -lt 3 ]]; then
				usage
			fi
			lowerboundSymMs=( ${lowerboundSymMs[@]} $2 )
			lowerboundSymPs=( ${lowerboundSymPs[@]} $3 )
			shift 2
			;;
		"-rm")
			if [[ $# -lt 2 ]]; then
				usage
			fi
			reasonSymMs=( ${reasonSymMs[@]} $2 )
			shift
			;;
		"-rp")
			if [[ $# -lt 2 ]]; then
				usage
			fi
			reasonSymPs=( ${reasonSymPs[@]} $2 )
			shift
			;;
		"--incomplete")
			complete_prop_cnf=0
			;;
		*)
			usage
			;;
	esac
	shift
done

cat $main_file | sed -n "/^\(-\)\{0,1\}[1-9][0-9]*\( \(-\)\{0,1\}[1-9][0-9]*\)* 0$/d;/.*/p"

prop_var_count=$(cat $prop_file | sed "s/^p cnf \([0-9][0-9]*\) .*/p\1/;/^[^p].*/d;s/p//")

printf "c propagator %d %d " $prop_var_count $complete_prop_cnf

table=( )
for (( i=0; i < ${#upperboundSymMs[@]} ; i++ ))
do
	table=( ${table[@]} $(generate_translation_table ${upperboundSymMs[$i]} ${upperboundSymPs[$i]} $main_file $prop_file) )
done

table_len=${#table[@]}
printf "%d " $(( table_len / 2 ))
for (( i=0; i < table_len; i++))
do
	printf "%d " ${table[$i]}
done

table=( )
for (( i=0; i < ${#lowerboundSymMs[@]} ; i++ ))
do
	table=( ${table[@]} $(generate_translation_table ${lowerboundSymMs[$i]} ${lowerboundSymPs[$i]} $main_file $prop_file) )
done

table_len=${#table[@]}
printf "%d " $(( table_len / 2 ))
for (( i=0; i < table_len; i++))
do
	printf "%d " ${table[$i]}
done

for (( i=0; i < ${#reasonSymMs[@]} ; i++ ))
do
	table=( $(generate_translation_table ${reasonSymMs[$i]} ${reasonSymMs[$i]} $reason_file $main_file) )
	populate_translation_table
done

for (( i=0; i < ${#reasonSymPs[@]} ; i++ ))
do
	table=( $(generate_translation_table ${reasonSymPs[$i]} ${reasonSymPs[$i]} $reason_file $prop_file) )
	populate_translation_table
done

temp_file_name=`mktemp`
cat $reason_file | sed "/^c /d" | sed "/^p /d" | sed "/^[0-9][0-9]* 0/d" >$temp_file_name
line_num=$(cat $temp_file_name | wc | sed -e "s/^\s\{1,\}\([0-9]\{1,\}\)\s.*/\1/")
printf "%d " $line_num

while read line
do
	sep_line=( $line )
	print_translated_literal ${sep_line[0]}
	printf " %d " $((${#sep_line[@]} - 2))
	for (( i=1; i < ${#sep_line[@]} - 1; i++ ))
	do
		print_translated_literal ${sep_line[$i]}
		printf " "
	done
done <$temp_file_name
rm $temp_file_name

printf "\n"

cat $prop_file | sed "/^c [0-9][0-9]* /d" | sed "/^p /d"
echo "c endpropagator"

cat $main_file | sed -n "/^\(-\)\{0,1\}[1-9][0-9]*\( \(-\)\{0,1\}[1-9][0-9]*\)* 0$/p"