Add export/import Assignment features for debugging (#586)

src/configuration/OptionParser.cpp

@@ -43,7 +43,7 @@ void OptionParser::initialize()
     _positional.add_options()
         ( "input",
           boost::program_options::value<std::string>( &(*_stringOptions)[Options::INPUT_FILE_PATH] )->default_value( (*_stringOptions)[Options::INPUT_FILE_PATH] ),
-          "Neural netowrk file." )
+          "Neural network file." )
         ( "property",
           boost::program_options::value<std::string>( &(*_stringOptions)[Options::PROPERTY_FILE_PATH] )->default_value( (*_stringOptions)[Options::PROPERTY_FILE_PATH] ),
           "Property file." )
@@ -94,6 +94,18 @@ void OptionParser::initialize()
         ( "summary-file",
           boost::program_options::value<std::string>( &((*_stringOptions)[Options::SUMMARY_FILE]) )->default_value( (*_stringOptions)[Options::SUMMARY_FILE] ),
           "Produce a summary file of the run." )
+        ( "export-assignment",
+          boost::program_options::bool_switch( &((*_boolOptions)[Options::EXPORT_ASSIGNMENT]) )->default_value( (*_boolOptions)[Options::EXPORT_ASSIGNMENT] ),
+          "Export a satisfying assignment if found." )
+        ( "export-assignment-file",
+          boost::program_options::value<std::string>( &(*_stringOptions)[Options::EXPORT_ASSIGNMENT_FILE_PATH] )->default_value( (*_stringOptions)[Options::EXPORT_ASSIGNMENT_FILE_PATH] ),
+          "Specifies a file to export the assignment." )
+        ( "debug-assignment",
+          boost::program_options::bool_switch( &((*_boolOptions)[Options::DEBUG_ASSIGNMENT]) )->default_value( (*_boolOptions)[Options::DEBUG_ASSIGNMENT] ),
+          "Import an assignment for debugging." )
+        ( "debug-assignment-file",
+          boost::program_options::value<std::string>( &(*_stringOptions)[Options::EXPORT_ASSIGNMENT_FILE_PATH] )->default_value( (*_stringOptions)[Options::EXPORT_ASSIGNMENT_FILE_PATH] ),
+          "Specifies a file to import the assignment for debugging." )
 #ifdef ENABLE_GUROBI
 #endif // ENABLE_GUROBI
         ;

src/configuration/Options.cpp

@@ -49,6 +49,8 @@ void Options::initializeDefaultValues()
     _boolOptions[SOLVE_WITH_MILP] = false;
     _boolOptions[PERFORM_LP_TIGHTENING_AFTER_SPLIT] = false;
     _boolOptions[NO_PARALLEL_DEEPSOI] = false;
+    _boolOptions[EXPORT_ASSIGNMENT] = false;
+    _boolOptions[DEBUG_ASSIGNMENT] = false;
 
     /*
       Int options
@@ -86,6 +88,8 @@ void Options::initializeDefaultValues()
     _stringOptions[SYMBOLIC_BOUND_TIGHTENING_TYPE] = "deeppoly";
     _stringOptions[MILP_SOLVER_BOUND_TIGHTENING_TYPE] = "none";
     _stringOptions[QUERY_DUMP_FILE] = "";
+    _stringOptions[IMPORT_ASSIGNMENT_FILE_PATH] = "assignment.txt";
+    _stringOptions[EXPORT_ASSIGNMENT_FILE_PATH] = "assignment.txt";
     _stringOptions[SOI_SEARCH_STRATEGY] = "mcmc";
     _stringOptions[SOI_INITIALIZATION_STRATEGY] = "input-assignment";
     _stringOptions[LP_SOLVER] = gurobiEnabled() ? "gurobi" : "native";

src/configuration/Options.h

@@ -64,6 +64,12 @@ class Options
         // with a different random seed on each thread. The problem is solved once
         // any of the thread finishes.
         NO_PARALLEL_DEEPSOI,
+
+        // Export SAT assignment into a file, use EXPORT_ASSIGNMENT_FILE to specify the file (default: assignment.txt)
+        EXPORT_ASSIGNMENT,
+
+        // Import assignment for debugging purposes, use IMPORT_ASSIGNMENT_FILE to specify the file (default: assignment.txt)
+        DEBUG_ASSIGNMENT,
     };
 
     enum IntOptions {
@@ -90,7 +96,7 @@ class Options
 
         // The random seed used throughout the execution.
         SEED,
-      
+
         // The number of threads to use for OpenBLAS matrix multiplication.
         NUM_BLAS_THREADS,
     };
@@ -119,6 +125,8 @@ class Options
         SYMBOLIC_BOUND_TIGHTENING_TYPE,
         MILP_SOLVER_BOUND_TIGHTENING_TYPE,
         QUERY_DUMP_FILE,
+        EXPORT_ASSIGNMENT_FILE_PATH,
+        IMPORT_ASSIGNMENT_FILE_PATH,
 
         // The strategy used for soi minimization
         SOI_SEARCH_STRATEGY,
@@ -127,6 +135,7 @@ class Options
 
         // The procedure/solver for solving the LP
         LP_SOLVER,
+
     };
 
     /*

src/engine/Marabou.cpp

@@ -15,6 +15,7 @@
  **/
 
 #include "AcasParser.h"
+#include "AutoFile.h"
 #include "GlobalConfiguration.h"
 #include "File.h"
 #include "MStringf.h"
@@ -54,6 +55,9 @@ void Marabou::run()
 
     unsigned long long totalElapsed = TimeUtils::timePassed( start, end );
     displayResults( totalElapsed );
+
+    if( Options::get()->getBool( Options::EXPORT_ASSIGNMENT ) )
+        exportAssignment();
 }
 
 void Marabou::prepareInputQuery()
@@ -107,6 +111,9 @@ void Marabou::prepareInputQuery()
         printf( "\n" );
     }
 
+    if ( Options::get()->getBool( Options::DEBUG_ASSIGNMENT ) )
+        importDebuggingSolution();
+
     String queryDumpFilePath = Options::get()->getString( Options::QUERY_DUMP_FILE );
     if ( queryDumpFilePath.length() > 0 )
     {
@@ -116,6 +123,60 @@ void Marabou::prepareInputQuery()
     }
 }
 
+void Marabou::importDebuggingSolution()
+{
+    String fileName=  Options::get()->getString( Options::IMPORT_ASSIGNMENT_FILE_PATH );
+    AutoFile input( fileName );
+
+    if ( !IFile::exists( fileName ) )
+    {
+        throw MarabouError( MarabouError::FILE_DOES_NOT_EXIST, Stringf( "File %s not found.\n", fileName.ascii() ).ascii() );
+    }
+
+    input->open( IFile::MODE_READ );
+
+    unsigned numVars = atoi( input->readLine().trim().ascii() );
+    ASSERT( numVars == _inputQuery.getNumberOfVariables() );
+
+    unsigned var;
+    double value;
+    String line;
+
+    // Import each assignment
+    for ( unsigned i = 0;  i < numVars; ++i )
+    {
+        line = input->readLine();
+        List<String> tokens = line.tokenize( "," );
+        auto it = tokens.begin();
+        var = atoi( it->ascii() );
+        ASSERT( var == i );
+        it++;
+        value = atof( it->ascii() );
+        it++;
+        ASSERT( it == tokens.end() );
+        _inputQuery.storeDebuggingSolution( var, value);
+    }
+
+    input->close();
+}
+
+void Marabou::exportAssignment() const
+{
+    String assignmentFileName = "assignment.txt";
+    AutoFile exportFile( assignmentFileName );
+    exportFile->open( IFile::MODE_WRITE_TRUNCATE );
+
+    unsigned numberOfVariables = _inputQuery.getNumberOfVariables();
+    // Number of Variables
+    exportFile->write( Stringf( "%u\n", numberOfVariables ) );
+
+    // Export each assignment
+    for ( unsigned var = 0;  var < numberOfVariables; ++var )
+        exportFile->write( Stringf( "%u, %f\n", var, _inputQuery.getSolutionValue( var ) ) );
+
+    exportFile->close();
+}
+
 void Marabou::solveQuery()
 {
     if ( _engine.processInputQuery( _inputQuery ) )

src/engine/Marabou.h

@@ -51,6 +51,16 @@ class Marabou
     */
     void displayResults( unsigned long long microSecondsElapsed ) const;
 
+    /*
+      Export assignment as per Options
+     */
+    void exportAssignment() const;
+
+    /*
+      Import assignment for debugging as per Options
+     */
+    void importDebuggingSolution();
+
     /*
       ACAS network parser
     */