diff --git a/src/solve.cpp b/src/solve.cpp index 2bc585b..404f535 100644 --- a/src/solve.cpp +++ b/src/solve.cpp @@ -276,10 +276,10 @@ void light::seperate_groups() { int worker_procs = num_procs - 1; if(worker_procs >= 8) { - int sat_procs = worker_procs / 8; - int unsat_procs = worker_procs / 4; - int lstech_procs = 3; - int default_procs = worker_procs - sat_procs - unsat_procs - lstech_procs; + int sat_procs = worker_procs / 8; // 8 + int unsat_procs = worker_procs / 4; // 16 + int maple_procs = worker_procs / 8; // 8 + int default_procs = worker_procs - sat_procs - unsat_procs - maple_procs; // 32 std::vector tmp; @@ -305,25 +305,25 @@ void light::seperate_groups() { sharing_groups.push_back(tmp); - // [sat_procs+unsat_procs+1, sat_procs+unsat_procs+lstech_procs] for ls-tech - if(rank >= sat_procs+unsat_procs+1 && rank <= sat_procs+unsat_procs+lstech_procs) { + // [sat_procs+1, sat_procs+maple_procs] for ls-tech + if(rank >= sat_procs+unsat_procs+1 && rank <= sat_procs+unsat_procs+maple_procs) { solver_type = MAPLE; - OPT(share) = 0; + worker_type = light::UNSAT; } 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); } sharing_groups.push_back(tmp); // [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; } 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); } sharing_groups.push_back(tmp); diff --git a/src/solver_api/baselstech.cpp b/src/solver_api/baselstech.cpp deleted file mode 100755 index 093a7b9..0000000 --- a/src/solver_api/baselstech.cpp +++ /dev/null @@ -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 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 &cls) { - basemaple* mp = (basemaple*)issuer; - if (lbd > mp->good_clause_lbd) return; - - shared_ptr ncls = std::make_shared(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 & mcls) { - basemaple* mp = (basemaple*)issuer; - shared_ptr 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> clause; - readinstance(instance, &vars, &clauses, clause); - maxvar = vars; - while (vars > solver->nVars()) solver->newVar(); - MapleCOMSPS::vec 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; -} \ No newline at end of file diff --git a/src/solver_api/baselstech.hpp b/src/solver_api/baselstech.hpp deleted file mode 100755 index e8be60b..0000000 --- a/src/solver_api/baselstech.hpp +++ /dev/null @@ -1,33 +0,0 @@ -#include "basesolver.hpp" - -namespace MapleCOMSPS -{ - class SimpSolver; - class Lit; - template 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_ptrcls, void *cl) { - puts("wrong"); - } - - basemaple(int id, light *light); - ~basemaple(); - - MapleCOMSPS::SimpSolver* solver; - friend bool cbkLstechImportClause(void *, int *, MapleCOMSPS::vec &); - friend void cbkLstechExportClause(void *, int, MapleCOMSPS::vec &); -};