<commit_before>#include "Mus.h"
#include "WaspFacade.h"
#include "QuickXPlain.h"
#include "ReasoningPredicateMinimization.h"
#include <unordered_map>
#include <string>
#include <cassert>
#include <iostream>
using namespace std;

void MUS::enumeration() {
    assert(wasp::Options::predicatesMUS.size() > 0);
    for(unsigned int j = 1; j <= waspFacade.numberOfVariables(); j++) {     
        if(VariableNames::isHidden(j)) { continue; }
        const string& name = VariableNames::getName(j);
        for( unsigned int i = 0; i < wasp::Options::predicatesMUS.size(); i++ ) {
            if(Utils::startsWith(name, wasp::Options::predicatesMUS[i])) { waspFacade.freeze(j); candidates.push_back(j); break; }
        }
    }

    if(candidates.size() == 0) {        
        vector<Literal> assumptions;
        vector<Literal> conflict;
        unsigned int result = waspFacade.solve(assumptions, conflict);
        if(result == INCOHERENT)
            printMUS(assumptions, conflict);        
    }
    else {
        if(wasp::Options::musAlgorithm == MUS_EMAX) {
            enumerationEmax();            
        }
        else
            enumerationCaMUS();
    }
    printAnswers();
}

void MUS::enumerationEmax() {
    WaspFacade checkFormula;
    Solver& s = const_cast<Solver&>(checkFormula.getSolver());
    s.initFrom(waspFacade.getSolver());
    unordered_map<Var,Var> idsmap;
    vector<Literal> preferredChoices;

    for(unsigned int i = 0; i < candidates.size(); i++) {
        Var newId = checkFormula.addVariable(true);
        idsmap[candidates[i]] = newId;
        preferredChoices.push_back(Literal(newId, POSITIVE));
    }
    checkFormula.setPreferredChoices(preferredChoices);        

    while(true) {
        vector<Literal> assumptions;
        vector<Literal> conflict;
        unsigned int result = checkFormula.solve(assumptions, conflict);
        if(result == INCOHERENT) break;

        assumptions.clear();
        conflict.clear();
        vector<Literal> clause;
        for(unsigned int i = 0; i < candidates.size(); i++) {
            if(checkFormula.isTrue(idsmap[candidates[i]]))
                assumptions.push_back(Literal(candidates[i], POSITIVE));
            else
                clause.push_back(Literal(idsmap[candidates[i]]));
        }
        result = waspFacade.solve(assumptions, conflict);        
        if(result == INCOHERENT) {            
            if(!computeAndPrintMUS(conflict))
                break;
            for(unsigned int i = 0; i < conflict.size(); i++)
                conflict[i] = Literal(idsmap[conflict[i].getVariable()], NEGATIVE);
            checkFormula.addClause(conflict);
        }
        else {
            checkFormula.addClause(clause);
        }
    }
}

void MUS::enumerationCaMUS() {    
    vector<Literal> assumptions;
    vector<Literal> conflict;
    vector<Literal> cardinalityConstraint;
    vector<Literal> preferredChoices;
    WaspFacade allMCS;

    unsigned int maxId = 0;
    for(unsigned int i = 0; i < candidates.size(); i++) {
        cardinalityConstraint.push_back(Literal(candidates[i], POSITIVE));
        Var auxId = waspFacade.addVariable(true);
        VariableNames::setName(auxId, "aux" + to_string(i+1));
        cardinalityConstraint.push_back(Literal(auxId, POSITIVE));
        assumptions.push_back(Literal(auxId, NEGATIVE));
        preferredChoices.push_back(Literal(candidates[i], NEGATIVE));        
        if(candidates[i] > maxId) maxId = candidates[i];
    }    
    
    bool res_ = waspFacade.addCardinalityConstraint(cardinalityConstraint, candidates.size());
    if(!res_) {
        printMUS(vector<Literal>(), conflict);
        return;
    }
    while(allMCS.numberOfVariables() < maxId) allMCS.addVariable(true);
    
    unsigned int k = 0;
    unsigned int result;
    unsigned int numberOfMCSes = 0;    
    while(k < candidates.size()) {
        result = waspFacade.solve(assumptions, conflict);
        if(result == INCOHERENT) {
            assumptions[k] = assumptions[k].getOppositeLiteral();
            k++;
        }
        else {
            vector<Literal> mcs;
            for(unsigned int i = 0; i < candidates.size(); i++)
                if(waspFacade.isFalse(candidates[i])) {                    
                    mcs.push_back(Literal(candidates[i]));                    
                }
            waspFacade.addClause(mcs);
            allMCS.addClause(mcs);
            if(++numberOfMCSes >= wasp::Options::mcsThreshold) {
                numberOfMCSes = 0;
                allMCS.setPreferredChoices(preferredChoices);
                unsigned int currentNumberOfMUSes = 0;
                while(numberOfMUSes < wasp::Options::musNumberOfMuses) {
                    vector<Literal> tmpAssumptions;                
                    unsigned int result = allMCS.solve(tmpAssumptions, conflict);
                    if(result == COHERENT) {
                        vector<Literal> toTest;
                        for(unsigned int i = 0; i < candidates.size(); i++)
                            if(allMCS.isTrue(candidates[i]))
                                toTest.push_back(Literal(candidates[i], POSITIVE));
                        result = waspFacade.solve(toTest, conflict);
                        if(result == COHERENT) break;
                        printMUS(toTest, conflict);
                        currentNumberOfMUSes++;
                        numberOfMUSes++;
                        if(wasp::Options::maxModels != 0 && numberOfMUSes >= wasp::Options::maxModels)
                            return;
                        for(unsigned int i = 0; i < toTest.size(); i++)
                            toTest[i] = toTest[i].getOppositeLiteral();
                        waspFacade.addClause(toTest);
                        allMCS.addClause(toTest);                        
                    }
                    else {
                        break;
                    }
                }
                vector<Literal> reset;
                allMCS.setPreferredChoices(reset);
            }
        }
    }
    reasoning = new ReasoningPredicateMinimization(allMCS, numberOfMUSes, true);    
    reasoning->setPrefix("MUS");
    reasoning->addCandidates(candidates);
    reasoning->setMaxNumberOfModelsInEnumeration(1);
    reasoning->enumerationPreferences();
    reasoning->printTotalNumberOfModels();
}

/*void MUS::enumerationCaMUS() {    <commit_msg>Fixed another bug in CAMUS.<commit_after>#include "Mus.h"
#include "WaspFacade.h"
#include "QuickXPlain.h"
#include "ReasoningPredicateMinimization.h"
#include <unordered_map>
#include <string>
#include <cassert>
#include <iostream>
using namespace std;

void MUS::enumeration() {
    assert(wasp::Options::predicatesMUS.size() > 0);
    for(unsigned int j = 1; j <= waspFacade.numberOfVariables(); j++) {     
        if(VariableNames::isHidden(j)) { continue; }
        const string& name = VariableNames::getName(j);
        for( unsigned int i = 0; i < wasp::Options::predicatesMUS.size(); i++ ) {
            if(Utils::startsWith(name, wasp::Options::predicatesMUS[i])) { waspFacade.freeze(j); candidates.push_back(j); break; }
        }
    }

    if(candidates.size() == 0) {        
        vector<Literal> assumptions;
        vector<Literal> conflict;
        unsigned int result = waspFacade.solve(assumptions, conflict);
        if(result == INCOHERENT)
            printMUS(assumptions, conflict);        
    }
    else {
        if(wasp::Options::musAlgorithm == MUS_EMAX) {
            enumerationEmax();            
        }
        else
            enumerationCaMUS();
    }
    printAnswers();
}

void MUS::enumerationEmax() {
    WaspFacade checkFormula;
    Solver& s = const_cast<Solver&>(checkFormula.getSolver());
    s.initFrom(waspFacade.getSolver());
    unordered_map<Var,Var> idsmap;
    vector<Literal> preferredChoices;

    for(unsigned int i = 0; i < candidates.size(); i++) {
        Var newId = checkFormula.addVariable(true);
        idsmap[candidates[i]] = newId;
        preferredChoices.push_back(Literal(newId, POSITIVE));
    }
    checkFormula.setPreferredChoices(preferredChoices);        

    while(true) {
        vector<Literal> assumptions;
        vector<Literal> conflict;
        unsigned int result = checkFormula.solve(assumptions, conflict);
        if(result == INCOHERENT) break;

        assumptions.clear();
        conflict.clear();
        vector<Literal> clause;
        for(unsigned int i = 0; i < candidates.size(); i++) {
            if(checkFormula.isTrue(idsmap[candidates[i]]))
                assumptions.push_back(Literal(candidates[i], POSITIVE));
            else
                clause.push_back(Literal(idsmap[candidates[i]]));
        }
        result = waspFacade.solve(assumptions, conflict);        
        if(result == INCOHERENT) {            
            if(!computeAndPrintMUS(conflict))
                break;
            for(unsigned int i = 0; i < conflict.size(); i++)
                conflict[i] = Literal(idsmap[conflict[i].getVariable()], NEGATIVE);
            checkFormula.addClause(conflict);
        }
        else {
            checkFormula.addClause(clause);
        }
    }
}

void MUS::enumerationCaMUS() {    
    vector<Literal> assumptions;
    vector<Literal> conflict;
    vector<Literal> cardinalityConstraint;
    vector<Literal> preferredChoices;
    WaspFacade allMCS;

    unsigned int maxId = 0;
    for(unsigned int i = 0; i < candidates.size(); i++) {
        cardinalityConstraint.push_back(Literal(candidates[i], POSITIVE));
        Var auxId = waspFacade.addVariable(true);
        VariableNames::setName(auxId, "aux" + to_string(i+1));
        cardinalityConstraint.push_back(Literal(auxId, POSITIVE));
        assumptions.push_back(Literal(auxId, NEGATIVE));
        preferredChoices.push_back(Literal(candidates[i], NEGATIVE));        
        if(candidates[i] > maxId) maxId = candidates[i];
    }    
    
    bool res_ = waspFacade.addCardinalityConstraint(cardinalityConstraint, candidates.size());
    if(!res_) {
        printMUS(vector<Literal>(), conflict);
        return;
    }
    while(allMCS.numberOfVariables() < maxId) allMCS.addVariable(true);
    
    unsigned int k = 0;
    unsigned int result;
    unsigned int numberOfMCSes = 0;    
    while(k < candidates.size()) {
        result = waspFacade.solve(assumptions, conflict);
        if(result == INCOHERENT) {
            assumptions[k] = assumptions[k].getOppositeLiteral();
            k++;
        }
        else {
            vector<Literal> mcs;
            for(unsigned int i = 0; i < candidates.size(); i++)
                if(waspFacade.isFalse(candidates[i])) {                    
                    mcs.push_back(Literal(candidates[i]));                    
                }
            waspFacade.addClause(mcs);
            allMCS.addClause(mcs);
            if(++numberOfMCSes >= wasp::Options::mcsThreshold) {
                numberOfMCSes = 0;
                allMCS.setPreferredChoices(preferredChoices);
                unsigned int currentNumberOfMUSes = 0;
                while(numberOfMUSes < wasp::Options::musNumberOfMuses) {
                    vector<Literal> tmpAssumptions;                
                    unsigned int result = allMCS.solve(tmpAssumptions, conflict);
                    if(result == COHERENT) {
                        vector<Literal> toTest;
                        unsigned int nbCandidates = 0;
                        for(unsigned int i = 0; i < candidates.size(); i++)
                            if(allMCS.isTrue(candidates[i]))
                                toTest.push_back(Literal(candidates[i], POSITIVE));
                        nbCandidates = toTest.size();
                        for(unsigned int i = 0; i < assumptions.size(); i++)
                            toTest.push_back(Literal(assumptions[i].getVariable(), POSITIVE));
                        result = waspFacade.solve(toTest, conflict);
                        if(result == COHERENT) break;
                        toTest.resize(nbCandidates);                        
                        printMUS(toTest, conflict);
                        currentNumberOfMUSes++;
                        numberOfMUSes++;
                        if(wasp::Options::maxModels != 0 && numberOfMUSes >= wasp::Options::maxModels)
                            return;
                        for(unsigned int i = 0; i < toTest.size(); i++)
                            toTest[i] = toTest[i].getOppositeLiteral();
                        //waspFacade.addClause(toTest);
                        allMCS.addClause(toTest);                        
                    }
                    else {
                        break;
                    }
                }
                vector<Literal> reset;
                allMCS.setPreferredChoices(reset);
            }
        }
    }
    reasoning = new ReasoningPredicateMinimization(allMCS, numberOfMUSes, true);    
    reasoning->setPrefix("MUS");
    reasoning->addCandidates(candidates);
    reasoning->setMaxNumberOfModelsInEnumeration(1);
    reasoning->enumerationPreferences();
    reasoning->printTotalNumberOfModels();
}

/*void MUS::enumerationCaMUS() {    
{'fraction_non_alphanumeric': 0.11683511841906773, 'fraction_numerical': 0.003017046311660884, 'mean_word_length': 1.9735366674142185, 'pattern_counts': {'":': 0, '<': 70, '<?xml version=': 0, '>': 63, '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': '4347419', 'n_tokens_mistral': 3977, 'n_tokens_neox': 3787, 'n_words': 638}