implemented basics

src/SConscript

@@ -0,0 +1,32 @@
+import os
+
+Import('globalEnv')
+
+env = globalEnv.Clone()
+
+files = Glob(os.path.join(".","*.cpp"))
+files.append(Glob(os.path.join("util", "*.cpp")))
+
+targetName = 'runMinisat'
+
+libs = ["mongocxx", "bsoncxx", "inihcpp", "minisat"]
+
+env.Append(CPPPATH=os.path.join(env["ROOTPATH"], "src"))
+
+env.Program(target=targetName, source=files, LIBS=libs)
+
+## create start script
+#
+
+startScriptName = "{}.sh".format(targetName)
+
+with open(startScriptName, "w") as startScript:
+	startScript.write("#!/bin/bash\n")
+
+	startScript.write("export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:{}\n"
+					   .format(os.path.join(env["MONGOCXX_LIB_PATH"], "lib")))
+
+	startScript.write("{}\n".format(os.path.join(env["BUILDPATH"], targetName)))
+
+#env.Install(env["BUILDPATH"], [startScriptName])
+

src/runMinisat.cpp

@@ -0,0 +1,96 @@
+#include <iostream>
+#include "bsoncxx/builder/stream/document.hpp"
+#include "bsoncxx/json.hpp"
+
+#include <mongocxx/client.hpp>
+#include <mongocxx/instance.hpp>
+#include <mongocxx/uri.hpp>
+
+#include "INIReader.h"
+
+#include "core/Solver.h"
+#include "mtl/Vec.h"
+#include "core/SolverTypes.h"
+
+#include "util/minisatsolver.h"
+#include "util/conversions.h"
+#include "util/ksatinstance.h"
+
+#include <string>
+#include <cmath>
+#include <vector>
+
+std::string getDbConfigFilePath();
+std::string getDBUrl();
+mongocxx::client connectToDatabase();
+
+int main(int argc, char** argv)
+{
+	mongocxx::instance inst{};
+    
+	mongocxx::client conn = connectToDatabase();
+    
+	mongocxx::database db = conn["experiments"];
+
+	mongocxx::collection instances = db["instances"];
+	
+	mongocxx::cursor cursor = instances.find({});
+
+    
+	for(auto doc : cursor)
+	{
+        satlab::MinisatSolver solver(satlab::types::convert<satlab::KSATinstance>(doc));
+        
+        bool modelFound = solver.solve();
+        
+        
+        auto result = satlab::convert<bsoncxx::builder::stream::document>(
+                        solver.getResult()
+                      );
+        
+        result << "instance" << doc["_id"].get_oid();
+        
+        db["minisat_runs"].insert_one(result.view());
+        
+	}	
+	
+	return 0;
+}
+
+mongocxx::client connectToDatabase()
+{
+    mongocxx::options::ssl sslOptions;
+    sslOptions.allow_invalid_certificates(true);
+     
+	mongocxx::options::client clientOptions{};
+	clientOptions.ssl_opts(sslOptions);
+    
+	return mongocxx::client{mongocxx::uri{getDBUrl()}, clientOptions};
+}
+
+
+std::string getDBUrl()
+{
+	INIReader iniReader(getDbConfigFilePath());
+
+	std::string connUrl("mongodb://");
+	connUrl.append(iniReader.Get("CONNECTION", "user", "NA") + ":");
+	connUrl.append(iniReader.Get("CONNECTION", "pw", "NA") + "@");
+	connUrl.append(iniReader.Get("CONNECTION", "url", "NA") + ":");
+	connUrl.append(iniReader.Get("CONNECTION", "port", "NA") + "/");
+	connUrl.append(iniReader.Get("CONNECTION", "database", "NA"));
+	connUrl.append("?ssl=true");
+
+	return connUrl;
+}
+
+std::string getDbConfigFilePath()
+{
+	std::cout << "Database config file: ";
+
+	std::string path;
+
+	std::cin >> path;
+
+	return path;
+}

src/util/bson2ksatClauseConverter.h

@@ -0,0 +1,59 @@
+#ifndef BSON2KSATCLAUSE_CONVERTER_H
+#define BSON2KSATCLAUSE_CONVERTER_H
+
+#include "util/convert.h"
+#include "util/ksatinstance.h"
+
+#include "bsoncxx/document/view.hpp"
+#include "bsoncxx/array/view.hpp"
+#include "bsoncxx/document/element.hpp"
+#include "bsoncxx/types.hpp"
+
+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
+{
+    
+template<typename = KSATinstance::CLAUSE, typename = bsoncxx::array::element>
+KSATinstance::CLAUSE 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;
+}
+
+}
+
+}
+
+#endif // BSON2KSATCLAUSE_CONVERTER_H

src/util/bson2ksatConverter.h

@@ -0,0 +1,69 @@
+#ifndef BSON2KSAT_CONVERTER_H
+#define BSON2KSAT_CONVERTER_H
+
+#include "bsoncxx/document/view.hpp"
+#include "bsoncxx/array/view.hpp"
+#include "bsoncxx/types.hpp"
+
+#include "util/convert.h"
+#include "util/ksatinstance.h"
+#include "util/bson2ksatClauseConverter.h"
+
+namespace satlab
+{
+    
+namespace types
+{
+
+template<typename = KSATinstance, typename = bsoncxx::document::view>
+KSATinstance convert(const bsoncxx::document::view& docView)
+{
+    using CLAUSE = KSATinstance::CLAUSE;
+    using CLAUSE_DOC = const bsoncxx::array::element&;
+    
+    KSATinstance ksat;
+    
+    bsoncxx::array::view clauses = docView["clauses"].get_array();
+    
+    for(auto clause : clauses)
+    {
+        ksat.addClause(convert<CLAUSE, CLAUSE_DOC>(clause));
+    }
+    
+    
+    return ksat;
+}
+
+}
+/*
+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;
+}
+*/
+
+}
+
+#endif // BSON2KSAT_CONVERTER_H

src/util/conversions.h

@@ -0,0 +1,11 @@
+#ifndef CONVERSIONS_H
+#define CONVERSIONS_H
+
+#include "util/bson2ksatClauseConverter.h"
+#include "util/bson2ksatConverter.h"
+#include "util/ksatClause2ministaClause.h"
+#include "util/minisatStats2bson.h"
+#include "util/minisatResult2bson.h"
+#include "util/ksatModel2bson.h"
+
+#endif //CONVERSIONS_H

src/util/convert.h

@@ -0,0 +1,27 @@
+#ifndef CONVERT_H
+#define CONVERT_H
+
+namespace satlab
+{
+/*
+template<typename TARGET_T, typename SOURCE_T>
+class Converter
+{
+public:
+    TARGET_T convert(const SOURCE_T& source);
+};
+*/
+
+namespace types
+{
+    
+template<typename TARGET_T, typename SOURCE_T>
+TARGET_T convert(const SOURCE_T& source);
+
+template<typename TARGET_T, typename SOURCE_T>
+void convertRef(TARGET_T&, const SOURCE_T& source);
+}
+
+}
+
+#endif // CONVERT_H

src/util/ksatClause2ministaClause.h

@@ -0,0 +1,33 @@
+#ifndef KSAT_CLAUSE_2_MINISAT_CLAUSE
+#define KSAT_CLAUSE_2_MINISAT_CLAUSE
+
+#include "util/convert.h"
+#include "util/ksatinstance.h"
+
+#include "core/SolverTypes.h"
+
+#include <cmath>
+
+namespace satlab
+{
+namespace types
+{
+
+template<typename = Minisat::vec<Minisat::Lit>, typename = KSATinstance::CLAUSE>
+void convertRef(Minisat::vec<Minisat::Lit>& clauseVec,
+                const KSATinstance::CLAUSE& clause)
+{
+    clauseVec.clear();
+    
+    int var;
+    for(auto lit : clause)
+    {
+        var = abs(lit) - 1;
+        
+        clauseVec.push(Minisat::mkLit(var, lit < 0));
+    }
+}
+
+}
+}
+#endif // KSAT_CLAUSE_2_MINISAT_CLAUSE

src/util/ksatModel2bson.h

@@ -0,0 +1,28 @@
+#ifndef KSAT_MODEL_2_BSON
+#define KSAT_MODEL_2_BSON
+
+#include "util/convert.h"
+#include "util/ksatinstance.h"
+
+#include "bsoncxx/array/value.hpp"
+#include "bsoncxx/builder/stream/array.hpp"
+
+namespace satlab
+{
+
+template<typename = bsoncxx::builder::stream::array, typename = KSATinstance::MODEL>
+bsoncxx::builder::stream::array convert(const KSATinstance::MODEL& model)
+{
+    bsoncxx::builder::stream::array builder;
+    
+    for(auto& lit : model)
+    {
+        builder << lit;
+    }
+    
+    return builder;
+}
+
+}
+
+#endif // KSAT_MODEL_2_BSON

src/util/ksatinstance.cpp

@@ -0,0 +1,22 @@
+#include "ksatinstance.h"
+
+namespace satlab
+{
+
+void KSATinstance::addClause(const CLAUSE& clause)
+{
+    clauses.push_back(clause);
+}
+
+void KSATinstance::addClause(CLAUSE&& clause)
+{
+    clauses.push_back(clause);
+}
+
+const std::vector<KSATinstance::CLAUSE>& KSATinstance::getClauses() const
+{
+    return clauses;
+}
+
+
+}

src/util/ksatinstance.h

@@ -0,0 +1,36 @@
+#ifndef KSATINSTANCE_H
+#define KSATINSTANCE_H
+
+#include <vector>
+
+namespace satlab
+{
+    
+class KSATinstance
+{
+public:
+    using LITERAL = int;
+    using CLAUSE = std::vector<LITERAL>;
+    using MODEL = std::vector<LITERAL>;
+    
+    KSATinstance() = default;
+    ~KSATinstance() = default;
+    
+    KSATinstance(const KSATinstance& other) = default;
+    KSATinstance(KSATinstance&& other) = default;
+    
+    KSATinstance& operator=(const KSATinstance& other) = default;
+    KSATinstance& operator=(KSATinstance&& other) = default;
+    
+    void addClause(const CLAUSE& clause);
+    void addClause(CLAUSE&& clause);
+    
+    const std::vector<CLAUSE>& getClauses() const;
+private:
+    
+    std::vector<CLAUSE> clauses;
+};
+
+}
+
+#endif // KSATINSTANCE_H

src/util/minisatResult2bson.h

@@ -0,0 +1,34 @@
+#ifndef MINISAT_RESULT_2_BSON
+#define MINISAT_RESULT_2_BSON
+
+#include "util/convert.h"
+#include "util/minisatresult.h"
+#include "util/ksatModel2bson.h"
+#include "util/minisatStats2bson.h"
+
+#include "bsoncxx/document/value.hpp"
+#include "bsoncxx/builder/stream/document.hpp"
+
+namespace satlab
+{
+
+    
+template<typename = bsoncxx::builder::stream::document, typename = MinisatResult>
+bsoncxx::builder::stream::document convert(const MinisatResult& result)
+{
+    using ARRAY_BUILDER = bsoncxx::builder::stream::array;
+    using DOCUMENT_BUILDER = bsoncxx::builder::stream::document;
+    
+    DOCUMENT_BUILDER builder;
+    
+    builder << "satisfiable" << result.getSatisfiable()
+            << "model" << convert<ARRAY_BUILDER>(result.getModel()).view()
+            << "stats" << convert<DOCUMENT_BUILDER>(result.getStats()).view();
+    
+    return builder;
+}
+
+
+}
+
+#endif // MINISAT_RESULT_2_BSON

src/util/minisatStats2bson.h

@@ -0,0 +1,35 @@
+#ifndef MINISAT_STATS_2_BSON
+#define MINISAT_STATS_2_BSON
+
+#include "util/convert.h"
+#include "util/minisatstats.h"
+
+#include "bsoncxx/document/value.hpp"
+#include "bsoncxx/builder/stream/document.hpp"
+
+namespace satlab
+{
+
+template<typename = bsoncxx::builder::stream::document, typename = MinisatStats>
+bsoncxx::builder::stream::document convert(const MinisatStats& stats)
+{
+    bsoncxx::builder::stream::document builder;
+    
+    builder << "solves" << static_cast<int>(stats.getSolves())
+            << "starts" << static_cast<int>(stats.getStarts())
+            << "decisions" << static_cast<int>(stats.getDecisions())
+            << "rnd_decisions" << static_cast<int>(stats.getRndDecisions())
+            << "propagations" << static_cast<int>(stats.getPropagations())
+            << "conflicts" << static_cast<int>(stats.getConflicts())
+            << "dec_vars" << static_cast<int>(stats.getDecVars())
+            << "clauses_literals" << static_cast<int>(stats.getClausesLiterals())
+            << "learnts_literals" << static_cast<int>(stats.getLearntsLiterals())
+            << "max_literals" << static_cast<int>(stats.getMaxLiterals())
+            << "tot_literals" << static_cast<int>(stats.getTotLiterals());
+    
+    return builder;
+}
+
+
+}
+#endif // MINISAT_STATS_2_BSON

src/util/minisatresult.cpp

@@ -0,0 +1,41 @@
+#include "util/minisatresult.h"
+
+namespace satlab
+{
+
+void MinisatResult::setModel(const KSATinstance::MODEL& model)
+{
+    this->model = model;
+}
+
+const KSATinstance::MODEL& MinisatResult::getModel() const
+{
+    return model;
+}
+
+void MinisatResult::addLiteralToModel(KSATinstance::LITERAL lit)
+{
+    model.push_back(lit);
+}
+
+void MinisatResult::setStats(MinisatStats&& stats)
+{
+    this->stats = MinisatStats(std::move(stats));
+}
+
+const MinisatStats& MinisatResult::getStats() const
+{
+    return stats;
+}
+
+void MinisatResult::setSatisfiable(bool value)
+{
+    satisfiable = value;
+}
+
+bool MinisatResult::getSatisfiable() const
+{
+    return satisfiable;
+}
+
+}

src/util/minisatresult.h

@@ -0,0 +1,41 @@
+#ifndef MINISATRESULT_H
+#define MINISATRESULT_H
+
+#include "util/ksatinstance.h"
+#include "util/minisatstats.h"
+
+namespace satlab
+{
+    
+class MinisatResult
+{
+public:
+    MinisatResult() = default;
+    virtual ~MinisatResult() = default;
+    
+    MinisatResult(const MinisatResult& other) = default;
+    MinisatResult(MinisatResult&& other) = default;
+    
+    MinisatResult& operator= (const MinisatResult& other) = default;
+    MinisatResult& operator= (MinisatResult&& other) = default;
+    
+    void setModel(const KSATinstance::MODEL& model);
+    const KSATinstance::MODEL& getModel() const;
+    
+    void addLiteralToModel(KSATinstance::LITERAL lit);
+    
+    void setStats(MinisatStats&& stats);
+    const MinisatStats& getStats() const;
+    
+    void setSatisfiable(bool value);
+    bool getSatisfiable() const;
+    
+private:
+    bool satisfiable;
+    KSATinstance::MODEL model;
+    MinisatStats stats;
+};
+
+}
+
+#endif // MINISATRESULT_H

src/util/minisatsolver.cpp

@@ -0,0 +1,85 @@
+#include "util/minisatsolver.h"
+
+#include "util/conversions.h"
+
+#include "core/SolverTypes.h"
+
+#include <cmath>
+
+namespace satlab
+{
+    
+MinisatSolver::MinisatSolver(const KSATinstance& ksat)
+{
+    for(auto& clause : ksat.getClauses())
+    {
+        addClause(clause);
+    }
+    
+}
+
+bool MinisatSolver::solve()
+{
+    satisfiable = BASE::solve();
+}
+
+void MinisatSolver::addClause(const KSATinstance::CLAUSE& clause)
+{
+    Minisat::vec<Minisat::Lit> clauseVec;
+    
+    types::convertRef<>(clauseVec, clause);
+    
+    addMissingVars(clauseVec);
+    
+    BASE::addClause(clauseVec);
+}
+
+void MinisatSolver::addMissingVars(const MINISAT_CLAUSE& clause)
+{
+    for(int i=0; i < clause.size(); i++)
+    {
+        while(BASE::nVars() <= Minisat::var(clause[i]))
+        {
+            BASE::newVar();
+        }
+    }
+}
+
+MinisatResult MinisatSolver::getResult() const
+{
+    MinisatResult result;
+    
+    KSATinstance::LITERAL lit;
+    for(int i = 0; i < BASE::model.size(); i++)
+    {
+        lit = BASE::model[i] == Minisat::lbool(true) ? i + 1 : -(i + 1);
+        
+        result.addLiteralToModel(lit);
+    }
+    
+    result.setStats(getStats());
+    result.setSatisfiable(satisfiable);
+    
+    return result;
+}
+
+MinisatStats MinisatSolver::getStats() const
+{
+    MinisatStats stats;
+    
+    stats.setSolves(BASE::solves);
+    stats.setStarts(BASE::starts);
+    stats.setDecisions(BASE::decisions);
+    stats.setRndDecisions(BASE::rnd_decisions);
+    stats.setPropagations(BASE::propagations);
+    stats.setConflicts(BASE::conflicts);
+    stats.setDecVars(BASE::dec_vars);
+    stats.setClausesLiterals(BASE::clauses_literals);
+    stats.setLearntsLiterals(BASE::learnts_literals);
+    stats.setMaxLiterals(BASE::max_literals);
+    stats.setTotLiterals(BASE::tot_literals);
+    
+    return stats;
+}
+
+}

src/util/minisatsolver.h

@@ -0,0 +1,37 @@
+#ifndef MINISATSOLVER_H
+#define MINISATSOLVER_H
+
+#include "core/Solver.h"
+#include "core/SolverTypes.h"
+
+#include "util/ksatinstance.h"
+#include "util/minisatresult.h"
+#include "util/minisatstats.h"
+
+namespace satlab
+{
+    
+class MinisatSolver : public Minisat::Solver
+{
+private:
+    using MINISAT_CLAUSE = Minisat::vec<Minisat::Lit>;
+    using BASE = Minisat::Solver;
+    
+public:
+    MinisatSolver(const KSATinstance& ksat);
+    
+    bool solve();
+    
+    void addClause(const KSATinstance::CLAUSE& clause);
+    
+    MinisatResult getResult() const;
+    MinisatStats getStats() const;
+    
+private:
+    bool satisfiable;
+    void addMissingVars(const MINISAT_CLAUSE& clause);
+};
+
+}
+
+#endif // MINISATSOLVER_H

src/util/minisatstats.cpp

@@ -0,0 +1,116 @@
+#include "util/minisatstats.h"
+
+namespace satlab
+{
+    
+void MinisatStats::setSolves(uint64_t value)
+{
+    solves = value;
+}
+
+void MinisatStats::setStarts(uint64_t value)
+{
+    starts = value;
+}
+
+void MinisatStats::setDecisions(uint64_t value)
+{
+    decisions = value;
+}
+
+void MinisatStats::setRndDecisions(uint64_t value)
+{
+    rndDecisions = value;
+}
+
+void MinisatStats::setPropagations(uint64_t value)
+{
+    propagations = value;
+}
+
+void MinisatStats::setConflicts(uint64_t value)
+{
+    conflicts = value;
+}
+
+void MinisatStats::setDecVars(uint64_t value)
+{
+    decVars = value;
+}
+
+void MinisatStats::setClausesLiterals(uint64_t value)
+{
+    clausesLiterals = value;
+}
+
+void MinisatStats::setLearntsLiterals(uint64_t value)
+{
+    learntsLiterals = value;
+}
+
+void MinisatStats::setMaxLiterals(uint64_t value)
+{
+    maxLiterals = value;
+}
+
+void MinisatStats::setTotLiterals(uint64_t value)
+{
+    totLiterals = value;
+}
+
+uint64_t MinisatStats::getSolves() const
+{
+    return solves;
+}
+
+uint64_t MinisatStats::getStarts() const
+{
+    return starts;
+}
+
+uint64_t MinisatStats::getDecisions() const
+{
+    return decisions;
+}
+
+uint64_t MinisatStats::getRndDecisions() const
+{
+    return rndDecisions;
+}
+
+uint64_t MinisatStats::getPropagations() const
+{
+    return propagations;
+}
+
+uint64_t MinisatStats::getConflicts() const
+{
+    return conflicts;
+}
+
+uint64_t MinisatStats::getDecVars() const
+{
+    return decVars;
+}
+
+uint64_t MinisatStats::getClausesLiterals() const
+{
+    return clausesLiterals;
+}
+
+uint64_t MinisatStats::getLearntsLiterals() const
+{
+    return learntsLiterals;
+}
+
+uint64_t MinisatStats::getMaxLiterals() const
+{
+    return maxLiterals;
+}
+
+uint64_t MinisatStats::getTotLiterals() const
+{
+    return totLiterals;
+}
+
+}

src/util/minisatstats.h

@@ -0,0 +1,62 @@
+#ifndef MINISATSTATS_H
+#define MINISATSTATS_H
+
+#include <stdint.h>
+
+namespace satlab
+{
+    
+class MinisatStats
+{
+public:
+    MinisatStats() = default;
+    virtual ~MinisatStats() = default;
+    
+    MinisatStats(const MinisatStats& other) = default;
+    MinisatStats(MinisatStats&& other) = default;
+    
+    MinisatStats& operator=(const MinisatStats& other) = default;
+    MinisatStats& operator=(MinisatStats&& other) = default;
+    
+    
+    void setSolves(uint64_t value);
+    void setStarts(uint64_t value);
+    void setDecisions(uint64_t value);
+    void setRndDecisions(uint64_t value);
+    void setPropagations(uint64_t value);
+    void setConflicts(uint64_t value);
+    void setDecVars(uint64_t value);
+    void setClausesLiterals(uint64_t value);
+    void setLearntsLiterals(uint64_t value);
+    void setMaxLiterals(uint64_t value);
+    void setTotLiterals(uint64_t value);
+    
+    uint64_t getSolves() const;
+    uint64_t getStarts() const;
+    uint64_t getDecisions() const;
+    uint64_t getRndDecisions() const;
+    uint64_t getPropagations() const;
+    uint64_t getConflicts() const;
+    uint64_t getDecVars() const;
+    uint64_t getClausesLiterals() const;
+    uint64_t getLearntsLiterals() const;
+    uint64_t getMaxLiterals() const;
+    uint64_t getTotLiterals() const;
+    
+private:
+    uint64_t solves;
+    uint64_t starts;
+    uint64_t decisions;
+    uint64_t rndDecisions;
+    uint64_t propagations;
+    uint64_t conflicts;
+    uint64_t decVars;
+    uint64_t clausesLiterals;
+    uint64_t learntsLiterals;
+    uint64_t maxLiterals;
+    uint64_t totLiterals;
+};
+
+}
+
+#endif // MINISATSTATS_H