#include "Strategy.h"
#include <iostream>

static const char *NOT = "not";
std::vector<std::string> Branches;
/**
 * Implement your search strategy.
 */

void recordBranches(z3::expr_vector &OldVec){
    for (auto && E : OldVec) {
        if(E.to_string().find('X') == std::string::npos){
            continue;
        }
        if(std::find(Branches.begin(), Branches.end(),E.to_string()) == Branches.end()){
            Branches.push_back(E.to_string().c_str());
        }
    }
}

void searchStrategy(z3::expr_vector &OldVec) {
    int i = OldVec.size()-1;
    if(i<0){
        return;
    }
    auto e = OldVec[i];
    if(e.to_string().find('X') == std::string::npos){
        OldVec.pop_back();
        searchStrategy(OldVec);
        return;
    }
    if(e.to_string().substr(1, 3) != NOT){
        std::string newExpr = e.to_string();
        if(newExpr.find("false") != std::string::npos){
            newExpr = newExpr.replace(newExpr.end()-6, newExpr.end()-1,"true");
        } else{
            newExpr = newExpr.replace(newExpr.end()-5, newExpr.end()-1,"false");
        }
        if(std::find(Branches.begin(), Branches.end(), newExpr) == Branches.end()){
            OldVec.pop_back();
            OldVec.push_back(not e);
        } else{
            OldVec.pop_back();
            searchStrategy(OldVec);
        }
    }
    else {
        OldVec.pop_back();
        searchStrategy(OldVec);
    }
}
