cloud-sat/workers/basekissat.hpp

#include "basesolver.hpp"
#include "clause.hpp"
#include <boost/thread/thread.hpp>
#include <boost/lockfree/spsc_queue.hpp>

struct kissat;
struct cvec;

class basekissat : public basesolver {
public:
    void parse_dimacs(char* filename);
    void import_original_clause(preprocess *pre);
    void diversity(int id);
    void terminate();
    int  solve();
    void get_model(vec<int> &model);
    int  get_reset_data();
    void reset();
    void export_clauses_to(vec<clause_store *> &clauses);
    void import_clauses_from(vec<clause_store *> &clauses);
    void broaden_export_limit();
    void restrict_export_limit();

    basekissat(int id, light *light);
    ~basekissat();
    int x1 = 0, x2 = 0;
    kissat* solver;
    int good_clause_lbd = 0;
    
    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> import_clause;
    boost::lockfree::spsc_queue<clause_store*, boost::lockfree::capacity<1024000>> export_clause;
    friend int cbkImportClause(void *, int *, cvec *);
    friend int cbkExportClause(void *, int *, cvec *);
    friend void cbkWaitSharing(void *);
    std::ofstream outimport;
    std::ofstream outexport;
    std::ofstream outfree;
};