Merge pull request #30 from nbulsi/stochastic

Stochastic
nbulsi · Nov 10, 2020 · 42a4f15 · 42a4f15
2 parents a4cc494 + 40a80c4
commit 42a4f15
Show file tree

Hide file tree

Showing 9 changed files with 1,455 additions and 262 deletions.
diff --git a/src/commands/exact_m3ig.hpp b/src/commands/exact_m3ig.hpp
@@ -51,73 +51,6 @@ namespace alice
       int num_steps = 1;
       float error_rate = 0.1;
 
-      std::string print_expr( const also::mig3& mig3, const int& step_idx )
-      {
-        std::stringstream ss;
-        std::vector<char> inputs;
-
-        for( auto i = 0; i < 3; i++ )
-        {
-          if( mig3.steps[step_idx][i] == 0 )
-          {
-            inputs.push_back( '0' );
-          }
-          else
-          {
-            inputs.push_back( char( 'a' + mig3.steps[step_idx][i] - 1 ) );
-          }
-        }
-
-        switch( mig3.operators[ step_idx ] )
-        {
-          default:
-            assert( false && "illegal operator id" );
-            break;
-
-          case 0:
-            ss << "<" << inputs[0] << inputs[1] << inputs[2] << "> "; 
-            break;
-
-          case 1:
-            ss << "<!" << inputs[0] << inputs[1] << inputs[2] << "> "; 
-            break;
-
-          case 2:
-            ss << "<" << inputs[0] << "!" << inputs[1] << inputs[2] << "> "; 
-            break;
-
-          case 3:
-            ss << "<" << inputs[0] << inputs[1] << "!" << inputs[2] << "> "; 
-            break;
-        }
-
-        return ss.str();
-      }
-
-      std::string print_all_expr( const spec& spec, const also::mig3& mig3 )
-      {
-        std::stringstream ss;
-
-        char pol = spec.out_inv ? '!' : ' ';
-
-        std::cout << "[i] " << spec.nr_steps << " steps are required " << std::endl;
-        for(auto i = 0; i < spec.nr_steps; i++ )
-        {
-          if(  i == spec.nr_steps - 1 ) 
-          {
-            ss << pol;
-            ss << char( i + spec.nr_in + 'a' ) << "=" << print_expr( mig3, i ); 
-          }
-          else
-          {
-            ss << char( i + spec.nr_in + 'a' ) << "=" << print_expr( mig3, i ); 
-          }
-        }
-
-        std::cout << "[expressions] " << ss.str() << std::endl;
-        return ss.str();
-      }
-
       void enumerate_m3ig( const kitty::dynamic_truth_table& tt )
       {
         bsat_wrapper solver;
@@ -174,7 +107,6 @@ namespace alice
           spec[0] = copy;
         }
 
-
         stopwatch<>::duration time{0};
         if( is_set( "cegar" ) )
         {

diff --git a/src/commands/stochastic.hpp b/src/commands/stochastic.hpp
@@ -37,12 +37,13 @@ namespace alice
         if( myfile.is_open() )
         {
           unsigned line_index = 0u;
+          vector.clear();
 
           while( std::getline( myfile, line ) )
           {
             if( line_index == 0u ) { num_vars = std::stoi( line ); } 
-            if( line_index == 1u ) { n = std::stoi( line ); } 
-            if( line_index == 2u ) { m = std::stoi( line ); } 
+            if( line_index == 1u ) { m = std::stoi( line ); } 
+            if( line_index == 2u ) { n = std::stoi( line ); } 
 
             if( line_index == 3u ) 
             {
@@ -63,19 +64,19 @@ namespace alice
 
           if( is_set( "verbose" ) )
           {
-            std::cout << " num_vars : " << num_vars << "\n" 
-                      << " n        : " << n << "\n"
-                      << " m        : " << m << std::endl;
+            std::cout << "[i] num_vars : " << num_vars << "\n" 
+                      << "[i] m        : " << m << "\n" 
+                      << "[i] n        : " << n << "\n";
 
-            std::cout << "Problem vector: ";
+            std::cout << "[i] Problem vector: ";
             for( auto const& e : vector )
             {
               std::cout << e << " ";
             }
             std::cout << std::endl;
           }
 
-          stochastic_synthesis( num_vars, n, m, vector );
+          stochastic_synthesis( num_vars, m, n, vector );
         }
         else
         {