added conflicts and degrees_of_variables to instance db entries

.gitmodules

@@ -6,6 +6,7 @@
 [submodule "contrib/iniParser/inih"]
 	path = contrib/iniParser/inih
 	url = https://github.com/benhoyt/inih.git
+
 [submodule "contrib/mongoc/mongo-c-driver"]
 	path = contrib/mongoc/mongo-c-driver
 	url = https://github.com/mongodb/mongo-c-driver.git

generateRandomKsatDataSet_db.py

@@ -23,13 +23,52 @@ def __generateExperiment(args, dbContext):
                                            args["variables"],
                                            args["variablesPerClause"])
         
-        instanceId = dbContext["instances"].insert_one(sat.writeJSONLike()).inserted_id
+        
+        instanceId = dbContext["instances"].insert_one(__packDocument(sat)).inserted_id
         
         experimentScope["instances"].append(instanceId)
 
     dbContext["experimentScopes"].insert_one(experimentScope)
 
+def __packDocument(instance):
+    doc = instance.writeJSONLike();
     
+    doc["degrees_of_variables"] = __packDegreesOfVariables(instance)
+    
+    doc["conflicts"] = __packConflicts(instance)
+    
+    return doc
+
+def __packDegreesOfVariables(instance):
+    doc = []
+    
+    for var, degree in instance.getDegreesOfVariables().items():
+        doc.append({"var": var, "deg": degree})
+    
+    return doc
+
+def __packConflicts(instance):
+    doc = [{"var": i + 1,
+            "clauses": {
+                "pos_lit": [],
+                "neg_lit": []}} for i in range(instance.getNumberOfVariables())]
+    
+    for conflict in instance.getConflicts():
+        
+        for binding in conflict:
+            clause = binding[0]
+            lit = binding[1]
+            varIndex = abs(lit) - 1
+            
+            if lit > 0:
+                if clause not in doc[varIndex]["clauses"]["pos_lit"]:
+                    doc[varIndex]["clauses"]["pos_lit"].append(clause)
+            else:
+                if clause not in doc[varIndex]["clauses"]["neg_lit"]:
+                    doc[varIndex]["clauses"]["neg_lit"].append(clause)
+                
+    
+    return doc
 
 def __prepareExperimentScope(args):
     experimentScope = {}

src/runMinisat.cpp

@@ -41,9 +41,6 @@ int main(int argc, char** argv)
 	{
         satlab::MinisatSolver solver(satlab::types::convert<satlab::KSATinstance>(doc));
         
-        bool modelFound = solver.solve();
-        
-        
         auto result = satlab::convert<bsoncxx::builder::stream::document>(
                         solver.getResult()
                       );

src/util/bson2ksatClauseConverter.h

@@ -11,30 +11,6 @@
 
 namespace satlab
 {
-/*
-using BSON2KSATCLAUSE_CONVERTER = Converter<KSATinstance::CLAUSE,
-                                            bsoncxx::array::element>;
-                                            
-template<>
-class Converter<KSATinstance::CLAUSE, bsoncxx::array::element>
-{
-public:
-    KSATinstance::CLAUSE convert(const bsoncxx::array::element& docView);
-};
-
-KSATinstance::CLAUSE
-BSON2KSATCLAUSE_CONVERTER::convert(const bsoncxx::array::element& docView)
-{
-    KSATinstance::CLAUSE clause;
-    
-    for(auto lit : static_cast<bsoncxx::array::view>(docView.get_array()))
-    {
-        clause.push_back(lit.get_int32());
-    }
-    
-    return clause;
-}
-*/
 
 namespace types
 {

src/util/bson2ksatConverter.h

@@ -35,34 +35,6 @@ KSATinstance convert(const bsoncxx::document::view& docView)
 }
 
 }
-/*
-using BSON2KSAT_CONVERTER = Converter<KSATinstance, bsoncxx::document::view>;
-
-template<>
-class Converter<KSATinstance, bsoncxx::document::view>
-{
-public:
-    KSATinstance convert(const bsoncxx::document::view& docView);
-    
-private:
-    BSON2KSATCLAUSE_CONVERTER clauseConverter;
-};
-
-KSATinstance BSON2KSAT_CONVERTER::convert(const bsoncxx::document::view& docView)
-{
-    KSATinstance ksat;
-    
-    bsoncxx::array::view clauses = docView["clauses"].get_array();
-    
-    for(auto clause : clauses)
-    {
-        ksat.addClause(clauseConverter.convert(clause));
-    }
-    
-    
-    return ksat;
-}
-*/
 
 }
 

src/util/convert.h

@@ -3,14 +3,6 @@
 
 namespace satlab
 {
-/*
-template<typename TARGET_T, typename SOURCE_T>
-class Converter
-{
-public:
-    TARGET_T convert(const SOURCE_T& source);
-};
-*/
 
 namespace types
 {