Go to the documentation of this file.00001 #ifndef DOMAIN_TRANSITION_GRAPH_SUBTERM_H
00002 #define DOMAIN_TRANSITION_GRAPH_SUBTERM_H
00003
00004 #include <vector>
00005 #include "domain_transition_graph.h"
00006 #include "helper_functions.h"
00007 #include "operator.h"
00008 using namespace std;
00009
00010 class Axiom_relational;
00011 class Variable;
00012
00013 class DomainTransitionGraphSubterm: public DomainTransitionGraph
00014 {
00015
00016 private:
00017 int level;
00018 Variable* left_var;
00019 Variable* right_var;
00020 compoperator cop;
00021 foperator fop;
00022 bool is_comparison;
00023
00024 public:
00025 DomainTransitionGraphSubterm(const Variable &var);
00026 void addTransition(int from, int to, const Operator &op, int op_index,
00027 trans_type type, vector<Variable *> variables);
00028 void addAxRelTransition(int from, int to, const Axiom_relational &ax,
00029 int ax_index);
00030 void setRelation(Variable* left_var,
00031 compoperator op, Variable* right_var);
00032 void setRelation(Variable* left_var,
00033 foperator op, Variable* right_var);
00034 void finalize();
00035 void dump() const;
00036 void generate_cpp_input(ostream &outfile) const;
00037 bool is_strongly_connected() const;
00038 };
00039
00040 #endif
