smt2: emit smtlib2_comb_expr outputs after all inputs

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index aa865e7fa66be9e30af4f963098f7f8d6fbcfbf0..7481e0510559dabfe6282f26c55aed0ca9b7ef8e 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -927,6 +927,7 @@ struct Smt2Worker
                        }
 
                std::string smtlib2_inputs;
+               std::vector<std::string> smtlib2_decls;
                if (is_smtlib2_module) {
                        for (auto wire : module->wires()) {
                                if (!wire->port_input)
@@ -968,11 +969,12 @@ struct Smt2Worker
                                                log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
                                                          log_id(module), log_id(wire));
                                }
+                               auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
                                if (bvmode && GetSize(sig) > 1) {
                                        std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bv(sig);
                                        if (!comments.empty())
-                                               decls.insert(decls.end(), comments.begin(), comments.end());
-                                       decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
+                                               out_decls.insert(out_decls.end(), comments.begin(), comments.end());
+                                       out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
                                                        get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
                                        if (wire->port_input)
                                                ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -983,16 +985,16 @@ struct Smt2Worker
                                                sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
                                        }
                                        if (!comments.empty())
-                                               decls.insert(decls.end(), comments.begin(), comments.end());
+                                               out_decls.insert(out_decls.end(), comments.begin(), comments.end());
                                        for (int i = 0; i < GetSize(sig); i++) {
                                                if (GetSize(sig) > 1) {
-                                                       decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
+                                                       out_decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
                                                                        get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
                                                        if (wire->port_input)
                                                                ex_input_eq.push_back(stringf("  (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
                                                                                get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
                                                } else {
-                                                       decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
+                                                       out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
                                                                        get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
                                                        if (wire->port_input)
                                                                ex_input_eq.push_back(stringf("  (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -1003,6 +1005,8 @@ struct Smt2Worker
                        }
                }
 
+               decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end());
+
                if (verbose) log("=> export logic associated with the initial state\n");
 
                vector<string> init_list;

diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2
index bb869c08a5bf504dd1b3e1292debb5d35833672f..ace858ca8a70496f5cca996704e9dfaf96be5749 100644 (file)
--- a/tests/various/smtlib2_module-expected.smt2
+++ b/tests/various/smtlib2_module-expected.smt2
@@ -5,6 +5,9 @@
 (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
 ; yosys-smt2-input a 8
 (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
+(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
+; yosys-smt2-input b 8
+(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
 ; yosys-smt2-output add 8
 (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
 (|a| (|smtlib2_n a| state))
@@ -12,9 +15,6 @@
 )
 (bvadd a b)
 ))
-(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
-; yosys-smt2-input b 8
-(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
 ; yosys-smt2-output eq 1
 (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
 (|a| (|smtlib2_n a| state))
@@ -64,10 +64,10 @@
   (|uut_a 2| state)
   (|smtlib2_a| (|uut_h s| state))
 ))
-(define-fun |uut_u| ((state |uut_s|)) Bool 
+(define-fun |uut_u| ((state |uut_s|)) Bool
   (|smtlib2_u| (|uut_h s| state))
 )
-(define-fun |uut_i| ((state |uut_s|)) Bool 
+(define-fun |uut_i| ((state |uut_s|)) Bool
   (|smtlib2_i| (|uut_h s| state))
 )
 (define-fun |uut_h| ((state |uut_s|)) Bool (and

diff --git a/tests/various/smtlib2_module.sh b/tests/various/smtlib2_module.sh
index 9b2f24f9f81ef73a4f60dc3703ee264944810a23..491f6514877805692c91110ede6af6a02ed8939e 100755 (executable)
--- a/tests/various/smtlib2_module.sh
+++ b/tests/various/smtlib2_module.sh
@@ -1,5 +1,5 @@
 #!/bin/bash
 set -ex
 ../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
-sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
+sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/  *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
 diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2