cloud-sat/workers/basekissat.cpp

#include "basekissat.hpp"
#include "sharer.hpp"
#include <thread>
#include <condition_variable>

extern "C" {
   #include "src/application.h"
   #include "src/parse.h"
   #include "src/internal.h"
   #include "src/witness.h"
   #include "src/import.h"
}

void kissat_export_clause(void *solver, int lbd, cvec* c) {
    basekissat* S = (basekissat *) solver;
    ++S->x1;
    if (S->solver->nconflict != S->x1 - 1) printf("%d %d\n", S->solver->nconflict, S->x1);
    if (lbd > S->good_clause_lbd) return;
    clause_store* cls = new clause_store(c->sz);
    for (int i = 0; i < c->sz; i++) {
        int v = cvec_data(c, i);
        int eidx = PEEK_STACK(S->solver->exportk, (v >> 1));
        cls->data[i] = v & 1 ? -eidx : eidx;
    }
    ++S->x2;
    // if (S->id == 0) puts("");
    cls->lbd = lbd;
    S->export_clause.push(cls);
}

int kissat_import_clause(void *solver, int *lbd, cvec* c) {
    basekissat* S = (basekissat *) solver;
    clause_store* cls = NULL;
    if (S->import_clause.pop(cls) == false) return -1;

    bool eliminated = false;
    for (int i = 0; i < cls->size; i++) {
        // S->outimport << cls->data[i] << std::endl;
        int eidx = abs(cls->data[i]);
        import *import = &PEEK_STACK (S->solver->import, eidx);
        if (import->eliminated) {
            eliminated = true;
        }
        else {
            int ilit = import->lit;
            if (cls->data[i] < 0) ilit = ilit ^ 1;
            cvec_push(c, ilit);
        }
    }
    *lbd = cls->lbd;
    cls->free_clause();
    if (eliminated) return -10;
    return 1;
} 

void kissat_wait_sharing(void *solver) {
    basekissat* S = (basekissat *) solver;
    // printf("c %d into Light wait\n", S->id);
    S->x1 = S->x2 = 0;
    sharer *s = S->in_sharer;
    {
        boost::mutex::scoped_lock lock(s->mtx);
        if (s->terminated) return;
        s->waitings += 1;
        lock.unlock();
        // printf("c %d start wait with number %d\n", S->id, s->waitings);
    }
    if (s->should_sharing()) s->cond.notify_one(); 
    
    boost::mutex::scoped_lock lock(s->mtx);
    while (s->waitings > 0) {
        s->cond.wait(lock);
    }
    // printf("c %d finish sharing\n", S->id);
}

basekissat::basekissat(int id, light* light) : basesolver(id, light) {
    good_clause_lbd = 2;
    // outexport.open("export.txt");
    // outimport.open("import.txt");
    // outfree.open("free.txt");
    solver = kissat_init();
    solver -> issuer = this;
    solver -> cbkImportClause = NULL;
    solver -> cbkExportClause = NULL;
    solver -> cbkWaitSharing  = NULL;
    if (light->opt->share) {
        solver -> cbkImportClause = kissat_import_clause;
        solver -> cbkExportClause = kissat_export_clause;
        solver -> cbkWaitSharing  = kissat_wait_sharing;
    }
}

basekissat::~basekissat(){
    delete solver;
}

void basekissat::parse_dimacs(char* filename) {
    kissat_mab_parse(solver);
    strictness strict = NORMAL_PARSING;
    file in;
    uint64_t lineno;
    kissat_open_to_read_file(&in, filename);
    kissat_parse_dimacs(solver, strict, &in, &lineno, &solver->max_var);
    kissat_close_file(&in);
}

void basekissat::import_original_clause(preprocess* pre) {
    solver->max_var = pre->vars;
    kissat_mab_parse(solver);
    kissat_reserve(solver, pre->vars);
    for (int i = 1; i <= pre->clauses; i++) {
        int l = pre->clause[i].size();
        for (int j = 0; j < l; j++)
            kissat_add(solver, pre->clause[i][j]);
        kissat_add(solver, 0);
    }
}

void basekissat::diversity(int id) {
    if (id) solver->order_reset = id;
}

int  basekissat::solve() {
    return kissat_solve(solver);
}

void basekissat::terminate() {
    kissat_terminate(solver);
}

void basekissat::get_model(vec<int> &model) {
    model.clear();
    for (int i = 1; i <= solver->max_var; i++) {
      int tmp = kissat_value(solver, i);
      if (!tmp) tmp = i;
      model.push(tmp);
   }
}

int basekissat::get_reset_data() {
    return solver->best_assigned;
}

void basekissat::reset() {
    solver->reseting = 1;
}

void basekissat::export_clauses_to(vec<clause_store *> &clauses) {
    clause_store *cls;
    while (export_clause.pop(cls)) {
        clauses.push(cls);
        // outexport << id << ": ";
        // for (int i = 0; i < cls->size; i++)
        //     outexport << cls->data[i] << " ";
        // outexport << std::endl;
    }
}

void basekissat::import_clauses_from(vec<clause_store *> &clauses) {
    for (int i = 0; i < clauses.size(); i++) {
        import_clause.push(clauses[i]);
        // outimport << id << ": ";
        // for (int j = 0; j < clauses[i]->size; j++) 
        //     outimport << clauses[i]->data[j] << " ";
        // outimport << std::endl;
    }
}

void basekissat::broaden_export_limit() {
    // ++good_clause_lbd;
}

void basekissat::restrict_export_limit() {
    if (good_clause_lbd > 2)
        --good_clause_lbd;
}