package require Expect

# disable Expect logging
log_user 0

# include configuration file
source abctclconfig.tcl


# lock variable
# all implemented commands set it to 1 when communicating with ABC - in this
# state all other commands called from other processes (especially in GUI) are
# refused to communicate with ABC
# variable is set to 0 when communication completed
set abcBusy 0



# executes ABC program, waits for first prompt
# resultArrayName is optional and contains fields:
#     spawn_id    [int]    id returned from 'spawn'
#     rawOutput   [string] first ABC's output including prompt
#     success     [int]    return
#           1 program successfully executed, prompt catched - Everything went ok.
#           0 error during program execution
#           -1 ABC executable or ABC directory does not exist
#           -2 - no prompt, timeout
#           -3 - no prompt, eof
proc abcInit { { resultArrayName {}} } {
	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}
	global abcDir abcExe
	global spawn_id

	set res(success) 0
	set res(rawOutput) null
	set res(spawn_id) null

	# test wheather $abcDir is directory
	if {[file isdirectory $abcDir] == 0} {
		# directory does not exist
		set res(success) -1
		return $res(success)
	}

	cd $abcDir

	# test wheather $abcExe file exists
	if {[file exists $abcExe] == 0} {
		# file does not exist
		set res(success) -1
		return $res(success)
	}

	# program execution
	set res(spawn_id) [spawn $abcExe]

	if {$res(spawn_id) == 0} {
		# error during execution
		set res(success) 0
		return $res(success)
	} else {
		# process successfully spawned - waiting for first prompt
		# 1 prompt ok, -2   timeout, -3   eof
		set res(success) [expectPrompt expectResult]
		set res(rawOutput) $expectResult(buffer)

		return $res(success)
	}
}





# kills ABC process, closes communication channel
proc abcDone {} {
	# alias for send
	exp_send "quit\r"
	close
}






# send command to ABC and wait for prompt
# resultArrayName optional return parameter - an array which contains following
# fields (key, value)
# keys:   contains 'null' when no prompt catched:
#         rawOutput     [string]   whole ABC's output including prompt
#         promptNumber  [int]      prompt number
#
#         success       [int]      return value
#                                    1    prompt succesfully catched
#                                    -2   timeout
#                                    -3   eof
#                                    -4   ABC busy
proc abcAnyCommand {command {resultArrayName {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(rawOutput) null
	set res(promptNumber) null
	set res(success) -2

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send "$command\r"

	expectPrompt expectResult

	set abcBusy 0

	if {$expectResult(success) == 1} {
		set res(rawOutput) $expectResult(buffer)
		set res(promptNumber) $expectResult(promptNumber)
		set res(success) 1
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectResult(success)
	}

	return $res(success)
}






# tool for testing ABC commands
# send command to ABC, wait for output and print it, print elapsed time
proc abcTestCommand {command} {
	global abcBusy

	if {$abcBusy == 1} {
		puts "ABC busy"
		return
	}
	set abcBusy 1

	exp_send $command
	exp_send "\r"

	puts -nonewline "'$command' sent, waiting for output ... "

	set timeStart [clock clicks -milliseconds]
	expectPrompt res
	set timeStop [clock clicks -milliseconds]

	set abcBusy 0

	if {$res(success) == 1} {
		puts "ok"
		puts "time elapsed: [expr {$timeStop - $timeStart}]ms"
		parray res
	} else {
		puts "error while expecting prompt"
		parray res
	}
}





# expects prompt as output from ABC, waits for only first occurence, prompt looks
# like this: 'abc 123> '
# waits maximal 'timeout' seconds - set in settings file
# no. of bytes returned in buffer is maximaly expect_buffer_size - set in settings file
# return: resultArrayName:success
# resultArrayName is optional return parameter - array of pairs (key, value):
#         success       [int]      1    prompt succesfully catched
#                                  -2   timeout
#                                  -3   eof
#         contains 'null' on non-success:
#         buffer        [string]   whole ABC's output including prompt
#         promptNumber  [int]      prompt number
proc expectPrompt { {resultArrayName {}} } {
	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	global expect_buffer_size

	set res(success) -2
	set res(buffer) null
	set res(promptNumber) null

	match_max $expect_buffer_size

	expect {
		-re {abc ([0-9]+)> } {
			# prompt succesfully catched
			set res(success) 1
			set res(buffer) $expect_out(buffer)
			set res(promptNumber) $expect_out(1,string)
		}
		eof {
			set res(success) -3
		}
		timeout {
			set res(success) -2
		}
	}

	return $res(success)
}














# send print_stats command to ABC
# resultArrayName optional return parameter - an array which contains following
# fields (key, value)
# keys:   contains 'null' when value was not recognized:
#         i           [int]
#         o           [int]
#         a           [int]
#         lat         [int]
#         lev         [int]
#         edge        [int]
#         net         [int]
#         nd          [int]
#         wbox        [int]
#         bbox        [int]
#         choice      [int]
#         exor        [int]
#         mux         [int]
#         pure_and    [int]
#         and         [int]
#         cube        [int]
#         aig         [int]
#         lit_fac     [int]
#         area        [double]
#         delay       [double]
#         power       [double]
#         glitch      [double]
#         rawOutput   [string]
# 
#         success     [int]
#           1 - prompt ok, output recognized - Everything (or at least something) went ok.
#           3 - prompt ok, error "Empty network." recognized
#           -1 - prompt ok, output not recognized - output in raw form returned
#           -2 - no prompt, timeout
#           -3 - no prompt, eof
#           -4 - ABC busy
# paramsString - optional string containing parameters for print_stats command,
# string is passed onto print_stats 'as is'
# return: same as keys:success
# abc90813_source\src\base\abci\abcPrint.c
proc abc_print_stats { {resultArrayName {}}  {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}
	set res(success) -2

	set res(i) null
	set res(o) null
	set res(a) null
	set res(lat) null
	set res(lev) null
	set res(edge) null
	set res(net) null
	set res(nd) null
	set res(wbox) null
	set res(bbox) null
	set res(choice) null
	set res(exor) null
	set res(mux) null
	set res(pure_and) null
	set res(and) null
	set res(cube) null
	set res(aig) null
	set res(lit_fac) null
	set res(area) null
	set res(delay) null
	set res(power) null
	set res(glitch) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_stats %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		# parse output - apply series of regular expressions to output string
		set regexpRes [regexp -- {[[:blank:]]+(i)/(o) =[[:blank:]]*([0-9]+)/[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1 v2 v3 v4]
		if {$regexpRes} {
			set res($v1) $v3
			set res($v2) $v4
			set res(success) 1
		}

		set regexpRes [regexp -- {[[:blank:]]+(i)/(o)/(a) =[[:blank:]]*([0-9]+)/[[:blank:]]*([0-9]+)/[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1 v2 v3 v4 v5 v6]
		if {$regexpRes} {
			set res($v1) $v4
			set res($v2) $v5
			set res($v3) $v6
			set res(success) 1
		}
		set regexpRes [regexp -- {[[:blank:]]+(lat) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}
		set regexpRes [regexp -- {[[:blank:]]+(lev) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}
		set regexpRes [regexp -- {[[:blank:]]+(edge) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}


		if { [regexp -- {[[:blank:]]+(net) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {[[:blank:]]+(nd) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {[[:blank:]]+(wbox) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {[[:blank:]]+(bbox) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}

		if { [regexp -- {\((choice) =[[:blank:]]*([0-9]+)\)} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {\((exor) =[[:blank:]]*([0-9]+)\)} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {\((mux) =[[:blank:]]*([0-9]+)\)} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {\(pure and =[[:blank:]]*([0-9]+)\)} $expectRes(buffer) match v1] } {
			set res(pure_and) $v1
			set res(success) 1
		}

		set regexpRes [regexp -- {[[:blank:]]+(and) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}

		set regexpRes [regexp -- {[[:blank:]]+(cube) =[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {[[:blank:]]+lit\(fac\) =[[:blank:]]*([0-9]+)[[:blank:]]+} $expectRes(buffer) match v1] } {
			set res(lit_fac) $v1
			set res(success) 1
		}

		set regexpRes [regexp -- {[[:blank:]]+(aig)[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2]
		if {$regexpRes} {
			set res($v1) $v2
			set res(success) 1
		}

		if { [regexp -- {[[:blank:]]+(bdd)[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]*} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}

		if { [regexp -- {[[:blank:]]*(area) =[[:blank:]]*([0-9]+.[0-9]+)[[:blank:]]} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}
		if { [regexp -- {[[:blank:]]*(delay) =[[:blank:]]*([0-9]+.[0-9]+)[[:blank:]]} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}

		if { [regexp -- {[[:blank:]]*(power) =[[:blank:]]*([0-9]+.[0-9]+)[[:blank:]]} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}

		if { [regexp -- {[[:blank:]]*(glitch) =[[:blank:]]*([0-9]+.[0-9]+)[[:blank:]]} $expectRes(buffer) match v1 v2] } {
			set res($v1) $v2
			set res(success) 1
		}


		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}





# executes ABC's 'print_latch' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       total_latches    [int]
#       init0            [int]
#       init1            [int]
#       initDC           [int]
#       const_data       [int]
#       rawOutput        [string]
#
#       success          [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_latch command,
# string is passed onto print_latch 'as is'
# return: same as keys:success
proc abc_print_latch { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}
	set res(success) -2
	set res(total_latches) null
	set res(init0) null
	set res(init1) null
	set res(initDC) null
	set res(const_data) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_latch %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Total latches =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_latches) $v1
			set res(success) 1
		}
		if {[regexp -- {Init0 =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(init0) $v1
			set res(success) 1
		}
		if {[regexp -- {Init1 =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(init1) $v1
			set res(success) 1
		}
		if {[regexp -- {InitDC =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(initDC) $v1
			set res(success) 1
		}
		if {[regexp -- {Const data =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(const_data) $v1
			set res(success) 1
		}

		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}





# executes ABC's 'print_auto' command
# parses only cumulative statistics, ToDo: parse Output-Input-AutoK table
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       ins        [int]
#       inMax      [int]
#       outs       [int]
#       auto       [int]
#       sumK       [int]
#       kMax       [int]
#       supp       [int]
#       time       [float]
#       rawOutput  [string]
#
#       success    [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_auto command,
# string is passed onto print_auto 'as is'
# return: same as keys:success
proc abc_print_auto { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2

	set res(ins) null
	set res(inMax) null
	set res(outs) null
	set res(auto) null
	set res(sumK) null
	set res(kMax) null
	set res(supp) null
	set res(time) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_auto %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Ins=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(ins) $v1
			set res(success) 1
		}
		if {[regexp -- {InMax=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(inMax) $v1
			set res(success) 1
		}
		if {[regexp -- {Outs=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(outs) $v1
			set res(success) 1
		}
		if {[regexp -- {Auto=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(auto) $v1
			set res(success) 1
		}
		if {[regexp -- {SumK=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(sumK) $v1
			set res(success) 1
		}
		if {[regexp -- {KMax=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(kMax) $v1
			set res(success) 1
		}
		if {[regexp -- {Supp=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(supp) $v1
			set res(success) 1
		}
		if {[regexp -- {Time=[[:blank:]]*([0-9]+.[0-9]+)} $expectRes(buffer) match v1]} {
			set res(time) $v1
			set res(success) 1
		}
		

		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}
	
	return $res(success)
}






# executes ABC's 'print_fanio' command
# parses only fanins/fanouts statistics, ToDo: parse Nodes table
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       fanins_max   [int]
#       fanins_ave   [float]
#       fanouts_max  [int]
#       fanouts_ave  [float]
#       rawOutput    [string]
#
#       success      [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_fanio command,
# string is passed onto print_fanio 'as is'
# return: same as keys:success
proc abc_print_fanio { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2

	set res(fanins_max) null
	set res(fanins_ave) null
	set res(fanouts_max) null
	set res(fanouts_ave) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_fanio %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Fanins: Max = ([0-9]+). Ave = ([0-9]*.[0-9]*).  Fanouts: Max = ([0-9]+). Ave =  ([0-9]*.[0-9]*).} $expectRes(buffer) match v1 v2 v3 v4]} {
			set res(fanins_max) $v1
			set res(fanins_ave) $v2
			set res(fanouts_max) $v3
			set res(fanouts_ave) $v4
			set res(success) 1
		}

		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}
	

	return $res(success)
}





# executes ABC's 'print_gates' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       const             [int]
#       const_percent     [float]
#       buffer            [int]
#       buffer_percent    [float]
#       inverter          [int]
#       inverter_percent  [float]
#       and               [int]
#       and_percent       [float]
#       or                [int]
#       or_percent        [float]
#       other             [int]
#       other_percent     [float]
#       total             [int]
#       total_percent     [float]
#       rawOutput         [string]
#
#       success           [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_gates command,
# string is passed onto print_gates 'as is'
# return: same as keys:success
proc abc_print_gates { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2

	set res(const) null
	set res(const_percent) null
	set res(buffer) null
	set res(buffer_percent) null
	set res(inverter) null
	set res(inverter_percent) null
	set res(and) null
	set res(and_percent) null
	set res(or) null
	set res(or_percent) null
	set res(other) null
	set res(other_percent) null
	set res(total) null
	set res(total_percent) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_gates %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Const[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(const) $v1
			set res(const_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {Buffer[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(buffer) $v1
			set res(buffer_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {Inverter[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(inverter) $v1
			set res(inverter_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {And[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(and) $v1
			set res(and_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {Or[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(or) $v1
			set res(or_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {Other[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(other) $v1
			set res(other_percent) $v2
			set res(success) 1
		}
		if {[regexp -- {TOTAL[[:blank:]]*=[[:blank:]]*([0-9]+)[[:blank:]]+([0-9]+.[0-9]+) %} $expectRes(buffer) match v1 v2]} {
			set res(total) $v1
			set res(total_percent) $v2
			set res(success) 1
		}

		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}






# executes ABC's 'print_symm' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
#
# keys: contains 'null' when value was not recognized:
#       some fields in output have same names - only 6 out of 23 fields were
#       implemented
#       total_func_supps   [int]
#       total_struct_supps [int]
#       total_symm         [int]
#       structural_symm    [int]
#       total_non_sym      [int]
#       total_var_pairs    [int]
#       rawOutput          [string]
#
#       success            [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_symm command,
# string is passed onto print_symm 'as is'
# return: same as keys:success
proc abc_print_symm { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(total_func_supps) null
	set res(total_struct_supps) null
	set res(total_symm) null
	set res(structural_symm) null
	set res(total_non_sym) null
	set res(total_var_pairs) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_symm %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Total func supps[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_func_supps) $v1
			set res(success) 1
		}
		if {[regexp -- {Total struct supps[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_struct_supps) $v1
			set res(success) 1
		}
		if {[regexp -- {Total symm[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_symm) $v1
			set res(success) 1
		}
		if {[regexp -- {Structural symm[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(structural_symm) $v1
			set res(success) 1
		}
		if {[regexp -- {Total non-sym[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_non_sym) $v1
			set res(success) 1
		}
		if {[regexp -- {Total var pairs[[:blank:]]*=[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_var_pairs) $v1
			set res(success) 1
		}

		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}








# executes ABC's 'print_unate' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       shared_BDD_size [int]
#       ins             [int]
#       outs            [int]
#       glob_BDDs       [float]
#       total_supp      [int]
#       total_unate     [int]
#       unateness       [float]
#       total           [float]
#       rawOutput       [string]
#
#       success         [int]
#         1 - prompt ok, output recognized - Everything (or at least something) went ok.
#         3 - prompt ok, error "Empty network." recognized
#         -1 - prompt ok, output not recognized - output in raw form returned
#         -2 - no prompt, timeout
#         -3 - no prompt, eof
#         -4 - ABC busy
# paramsString - optional string containing parameters for print_unate command,
# string is passed onto print_unate 'as is'
# return: same as keys:success
proc abc_print_unate { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2

	set res(shared_BDD_size) null
	set res(ins) null
	set res(outs) null
	set res(glob_BDDs) null
	set res(total_supp) null
	set res(total_unate) null
	set res(unateness) null
	set res(total) null
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "print_unate %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {Shared BDD size =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(shared_BDD_size) $v1
			set res(success) 1
		}
		if {[regexp -- {Ins/Outs =[[:blank:]]*([0-9]+)/[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1 v2]} {
			set res(ins) $v1
			set res(outs) $v2
			set res(success) 1
		}
		if {[regexp -- {Glob BDDs =[[:blank:]]*([0-9]*.[0-9]*)} $expectRes(buffer) match v1]} {
			set res(glob_BDDs) $v1
			set res(success) 1
		}
		if {[regexp -- {Total supp =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_supp) $v1
			set res(success) 1
		}
		if {[regexp -- {Total unate =[[:blank:]]*([0-9]+)} $expectRes(buffer) match v1]} {
			set res(total_unate) $v1
			set res(success) 1
		}
		if {[regexp -- {Unateness =[[:blank:]]*([0-9]*.[0-9]*)} $expectRes(buffer) match v1]} {
			set res(unateness) $v1
			set res(success) 1
		}
		if {[regexp -- {Total[[:blank:]]*=[[:blank:]]*([0-9]*.[0-9]*)} $expectRes(buffer) match v1]} {
			set res(total) $v1
			set res(success) 1
		}
		if {[regexp -- {Empty network} $expectRes(buffer)]} {
			set res(success) 3
		}

		if {$res(success) == -1} {
			set res(rawOutput) $expectRes(buffer)
		}

	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}







# paramsString - optional string containing parameters for read command,
# including filename, string is passed onto read 'as is'
# resultArrayName is an optional parameter, consists of pairs (key, value)
# keys: success    [int] procedure result
#                          1 file successfully read
#                          2 error: "Cannot open input file"
#                          3 error: wrong parameters
#                          4 error: "The generic file reader requires a known file extension"
#                          5 error: "Reading network from file has failed"
#                          -2 timeout
#                          -3 eof
#                          -4 ABC busy
#       rawOutput  [string] ABC's raw output
proc abc_read {{resultArrayName {}}  {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) 1
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "read %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) 1

		set regexpRes [regexp -- {Cannot open input file} $expectRes(buffer)]
		if {$regexpRes} {
			set res(success) 2
		}
		set regexpRes [regexp -- {usage: read} $expectRes(buffer)]
		if {$regexpRes} {
			set res(success) 3
		}
		set regexpRes [regexp -- {The generic file reader requires a known file extension} $expectRes(buffer)]
		if {$regexpRes} {
			set res(success) 4
		}
		if {[regexp -- {Reading network from file has failed} $expectRes(buffer)]} {
			set res(success) 5
		}

		set res(rawOutput) $expectRes(buffer)
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}







# tests given string and sets output values according to its content
# called from within: abc_sec, abc_cec, abc_dsec, abc_dprove
# parameters: buffer    [string]    string to test
# return:               [int]       0 not equivalent
#                                   1 equivalent
#                                   2 undecided
#                                   3 error "Empty network."
#                                   -1 no pattern recognized
proc checkEquivalence {buffer} {
	set result -1

	if {[regexp -nocase -- {equivalent} $buffer]} {
		set result 1
	}

	if {[regexp -nocase -- {not equivalent} $buffer]} {		
		set result 0
	}

	if {[regexp -nocase -- {undecided} $buffer]} {
		set result 2
	}

	if {[regexp -nocase -- {Empty (?:current |)network} $buffer]} {
		set result 3
	}

	return $result
}






# executes ABC's 'sec' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success [int]   procedure result
#           when ABC's output successfully recognized:
#             0 not equivalent
#             1 equivalent
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for sec command,
# string is passed onto sec 'as is'
proc abc_sec { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "sec %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkEquivalence $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}







# executes ABC's 'cec' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success [int]   procedure result
#           when ABC's output successfully recognized:
#             0 not equivalent
#             1 equivalent
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for cec command,
# string is passed onto cec 'as is'
proc abc_cec { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "cec %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkEquivalence $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}







# executes ABC's 'dsec' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success         [int]   procedure result
#           when ABC's output successfully recognized:
#             0 not equivalent
#             1 equivalent
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for dsec command,
# string is passed onto dsec 'as is'
proc abc_dsec { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "dsec %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkEquivalence $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}






# executes ABC's 'dprove' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success         [int]   procedure result
#           when ABC's output successfully recognized:
#             0 not equivalent
#             1 equivalent
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for dprove command,
# string is passed onto dprove 'as is'
proc abc_dprove { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "dprove %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkEquivalence $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}








# tests given string and sets output values according to its content
# called from within: abc_iprove, abc_prove, abc_sat
# parameters: buffer    [string]    string to test
# return:               [int]       0 unsatisfiable
#                                   1 satisfiable
#                                   2 undecided
#                                   3 error "Empty network."
#                                   -1 no pattern recognized
proc checkSatisfiability {buffer} {
	set result -1

	if {[regexp -nocase -- {satisfiable} $buffer]} {
		set result 1
	}

	if {[regexp -nocase -- {unsatisfiable} $buffer]} {		
		set result 0
	}

	if {[regexp -nocase -- {undecided} $buffer]} {
		set result 2
	}

	if {[regexp -nocase -- {Empty (?:current |)network} $buffer]} {
		set result 3
	}

	return $result
}







# executes ABC's 'iprove' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success         [int]   procedure result
#           when ABC's output successfully recognized:
#             0 unsatisfiable
#             1 satisfiable
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for iprove command,
# string is passed onto iprove 'as is'
proc abc_iprove { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "iprove %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkSatisfiability $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}






# executes ABC's 'prove' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success         [int]   procedure result
#           when ABC's output successfully recognized:
#             0 unsatisfiable
#             1 satisfiable
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for prove command,
# string is passed onto prove 'as is'
proc abc_prove { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "prove %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkSatisfiability $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}







# executes ABC's 'sat' command
# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: success         [int]   procedure result
#           when ABC's output successfully recognized:
#             0 unsatisfiable
#             1 satisfiable
#             2 undecided
#             3 error "Empty network."
#           when error occured:
#             -1 - prompt ok, output not recognized - output in raw form returned
#             -2 - no prompt, timeout
#             -3 - no prompt, eof
#             -4 - ABC busy
#       rawOutput       [string]
# paramsString - optional string containing parameters for sat command,
# string is passed onto sat 'as is'
proc abc_sat { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "sat %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) [checkSatisfiability $expectRes(buffer)]
		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}








# resultArrayName is an optional parameter, consists of pairs (key, value):
# keys: contains 'null' when value was not recognized:
#       elapse     [float]
#       total      [float]
#       rawOutput  [string]
#       success    [int]
#          1 - prompt ok, output recognized - Everything (or at least something) went ok.
#          -1 - prompt ok, output not recognized - output in raw form returned
#          -2 - no prompt, timeout
#          -3 - no prompt, eof
#          -4 - ABC busy
# paramsString - optional string containing parameters for time command,
# string is passed onto time 'as is'
# procedure return: same as keys:success
proc abc_time { {resultArrayName {}} {paramsString {}} } {
	global abcBusy

	if {$resultArrayName != {}} {
		upvar $resultArrayName res
	}

	set res(success) -2
	set res(rawOutput) null
	set res(elapse) null
	set res(total) null

	if {$abcBusy == 1} {
		set res(success) -4
		return $res(success)
	}
	set abcBusy 1

	exp_send [format "time %s\r" $paramsString]
	expectPrompt expectRes

	set abcBusy 0

	if {$expectRes(success) == 1} {
		set res(success) -1

		if {[regexp -- {(elapse):[[:blank:]]*([0-9]+.[0-9]+)} $expectRes(buffer) match v1 v2]} {
			set res($v1) $v2
			set res(success) 1
		}
		if {[regexp -- {(total):[[:blank:]]*([0-9]+.[0-9]+)} $expectRes(buffer) match v1 v2]} {
			set res($v1) $v2
			set res(success) 1
		}

		if {$res(success) == -1} {
			# return raw output when nothing recognized
			set res(rawOutput) $expectRes(buffer)
		}
	} else {
		# -2 = timeout, -3 = eof
		set res(success) $expectRes(success)
	}

	return $res(success)
}






