Support "signed word [N](int)" conversion operator on SMV frontend

Author: augustomafra

frontends/smvparser.y

@@ -1286,15 +1286,19 @@ simple_expr: constant {
                 SMVnode *word = $3;
                 SMVnode::Type word_type = word->getType();
 
-                if(word_type != SMVnode::Signed && word_type != SMVnode::Unsigned){
+                if(word_type != SMVnode::Integer && word_type != SMVnode::Signed && word_type != SMVnode::Unsigned){
                   throw PonoException("Resize word type is uncompatible");
                 }
 
                 int integer = stoi($5);
                 smt::Sort word_sort = word->getTerm()->get_sort();
-                uint64_t word_width = word_sort->get_width();
+                uint64_t word_width = word_type != SMVnode::Integer ? word_sort->get_width() : 0;
 
-                if(integer == word_width){
+                if (word_type == SMVnode::Integer){
+                  smt::Term res = enc.solver_->make_term(smt::Op(smt::Int_To_BV, integer), word->getTerm());
+                  assert(res);
+                  $$ = new SMVnode(res, SMVnode::Signed);                  
+                }else if(integer == word_width){
                   $$ = word;
                 }else if(integer < word_width){
                   smt::Term res;
@@ -1319,7 +1323,21 @@ simple_expr: constant {
               }
             }
             | signed_word sizev "(" basic_expr ")"{
-               throw PonoException("No resize");
+              if(enc.module_flat){
+                SMVnode *expr = $4;
+                SMVnode::Type expr_type = expr->getType();
+                
+                if(expr_type != SMVnode::Integer){
+                  throw PonoException("Signed word conversion type is uncompatible");
+                }
+                assert(expr);
+                smt::Term res = enc.solver_->make_term(smt::Op(smt::Int_To_BV, $2), expr->getTerm());
+                assert(res);
+                $$ = new SMVnode(res, SMVnode::Signed);
+              }else{
+                SMVnode *integer = new constant(std::to_string($2));
+                $$ = new resize_expr($4,integer);
+              }
             }
             | unsigned_word sizev "(" basic_expr ")"{
                throw PonoException("No resize");