smt.h

Go to the documentation of this file.

 
#pragma once
#include "gd.h"
#include "sat.h"
namespace gymbo {
 
inline void initialize_params(std::unordered_map<int, float> &params,
                              SymState &state, bool ignore_memory) {
    params = {};
    if (!ignore_memory) {
        for (auto &p : state.mem) {
            params.emplace(std::make_pair(p.first, wordToFloat(p.second)));
        }
    }
}
 
inline void smt_union_solver(bool &is_sat, SymState &state,
                             std::unordered_map<int, float> &params,
                             GDOptimizer &optimizer, int max_num_trials,
                             bool ignore_memory) {
    for (int j = 0; j < max_num_trials; j++) {
        is_sat = optimizer.solve(state.path_constraints, params);
        if (is_sat) {
            break;
        }
        optimizer.seed += 1;
        int total_num_params = params.size();
        initialize_params(params, state, ignore_memory);
        int total_num_consts = params.size();
        if (total_num_consts == total_num_params) {
            break;
        }
    }
}
 
inline void smt_dpll_solver(bool &is_sat, SymState &state,
                            std::unordered_map<int, float> &params,
                            GDOptimizer &optimizer, int max_num_trials,
                            bool ignore_memory) {
    std::unordered_map<std::string, gymbo::Sym *> unique_terms_map;
    std::unordered_map<std::string, bool> assignments_map;
    std::shared_ptr<gymbosat::Expr> path_constraints_expr =
        gymbosat::pathconstraints2expr(state.path_constraints,
                                       unique_terms_map);
 
    while (satisfiableDPLL(path_constraints_expr, assignments_map)) {
        std::vector<Sym> new_constraints;
        for (auto &ass : assignments_map) {
            if (ass.second) {
                new_constraints.emplace_back(*unique_terms_map[ass.first]);
            } else {
                new_constraints.emplace_back(
                    Sym(SymType::SNot, unique_terms_map[ass.first]));
            }
        }
 
        for (int j = 0; j < max_num_trials; j++) {
            is_sat = optimizer.solve(new_constraints, params);
            if (is_sat) {
                break;
            }
            optimizer.seed += 1;
            initialize_params(params, state, ignore_memory);
        }
 
        if (is_sat) {
            break;
        }
 
        // add feedback
        std::shared_ptr<gymbosat::Expr> learnt_constraints =
            std::make_shared<gymbosat::Const>(false);
        for (auto &ass : assignments_map) {
            if (ass.second) {
                learnt_constraints = std::make_shared<gymbosat::Or>(
                    learnt_constraints,
                    std::make_shared<gymbosat::Not>(
                        std::make_shared<gymbosat::Var>(ass.first)));
            } else {
                learnt_constraints = std::make_shared<gymbosat::Or>(
                    learnt_constraints,
                    std::make_shared<gymbosat::Var>(ass.first));
            }
        }
 
        path_constraints_expr = std::make_shared<gymbosat::And>(
            path_constraints_expr, learnt_constraints);
    }
}
 
}  // namespace gymbo