type.h

Go to the documentation of this file.

 
#pragma once
#include <unordered_map>
#include <unordered_set>
#include <utility>
 
#include "utils.h"
 
namespace gymbo {
 
using Word32 = uint32_t;
 
enum class InstrType {
    Add,
    Sub,
    Mul,
    JmpIf,
    Jmp,
    And,
    Or,
    Not,
    Lt,
    Le,
    Eq,
    Push,
    Store,
    Load,
    Pop,
    Read,
    Print,
    Swap,
    Dup,
    Over,
    RotL,
    Done,
    Nop,
};
 
class Instr {
   public:
    InstrType instr;
    Word32 word;
 
    Instr(InstrType instr) : instr(instr) {}
 
    Instr(InstrType instr, Word32 word) : instr(instr), word(word) {}
 
    void print() const { printf("%s\n", toString().c_str()); }
 
    std::string toString() const {
        switch (instr) {
            case (InstrType::Add): {
                return "add";
            }
            case (InstrType::Sub): {
                return "sub";
            }
            case (InstrType::Mul): {
                return "mul";
            }
            case (InstrType::And): {
                return "and";
            }
            case (InstrType::Or): {
                return "or";
            }
            case (InstrType::Not): {
                return "not";
            }
            case (InstrType::JmpIf): {
                return "jmpIf";
            }
            case (InstrType::Jmp): {
                return "jmp";
            }
            case (InstrType::Lt): {
                return "lt";
            }
            case (InstrType::Le): {
                return "le";
            }
            case (InstrType::Load): {
                return "load";
            }
            case (InstrType::Read): {
                return "read";
            }
            case (InstrType::Done): {
                return "ret";
            }
            case (InstrType::Nop): {
                return "nop";
            }
            case (InstrType::Swap): {
                return "swap";
            }
            case (InstrType::Store): {
                return "store";
            }
            case (InstrType::Push): {
                return "push " + std::to_string(word);
            }
            default: {
                return "unknown";
            }
        }
    }
};
 
using Prog = std::vector<Instr>;
 
using Mem = std::unordered_map<Word32, Word32>;
 
struct Grad {
    std::unordered_map<int, float>
        val; 
    Grad(std::unordered_map<int, float> val) : val(val) {}
 
    Grad operator+(const Grad &other) {
        std::unordered_map<int, float> result = val;
        for (auto &r : result) {
            if (other.val.find(r.first) != other.val.end()) {
                result.at(r.first) += other.val.at(r.first);
            }
        }
        for (auto &r : other.val) {
            if (result.find(r.first) == result.end()) {
                result.emplace(std::make_pair(r.first, r.second));
            }
        }
        return Grad(result);
    }
 
    Grad operator+(float w) {
        std::unordered_map<int, float> result = val;
        for (auto &r : result) {
            result.at(r.first) += w;
        }
        return Grad(result);
    }
 
    Grad operator-(const Grad &other) {
        std::unordered_map<int, float> result = val;
        for (auto &r : result) {
            if (other.val.find(r.first) != other.val.end()) {
                result.at(r.first) -= other.val.at(r.first);
            }
        }
        for (auto &r : other.val) {
            if (result.find(r.first) == result.end()) {
                result.emplace(std::make_pair(r.first, -1.0f * r.second));
            }
        }
        return Grad(result);
    }
 
    Grad operator*(float w) {
        std::unordered_map<int, float> result = val;
        for (auto &r : result) {
            result.at(r.first) *= w;
        }
        return Grad(result);
    }
 
    Grad abs() {
        std::unordered_map<int, float> result = val;
        for (auto &r : result) {
            result.emplace(std::make_pair(r.first, std::abs(r.second)));
        }
        return Grad(result);
    }
};
 
enum class SymType {
    SAdd,
    SSub,
    SMul,
    SEq,
    SNot,
    SOr,
    SCon,
    SCnt,
    SAnd,
    SLt,
    SLe,
    SAny
};
 
struct Sym {
    SymType symtype; 
    Sym *left;       
    Sym *right;      
    Word32 word;     
    int var_idx; 
    std::unordered_map<int, float>
        assign; 
    Sym() {}
 
    Sym(SymType symtype, Sym *left) : symtype(symtype), left(left) {}
 
    Sym(SymType symtype, Sym *left, std::unordered_map<int, float> &assign)
        : symtype(symtype), left(left), assign(assign) {}
 
    Sym(SymType symtype, Sym *left, Sym *right)
        : symtype(symtype), left(left), right(right) {}
 
    Sym(SymType symtype, Word32 val) : symtype(symtype) {
        if (symtype == SymType::SAny) {
            var_idx = val;
        } else {
            word = val;
        }
    }
 
    Sym(SymType symtype, Sym *left, Sym *right, Word32 word, int var_idx)
        : symtype(symtype),
          left(left),
          right(right),
          word(word),
          var_idx(var_idx) {}
 
    Sym *copy() { return new Sym(symtype, left, right, word, var_idx); }
 
    void gather_var_ids(std::unordered_set<int> &result) const {
        switch (symtype) {
            case (SymType::SAdd): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SSub): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SMul): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SAny): {
                result.emplace(var_idx);
                return;
            }
            case (SymType::SEq): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SNot): {
                left->gather_var_ids(result);
                return;
            }
            case (SymType::SCnt): {
                left->gather_var_ids(result);
                for (auto &a : assign) {
                    result.erase(a.first);
                }
                return;
            }
            case (SymType::SAnd): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SOr): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SLt): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            case (SymType::SLe): {
                left->gather_var_ids(result);
                right->gather_var_ids(result);
                return;
            }
            default:
                return;
        }
    }
 
    Sym *psimplify(const Mem &cvals) {
        Sym *tmp_left, *tmp_right;
 
        switch (symtype) {
            case (SymType::SAny): {
                if (cvals.find(var_idx) != cvals.end()) {
                    return new Sym(SymType::SCon, cvals.at(var_idx));
                } else {
                    return this;
                }
            }
            case (SymType::SAdd): {
                if (left->symtype == SymType::SCon &&
                    right->symtype == SymType::SCon) {
                    return new Sym(SymType::SCon,
                                   FloatToWord(wordToFloat(left->word) +
                                               wordToFloat(right->word)));
                } else {
                    tmp_left = left->psimplify(cvals);
                    tmp_right = right->psimplify(cvals);
                    if (tmp_left->symtype == SymType::SCon &&
                        tmp_right->symtype == SymType::SCon) {
                        return new Sym(
                            SymType::SCon,
                            FloatToWord(wordToFloat(tmp_left->word) +
                                        wordToFloat(tmp_right->word)));
                    }
                    return new Sym(SymType::SAdd, tmp_left, tmp_right);
                }
            }
            case (SymType::SSub): {
                if (left->symtype == SymType::SCon &&
                    right->symtype == SymType::SCon) {
                    return new Sym(SymType::SCon,
                                   FloatToWord(wordToFloat(left->word) -
                                               wordToFloat(right->word)));
                } else {
                    tmp_left = left->psimplify(cvals);
                    tmp_right = right->psimplify(cvals);
                    if (tmp_left->symtype == SymType::SCon &&
                        tmp_right->symtype == SymType::SCon) {
                        return new Sym(
                            SymType::SCon,
                            FloatToWord(wordToFloat(tmp_left->word) -
                                        wordToFloat(tmp_right->word)));
                    }
                    return new Sym(SymType::SSub, tmp_left, tmp_right);
                }
            }
            case (SymType::SMul): {
                if (left->symtype == SymType::SCon &&
                    right->symtype == SymType::SCon) {
                    return new Sym(SymType::SCon,
                                   FloatToWord(wordToFloat(left->word) *
                                               wordToFloat(right->word)));
                } else {
                    tmp_left = left->psimplify(cvals);
                    tmp_right = right->psimplify(cvals);
                    if (tmp_left->symtype == SymType::SCon &&
                        tmp_right->symtype == SymType::SCon) {
                        return new Sym(
                            SymType::SCon,
                            FloatToWord(wordToFloat(tmp_left->word) *
                                        wordToFloat(tmp_right->word)));
                    }
                    return new Sym(SymType::SMul, tmp_left, tmp_right);
                }
            }
            case (SymType::SEq): {
                return new Sym(SymType::SEq, left->psimplify(cvals),
                               right->psimplify(cvals));
            }
            case (SymType::SAnd): {
                return new Sym(SymType::SAnd, left->psimplify(cvals),
                               right->psimplify(cvals));
            }
            case (SymType::SOr): {
                return new Sym(SymType::SOr, left->psimplify(cvals),
                               right->psimplify(cvals));
            }
            case (SymType::SLt): {
                return new Sym(SymType::SLt, left->psimplify(cvals),
                               right->psimplify(cvals));
            }
            case (SymType::SLe): {
                return new Sym(SymType::SLe, left->psimplify(cvals),
                               right->psimplify(cvals));
            }
            case (SymType::SNot): {
                return new Sym(SymType::SNot, left->psimplify(cvals));
            }
            case (SymType::SCnt): {
                return new Sym(SymType::SCnt, left->psimplify(cvals));
            }
            default: {
                return this;
            }
        }
    }
 
    float eval(const std::unordered_map<int, float> &cvals,
               const float eps) const {
        switch (symtype) {
            case (SymType::SAdd): {
                return left->eval(cvals, eps) + right->eval(cvals, eps);
            }
            case (SymType::SSub): {
                return left->eval(cvals, eps) - right->eval(cvals, eps);
            }
            case (SymType::SMul): {
                return left->eval(cvals, eps) * right->eval(cvals, eps);
            }
            case (SymType::SCon): {
                return wordToFloat(word);
            }
            case (SymType::SCnt): {
                switch (left->symtype) {
                    case (SymType::SAdd): {
                        return 1;
                    }
                    case (SymType::SSub): {
                        return 1;
                    }
                    case (SymType::SMul): {
                        return 1;
                    }
                    case (SymType::SCon): {
                        return 1;
                    }
                    case (SymType::SCnt): {
                        return 1;
                    }
                    case (SymType::SAny): {
                        return 1;
                    }
                    default: {
                        std::unordered_map<int, float> nvals(cvals);
                        for (const auto &a : assign) {
                            nvals.emplace(a.first, a.second);
                        }
                        if (left->eval(nvals, eps) <= 0.0f) {
                            return 1.0f;
                        } else {
                            return 0.0;
                        }
                    }
                }
            }
            case (SymType::SAny): {
                if (cvals.find(var_idx) != cvals.end()) {
                    return cvals.at(var_idx);
                } else {
                    fprintf(stderr,
                            "\x1b[33m Warning!! var_%d should be specified to "
                            "correctly evaluate this "
                            "symbolic expression\x1b[39m\n",
                            var_idx);
                    return 0;
                }
            }
            case (SymType::SEq): {
                return std::abs(left->eval(cvals, eps) -
                                right->eval(cvals, eps));
            }
            case (SymType::SNot): {
                return left->eval(cvals, eps) * (-1.0f) + eps;
            }
            case (SymType::SAnd): {
                return std::max(left->eval(cvals, eps),
                                right->eval(cvals, eps));
            }
            case (SymType::SOr): {
                return std::min(left->eval(cvals, eps),
                                right->eval(cvals, eps));
            }
            case (SymType::SLt): {
                return left->eval(cvals, eps) - right->eval(cvals, eps) + eps;
            }
            case (SymType::SLe): {
                return left->eval(cvals, eps) - right->eval(cvals, eps);
            }
            default: {
                return 0.0f;
            }
        }
    }
 
    Grad grad(const std::unordered_map<int, float> &cvals,
              const float eps) const {
        switch (symtype) {
            case (SymType::SAdd): {
                return left->grad(cvals, eps) + right->grad(cvals, eps);
            }
            case (SymType::SSub): {
                return left->grad(cvals, eps) - right->grad(cvals, eps);
            }
            case (SymType::SMul): {
                return left->grad(cvals, eps) * right->eval(cvals, eps) +
                       right->grad(cvals, eps) * left->eval(cvals, eps);
            }
            case (SymType::SCon): {
                return Grad({});
            }
            case (SymType::SCnt): {
                switch (left->symtype) {
                    case (SymType::SAdd): {
                        return Grad({});
                    }
                    case (SymType::SSub): {
                        return Grad({});
                    }
                    case (SymType::SMul): {
                        return Grad({});
                    }
                    case (SymType::SCon): {
                        return Grad({});
                    }
                    case (SymType::SCnt): {
                        return Grad({});
                    }
                    case (SymType::SAny): {
                        return Grad({});
                    }
                    default: {
                        std::unordered_map<int, float> nvals(cvals);
                        for (const auto &a : assign) {
                            nvals.emplace(a.first, a.second);
                        }
                        if (left->eval(nvals, eps) <= 0.0f) {
                            return left->grad(nvals, eps);
                        } else {
                            return left->grad(nvals, eps) * -1;
                        }
                    }
                }
            }
            case (SymType::SAny): {
                std::unordered_map<int, float> tmp = {{var_idx, 1.0f}};
                return Grad(tmp);
            }
            case (SymType::SEq): {
                float lv = left->eval(cvals, eps);
                float rv = right->eval(cvals, eps);
                Grad lg = left->grad(cvals, eps);
                Grad rg = right->grad(cvals, eps);
                if (lv == rv) {
                    return Grad({});
                } else if (lv > rv) {
                    return lg - rg;
                } else {
                    return rg - lg;
                }
            }
            case (SymType::SNot): {
                return left->grad(cvals, eps) * (-1.0f);
            }
            case (SymType::SAnd): {
                if (left->eval(cvals, eps) < right->eval(cvals, eps)) {
                    return right->grad(cvals, eps);
                } else {
                    return left->grad(cvals, eps);
                }
            }
            case (SymType::SOr): {
                if (left->eval(cvals, eps) > right->eval(cvals, eps)) {
                    return right->grad(cvals, eps);
                } else {
                    return left->grad(cvals, eps);
                }
            }
            case (SymType::SLt): {
                return left->grad(cvals, eps) - right->grad(cvals, eps);
            }
            case (SymType::SLe): {
                return left->grad(cvals, eps) - right->grad(cvals, eps);
            }
            default: {
                return Grad({});
            }
        }
    }
 
    std::string toString(bool convert_to_num) const {
        std::string result = "";
        float tmp_word;
 
        switch (symtype) {
            case (SymType::SAdd): {
                result = "(" + left->toString(convert_to_num) + "+" +
                         right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SSub): {
                result = "(" + left->toString(convert_to_num) + "-" +
                         right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SMul): {
                result = "(" + left->toString(convert_to_num) + "*" +
                         right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SCon): {
                if (convert_to_num) {
                    tmp_word = wordToFloat(word);
                    if (is_integer(tmp_word)) {
                        result += std::to_string((int)tmp_word);
                    } else {
                        result += std::to_string(tmp_word);
                    }
                } else {
                    result += std::to_string(word);
                }
                break;
            }
            case (SymType::SCnt): {
                result = "[" + left->toString(convert_to_num);
                if (assign.size() != 0) {
                    result += "{";
                    for (const auto &a : assign) {
                        result += std::to_string(a.first) + "->";
                        float tmp = a.second;
                        if (is_integer(tmp)) {
                            result += std::to_string((int)tmp) + ",";
                        } else {
                            result += std::to_string(tmp) + ",";
                        }
                    }
                    result += "}";
                }
                result += "]";
                return result;
            }
            case (SymType::SAny): {
                result += "var_" + std::to_string(var_idx);
                break;
            }
            case (SymType::SEq): {
                result += "(" + left->toString(convert_to_num) +
                          "==" + right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SNot): {
                result += "!" + left->toString(convert_to_num) + "";
                break;
            }
            case (SymType::SAnd): {
                result += "(" + left->toString(convert_to_num) + "&&" +
                          right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SOr): {
                result += "(" + left->toString(convert_to_num) + "||" +
                          right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SLt): {
                result += "(" + left->toString(convert_to_num) + "<" +
                          right->toString(convert_to_num) + ")";
                break;
            }
            case (SymType::SLe): {
                result += "(" + left->toString(convert_to_num) +
                          "<=" + right->toString(convert_to_num) + ")";
                break;
            }
        }
        return result;
    }
};
 
struct DiscreteDist {
    std::vector<int> vals;    
    std::vector<float> probs; 
    DiscreteDist() {}
};
 
struct DiscreteUniformDist : public DiscreteDist {
    int low;  
    int high; 
    DiscreteUniformDist(int low, int high) : low(low), high(high) {
        float p = 1.0f / (1.0f + (float)high - (float)low);
        for (int i = low; i <= high; i++) {
            vals.emplace_back(i);
            probs.emplace_back(p);
        }
    }
};
 
struct BernoulliDist : public DiscreteDist {
    float p ;
 
    BernoulliDist(float p) : p(p) {
        vals = {0, 1};
        probs = {1 - p, p};
    }
};
 
struct BinomialDist : public DiscreteDist {
    int n;   
    float p; 
    BinomialDist(int n, float p) : n(n), p(p) {
        std::vector<std::vector<long long>> v(n + 1,
                                              std::vector<long long>(n + 1, 0));
        for (int i = 0; i < v.size(); i++) {
            v[i][0] = 1;
            v[i][i] = 1;
        }
        for (int j = 1; j < v.size(); j++) {
            for (int k = 1; k < j; k++) {
                v[j][k] = (v[j - 1][k - 1] + v[j - 1][k]);
            }
        }
 
        for (int i = 0; i <= n; i++) {
            vals.emplace_back(i);
            probs.emplace_back((float)v[n][i] * std::pow(p, (float)i) *
                               std::pow(1.0f - p, (float)n - (float)i));
        }
    }
};
 
using SMem = std::unordered_map<Word32, Sym>;
 
struct SymProb {
    Sym *numerator;   
    Sym *denominator; 
    SymProb()
        : numerator(new Sym(SymType::SCon, FloatToWord(1.0f))),
          denominator(new Sym(SymType::SCon, FloatToWord(1.0f))) {}
 
    SymProb(Sym *numerator, Sym *denominator)
        : numerator(numerator), denominator(denominator) {}
 
    std::string toString() {
        return "(" + numerator->toString(true) + ")/(" +
               denominator->toString(true) + ")";
    }
 
    SymProb operator*(SymProb other) {
        if (denominator->toString(true) == other.numerator->toString(true)) {
            return SymProb(numerator, other.denominator);
        } else if (numerator->toString(true) ==
                   other.denominator->toString(true)) {
            return SymProb(other.numerator, denominator);
        } else {
            return SymProb(
                new Sym(SymType::SMul, numerator, (other.numerator)),
                new Sym(SymType::SMul, denominator, (other.denominator)));
        }
    }
 
    SymProb *pmul(SymProb *other) {
        if (denominator->toString(true) == other->numerator->toString(true)) {
            return new SymProb(numerator, other->denominator);
        } else if (numerator->toString(true) ==
                   other->denominator->toString(true)) {
            return new SymProb(other->numerator, denominator);
        } else {
            return new SymProb(
                new Sym(SymType::SMul, numerator, (other->numerator)),
                new Sym(SymType::SMul, denominator, (other->denominator)));
        }
    }
 
    std::pair<Sym *, Sym *> marginalize(
        std::unordered_map<int, DiscreteDist> &var2dist,
        std::vector<std::vector<int>> &D) {
        int total_num_pvar_combinations = D.size();
        Sym *q_numerator = new Sym(SymType::SCon, FloatToWord(0.0f));
        Sym *q_denominator = new Sym(SymType::SCon, FloatToWord(0.0f));
 
        for (int i = 0; i < total_num_pvar_combinations; i++) {
            int j = 0;
            float tmp_p = 1.0f;
            std::unordered_map<int, float> tmp_assign;
            for (auto &vd : var2dist) {
                tmp_assign.emplace(vd.first, D[i][j]);
                tmp_p *= vd.second.probs[j];
                j++;
            }
            Sym *weight = new Sym(SymType::SCon, FloatToWord(tmp_p));
            q_numerator =
                new Sym(SymType::SAdd, q_numerator,
                        new Sym(SymType::SMul, weight,
                                new Sym(SymType::SCnt, numerator, tmp_assign)));
            q_denominator = new Sym(
                SymType::SAdd, q_denominator,
                new Sym(SymType::SMul, weight,
                        new Sym(SymType::SCnt, denominator, tmp_assign)));
        }
 
        return std::make_pair(q_numerator, q_denominator);
    }
 
    float eval(std::unordered_map<int, float> &params, float eps,
               std::unordered_map<int, DiscreteDist> &var2dist,
               std::vector<std::vector<int>> &D) {
        std::pair<Sym *, Sym *> mq = marginalize(var2dist, D);
        Sym *q_n = mq.first;
        Sym *q_d = mq.second;
 
        float v_n = q_n->eval(params, eps);
        float v_d = q_d->eval(params, eps);
 
        if (v_d == 0.0f) {
            return 0.0f;
        } else {
            return v_n / v_d;
        }
    }
 
    Sym query(SymType symtype, Sym &other,
              std::unordered_map<int, DiscreteDist> &var2dist,
              std::vector<std::vector<int>> &D) {
        std::pair<Sym *, Sym *> mq = marginalize(var2dist, D);
        Sym *q_left = mq.first;
        Sym *q_right = mq.second;
        q_right = new Sym(SymType::SMul, q_right, &other);
        return Sym(symtype, q_left, q_right);
    }
};
 
struct SymState {
    int pc;                         
    int var_cnt;                    
    Mem mem;                        
    SMem smem;                      
    Linkedlist<Sym> symbolic_stack; 
    std::vector<Sym>
        path_constraints; 
    SymProb *p;           
    SymProb *cond_p; 
    bool has_observed_p_cond 
        ;
 
    SymState()
        : pc(0),
          var_cnt(0),
          p(new SymProb()),
          cond_p(new SymProb()),
          has_observed_p_cond(false){};
 
    SymState(int pc, int var_cnt, Mem &mem, SMem &smem,
             Linkedlist<Sym> &symbolic_stack,
             std::vector<Sym> &path_constraints, SymProb *p, SymProb *cond_p,
             bool has_observed_p_cond)
        : pc(pc),
          var_cnt(var_cnt),
          mem(mem),
          smem(smem),
          symbolic_stack(symbolic_stack),
          path_constraints(path_constraints),
          p(p),
          cond_p(cond_p),
          has_observed_p_cond(has_observed_p_cond) {}
 
    SymState *copy() {
        return new SymState(pc, var_cnt, mem, smem, symbolic_stack,
                            path_constraints, p, cond_p, has_observed_p_cond);
    }
 
    void set_concrete_val(int var_id, float val) {
        mem.emplace(var_id, FloatToWord(val));
    }
 
    std::string toString(bool include_memory = true) const {
        std::string expr = "";
 
        if (include_memory) {
            expr += "Concrete Memory: {";
            float tmp_word;
            for (auto &t : mem) {
                tmp_word = wordToFloat(t.second);
                if (is_integer(tmp_word)) {
                    expr += ("var_" + std::to_string(((int)t.first)) + ": " +
                             std::to_string((int)tmp_word)) +
                            ", ";
                } else {
                    expr += ("var_" + std::to_string(((int)t.first)) + ": " +
                             std::to_string(tmp_word)) +
                            ", ";
                }
            }
            expr += "}\n";
 
            expr += "Symbolic Memory: {";
            for (auto &t : smem) {
                expr += "var_" + std::to_string((int)t.first) + ": " +
                        t.second.toString(true) + ", ";
            }
            expr += "}\n";
        }
 
        expr += "Path Constraints: ";
        if (path_constraints.size() > 0) {
            expr += path_constraints[0].toString(true);
        }
        for (int i = 1; i < path_constraints.size(); i++) {
            expr += "&&" + path_constraints[i].toString(true);
        }
        expr += "\n";
 
        return expr;
    }
 
    void print() const {
        printf("Stack: [");
        LLNode<Sym> *tmp = symbolic_stack.head;
        while (tmp != NULL) {
            printf("%s, ", tmp->data.toString(false).c_str());
            tmp = tmp->next;
        }
        printf("]\n");
 
        printf("%s", toString().c_str());
    }
};
 
using PathConstraintsTable =
    std::unordered_map<std::string,
                       std::pair<bool, std::unordered_map<int, float>>>;
 
using ProbPathConstraintsTable =
    std::unordered_map<int, std::vector<std::tuple<Sym, Mem, SymProb>>>;
 
struct Trace {
    SymState data;               
    std::vector<Trace> children; 
    Trace(SymState data, std::vector<Trace> children)
        : data(data), children(children) {}
 
    void print(int indent_cnt = 0) const {
        printf("PC: %d\n", data.pc);
        data.print();
        for (const Trace &trace : children) {
            trace.print();
        }
    }
};
 
}  // namespace gymbo