Skip to content

Commit b4c706a

Browse files
danbrycedanbryce
committed
fix(heuristics): missed some changes to hybrid_heuristic
1 parent 0097748 commit b4c706a

File tree

9 files changed

+81
-138
lines changed

9 files changed

+81
-138
lines changed

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_0.bh

+1-4
Original file line numberDiff line numberDiff line change
@@ -1,4 +1 @@
1-
[[1, [2], 0], {
2-
"1": "0.000000",
3-
"2": "1.000000"
4-
},[[2],[1]]]
1+
[[[1],[[2]], 0], [{"1" : "0.000000","2" : "1.000000"}],[[[[[],2],[[],1]],[[[],1],[[],2]]]]]

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_1.bh

+1-4
Original file line numberDiff line numberDiff line change
@@ -1,4 +1 @@
1-
[[1, [2], 1], {
2-
"1": "0.000000",
3-
"2": "1.000000"
4-
},[[2],[1]]]
1+
[[[1],[[2]], 1], [{"1" : "0.000000","2" : "1.000000"}],[[[[[],2],[[],1]],[[[],1],[[],2]]]]]

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_1_0.smt2.model

-13
This file was deleted.

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_2.bh

+1-4
Original file line numberDiff line numberDiff line change
@@ -1,4 +1 @@
1-
[[1, [2], 2], {
2-
"1": "0.000000",
3-
"2": "1.000000"
4-
},[[2],[1]]]
1+
[[[1],[[2]], 2], [{"1" : "0.000000","2" : "1.000000"}],[[[[[],2],[[],1]],[[[],1],[[],2]]]]]

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_3.bh

-4
This file was deleted.

‎benchmarks/hybrid_systems/bouncing_ball/bouncing_ball_3_0.smt2.model

-25
This file was deleted.

‎src/opensmt/heuristics/hybrid_heuristic.cpp

+78-79
Original file line numberDiff line numberDiff line change
@@ -115,51 +115,50 @@ int get_mode(Enode * lit) {
115115
m_cost.push_back(mc);
116116
}
117117

118-
DREAL_LOG_DEBUG << "hybrid_heuristic::initialize() adjacency " << hinfo[2].dump();
119-
120-
// build reverse adjanceny map (succ -> set(predecessors))
121-
for(unsigned long j = 0; j < hinfo[2].size(); j++){ // loop over automata
122-
//DREAL_LOG_DEBUG << "Getting Transitions For Autom ";
123-
vector<vector<labeled_transition*>*>* aut_predecessors = new vector<vector<labeled_transition*>*>();
124-
for (unsigned int i = 0; i < hinfo[2][j].size(); i++){ // loop over modes
125-
// DREAL_LOG_DEBUG << "Getting Transitions From " << i;
126-
vector<labeled_transition*>* mp = new vector<labeled_transition*>();
127-
aut_predecessors->push_back(mp);
128-
}
129-
for (unsigned int src = 0; src < hinfo[2][j].size(); src++){
130-
//DREAL_LOG_DEBUG << "Getting Transitions From " << src << " " << hinfo[2][j][src].dump();
131-
m_aut_labels.push_back(new set<int>());
132-
auto adj = hinfo[2][j][src]; // transitions from src
133-
for(auto adj_trans : adj){ // loop over transitions
134-
//DREAL_LOG_DEBUG << "Getting Transition " << adj_trans.dump();
135-
labeled_transition *trans = new labeled_transition();
136-
trans->first = new set<int>();
137-
trans->second = src+1;
138-
139-
auto labels = adj_trans[0];
140-
for(auto l : labels){
141-
142-
string label_string = l.dump().c_str();
143-
auto li = label_indices.find(label_string);
144-
int ind;
145-
if(li == label_indices.end()){
146-
label_indices[label_string] = num_labels++;
147-
ind = num_labels-1;
148-
} else {
149-
ind = li->second;
150-
}
151-
m_aut_labels[j]->insert(ind);
152-
trans->first->insert(ind);
153-
}
154-
155-
int dest = adj_trans[1];
156-
(*aut_predecessors)[dest-1]->push_back(trans);
157-
//DREAL_LOG_DEBUG << "Got Transition " << adj_trans.dump();
158-
}
159-
}
160-
predecessors.push_back(aut_predecessors);
118+
// build reverse adjanceny map (succ -> set(predecessors))
119+
for(unsigned int j = 0; j < hinfo[2].size(); j++){ // loop over automata
120+
//DREAL_LOG_DEBUG << "Getting Transitions For Autom ";
121+
vector<vector<labeled_transition*>*>* aut_predecessors = new vector<vector<labeled_transition*>*>();
122+
for (unsigned int i = 0; i < hinfo[2][j].size(); i++){ // loop over modes
123+
// DREAL_LOG_DEBUG << "Getting Transitions From " << i;
124+
vector<labeled_transition*>* mp = new vector<labeled_transition*>();
125+
aut_predecessors->push_back(mp);
126+
}
127+
for (unsigned int src = 0; src < hinfo[2][j].size(); src++){
128+
//DREAL_LOG_DEBUG << "Getting Transitions From " << src << " " << hinfo[2][j][src].dump();
129+
m_aut_labels.push_back(new set<int>());
130+
auto adj = hinfo[2][j][src]; // transitions from src
131+
for(auto adj_trans : adj){ // loop over transitions
132+
//DREAL_LOG_DEBUG << "Getting Transition " << adj_trans.dump();
133+
labeled_transition *trans = new labeled_transition();
134+
trans->first = new set<int>();
135+
trans->second = src+1;
136+
137+
auto labels = adj_trans[0];
138+
for(auto l : labels){
139+
140+
string label_string = l.dump().c_str();
141+
auto li = label_indices.find(label_string);
142+
int ind;
143+
if(li == label_indices.end()){
144+
label_indices[label_string] = num_labels++;
145+
ind = num_labels-1;
146+
} else {
147+
ind = li->second;
148+
}
149+
m_aut_labels[j]->insert(ind);
150+
trans->first->insert(ind);
151+
}
152+
153+
int dest = adj_trans[1];
154+
(*aut_predecessors)[dest-1]->push_back(trans);
155+
//DREAL_LOG_DEBUG << "Got Transition " << adj_trans.dump();
156+
}
157+
}
158+
predecessors.push_back(aut_predecessors);
161159
}
162160

161+
163162
// initialize decision stack
164163
pair<int, vector<labeled_transition*>*>* astack = new pair<int, vector<labeled_transition*>*>();
165164
m_decision_stack.push_back(astack);
@@ -176,24 +175,24 @@ int get_mode(Enode * lit) {
176175
astack->second = dec;
177176

178177

179-
for(int a = 0; a < num_autom; a++){
180-
mode_literals.push_back(new map<Enode*, pair<int,int>*>());
181-
182-
vector<vector<Enode*>*>* tme = new vector<vector<Enode*>*>();
183-
vector<vector<Enode*>*>* tmi = new vector<vector<Enode*>*>();
184-
time_mode_enodes.push_back(tme);
185-
time_mode_integral_enodes.push_back(tmi);
186-
for (int i = 0; i < m_depth+1; i++){
187-
vector< Enode* > * en = new vector< Enode* >();
188-
en->assign(static_cast<int>(predecessors[a]->size()), NULL);
189-
tme->push_back(en);
190-
// if (m_egraph->stepped_flows){
191-
en = new vector< Enode* >();
192-
en->assign(static_cast<int>(predecessors.size()), NULL);
193-
tmi->push_back(en);
194-
// }
195-
}
196-
}
178+
for(int a = 0; a < num_autom; a++){
179+
mode_literals.push_back(new map<Enode*, pair<int,int>*>());
180+
181+
vector<vector<Enode*>*>* tme = new vector<vector<Enode*>*>();
182+
vector<vector<Enode*>*>* tmi = new vector<vector<Enode*>*>();
183+
time_mode_enodes.push_back(tme);
184+
time_mode_integral_enodes.push_back(tmi);
185+
for (int i = 0; i < m_depth+1; i++){
186+
vector< Enode* > * en = new vector< Enode* >();
187+
en->assign(static_cast<int>(predecessors[a]->size()), NULL);
188+
tme->push_back(en);
189+
// if (m_egraph->stepped_flows){
190+
en = new vector< Enode* >();
191+
en->assign(static_cast<int>(predecessors.size()), NULL);
192+
tmi->push_back(en);
193+
// }
194+
}
195+
}
197196

198197
}
199198
}
@@ -210,24 +209,24 @@ void hybrid_heuristic::inform(Enode * e){
210209
ss << v;
211210
string var = ss.str();
212211
if (var.find("mode") != string::npos) {
213-
int autom_pos = var.find("_")+1;
214-
int time_pos = var.rfind("_")+1;
215-
int time = atoi(var.substr(time_pos).c_str());
216-
int autom = (predecessors.size() == 1 ?
217-
0 :
218-
atoi(var.substr(autom_pos, time_pos-1).c_str()));
219-
int mode = get_mode(e);
220-
221-
DREAL_LOG_INFO << "autom = " << autom << " mode = " << mode << " time = " << time << endl;
222-
(*mode_literals[autom-1])[ e ] = new pair<int, int>(mode, time);
223-
DREAL_LOG_INFO << "Mode_lit[" << (e->getPolarity() == l_True ? " " : "(not ")
224-
<< e
225-
<< (e->getPolarity() == l_True ? "" : ")")
226-
<< "] = " << mode << " " << time << endl;
227-
228-
(*(*time_mode_enodes[autom-1])[time])[mode-1] = e;
229-
found_mode_literal = true;
230-
mode_enodes.insert(e);
212+
int autom_pos = var.find("_")+1;
213+
int time_pos = var.rfind("_")+1;
214+
int time = atoi(var.substr(time_pos).c_str());
215+
int autom = (predecessors.size() == 1 ?
216+
1 :
217+
atoi(var.substr(autom_pos, time_pos-1).c_str()));
218+
int mode = get_mode(e);
219+
220+
DREAL_LOG_INFO << "autom = " << autom << " mode = " << mode << " time = " << time << endl;
221+
(*mode_literals[autom-1])[ e ] = new pair<int, int>(mode, time);
222+
DREAL_LOG_INFO << "Mode_lit[" << (e->getPolarity() == l_True ? " " : "(not ")
223+
<< e
224+
<< (e->getPolarity() == l_True ? "" : ")")
225+
<< "] = " << mode << " " << time << endl;
226+
227+
(*(*time_mode_enodes[autom-1])[time])[mode-1] = e;
228+
found_mode_literal = true;
229+
mode_enodes.insert(e);
231230
}
232231
}
233232
if (!found_mode_literal){

‎src/opensmt/smtsolvers/.#SimpSMTSolver.C

-1
This file was deleted.

‎src/opensmt/smtsolvers/SimpSMTSolver.C

-4
Original file line numberDiff line numberDiff line change
@@ -541,11 +541,7 @@ bool SimpSMTSolver::addSMTClause( vector< Enode * > & smt_clause, uint64_t in )
541541
// Just add the literal
542542
//
543543
Lit l = theory_handler->enodeToLit( e );
544-
<<<<<<< HEAD
545-
heuristic.inform(e);
546-
=======
547544
heuristic->inform(e);
548-
>>>>>>> 07de9d5... feat(heuristics): call the appropriate heuristic
549545
#if NEW_SIMPLIFICATIONS
550546
if ( e->isTAtom( ) )
551547
{

0 commit comments

Comments
 (0)