updated main.rkt to support selective generation of rosette's output-…

[cknizek]

…smt feature from the commandline

(PR in response to @gussmith23's issue)

What this change does:

This change modifies main.rkt to support the command line flag --output-smt-path "path". The specified path will be used as the output to Rosette's output-smt feature.

The path you specify will become a folder, as there may be many SMT output files generated and placed in the selected path.

How this change does it:

It adds a new parameter, output-smt-path (initially set to #f) to main.rkt.

If output-smt-path becomes no longer equal to #f (i.e. it has been assigned in the commandline arguments to become something), the SMT output feature of Rosette will be activated. The output will be directed to the path specified.

How to use this change (see line 2 of the below code block):

// RUN: racket $LAKEROAD_DIR/bin/main.rkt \
// RUN:  --output-smt-path "example_test_using_include_smt_output_test" \
// RUN:  --solver bitwuzla \
// RUN:  --verilog-module-filepath %s \
// RUN:  --architecture xilinx-ultrascale-plus \
// RUN:  --template dsp \
// RUN:  --out-format verilog \
// RUN:  --top-module-name top \
// RUN:  --verilog-module-out-signal out:11 \
// RUN:  --pipeline-depth 1 \
// RUN:  --clock-name clk \
// RUN:  --module-name out \
// RUN:  --input-signal a:11 \
// RUN:  --input-signal b:11 \
// RUN:  --input-signal c:11 \
// RUN:  --input-signal d:11 \
// RUN:  --extra-cycles 3 \
// RUN:  --timeout 120 \
// RUN: | FileCheck %s

[gussmith23]

Wonderful!!!! Great initiative on adding this!!!

[gussmith23]

This path actually refers to the directory where the files will be placed, not the file

[cknizek]

Oops yeah you're right, I'll change the line to reflect this

[gussmith23]

See this thread, still unresolved

[gussmith23]

Looks like you accidentally deleted main.rkt...

[cknizek]

Looks like you accidentally deleted main.rkt...

Dang, thanks for checking this... I think this somehow happened when I was trying to pipe the raco fmt bin/main.rkt output directly into bin/main.rkt.

I think the issue should be resolved now

[cknizek]

I have re-added main.rkt. I think this PR should be good to go

[gussmith23]

Again, this is a directory, not a file. Please change the docstring here.

[gussmith23]

When CI goes through, go ahead and merge!