<commit_before>/* CNF formula class. */
#include <vector>
#include <algorithm>
#include <iostream>
#include <fstream>
#include <cassert>
#include "cnfformula.h"
#include "assignment.h"
#include "structs.h"
#include "solvedcnf.h"

CNFFormula::CNFFormula(unsigned int n, int k, const std::vector<CNFClause> & clauses):n(n), k(k), clauses(clauses){
}

CNFFormula::CNFFormula(){}

bool CNFFormula::check_bitstring(const Assignment & bitstring) const {
  //we just check if it satisfies all clauses
  for(const auto & clause : clauses){
    if(!clause.check_bitstring(bitstring)){
      return false;
    }
  }
  return true;
}

void CNFFormula::add_clause(const CNFClause & clause){
  clauses.push_back(clause);
}

void CNFFormula::minimalize(){
  CNFFormula backup(*this);
  CNFFormula inprogress(*this);
  SolvedCNF solved(*this);

  std::random_shuffle(backup.begin(), backup.end());
  for(const auto & clause : backup){
    inprogress.clauses.erase(std::remove(inprogress.clauses.begin(), inprogress.clauses.end(), clause), std::end(inprogress.clauses));
    SolvedCNF tmpsolved(inprogress);
    if(tmpsolved.get_satisfying_assignments().size() != solved.get_satisfying_assignments().size()){
      inprogress.add_clause(clause);
    }
  }
  clauses = inprogress.clauses;
}

std::ostream& operator<<(std::ostream& out, const CNFFormula & formula){
  for(const auto & clause : formula.clauses){
    out << clause;<commit_msg>seed the random generator (oops)<commit_after>/* CNF formula class. */
#include <vector>
#include <algorithm>
#include <iostream>
#include <fstream>
#include <cassert>
#include <ctime>
#include <cstdlib>
#include "cnfformula.h"
#include "assignment.h"
#include "structs.h"
#include "solvedcnf.h"

CNFFormula::CNFFormula(unsigned int n, int k, const std::vector<CNFClause> & clauses):n(n), k(k), clauses(clauses){
}

CNFFormula::CNFFormula(){}

bool CNFFormula::check_bitstring(const Assignment & bitstring) const {
  //we just check if it satisfies all clauses
  for(const auto & clause : clauses){
    if(!clause.check_bitstring(bitstring)){
      return false;
    }
  }
  return true;
}

void CNFFormula::add_clause(const CNFClause & clause){
  clauses.push_back(clause);
}

void CNFFormula::minimalize(){
  CNFFormula backup(*this);
  CNFFormula inprogress(*this);
  SolvedCNF solved(*this);
  std::srand(unsigned (std::time(0)));
  std::random_shuffle(backup.begin(), backup.end());
  for(const auto & clause : backup){
    inprogress.clauses.erase(std::remove(inprogress.clauses.begin(), inprogress.clauses.end(), clause), std::end(inprogress.clauses));
    SolvedCNF tmpsolved(inprogress);
    if(tmpsolved.get_satisfying_assignments().size() != solved.get_satisfying_assignments().size()){
      inprogress.add_clause(clause);
    }
  }
  clauses = inprogress.clauses;
}

std::ostream& operator<<(std::ostream& out, const CNFFormula & formula){
  for(const auto & clause : formula.clauses){
    out << clause;
{'fraction_non_alphanumeric': 0.15198911934716083, 'fraction_numerical': 0.00034002040122407346, 'mean_word_length': 5.5377777777777775, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2836944', 'n_tokens_mistral': 1045, 'n_tokens_neox': 1026, 'n_words': 203}