#pragma once

#include <vector>
#include <unordered_map>
#include <unordered_set>

#include "circuit.h"

class Clause {
public:
int satisfied_lit_count;
int weight;
static ll total_cost;
std::vector<int> lits;
void update_satisfied_lit_count();
};

namespace ClauseLS {

    extern int num_vars;
    extern int num_clauses;

    extern std::vector<Clause*> clauses;
    extern std::vector<Clause*> *lit_related_clauses;
    extern int *lit_value;
    extern int *CC;
    extern int *score;
    extern std::unordered_set<Clause*> satisfied_clauses;
    extern std::unordered_set<Clause*> falsified_clauses;

    void init_data_structs(Circuit* circuit);
    void reset_data_structs();
    void add_to_tmp_clause(int x);
    void build_clauses(Circuit* circuit);

    void write_cnf();

    void flip(int var);

}