Go to the documentation of this file.00001 #include "axioms.h"
00002 #include "globals.h"
00003 #include "operator.h"
00004 #include "state.h"
00005
00006 #include <deque>
00007 #include <iostream>
00008 using namespace std;
00009
00010 LogicAxiom::LogicAxiom(istream &in)
00011 {
00012 check_magic(in, "begin_rule");
00013 int cond_count;
00014 in >> cond_count;
00015 for(int i = 0; i < cond_count; i++)
00016 prevail.push_back(Prevail(in));
00017 in >> affected_variable >> old_value >> new_value;
00018 check_magic(in, "end_rule");
00019 }
00020
00021 NumericAxiom::NumericAxiom(istream &in)
00022 {
00023 in >> affected_variable >> op >> var_lhs >> var_rhs;
00024 if(op == lt || op == eq || op == gt || op == ge || op == le || op == ue)
00025 g_variable_types[affected_variable] = comparison;
00026 else
00027 g_variable_types[affected_variable] = subterm_functional;
00028 }
00029
00030 AxiomEvaluator::AxiomEvaluator()
00031 {
00032
00033
00034
00035
00036
00037
00038
00039 g_last_arithmetic_axiom_layer = -1;
00040 g_comparison_axiom_layer = -1;
00041 g_first_logic_axiom_layer = -1;
00042 g_last_logic_axiom_layer = -1;
00043 for(int i = 0; i < g_axiom_layers.size(); i++) {
00044 int layer = g_axiom_layers[i];
00045 if(layer == -1)
00046 continue;
00047 if(g_variable_types[i] == logical) {
00048 g_last_logic_axiom_layer = max(g_last_logic_axiom_layer, layer);
00049 if(layer < g_first_logic_axiom_layer || g_first_logic_axiom_layer == -1)
00050 g_first_logic_axiom_layer = layer;
00051 } else if(g_variable_types[i] == comparison) {
00052 assert(g_comparison_axiom_layer == -1 || g_comparison_axiom_layer == layer);
00053 g_comparison_axiom_layer = layer;
00054 } else {
00055 g_last_arithmetic_axiom_layer = max(g_last_arithmetic_axiom_layer,
00056 layer);
00057 }
00058 }
00059
00060 int max_axiom_layer = max(g_last_logic_axiom_layer, g_comparison_axiom_layer);
00061 max_axiom_layer = max(max_axiom_layer, g_last_arithmetic_axiom_layer);
00062 assert(g_last_arithmetic_axiom_layer < g_comparison_axiom_layer || g_comparison_axiom_layer == -1);
00063 assert(g_comparison_axiom_layer < g_first_logic_axiom_layer || g_first_logic_axiom_layer == -1);
00064 assert(g_last_arithmetic_axiom_layer < g_first_logic_axiom_layer || g_first_logic_axiom_layer == -1);
00065 assert(g_first_logic_axiom_layer <= g_last_logic_axiom_layer);
00066 assert(g_first_logic_axiom_layer > -1 || g_last_logic_axiom_layer == -1);
00067 assert(g_first_logic_axiom_layer == -1 || g_last_logic_axiom_layer > -1);
00068
00069
00070 axioms_by_layer.resize(g_last_logic_axiom_layer + 2);
00071 for(int i = 0; i < max_axiom_layer + 2; i++)
00072 axioms_by_layer.push_back(vector<Axiom*>());
00073
00074 for(int i = 0; i < g_axioms.size(); i++) {
00075 int layer = g_axiom_layers[g_axioms[i]->affected_variable];
00076 axioms_by_layer[layer].push_back(g_axioms[i]);
00077 }
00078
00079
00080 for(int i = 0; i < g_variable_domain.size(); i++)
00081 axiom_literals.push_back(vector<LogicAxiomLiteral>(
00082 max(g_variable_domain[i], 0))
00083 );
00084
00085
00086 if(g_first_logic_axiom_layer != -1) {
00087 for(int layer = g_first_logic_axiom_layer;
00088 layer <= g_last_logic_axiom_layer; layer++) {
00089 for(int i = 0; i < axioms_by_layer[layer].size(); i++) {
00090 LogicAxiom *axiom =
00091 static_cast<LogicAxiom*>(axioms_by_layer[layer][i]);
00092 int cond_count = axiom->prevail.size();
00093 int eff_var = axiom->affected_variable;
00094 int eff_val = static_cast<int>(axiom->new_value);
00095 LogicAxiomLiteral *eff_literal =
00096 &axiom_literals[eff_var][eff_val];
00097 rules.push_back(LogicAxiomRule(cond_count, eff_var, eff_val, eff_literal));
00098 }
00099 }
00100
00101
00102 int sum_of_indices = 0;
00103 for(int layer = g_first_logic_axiom_layer;
00104 layer <= g_last_logic_axiom_layer; layer++) {
00105 for(int i = 0; i < axioms_by_layer[layer].size(); i++, sum_of_indices++) {
00106 LogicAxiom *axiom =
00107 static_cast<LogicAxiom*>(axioms_by_layer[layer][i]);
00108 const vector<Prevail> &conditions = axiom->prevail;
00109 for(int j = 0; j < conditions.size(); j++) {
00110 const Prevail &cond = conditions[j];
00111 axiom_literals[cond.var][static_cast<int>(cond.prev)].condition_of.push_back(
00112 &rules[sum_of_indices]);
00113 }
00114 }
00115 }
00116 }
00117
00118
00119 nbf_info_by_layer.resize(max_axiom_layer + 2);
00120
00121 for(int var_no = 0; var_no < g_axiom_layers.size(); var_no++) {
00122 int layer = g_axiom_layers[var_no];
00123 if(layer > -1 && layer >= g_first_logic_axiom_layer &&
00124 layer <= g_last_logic_axiom_layer) {
00125 int nbf_value = static_cast<int>(g_default_axiom_values[var_no]);
00126 LogicAxiomLiteral *nbf_literal = &axiom_literals[var_no][nbf_value];
00127 NegationByFailureInfo nbf_info(var_no, nbf_literal);
00128 nbf_info_by_layer[layer].push_back(nbf_info);
00129 }
00130 }
00131
00132 }
00133
00134 void AxiomEvaluator::evaluate(TimeStampedState &state)
00135 {
00136 evaluate_arithmetic_axioms(state);
00137 evaluate_comparison_axioms(state);
00138 evaluate_logic_axioms(state);
00139
00140 }
00141
00142 void AxiomEvaluator::evaluate_arithmetic_axioms(TimeStampedState &state)
00143 {
00144 for(int layer_no = 0; layer_no <= g_last_arithmetic_axiom_layer; layer_no++) {
00145 for(int i = 0; i < axioms_by_layer[layer_no].size(); i++) {
00146 NumericAxiom* ax =
00147 static_cast<NumericAxiom*>(axioms_by_layer[layer_no][i]);
00148
00149 int var = ax->affected_variable;
00150 int lhs = ax->var_lhs;
00151 int rhs = ax->var_rhs;
00152
00153 switch(ax->op) {
00154 case add:
00155 state[var] = state[lhs] + state[rhs];
00156 break;
00157 case subtract:
00158 state[var] = state[lhs] - state[rhs];
00159 break;
00160 case mult:
00161 state[var] = state[lhs] * state[rhs];
00162 break;
00163 case divis:
00164 state[var] = state[lhs] / state[rhs];
00165 break;
00166 default:
00167 cout << "Error: No comparison operators are allowed here." << endl;
00168 assert(false);
00169 break;
00170 }
00171
00172 }
00173 }
00174 }
00175
00176 void AxiomEvaluator::evaluate_comparison_axioms(TimeStampedState &state)
00177 {
00178
00179
00180
00181 if(g_comparison_axiom_layer == -1)
00182 return;
00183 for(int i = 0; i < axioms_by_layer[g_comparison_axiom_layer].size(); i++) {
00184 NumericAxiom* ax =
00185 static_cast<NumericAxiom*>(axioms_by_layer[g_comparison_axiom_layer][i]);
00186
00187
00188
00189 int var = ax->affected_variable;
00190 int lhs = ax->var_lhs;
00191 int rhs = ax->var_rhs;
00192 switch(ax->op) {
00193 case lt:
00194 state[var] = (state[lhs] < state[rhs]) ? 0.0 : 1.0;
00195 break;
00196 case le:
00197 state[var] = (state[lhs] <= state[rhs]) ? 0.0 : 1.0;
00198 break;
00199 case eq:
00200 state[var] = double_equals(state[lhs], state[rhs]) ? 0.0 : 1.0;
00201 break;
00202 case ge:
00203 state[var] = (state[lhs] >= state[rhs]) ? 0.0 : 1.0;
00204 break;
00205 case gt:
00206 state[var] = (state[lhs] > state[rhs]) ? 0.0 : 1.0;
00207 break;
00208 case ue:
00209 state[var] = !double_equals(state[lhs], state[rhs]) ? 0.0 : 1.0;
00210 break;
00211 default:
00212 cout << "Error: ax->op is " << ax->op << "." << endl;
00213 cout << "Error: No arithmetic operators are allowed here." << endl;
00214 assert(false);
00215 break;
00216 }
00217
00218 }
00219 }
00220
00221 void AxiomEvaluator::evaluate_logic_axioms(TimeStampedState &state)
00222 {
00223
00224 deque<LogicAxiomLiteral *> queue;
00225 for(int i = 0; i < g_axiom_layers.size(); i++) {
00226 if(g_axiom_layers[i] == -1) {
00227
00228 const variable_type& vt = g_variable_types[i];
00229 if (vt != comparison && vt != logical) {
00230
00231
00232
00233 } else {
00234
00235 queue.push_back(&axiom_literals[i][static_cast<int>(state[i])]);
00236 }
00237 } else if(g_axiom_layers[i] <= g_last_arithmetic_axiom_layer) {
00238
00239
00240 } else if(g_axiom_layers[i] == g_comparison_axiom_layer) {
00241
00242
00243 queue.push_back(&axiom_literals[i][static_cast<int>(state[i])]);
00244 } else if(g_axiom_layers[i] >= g_first_logic_axiom_layer) {
00245
00246 state[i] = g_default_axiom_values[i];
00247 } else {
00248
00249 cout << "Error: Encountered a variable with an axiom layer exceeding "
00250 << "the maximal computed axiom layer." << endl;
00251 exit(1);
00252 }
00253 }
00254
00255 for(int i = 0; i < rules.size(); i++) {
00256 rules[i].unsatisfied_conditions = rules[i].condition_count;
00257
00258
00259
00260
00261
00262 if(rules[i].condition_count == 0) {
00263
00264
00265
00266 int var_no = rules[i].effect_var;
00267 int val = rules[i].effect_val;
00268 if(!double_equals(state[var_no], val)) {
00269
00270 state[var_no] = val;
00271 queue.push_back(rules[i].effect_literal);
00272 }
00273 }
00274 }
00275
00276 if(g_first_logic_axiom_layer != -1) {
00277 for(int layer_no = g_first_logic_axiom_layer;
00278 layer_no < g_last_logic_axiom_layer + 1; layer_no++) {
00279
00280 while(!queue.empty()) {
00281 LogicAxiomLiteral *curr_literal = queue.front();
00282 queue.pop_front();
00283 for(int i = 0; i < curr_literal->condition_of.size(); i++) {
00284 LogicAxiomRule *rule = curr_literal->condition_of[i];
00285 if(--(rule->unsatisfied_conditions) == 0) {
00286 int var_no = rule->effect_var;
00287 int val = rule->effect_val;
00288 if(!double_equals(state[var_no], val)) {
00289
00290 state[var_no] = val;
00291 queue.push_back(rule->effect_literal);
00292 }
00293 }
00294 }
00295 }
00296
00297
00298 const vector<NegationByFailureInfo> &nbf_info = nbf_info_by_layer[layer_no];
00299 for(int i = 0; i < nbf_info.size(); i++) {
00300 int var_no = nbf_info[i].var_no;
00301 if(double_equals(state[var_no], g_default_axiom_values[var_no]))
00302 queue.push_back(nbf_info[i].literal);
00303 }
00304 }
00305 }
00306 }