#!/bin/sh
# the next line restarts using tclsh \
exec tclsh "$0" "$@"

# cat on the depths file

exec echo cvar_levels >> [lindex $argv 0]
exec cat smv.cnfdepths >> [lindex $argv 0]

set f [open "|sat56 [lindex $argv 0]" "r"]
set outfile [open [lindex $argv 1] "w"]

while {![eof $f]} {
    gets $f l
    if {[string match *solution=* $l]} {
	puts $outfile 1
	set sol [string range $l [expr [string first = $l] + 1] end]
	set lc [string length $sol]
	set c 0
	while {$c < $lc} {
	    if {! [string index $sol $c] } {
		puts $outfile [expr $c + 1]
	    }
	    incr c
	}
    } else {
	puts $l
	if {[string match "*: tautology*" $l]} {
	    puts $outfile 0
	}
    }
}

close $f
close $outfile
