From e8ca1816e6c5109f9c1ccc2f24cc2b321ecd5817 Mon Sep 17 00:00:00 2001 From: Daniel Bryce Date: Wed, 30 Aug 2017 10:09:33 -0500 Subject: [PATCH] fix(schedule_heuristic): refactored heursitic to use new literals for decision points --- src/opensmt/egraph/EgraphStore.C | 3 +- src/opensmt/heuristics/schedule_heuristic.cpp | 83 +++++++++++-------- src/opensmt/heuristics/schedule_heuristic.h | 4 +- src/util/mcts_expander.cpp | 6 ++ 4 files changed, 59 insertions(+), 37 deletions(-) diff --git a/src/opensmt/egraph/EgraphStore.C b/src/opensmt/egraph/EgraphStore.C index be4613011..28169a127 100644 --- a/src/opensmt/egraph/EgraphStore.C +++ b/src/opensmt/egraph/EgraphStore.C @@ -665,6 +665,7 @@ Enode * Egraph::mkFun( const char * name, Enode * args ) // ostringstream ss; ss << name; + std::cout << "[" << name << "]" << std::endl; for ( Enode * l = args ; !l->isEnil( ) ; l = l->getCdr( ) ) { ss << " "; @@ -672,7 +673,7 @@ Enode * Egraph::mkFun( const char * name, Enode * args ) } Enode * e = lookupSymbol( ss.str( ).c_str( ) ); - if ( e == nullptr ) opensmt_error2( "undeclared function symbol ", ss.str( ).c_str( ) ); + if ( e == nullptr ) opensmt_error2( "undeclared function symbol [", ss.str( ).c_str( ) ); Enode * ret = cons( e, args ); diff --git a/src/opensmt/heuristics/schedule_heuristic.cpp b/src/opensmt/heuristics/schedule_heuristic.cpp index ed6baa1aa..042b3c347 100644 --- a/src/opensmt/heuristics/schedule_heuristic.cpp +++ b/src/opensmt/heuristics/schedule_heuristic.cpp @@ -47,8 +47,8 @@ namespace dreal { m_config = &c; m_is_initialized = true; - m_depth = 10; - num_choices_per_happening = 20; //num actions * 2 + m_depth = 13; + num_choices_per_happening = 36; //num actions * 2 for(int i = 0; i < m_depth+1; i++){ at_time_enodes.push_back(new vector(num_choices_per_happening, NULL)); @@ -124,7 +124,7 @@ void schedule_heuristic::inform(Enode * e) { return; m_atoms.insert(e); - // DREAL_LOG_INFO << "schedule_heuristic::inform(): " << e << endl; + DREAL_LOG_INFO << "schedule_heuristic::inform(): " << e << endl; // if (!e->isTAtom() && !e->isNot()) { // unordered_set const & vars = e->get_vars(); // //unordered_set const & consts = e->get_constants(); @@ -210,44 +210,55 @@ void schedule_heuristic::inform(Enode * e) { // } else if (e->isEq()) { unordered_set const & vars = e->get_vars(); - unordered_set const & consts = e->get_constants(); + // unordered_set const & consts = e->get_constants(); + Enode* time_point = NULL; + Enode* happening = NULL; for (auto const & v : vars) { stringstream ss; ss << v; string var = ss.str(); - if (var.find("time") != string::npos) { - int time = atoi(var.substr(var.find_last_of("_")+1).c_str()); - for (auto const & c : consts) { - stringstream css; - css << c; - int cs = atoi(css.str().c_str()); - if (cs == 0) { // only care about assinging time if wait is possible - DREAL_LOG_INFO << "time time = " << time << endl; - time_enodes[time] = e; - } - } - } else if (var.find("duract") == 0 && var.find("_at") != string::npos){ - DREAL_LOG_INFO << "var = " << var; - for (auto const & c : consts) { - stringstream css; - css << c; - int time = atoi(css.str().c_str()); - DREAL_LOG_INFO << "time = " << time << endl; - auto at = at_id.find(var); - if(at == at_id.end()){ - at_id[var] = num_acts++; - at = at_id.find(var); - } - - DREAL_LOG_INFO << "index = " << (*at).second; - (*at_time_enodes[time])[(*at).second] = e; - at_enodes.insert(e); - DREAL_LOG_INFO << "Got = " << (*at_time_enodes[time])[(*at).second]; - - } + if (var.find("duract") == 0 ){ + time_point = v; + } else if (var.find("happening") == 0 ){ + happening = v; + } + } + + if (time_point != NULL && happening != NULL){ + stringstream ss; + ss << happening; + string happening_str = ss.str(); + + stringstream ss1; + ss1 << time_point; + string time_point_str = ss1.str(); + + + int time_pos = happening_str.find_last_of("_")+1; + int time = atoi(happening_str.substr(time_pos).c_str()); + + DREAL_LOG_INFO << "time = " << time << endl; + + string name = time_point_str; + + DREAL_LOG_INFO << "name = " << name << endl; + + + auto at = at_id.find(name); + if(at == at_id.end()){ + at_id[name] = num_acts++; + at = at_id.find(name); } + + DREAL_LOG_INFO << "index = " << (*at).second; + (*at_time_enodes[time])[(*at).second] = e; + at_enodes.insert(e); + DREAL_LOG_INFO << "Got = " << (*at_time_enodes[time])[(*at).second]; + } } + //DREAL_LOG_INFO << "schedule_heuristic::inform(): " << e << endl; + } int schedule_heuristic::getChoiceIndex(Enode *e) { @@ -417,11 +428,12 @@ void schedule_heuristic::inform(Enode * e) { DREAL_LOG_DEBUG << "Suggesting: " << decision->first << " " << decision->second->back(); for(int time = 0; time <= m_depth; time++){ Enode* decision_enode = (*at_time_enodes[time])[decision->first]; + if(!decision_enode) continue; DREAL_LOG_DEBUG << "Suggesting: " << decision_enode << " = " << (time == decision->second->back()); if (time == decision->second->back()){ m_suggestions.push_back(new std::pair(decision_enode, true)); } else { - m_suggestions.push_back(new std::pair(decision_enode, false)); + //m_suggestions.push_back(new std::pair(decision_enode, false)); } } } @@ -493,6 +505,7 @@ std::pair* schedule_heuristic::on_stack(Enode* act) { std::vector* decisions = new vector(); for (int i = m_depth-1; i >= 0; i--) { Enode* act_at_step = (*at_time_enodes[i])[act]; + if(!act_at_step) continue; pair* on = on_stack(act_at_step); if (on == NULL) { //no decisions for act on stack decisions->push_back(i); diff --git a/src/opensmt/heuristics/schedule_heuristic.h b/src/opensmt/heuristics/schedule_heuristic.h index 83cbcb1ab..23260ab21 100644 --- a/src/opensmt/heuristics/schedule_heuristic.h +++ b/src/opensmt/heuristics/schedule_heuristic.h @@ -60,8 +60,10 @@ class schedule_heuristic : public heuristic { bool expand_path(bool first_expansion); void displayDecisions(); - std::map at_id; //not used + std::map at_id; + std::map at_names; std::vector*> at_time_enodes; + std::set at_enodes; std::vector* get_possible_decisions(int act); std::pair* on_stack(Enode* act); diff --git a/src/util/mcts_expander.cpp b/src/util/mcts_expander.cpp index ad9f6a65b..c36b7ade9 100644 --- a/src/util/mcts_expander.cpp +++ b/src/util/mcts_expander.cpp @@ -257,6 +257,9 @@ int get_step(std::string var, bool & at_start) { int last_underscore = var.find_last_of("_"); // DREAL_LOG_INFO << first_underscore << " " << last_underscore; int step = -1; + + try{ + if (first_underscore == last_underscore) { // is a time_x variable step = std::stoi(var.substr(first_underscore + 1)); at_start = false; @@ -271,6 +274,9 @@ int get_step(std::string var, bool & at_start) { else at_start = true; } + } catch (std::exception e) { + return 0; + } return step; }