<commit_before>
#include <iostream>
#include <fstream>
#include <set>
#include <algorithm>
#include "SatWrapper.hpp"


Lit Lit_True;
Lit Lit_False;


void addAMOClauses(Lits literals, Lits auxiliary, SatWrapperSolver *solver, EncodingConfiguration::AMOEncoding amo_encoding){
    /*
        'literals' is the vector of literals for which we are constraining AMO to be true.
        'auxiliary' is a vector of aux variables used for encodings such as the ladder encoding.
            If the ladder encoding is used then 'auxiliary' should contain literals.size()-1
            literals, or else 0 in which case auxiliary variables will be created.
    */
    Lits lits;
    if(amo_encoding == EncodingConfiguration::Pairwise){
        for(unsigned int i=0; i<literals.size(); i++){
            for(unsigned int j=i+1; j<literals.size(); j++){
                lits.clear();
                lits.push_back(~(literals[i]));
                lits.push_back(~(literals[j]));
                solver->addClause(lits);
            }
        }
    } else if(amo_encoding == EncodingConfiguration::Ladder){
        if(auxiliary.size() == 0){
            for(unsigned int i=0; i<literals.size()-1; i++){
                Lit l = Lit(solver->create_atom(NULL,0));
                auxiliary.push_back(l);
                if(i > 0){
                    // chain the bounds x<=i -> x<=i+1
                    lits.clear();
                    lits.push_back(~(auxiliary[i-1]));
                    lits.push_back(l);
                    solver->addClause(lits);
                }
            }
        } else if(auxiliary.size() != literals.size() - 1){
            std::cerr << "ERROR: mismatch in size of auxiliary literals to liters when using ladder encoding." << std::endl;
            exit(1);
        }
        for(unsigned int i=0; i<literals.size(); ++i) {
            // channel x=i -> x>i-1
            if(i) {
                lits.clear();
                lits.push_back(~(literals[i]));
                lits.push_back(~(auxiliary[i-1]));
                solver->addClause(lits);
            }

            // channel x=i -> x<=i
            if(i<literals.size()-1) {
                lits.clear();
                lits.push_back(~literals[i]);
                lits.push_back(auxiliary[i]);
                solver->addClause(lits);<commit_msg>Spelling typo in error message.<commit_after>
#include <iostream>
#include <fstream>
#include <set>
#include <algorithm>
#include "SatWrapper.hpp"


Lit Lit_True;
Lit Lit_False;


void addAMOClauses(Lits literals, Lits auxiliary, SatWrapperSolver *solver, EncodingConfiguration::AMOEncoding amo_encoding){
    /*
        'literals' is the vector of literals for which we are constraining AMO to be true.
        'auxiliary' is a vector of aux variables used for encodings such as the ladder encoding.
            If the ladder encoding is used then 'auxiliary' should contain literals.size()-1
            literals, or else 0 in which case auxiliary variables will be created.
    */
    Lits lits;
    if(amo_encoding == EncodingConfiguration::Pairwise){
        for(unsigned int i=0; i<literals.size(); i++){
            for(unsigned int j=i+1; j<literals.size(); j++){
                lits.clear();
                lits.push_back(~(literals[i]));
                lits.push_back(~(literals[j]));
                solver->addClause(lits);
            }
        }
    } else if(amo_encoding == EncodingConfiguration::Ladder){
        if(auxiliary.size() == 0){
            for(unsigned int i=0; i<literals.size()-1; i++){
                Lit l = Lit(solver->create_atom(NULL,0));
                auxiliary.push_back(l);
                if(i > 0){
                    // chain the bounds x<=i -> x<=i+1
                    lits.clear();
                    lits.push_back(~(auxiliary[i-1]));
                    lits.push_back(l);
                    solver->addClause(lits);
                }
            }
        } else if(auxiliary.size() != literals.size() - 1){
            std::cerr << "ERROR: mismatch in size of auxiliary literals to literals when using ladder encoding." << std::endl;
            exit(1);
        }
        for(unsigned int i=0; i<literals.size(); ++i) {
            // channel x=i -> x>i-1
            if(i) {
                lits.clear();
                lits.push_back(~(literals[i]));
                lits.push_back(~(auxiliary[i-1]));
                solver->addClause(lits);
            }

            // channel x=i -> x<=i
            if(i<literals.size()-1) {
                lits.clear();
                lits.push_back(~literals[i]);
                lits.push_back(auxiliary[i]);
                solver->addClause(lits);
{'fraction_non_alphanumeric': 0.1315004262574595, 'fraction_numerical': 0.007246376811594203, 'mean_word_length': 1.7868171021377672, 'pattern_counts': {'":': 0, '<': 35, '<?xml version=': 0, '>': 31, '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': '7366777', 'n_tokens_mistral': 1455, 'n_tokens_neox': 1380, 'n_words': 325}