implemented ExperimentScope
This commit is contained in:
@@ -15,12 +15,14 @@
|
||||
#include "util/minisatsolver.h"
|
||||
#include "util/conversions.h"
|
||||
#include "util/ksatinstance.h"
|
||||
#include "util/mongodbexperimentscope.h"
|
||||
|
||||
#include <string>
|
||||
#include <cmath>
|
||||
#include <vector>
|
||||
|
||||
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<satlab::KSATinstance>(doc));
|
||||
for(auto sat : satlab::MongoDBExperimentScope(db, getScopeName()))
|
||||
{
|
||||
satlab::MinisatSolver solver(sat);
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
@@ -91,3 +89,14 @@ std::string getDbConfigFilePath()
|
||||
|
||||
return path;
|
||||
}
|
||||
|
||||
std::string getScopeName()
|
||||
{
|
||||
std::cout << "Experiment scope: ";
|
||||
|
||||
std::string scope;
|
||||
|
||||
std::cin >> scope;
|
||||
|
||||
return scope;
|
||||
}
|
||||
|
@@ -30,6 +30,7 @@ KSATinstance convert(const bsoncxx::document::view& docView)
|
||||
ksat.addClause(convert<CLAUSE, CLAUSE_DOC>(clause));
|
||||
}
|
||||
|
||||
ksat.setId(docView["_id"].get_oid().value.to_string());
|
||||
|
||||
return ksat;
|
||||
}
|
||||
|
76
src/util/experimentscope.cpp
Normal file
76
src/util/experimentscope.cpp
Normal file
@@ -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));
|
||||
}
|
||||
|
||||
|
||||
}
|
94
src/util/experimentscope.h
Normal file
94
src/util/experimentscope.h
Normal file
@@ -0,0 +1,94 @@
|
||||
#ifndef EXPERIMENTSCOPE_H
|
||||
#define EXPERIMENTSCOPE_H
|
||||
|
||||
#include "util/ksatinstance.h"
|
||||
#include <memory>
|
||||
#include <functional>
|
||||
|
||||
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<InstanceIncrementer>;
|
||||
|
||||
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<bool(const P_INCR_T& lhs,
|
||||
const P_INCR_T& rhs)>;
|
||||
|
||||
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
|
@@ -18,5 +18,20 @@ const std::vector<KSATinstance::CLAUSE>& 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;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
@@ -2,6 +2,7 @@
|
||||
#define KSATINSTANCE_H
|
||||
|
||||
#include <vector>
|
||||
#include <iostream>
|
||||
|
||||
namespace satlab
|
||||
{
|
||||
@@ -26,8 +27,15 @@ public:
|
||||
void addClause(CLAUSE&& clause);
|
||||
|
||||
const std::vector<CLAUSE>& 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<CLAUSE> clauses;
|
||||
};
|
||||
|
||||
|
@@ -11,7 +11,6 @@
|
||||
|
||||
namespace satlab
|
||||
{
|
||||
|
||||
|
||||
template<typename = bsoncxx::builder::stream::document, typename = MinisatResult>
|
||||
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<ARRAY_BUILDER>(result.getModel()).view()
|
||||
<< "stats" << convert<DOCUMENT_BUILDER>(result.getStats()).view();
|
||||
<< "stats" << convert<DOCUMENT_BUILDER>(result.getStats()).view()
|
||||
<< "instance" << bsoncxx::oid(result.getInstanceId());
|
||||
|
||||
return builder;
|
||||
}
|
||||
|
@@ -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;
|
||||
}
|
||||
|
||||
}
|
||||
|
@@ -4,6 +4,8 @@
|
||||
#include "util/ksatinstance.h"
|
||||
#include "util/minisatstats.h"
|
||||
|
||||
#include <string>
|
||||
|
||||
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;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
@@ -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;
|
||||
}
|
||||
|
@@ -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;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
147
src/util/mongodbexperimentscope.cpp
Normal file
147
src/util/mongodbexperimentscope.cpp
Normal file
@@ -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 <iostream>
|
||||
|
||||
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<BASE::InstanceIncrementer>& lhs,
|
||||
const std::shared_ptr<BASE::InstanceIncrementer>& rhs)
|
||||
{
|
||||
auto derivedLhs = std::dynamic_pointer_cast<InstanceIncrementer>(lhs);
|
||||
auto derivedRhs = std::dynamic_pointer_cast<InstanceIncrementer>(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<BASE::InstanceIncrementer>& lhs,
|
||||
const std::shared_ptr<BASE::InstanceIncrementer>& rhs)
|
||||
{
|
||||
auto derivedLhs = std::dynamic_pointer_cast<InstanceIncrementer>(lhs);
|
||||
auto derivedRhs = std::dynamic_pointer_cast<InstanceIncrementer>(rhs);
|
||||
|
||||
if(derivedLhs && derivedRhs)
|
||||
{
|
||||
return derivedLhs->cursorIt == derivedRhs->cursorIt;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
);
|
||||
}
|
||||
|
||||
}
|
77
src/util/mongodbexperimentscope.h
Normal file
77
src/util/mongodbexperimentscope.h
Normal file
@@ -0,0 +1,77 @@
|
||||
#ifndef MONGODBEXPERIMENTSCOPE_H
|
||||
#define MONGODBEXPERIMENTSCOPE_H
|
||||
|
||||
#include "util/experimentscope.h"
|
||||
|
||||
#include "mongocxx/cursor.hpp"
|
||||
#include "mongocxx/database.hpp"
|
||||
|
||||
#include <string>
|
||||
|
||||
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
|
Reference in New Issue
Block a user