axioms.cpp
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     // Handle axioms in the following order:
00033     // 1) Arithmetic axioms (layers 0 through k-1)
00034     // 2) Comparison axioms (layer k)
00035     // 3) Logic axioms (layers k+1 through n)
00036 
00037     // determine layer where arithmetic axioms end and comparison
00038     // axioms and logic axioms start    
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 { //if(is_functional(i))
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     // Initialize axioms by layer
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     // Initialize literals
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     // Initialize rules
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         // Cross-reference rules and literals
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     // Initialize negation-by-failure information
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     // state.dump();
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     // There must be exactly one axiom layer containing all the 
00179     // comparison axioms. This is the one between the layers containing
00180     // numeric axioms and logic axioms.
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         // ax->dump();
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     // cout << "Evaluating axioms..." << endl;
00224     deque<LogicAxiomLiteral *> queue;
00225     for(int i = 0; i < g_axiom_layers.size(); i++) {
00226         if(g_axiom_layers[i] == -1) {
00227             // non-derived variable
00228             const variable_type& vt = g_variable_types[i];
00229             if (vt != comparison && vt != logical) {
00230                 // variable is functional
00231                 // do nothing (should have been handled by
00232                 // arithmetic/comparison axioms)
00233             } else {
00234                 // variable is a logic variable
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             // derived variable corresponding to an arithmetic (sub)term.
00239             // do nothing (should have been handled by arithmetic/comparison axioms)
00240         } else if(g_axiom_layers[i] == g_comparison_axiom_layer) {
00241             // derived variable corresponding to a comparison.
00242             // can be handled like a non-derived discrete variable
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             // derived discrete variable -> use default value first
00246             state[i] = g_default_axiom_values[i];
00247         } else {
00248             // cannot happen
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         // In a perfect world, trivial axioms would have been
00259         // compiled away, and we could have the following assertion
00260         // instead of the following block.
00261         // assert(rules[i].condition_counter != 0);
00262         if(rules[i].condition_count == 0) {
00263             // NOTE: This duplicates code from the main loop below.
00264             // I don't mind because this is (hopefully!) going away
00265             // some time.
00266             int var_no = rules[i].effect_var;
00267             int val = rules[i].effect_val;
00268             if(!double_equals(state[var_no], val)) {
00269                 // cout << "  -> deduced " << var_no << " = " << val << endl;
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             // Apply Horn rules.
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                             // cout << "  -> deduced " << var_no << " = " << val << endl;
00290                             state[var_no] = val;
00291                             queue.push_back(rule->effect_literal);
00292                         }
00293                     }
00294                 }
00295             }
00296 
00297             // Apply negation by failure rules.
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 }
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Defines


tfd_modules
Author(s): Maintained by Christian Dornhege (see AUTHORS file).
autogenerated on Tue Jan 22 2013 12:25:02