Go to the documentation of this file.00001 #include "domain_transition_graph_subterm.h"
00002 #include "operator.h"
00003 #include "axiom.h"
00004 #include "variable.h"
00005 #include "scc.h"
00006 #include "helper_functions.h"
00007
00008 #include <algorithm>
00009 #include <cassert>
00010 #include <iostream>
00011 using namespace std;
00012
00013 DomainTransitionGraphSubterm::DomainTransitionGraphSubterm(const Variable &var) {
00014
00015 level = var.get_level();
00016 if(var.is_comparison()) {
00017 is_comparison = true;
00018
00019 }
00020 else {
00021 is_comparison = false;
00022
00023 }
00024 assert(level != -1);
00025 }
00026
00027 void DomainTransitionGraphSubterm::addTransition(int from, int to,
00028 const Operator &op, int op_index, trans_type type,
00029 vector<Variable *> variables) {
00030 }
00031
00032 void DomainTransitionGraphSubterm::addAxRelTransition(int from, int to,
00033 const Axiom_relational &ax, int ax_index) {
00034 }
00035
00036 void DomainTransitionGraphSubterm::setRelation(Variable* left_var,
00037 compoperator op, Variable* right_var) {
00038 this->left_var = left_var;
00039 this->cop = op;
00040 this->right_var = right_var;
00041 }
00042
00043 void DomainTransitionGraphSubterm::setRelation(Variable* left_var,
00044 foperator op, Variable* right_var) {
00045 this->left_var = left_var;
00046 this->fop = op;
00047 this->right_var = right_var;
00048 }
00049
00050 void DomainTransitionGraphSubterm::finalize() {
00051
00052 }
00053
00054 bool DomainTransitionGraphSubterm::is_strongly_connected() const {
00055 return false;
00056 }
00057
00058 void DomainTransitionGraphSubterm::dump() const {
00059 if(!is_comparison)
00060 cout << "Subterm DTG!" << endl;
00061 else
00062 cout << "Comparison DTG!" << endl;
00063 cout << " Expression : " << left_var->get_name() << " ";
00064 if(is_comparison) {
00065 cout << cop;
00066 } else {
00067 cout << fop;
00068 }
00069 cout << " " << right_var->get_name() << endl;
00070 }
00071
00072 void DomainTransitionGraphSubterm::generate_cpp_input(ostream &outfile) const {
00073 if(!is_comparison) {
00074 outfile << left_var->get_level() << " " << fop << " "
00075 << right_var->get_level() << endl;
00076 } else {
00077 outfile << "1" << endl;
00078 outfile << left_var->get_level() << " " << get_inverse_op(cop) << " "
00079 << right_var->get_level() << endl;
00080 outfile << "0" << endl;
00081 outfile << left_var->get_level() << " " << cop << " "
00082 << right_var->get_level() << endl;
00083 }
00084 }
00085