add maple nodes
This commit is contained in:
ihan-o
parent
c9447a1291
commit
4aeae5f850
@ -276,10 +276,10 @@ void light::seperate_groups() {
|
|||||||
int worker_procs = num_procs - 1;
|
int worker_procs = num_procs - 1;
|
||||||
|
|
||||||
if(worker_procs >= 8) {
|
if(worker_procs >= 8) {
|
||||||
int sat_procs = worker_procs / 8;
|
int sat_procs = worker_procs / 8; // 8
|
||||||
int unsat_procs = worker_procs / 4;
|
int unsat_procs = worker_procs / 4; // 16
|
||||||
int lstech_procs = 3;
|
int maple_procs = worker_procs / 8; // 8
|
||||||
int default_procs = worker_procs - sat_procs - unsat_procs - lstech_procs;
|
int default_procs = worker_procs - sat_procs - unsat_procs - maple_procs; // 32
|
||||||
|
|
||||||
|
|
||||||
std::vector<int> tmp;
|
std::vector<int> tmp;
|
||||||
@ -305,25 +305,25 @@ void light::seperate_groups() {
|
|||||||
sharing_groups.push_back(tmp);
|
sharing_groups.push_back(tmp);
|
||||||
|
|
||||||
|
|
||||||
// [sat_procs+unsat_procs+1, sat_procs+unsat_procs+lstech_procs] for ls-tech
|
// [sat_procs+1, sat_procs+maple_procs] for ls-tech
|
||||||
if(rank >= sat_procs+unsat_procs+1 && rank <= sat_procs+unsat_procs+lstech_procs) {
|
if(rank >= sat_procs+unsat_procs+1 && rank <= sat_procs+unsat_procs+maple_procs) {
|
||||||
solver_type = MAPLE;
|
solver_type = MAPLE;
|
||||||
OPT(share) = 0;
|
worker_type = light::UNSAT;
|
||||||
}
|
}
|
||||||
|
|
||||||
tmp.clear();
|
tmp.clear();
|
||||||
for(int i=sat_procs+unsat_procs+1; i<=sat_procs+unsat_procs+lstech_procs; i++) {
|
for(int i=sat_procs+unsat_procs+1; i<=sat_procs+unsat_procs+maple_procs; i++) {
|
||||||
tmp.push_back(i);
|
tmp.push_back(i);
|
||||||
}
|
}
|
||||||
sharing_groups.push_back(tmp);
|
sharing_groups.push_back(tmp);
|
||||||
|
|
||||||
// [sat_procs+unsat_procs+lstech_procs+1, worker_procs]
|
// [sat_procs+unsat_procs+lstech_procs+1, worker_procs]
|
||||||
if(rank >= sat_procs+unsat_procs+lstech_procs+1 && rank <= worker_procs) {
|
if(rank >= sat_procs+unsat_procs+maple_procs+1 && rank <= worker_procs) {
|
||||||
worker_type = light::DEFAULT;
|
worker_type = light::DEFAULT;
|
||||||
}
|
}
|
||||||
|
|
||||||
tmp.clear();
|
tmp.clear();
|
||||||
for(int i=sat_procs+unsat_procs+lstech_procs+1; i<=worker_procs; i++) {
|
for(int i=sat_procs+unsat_procs+maple_procs+1; i<=worker_procs; i++) {
|
||||||
tmp.push_back(i);
|
tmp.push_back(i);
|
||||||
}
|
}
|
||||||
sharing_groups.push_back(tmp);
|
sharing_groups.push_back(tmp);
|
||||||
|
|||||||
@ -1,114 +0,0 @@
|
|||||||
#include "utils/System.h"
|
|
||||||
#include "core/Dimacs.h"
|
|
||||||
#include "simp/SimpSolver.h"
|
|
||||||
|
|
||||||
#include "basemaple.hpp"
|
|
||||||
|
|
||||||
// using namespace MapleCOMSPS;
|
|
||||||
|
|
||||||
// Macros for minisat literal representation conversion
|
|
||||||
#define MINI_LIT(lit) lit > 0 ? MapleCOMSPS::mkLit(lit - 1, false) : MapleCOMSPS::mkLit((-lit) - 1, true)
|
|
||||||
|
|
||||||
#define INT_LIT(lit) sign(lit) ? -(var(lit) + 1) : (var(lit) + 1)
|
|
||||||
|
|
||||||
void basemaple::add(int l) {
|
|
||||||
puts("wrong");
|
|
||||||
}
|
|
||||||
|
|
||||||
int basemaple::configure(const char* name, int val) {
|
|
||||||
// if (strcmp(name, "worker_index") == 0) solver->worker_index = val;
|
|
||||||
// if (strcmp(name, "worker_seed") == 0) solver->worker_seed = val;
|
|
||||||
// if (strcmp(name, "worker_number") == 0) solver->worker_number = val;
|
|
||||||
printf("c maple configure %d\n", id);
|
|
||||||
// solver->GE = 1;
|
|
||||||
if (id == 1) solver->GE = 1;
|
|
||||||
else solver->GE = 0;
|
|
||||||
if (id % 2) solver->VSIDS = false;
|
|
||||||
else solver->VSIDS = true;
|
|
||||||
if (id % 4 >= 2) solver->verso = false;
|
|
||||||
else solver->verso = true;
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
int basemaple::solve() {
|
|
||||||
MapleCOMSPS::vec<MapleCOMSPS::Lit> miniAssumptions;
|
|
||||||
MapleCOMSPS::lbool res = solver->solveLimited(miniAssumptions);
|
|
||||||
if (res == (MapleCOMSPS::lbool((uint8_t)0))) return 10;
|
|
||||||
if (res == (MapleCOMSPS::lbool((uint8_t)1))) return 20;
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
int basemaple::val(int l) {
|
|
||||||
if (solver->model[l] != (MapleCOMSPS::lbool((uint8_t)2))) {
|
|
||||||
int lit = solver->model[l] == (MapleCOMSPS::lbool((uint8_t)0)) ? l + 1 : -(l + 1);
|
|
||||||
return lit;
|
|
||||||
}
|
|
||||||
return l;
|
|
||||||
}
|
|
||||||
|
|
||||||
void basemaple::terminate() {
|
|
||||||
solver->interrupt();
|
|
||||||
}
|
|
||||||
|
|
||||||
void cbkLstechExportClause(void * issuer, int lbd, MapleCOMSPS::vec<MapleCOMSPS::Lit> &cls) {
|
|
||||||
basemaple* mp = (basemaple*)issuer;
|
|
||||||
if (lbd > mp->good_clause_lbd) return;
|
|
||||||
|
|
||||||
shared_ptr<clause_store> ncls = std::make_shared<clause_store>(cls.size());
|
|
||||||
for (int i = 0; i < cls.size(); i++) {
|
|
||||||
ncls->data[i] = INT_LIT(cls[i]);
|
|
||||||
}
|
|
||||||
|
|
||||||
ncls->lbd = lbd;
|
|
||||||
mp->export_clause.push(ncls);
|
|
||||||
}
|
|
||||||
|
|
||||||
bool cbkLstechImportClause(void * issuer, int * lbd, MapleCOMSPS::vec<MapleCOMSPS::Lit> & mcls) {
|
|
||||||
basemaple* mp = (basemaple*)issuer;
|
|
||||||
shared_ptr<clause_store> cls = NULL;
|
|
||||||
if (mp->import_clause.pop(cls) == false) return false;
|
|
||||||
*lbd = cls->lbd;
|
|
||||||
mcls.clear();
|
|
||||||
for (size_t i = 0; i < cls->size; i++) {
|
|
||||||
MapleCOMSPS::Lit lit = MINI_LIT(cls->data[i]);
|
|
||||||
mcls.push(lit);
|
|
||||||
}
|
|
||||||
cls->free_clause();
|
|
||||||
return true;
|
|
||||||
}
|
|
||||||
|
|
||||||
basemaple::basemaple(int id, light* light) : basesolver(id, light) {
|
|
||||||
printf("c id is %d\n", id);
|
|
||||||
solver = new MapleCOMSPS::SimpSolver();
|
|
||||||
solver->issuer = this;
|
|
||||||
solver->cbkExportClause = NULL;
|
|
||||||
solver->cbkImportClause = NULL;
|
|
||||||
if (OPT(share)) {
|
|
||||||
solver->cbkExportClause = cbkLstechExportClause;
|
|
||||||
solver->cbkImportClause = cbkLstechImportClause;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
basemaple::~basemaple()
|
|
||||||
{
|
|
||||||
delete solver;
|
|
||||||
}
|
|
||||||
|
|
||||||
void basemaple::parse_from_MEM(char* instance) {
|
|
||||||
int vars, clauses;
|
|
||||||
vec<vec<int>> clause;
|
|
||||||
readinstance(instance, &vars, &clauses, clause);
|
|
||||||
maxvar = vars;
|
|
||||||
while (vars > solver->nVars()) solver->newVar();
|
|
||||||
MapleCOMSPS::vec<MapleCOMSPS::Lit> lits;
|
|
||||||
for (int i = 1; i <= clauses; i++) {
|
|
||||||
int l = clause[i].size();
|
|
||||||
lits.clear();
|
|
||||||
for (int j = 0; j < l; j++)
|
|
||||||
lits.push(MINI_LIT(clause[i][j]));
|
|
||||||
solver->addClause_(lits);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
int basemaple::get_conflicts() {
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
@ -1,33 +0,0 @@
|
|||||||
#include "basesolver.hpp"
|
|
||||||
|
|
||||||
namespace MapleCOMSPS
|
|
||||||
{
|
|
||||||
class SimpSolver;
|
|
||||||
class Lit;
|
|
||||||
template<class T> class vec;
|
|
||||||
}
|
|
||||||
|
|
||||||
class basemaple : public basesolver {
|
|
||||||
public:
|
|
||||||
void terminate();
|
|
||||||
void add(int l);
|
|
||||||
int solve();
|
|
||||||
int val(int l);
|
|
||||||
int configure(const char* name, int id);
|
|
||||||
|
|
||||||
int get_conflicts();
|
|
||||||
void parse_from_MEM(char* instance);
|
|
||||||
void exp_clause(void *cl, int lbd) {
|
|
||||||
puts("wrong");
|
|
||||||
}
|
|
||||||
bool imp_clause(shared_ptr<clause_store>cls, void *cl) {
|
|
||||||
puts("wrong");
|
|
||||||
}
|
|
||||||
|
|
||||||
basemaple(int id, light *light);
|
|
||||||
~basemaple();
|
|
||||||
|
|
||||||
MapleCOMSPS::SimpSolver* solver;
|
|
||||||
friend bool cbkLstechImportClause(void *, int *, MapleCOMSPS::vec<MapleCOMSPS::Lit> &);
|
|
||||||
friend void cbkLstechExportClause(void *, int, MapleCOMSPS::vec<MapleCOMSPS::Lit> &);
|
|
||||||
};
|
|
||||||
Loading…
x
Reference in New Issue
Block a user