diff --git a/src/runMinisat.cpp b/src/runMinisat.cpp index e45b844..591c366 100644 --- a/src/runMinisat.cpp +++ b/src/runMinisat.cpp @@ -15,12 +15,14 @@ #include "util/minisatsolver.h" #include "util/conversions.h" #include "util/ksatinstance.h" +#include "util/mongodbexperimentscope.h" #include #include #include std::string getDbConfigFilePath(); +std::string getScopeName(); std::string getDBUrl(); mongocxx::client connectToDatabase(); @@ -33,24 +35,20 @@ int main(int argc, char** argv) 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(doc)); + for(auto sat : satlab::MongoDBExperimentScope(db, getScopeName())) + { + satlab::MinisatSolver solver(sat); + + solver.solve(); auto result = satlab::convert( solver.getResult() ); - result << "instance" << doc["_id"].get_oid(); - db["minisat_runs"].insert_one(result.view()); - - } - + } + return 0; } @@ -91,3 +89,14 @@ std::string getDbConfigFilePath() return path; } + +std::string getScopeName() +{ + std::cout << "Experiment scope: "; + + std::string scope; + + std::cin >> scope; + + return scope; +} diff --git a/src/util/bson2ksatConverter.h b/src/util/bson2ksatConverter.h index a4de091..98d0522 100644 --- a/src/util/bson2ksatConverter.h +++ b/src/util/bson2ksatConverter.h @@ -30,6 +30,7 @@ KSATinstance convert(const bsoncxx::document::view& docView) ksat.addClause(convert(clause)); } + ksat.setId(docView["_id"].get_oid().value.to_string()); return ksat; } diff --git a/src/util/experimentscope.cpp b/src/util/experimentscope.cpp new file mode 100644 index 0000000..90d46d9 --- /dev/null +++ b/src/util/experimentscope.cpp @@ -0,0 +1,76 @@ +#include "util/experimentscope.h" + +namespace satlab +{ + +KSATinstance* ExperimentScope::InstanceIncrementer::operator->() +{ + return &instance; +} + + +KSATinstance& ExperimentScope::InstanceIncrementer::operator*() +{ + return instance; +} + + +void ExperimentScope::InstanceIncrementer::next() +{ + step++; +} + + +bool ExperimentScope::iterator::operator==(const ExperimentScope::iterator& other) +{ + return cmp(pIncr, other.pIncr); +} + + +bool ExperimentScope::iterator::operator!=(const ExperimentScope::iterator& other) +{ + return !(cmp(pIncr, other.pIncr)); +} + +ExperimentScope::iterator::reference ExperimentScope::iterator::operator*() +{ + return (*pIncr).operator*(); +} + +ExperimentScope::iterator::pointer ExperimentScope::iterator::operator->() +{ + return (*pIncr).operator->(); +} + +ExperimentScope::iterator& ExperimentScope::iterator::operator++() +{ + pIncr->next(); + + return *this; +} + +ExperimentScope::iterator ExperimentScope::iterator::operator++(int) +{ + iterator copy(*this); + + pIncr->next(); + + return copy; +} + +ExperimentScope::iterator::iterator(ExperimentScope::P_INCR_T&& pIncr, + ExperimentScope::iterator::CMP_FNC_T&& cmp) +: cmp(std::move(cmp)), + pIncr(std::move(pIncr)) +{ +} + +ExperimentScope::iterator +ExperimentScope::createIterator(ExperimentScope::P_INCR_T&& pIncr, + ExperimentScope::iterator::CMP_FNC_T&& cmp) +{ + return iterator(std::move(pIncr), std::move(cmp)); +} + + +} diff --git a/src/util/experimentscope.h b/src/util/experimentscope.h new file mode 100644 index 0000000..4a271ab --- /dev/null +++ b/src/util/experimentscope.h @@ -0,0 +1,94 @@ +#ifndef EXPERIMENTSCOPE_H +#define EXPERIMENTSCOPE_H + +#include "util/ksatinstance.h" +#include +#include + +namespace satlab +{ + +class ExperimentScope +{ +protected: + + class InstanceIncrementer + { + public: + friend bool operator==(const ExperimentScope::InstanceIncrementer& lhs, + const ExperimentScope::InstanceIncrementer& rhs); + + InstanceIncrementer() = default; + virtual ~InstanceIncrementer() = default; + + InstanceIncrementer(const InstanceIncrementer& other) = default; + InstanceIncrementer(InstanceIncrementer&& other) = default; + + InstanceIncrementer& operator=(const InstanceIncrementer& other) = default; + InstanceIncrementer& operator=(InstanceIncrementer&& other) = default; + + virtual void next(); + + virtual KSATinstance* operator->(); + + virtual KSATinstance& operator*(); + + private: + int step; + + protected: + KSATinstance instance; + }; + + using P_INCR_T = std::shared_ptr; + +public: + class iterator + { + public: + friend class ExperimentScope; + + using iterator_category = std::forward_iterator_tag; + using value_type = KSATinstance; + using difference_type = int; + using pointer = KSATinstance*; + using reference = KSATinstance&; + + iterator() = default; + virtual ~iterator() = default; + + iterator(const iterator& other) = default; + iterator& operator=(const iterator& other) = default; + + virtual bool operator==(const iterator&other); + virtual bool operator!=(const iterator&other); + + virtual reference operator*(); + virtual pointer operator->(); + + virtual iterator& operator++(); + virtual iterator operator++(int); + + private: + using CMP_FNC_T = std::function; + + iterator(P_INCR_T&& pIncr, CMP_FNC_T&& cmp); + + CMP_FNC_T cmp; + + P_INCR_T pIncr; + }; + + virtual iterator begin() noexcept = 0; + + virtual iterator end() noexcept = 0; + +protected: + iterator createIterator(P_INCR_T&& pIncr, iterator::CMP_FNC_T&& cmp); + +}; + +} + +#endif // EXPERIMENTSCOPE_H diff --git a/src/util/ksatinstance.cpp b/src/util/ksatinstance.cpp index e1c6cb5..042556e 100644 --- a/src/util/ksatinstance.cpp +++ b/src/util/ksatinstance.cpp @@ -18,5 +18,20 @@ const std::vector& KSATinstance::getClauses() const return clauses; } +void KSATinstance::setId(const std::string& id) +{ + this->id = id; +} + +void KSATinstance::setId(std::string&& id) +{ + this->id = std::move(id); +} + +const std::string& KSATinstance::getId() const +{ + return id; +} + } diff --git a/src/util/ksatinstance.h b/src/util/ksatinstance.h index bbc4988..0f06e67 100644 --- a/src/util/ksatinstance.h +++ b/src/util/ksatinstance.h @@ -2,6 +2,7 @@ #define KSATINSTANCE_H #include +#include namespace satlab { @@ -26,8 +27,15 @@ public: void addClause(CLAUSE&& clause); const std::vector& getClauses() const; -private: + void setId(const std::string& id); + void setId(std::string&& id); + + const std::string& getId() const; + +private: + + std::string id; std::vector clauses; }; diff --git a/src/util/minisatResult2bson.h b/src/util/minisatResult2bson.h index ae6695d..2c8fb67 100644 --- a/src/util/minisatResult2bson.h +++ b/src/util/minisatResult2bson.h @@ -11,7 +11,6 @@ namespace satlab { - template bsoncxx::builder::stream::document convert(const MinisatResult& result) @@ -23,7 +22,8 @@ bsoncxx::builder::stream::document convert(const MinisatResult& result) builder << "satisfiable" << result.getSatisfiable() << "model" << convert(result.getModel()).view() - << "stats" << convert(result.getStats()).view(); + << "stats" << convert(result.getStats()).view() + << "instance" << bsoncxx::oid(result.getInstanceId()); return builder; } diff --git a/src/util/minisatresult.cpp b/src/util/minisatresult.cpp index 1fcad13..08fc1e3 100644 --- a/src/util/minisatresult.cpp +++ b/src/util/minisatresult.cpp @@ -38,4 +38,19 @@ bool MinisatResult::getSatisfiable() const return satisfiable; } +void MinisatResult::setInstanceId(const std::string& id) +{ + instanceId = id; +} + +void MinisatResult::setInstanceId(std::string&& id) +{ + instanceId = std::move(id); +} + +const std::string& MinisatResult::getInstanceId() const +{ + return instanceId; +} + } diff --git a/src/util/minisatresult.h b/src/util/minisatresult.h index 18d176c..435bf9a 100644 --- a/src/util/minisatresult.h +++ b/src/util/minisatresult.h @@ -4,6 +4,8 @@ #include "util/ksatinstance.h" #include "util/minisatstats.h" +#include + namespace satlab { @@ -30,10 +32,17 @@ public: void setSatisfiable(bool value); bool getSatisfiable() const; + void setInstanceId(const std::string& id); + void setInstanceId(std::string&& id); + + const std::string& getInstanceId() const; + private: bool satisfiable; KSATinstance::MODEL model; MinisatStats stats; + std::string instanceId; + }; } diff --git a/src/util/minisatsolver.cpp b/src/util/minisatsolver.cpp index 740bdfb..05b4204 100644 --- a/src/util/minisatsolver.cpp +++ b/src/util/minisatsolver.cpp @@ -10,12 +10,23 @@ namespace satlab { MinisatSolver::MinisatSolver(const KSATinstance& ksat) +: instance(ksat) { - for(auto& clause : ksat.getClauses()) + init(); +} + +MinisatSolver::MinisatSolver(KSATinstance&& ksat) +: instance(std::move(ksat)) +{ + init(); +} + +void MinisatSolver::init() +{ + for(auto& clause : instance.getClauses()) { addClause(clause); } - } bool MinisatSolver::solve() @@ -59,6 +70,7 @@ MinisatResult MinisatSolver::getResult() const result.setStats(getStats()); result.setSatisfiable(satisfiable); + result.setInstanceId(instance.getId()); return result; } diff --git a/src/util/minisatsolver.h b/src/util/minisatsolver.h index acd2056..1c9626c 100644 --- a/src/util/minisatsolver.h +++ b/src/util/minisatsolver.h @@ -19,6 +19,7 @@ private: public: MinisatSolver(const KSATinstance& ksat); + MinisatSolver(KSATinstance&& ksat); bool solve(); @@ -28,8 +29,12 @@ public: MinisatStats getStats() const; private: - bool satisfiable; void addMissingVars(const MINISAT_CLAUSE& clause); + void init(); + + bool satisfiable; + KSATinstance instance; + }; } diff --git a/src/util/mongodbexperimentscope.cpp b/src/util/mongodbexperimentscope.cpp new file mode 100644 index 0000000..34190fc --- /dev/null +++ b/src/util/mongodbexperimentscope.cpp @@ -0,0 +1,147 @@ +#include "util/mongodbexperimentscope.h" + +#include "util/conversions.h" + +#include "mongocxx/collection.hpp" +#include "mongocxx/pipeline.hpp" + +#include "bsoncxx/builder/stream/document.hpp" +#include "bsoncxx/oid.hpp" + +#include + +namespace satlab +{ + +MongoDBExperimentScope::InstanceIncrementer::InstanceIncrementer( + mongocxx::cursor::iterator&& cursorIt) +: cursorIt(std::move(cursorIt)) +{ +} + +void MongoDBExperimentScope::InstanceIncrementer::next() +{ + BASE::InstanceIncrementer::next(); + + cursorIt++; + + instanceIsUpdated = false; +} + +void MongoDBExperimentScope::InstanceIncrementer::updateInstance() +{ + if(instanceIsUpdated) + { + return; + } + + instance = KSATinstance(types::convert(*cursorIt)); + + instanceIsUpdated = true; +} + +KSATinstance* MongoDBExperimentScope::InstanceIncrementer::operator->() +{ + updateInstance(); + + return &instance; +} + +KSATinstance& MongoDBExperimentScope::InstanceIncrementer::operator*() +{ + updateInstance(); + + return instance; +} + + +MongoDBExperimentScope::MongoDBExperimentScope(mongocxx::cursor&& cursor) +: cursor(std::move(cursor)) +{ +} + +MongoDBExperimentScope::MongoDBExperimentScope(const mongocxx::database& db, + const std::string& scopeName) +: MongoDBExperimentScope(std::move(getCursor(db, scopeName))) +{ +} + +mongocxx::cursor MongoDBExperimentScope::getCursor(const mongocxx::database& db, + const std::string& scopeName) +{ + return db["experiment_scopes"].aggregate(createScopePipeline(scopeName)); +} + +mongocxx::pipeline +MongoDBExperimentScope::createScopePipeline(const std::string& scopeName) +{ + mongocxx::pipeline pipeline; + + pipeline.match(bsoncxx::builder::stream::document() + << "_id" << scopeName + << bsoncxx::builder::stream::finalize); + + pipeline.unwind("$instances"); + + pipeline.lookup(bsoncxx::builder::stream::document() + << "from" << "instances" + << "localField" << "instances" + << "foreignField" << "_id" + << "as" << "instance" + << bsoncxx::builder::stream::finalize); + + pipeline.unwind("$instance"); + + pipeline.replace_root(bsoncxx::builder::stream::document() + << "newRoot" << "$instance" + << bsoncxx::builder::stream::finalize); + + return pipeline; +} + +MongoDBExperimentScope::BASE::iterator MongoDBExperimentScope::begin() noexcept +{ + P_INCR_T incrementer = P_INCR_T(new InstanceIncrementer(cursor.begin())); + + return BASE::createIterator( + std::move(incrementer), + + [] (const std::shared_ptr& lhs, + const std::shared_ptr& rhs) + { + auto derivedLhs = std::dynamic_pointer_cast(lhs); + auto derivedRhs = std::dynamic_pointer_cast(rhs); + + if(derivedLhs && derivedRhs) + { + return derivedLhs->cursorIt == derivedRhs->cursorIt; + } + + return false; + } + ); +} + +MongoDBExperimentScope::BASE::iterator MongoDBExperimentScope::end() noexcept +{ + P_INCR_T incrementer = P_INCR_T(new InstanceIncrementer(cursor.end())); + + return BASE::createIterator( + std::move(incrementer), + + [] (const std::shared_ptr& lhs, + const std::shared_ptr& rhs) + { + auto derivedLhs = std::dynamic_pointer_cast(lhs); + auto derivedRhs = std::dynamic_pointer_cast(rhs); + + if(derivedLhs && derivedRhs) + { + return derivedLhs->cursorIt == derivedRhs->cursorIt; + } + return false; + } + ); +} + +} diff --git a/src/util/mongodbexperimentscope.h b/src/util/mongodbexperimentscope.h new file mode 100644 index 0000000..38116e6 --- /dev/null +++ b/src/util/mongodbexperimentscope.h @@ -0,0 +1,77 @@ +#ifndef MONGODBEXPERIMENTSCOPE_H +#define MONGODBEXPERIMENTSCOPE_H + +#include "util/experimentscope.h" + +#include "mongocxx/cursor.hpp" +#include "mongocxx/database.hpp" + +#include + +namespace satlab +{ + +class MongoDBExperimentScope : public ExperimentScope +{ +public: + using BASE = ExperimentScope; + + class InstanceIncrementer : public ExperimentScope::InstanceIncrementer + { + public: + friend class MongoDBExperimentScope; + + InstanceIncrementer() = default; + virtual ~InstanceIncrementer() = default; + + InstanceIncrementer(const InstanceIncrementer& other) = default; + InstanceIncrementer(InstanceIncrementer&& other) = default; + + InstanceIncrementer& operator=(const InstanceIncrementer& other) = default; + InstanceIncrementer& operator=(InstanceIncrementer&& other) = default; + + InstanceIncrementer(mongocxx::cursor::iterator&& cursorIt); + + virtual void next() override; + + virtual KSATinstance* operator->() override; + + virtual KSATinstance& operator*() override; + + private: + void updateInstance(); + + bool instanceIsUpdated = false; + mongocxx::cursor::iterator cursorIt; + }; + +public: + MongoDBExperimentScope() = default; + virtual ~MongoDBExperimentScope() = default; + + MongoDBExperimentScope(const MongoDBExperimentScope& other) = default; + MongoDBExperimentScope(MongoDBExperimentScope&& other) = default; + + MongoDBExperimentScope& operator=(const MongoDBExperimentScope& other) = default; + MongoDBExperimentScope& operator=(MongoDBExperimentScope&& other) = default; + + MongoDBExperimentScope(mongocxx::cursor&& cursor); + MongoDBExperimentScope(const mongocxx::database& db, const std::string& scopeName); + + virtual BASE::iterator begin() noexcept override; + virtual BASE::iterator end() noexcept override; + +private: + using P_INCR_T = BASE::P_INCR_T; + + mongocxx::cursor getCursor(const mongocxx::database& db, + const std::string& scopeName); + + mongocxx::pipeline createScopePipeline(const std::string& scopeName); + + mongocxx::cursor cursor; +}; + +} + +#endif // MONGODBEXPERIMENTSCOPE_H