Dev query logger

maraboupy/Marabou.py

@@ -30,3 +30,6 @@ def read_tf(filename, inputName=None, outputName=None, savedModel=False, savedMo
         marabouNetworkTF: (MarabouNetworkTF) representing network
     """
     return MarabouNetworkTF(filename, inputName, outputName, savedModel, savedModelTags)
+
+def load_query(filename, verbose=True):
+    MarabouNetwork.loadQuery(filename, verbose)

maraboupy/MarabouCore.cpp

@@ -112,7 +112,8 @@ PYBIND11_MODULE(MarabouCore, m) {
         .def("getUpperBound", &InputQuery::getUpperBound)
         .def("getLowerBound", &InputQuery::getLowerBound)
         .def("setNumberOfVariables", &InputQuery::setNumberOfVariables)
-        .def("addEquation", &InputQuery::addEquation);
+        .def("addEquation", &InputQuery::addEquation)
+        .def("saveQuery", &InputQuery::saveQuery);
     py::class_<Equation> eq(m, "Equation");
     eq.def(py::init());
     eq.def(py::init<Equation::EquationType>());

maraboupy/MarabouNetwork.py

@@ -177,6 +177,34 @@ def solve(self, filename="", verbose=True):
 
         return [vals, stats]
 
+    def loadQuery(self, filename="", verbose=True):
+        """
+        Function to solve query represented by this network
+        Arguments:
+            filename: (string) path to redirect output to
+            verbose: (bool) whether to print out solution
+        Returns:
+            vals: (dict: int->float) empty if UNSAT, else SATisfying solution
+            stats: (Statistics) a Statistics object as defined in Marabou,
+                    it has multiple methods that provide information related
+                    to how an input query was solved.
+        """
+        #ipq = self.getMarabouQuery()
+        ipq = MarabouCore.loadQuery(filename)
+        vals, stats = MarabouCore.solve(ipq, filename)
+        if verbose:
+            if len(vals)==0:
+                print("UNSAT")
+            else:
+                print("SAT")
+                for i in range(self.inputVars.size):
+                    print("input {} = {}".format(i, vals[self.inputVars.item(i)]))
+
+                for i in range(self.outputVars.size):
+                    print("output {} = {}".format(i, vals[self.outputVars.item(i)]))
+
+        return [vals, stats]
+
     def evaluateWithMarabou(self, inputValues, filename="evaluateWithMarabou.log"):
         """
         Function to evaluate network at a given point using Marabou as solver

src/Makefile

@@ -5,6 +5,7 @@ SUBDIRS += \
 	basis_factorization \
 	engine \
 	input_parsers \
+	query_loader \
 
 include $(ROOT_DIR)/Rules.mk
 

src/common/AutoFile.h

@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file AutoFile.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **/
+
+#ifndef __AutoFile_h__
+#define __AutoFile_h__
+
+#include "IFile.h"
+#include "T/FileFactory.h"
+
+class AutoFile
+{
+public:
+	AutoFile( const String &path )
+	{
+		_file = T::createFile( path );
+	}
+
+	~AutoFile()
+	{
+		T::discardFile( _file );
+		_file = 0;
+	}
+
+	operator IFile &()
+	{
+		return *_file;
+	}
+
+	IFile *operator->()
+	{
+		return _file;
+	}
+
+private:
+	IFile *_file;
+};
+
+#endif // __AutoFile_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/File.cpp

@@ -114,10 +114,11 @@ String File::readLine( char lineSeparatingChar )
 
     while ( !_readLineBuffer.contains( separatorAsString ) )
     {
-        char buffer[SIZE_OF_BUFFER + 1];
+        char *buffer = new char[SIZE_OF_BUFFER + 1];
         int n = T::read( _descriptor, buffer, sizeof(char) * SIZE_OF_BUFFER );
         if ( ( n == -1 ) || ( n == 0 ) )
         {
+            delete[] buffer;
             if ( _readLineBuffer != "" )
             {
                 String result = _readLineBuffer;
@@ -130,6 +131,7 @@ String File::readLine( char lineSeparatingChar )
 
         buffer[n] = 0;
         _readLineBuffer += buffer;
+        delete[] buffer;
     }
 
     String result = _readLineBuffer.substring( 0, _readLineBuffer.find( separatorAsString ) );

src/common/File.h

@@ -16,17 +16,12 @@
 class ConstSimpleData;
 class HeapData;
 
+#include "IFile.h"
 #include "MString.h"
 
-class File
+class File : public IFile
 {
 public:
-    enum Mode {
-        MODE_READ,
-        MODE_WRITE_APPEND,
-        MODE_WRITE_TRUNCATE,
-    };
-
     File( const String &path );
     virtual ~File();
     void close();

src/common/IFile.h

@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file IFile.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Guy Katz
+ ** This file is part of the Marabou project.
+ ** Copyright (c) 2016-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **/
+
+#ifndef __IFile_h__
+#define __IFile_h__
+
+class HeapData;
+class String;
+
+class IFile
+{
+public:
+    enum Mode {
+        MODE_READ,
+        MODE_WRITE_APPEND,
+        MODE_WRITE_TRUNCATE,
+    };
+
+    virtual void open( Mode openMode ) = 0;
+    virtual void write( const String &line ) = 0;
+    virtual String readLine( char lineSeparatingChar = '\n' ) = 0;
+    virtual void read( HeapData &buffer, unsigned maxReadSize ) = 0;
+    virtual void close() = 0;
+
+	virtual ~IFile() {}
+};
+
+#endif // __IFile_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/T/FileFactory.h

@@ -0,0 +1,36 @@
+#ifndef __T__FileFactory_h__
+#define __T__FileFactory_h__
+
+#include "cxxtest/Mock.h"
+
+class IFile;
+class String;
+
+namespace T
+{
+	IFile *createFile( const String &path );
+	void discardFile( IFile *file );
+}
+
+CXXTEST_SUPPLY( createFile,        /* => T::Base_AllocateIrp */
+				IFile *,           /* Return type            */
+				createFile,        /* Name of mock member    */
+				( const String &path ),  /* Prototype              */
+				T::createFile,        /* Name of real function  */
+				( path )       /* Parameter list         */ );
+
+CXXTEST_SUPPLY_VOID( discardFile,        /* => T::Base_AllocateIrp */
+					 discardFile,        /* Name of mock member    */
+					 ( IFile *file ),  /* Prototype              */
+					 T::discardFile,        /* Name of real function  */
+					 ( file )            /* Parameter list         */ );
+
+#endif // __T__FileFactory_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../.. "
+// tags-file-name: "../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/mock/FileFactory.cpp

@@ -0,0 +1,10 @@
+#define CXXTEST_MOCK_TEST_SOURCE_FILE
+#include "T/FileFactory.h"
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/mock/Sources.mk

@@ -0,0 +1,12 @@
+SOURCES += \
+	CommonMock.cpp \
+	Errno.cpp \
+	FileFactory.cpp \
+
+#
+# Local Variables:
+# compile-command: "make -C ../../.. "
+# tags-file-name: "../../../TAGS"
+# c-basic-offset: 4
+# End:
+#

src/common/real/FileFactory.cpp

@@ -0,0 +1,22 @@
+#include "File.h"
+
+namespace T
+{
+	IFile *createFile( const String &path )
+	{
+		return new File( path );
+	}
+
+	void discardFile( IFile *file )
+	{
+		delete file;
+	}
+}
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//

src/common/real/Sources.mk

@@ -1,6 +1,7 @@
 SOURCES += \
 	CommonReal.cpp \
 	Errno.cpp \
+	FileFactory.cpp \
 
 #
 # Local Variables:

src/common/tests/MockFile.h

@@ -0,0 +1,71 @@
+#ifndef __MockFile_h__
+#define __MockFile_h__
+
+#include "HeapData.h"
+#include "IFile.h"
+
+class MockFile : public IFile
+{
+public:
+	MockFile()
+	{
+		wasCreated = false;
+		wasDiscarded = false;
+    }
+
+	bool wasCreated;
+	bool wasDiscarded;
+    String lastPath;
+
+	void mockConstructor( const String &path )
+	{
+		TS_ASSERT( !wasCreated );
+        wasCreated = true;
+
+        lastPath = path;
+	}
+
+    void mockDestructor()
+    {
+        TS_ASSERT( wasCreated );
+        TS_ASSERT( !wasDiscarded );
+
+        wasDiscarded = true;
+    }
+
+    bool openWasCalled;
+    IFile::Mode lastOpenMode;
+
+    void open( Mode mode )
+    {
+        openWasCalled = true;
+        lastOpenMode = mode;
+    }
+
+    void write( const String &/* line */ )
+    {
+    }
+
+    String readLine( char /* lineSeparatingChar */ )
+    {
+        return "";
+    }
+
+    void read( HeapData &/* buffer */, unsigned /* maxReadSize */ )
+    {
+    }
+
+    void close()
+    {
+    }
+};
+
+#endif // __MockFile_h__
+
+//
+// Local Variables:
+// compile-command: "make -C ../../.. "
+// tags-file-name: "../../../TAGS"
+// c-basic-offset: 4
+// End:
+//