diff --git a/.gitmodules b/.gitmodules index a36b3c9..a23063c 100644 --- a/.gitmodules +++ b/.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 diff --git a/generateRandomKsatDataSet_db.py b/generateRandomKsatDataSet_db.py index 6aa11e1..b06bb35 100755 --- a/generateRandomKsatDataSet_db.py +++ b/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 = {} diff --git a/src/runMinisat.cpp b/src/runMinisat.cpp index 9f0548b..e45b844 100644 --- a/src/runMinisat.cpp +++ b/src/runMinisat.cpp @@ -41,9 +41,6 @@ int main(int argc, char** argv) { satlab::MinisatSolver solver(satlab::types::convert(doc)); - bool modelFound = solver.solve(); - - auto result = satlab::convert( solver.getResult() ); diff --git a/src/util/bson2ksatClauseConverter.h b/src/util/bson2ksatClauseConverter.h index 2566944..23ff911 100644 --- a/src/util/bson2ksatClauseConverter.h +++ b/src/util/bson2ksatClauseConverter.h @@ -11,30 +11,6 @@ namespace satlab { -/* -using BSON2KSATCLAUSE_CONVERTER = Converter; - -template<> -class Converter -{ -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(docView.get_array())) - { - clause.push_back(lit.get_int32()); - } - - return clause; -} -*/ namespace types { diff --git a/src/util/bson2ksatConverter.h b/src/util/bson2ksatConverter.h index 60e3470..a4de091 100644 --- a/src/util/bson2ksatConverter.h +++ b/src/util/bson2ksatConverter.h @@ -35,34 +35,6 @@ KSATinstance convert(const bsoncxx::document::view& docView) } } -/* -using BSON2KSAT_CONVERTER = Converter; - -template<> -class Converter -{ -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; -} -*/ } diff --git a/src/util/convert.h b/src/util/convert.h index 4df0078..8a65c16 100644 --- a/src/util/convert.h +++ b/src/util/convert.h @@ -3,14 +3,6 @@ namespace satlab { -/* -template -class Converter -{ -public: - TARGET_T convert(const SOURCE_T& source); -}; -*/ namespace types {