diff options
Diffstat (limited to 'omegalib/omega/src/pres_var.cc')
| -rw-r--r-- | omegalib/omega/src/pres_var.cc | 459 |
1 files changed, 459 insertions, 0 deletions
diff --git a/omegalib/omega/src/pres_var.cc b/omegalib/omega/src/pres_var.cc new file mode 100644 index 0000000..0ec406f --- /dev/null +++ b/omegalib/omega/src/pres_var.cc @@ -0,0 +1,459 @@ +#include <omega/pres_var.h> +#include <omega/pres_tree.h> +#include <omega/pres_conj.h> +#include <omega/omega_i.h> + +namespace omega { + +int wildCardInstanceNumber; + +const int Global_Input_Output_Tuple::initial_allocation = 10; + +// Declare named Variable +Var_Decl::Var_Decl(Const_String name, Var_Kind vkind, int pos): + base_name(name), + instance(999), + remap(this), + var_kind(vkind), + position(pos), + global_var(NULL), + of((Argument_Tuple) 0) { + assert(((vkind==Input_Var || vkind==Output_Var) && pos>0) || pos==0); +} + +// Declare unnamed variable +Var_Decl::Var_Decl(Var_Kind vkind, int pos): + instance(999), + remap(this), + var_kind(vkind), + position(pos), + global_var(NULL), + of((Argument_Tuple) 0) { + assert(((vkind==Input_Var || vkind==Output_Var) && pos>0) || pos==0); +} + +// Copy variable declaration +Var_Decl::Var_Decl(Variable_ID v): + base_name(v->base_name), + instance(v->instance), + remap(this), + var_kind(v->var_kind), + position(v->position), + global_var(v->global_var), + of(v->of) { +} + +Var_Decl::Var_Decl(Const_String name, Global_Var_ID v): + base_name(name), + instance(999), + remap(this), + var_kind(Global_Var), + position(0), + global_var(v), + of((Argument_Tuple) 0) { + assert(v->arity() == 0); +} + +Var_Decl::Var_Decl(Const_String name, Global_Var_ID v, Argument_Tuple function_of): + base_name(name), + instance(999), + remap(this), + var_kind(Global_Var), + position(0), + global_var(v), + of(function_of) { +} + +int Var_Decl::get_position() { + assert((var_kind == Input_Var || var_kind == Output_Var) && "Var_Decl::get_position: bad var_kind"); + return(position); +} + +Global_Var_ID Var_Decl::get_global_var() { + assert(var_kind == Global_Var && "Var_Decl::get_global_var: bad var_kind"); + return(global_var); +} + +Argument_Tuple Var_Decl::function_of() { + assert(var_kind == Global_Var); + return(of); +} + + +Omega_Var *Global_Var_Decl::really_omega_var() { + assert(0); + return(NULL); +} + +Coef_Var_Decl *Global_Var_Decl::really_coef_var() { + assert(0); + return(NULL); +} + +// +// Variable name. +// + +const int N_greek_letters = 19; + +char greek_letters[19][10] = { + "alpha" , "beta" , "gamma" , "delta" , "tau" , "sigma" , "chi" , + "omega" , "pi" , "ni" , "Alpha" , "Beta" , "Gamma" , "Delta" , + "Tau" , "Sigma" , "Chi" , "Omega" , "Pi" +}; + +const int numBuffers = 50; +const int bufferSize = 90; +char nameBuffers[numBuffers][bufferSize]; +int nextBuffer = 0; + +int use_ugly_names = 0; + +const char *Var_Decl::char_name() { + char *s = nameBuffers[nextBuffer++]; + char *start = s; + if (nextBuffer >= numBuffers) nextBuffer = 0; + int primes; + + if (use_ugly_names) + primes = 0; + else + primes = instance; + + switch(var_kind) { + case Input_Var: + if (!use_ugly_names && !base_name.null()) + sprintf(s,"%s",(const char *)base_name); + else { + primes = 0; + sprintf(s,"In_%d",position); + } + break; + case Output_Var: + if (!use_ugly_names && !base_name.null()) + sprintf(s,"%s",(const char *)base_name); + else { + primes = 0; + sprintf(s,"Out_%d",position); + } + break; + case Global_Var: + assert(!base_name.null()); + if (use_ugly_names) + sprintf(s,"%s@%p",(const char *)base_name, this); + else { + sprintf(s,"%s",(const char *)base_name); + primes = get_global_var()->instance; + } + break; + default: + if (use_ugly_names) { + if (!base_name.null()) + sprintf(s,"%s@%p",(const char *)base_name, this); + else + sprintf(s,"?@%p", this); + } + else if (!base_name.null()) sprintf(s,"%s",(const char *)base_name); + else { + assert(instance < 999); + sprintf(s,"%s", + greek_letters[instance % N_greek_letters]); + primes = instance/N_greek_letters; + } + break; + } + + while (*s) s++; + int i; + assert(primes < 999); + for(i=1; i<= primes; i++) *s++ = '\''; + *s = '\0'; + if (var_kind == Global_Var) { + int a = get_global_var()->arity(); + if (a) { + if (use_ugly_names) { + static const char *arg_names[4] = { "???", "In", "Out", "In == Out" }; + sprintf(s, "(%s[1#%d])", arg_names[function_of()], a); + } + else { + int f_of = function_of(); + assert(f_of == Input_Tuple || f_of == Output_Tuple); + *s++ = '('; + for(i = 1;i<=a;i++) { + if (f_of == Input_Tuple) + sprintf(s,"%s",(const char *)input_vars[i]->char_name()); + else + sprintf(s,"%s",(const char *)output_vars[i]->char_name()); + while (*s) s++; + if (i<a) *s++ = ','; + } + *s++ = ')'; + *s++ = 0; + } + } + } + + assert(s < start+bufferSize); + return start; +} + +std::string Var_Decl::name() { + return char_name(); +} + +// +// Copy variable declarations. +// +void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl) { + if (new_vl.size() < vl.size()) { + new_vl.reallocate(vl.size()); + } + for(int p=1; p<=vl.size(); p++) { + Variable_ID v = vl[p]; + if(v->kind()==Global_Var) { + new_vl[p] = v; + v->remap = v; + } + else { + new_vl[p] = new Var_Decl(vl[p]); + v->remap = new_vl[p]; + } + } +} + +// +// Name a variable. +// +void Var_Decl::name_variable(char *newname) { + base_name = newname; +} + + +static Const_String coef_var_name(int i, int v) { + char s[100]; + sprintf(s, "c_%d_%d", i, v); + return Const_String(s); +} + + +// +// Global variables stuff. +// +Global_Var_Decl::Global_Var_Decl(Const_String baseName): + loc_rep1(baseName, this, Input_Tuple), + loc_rep2(baseName, this, Output_Tuple) { +} + +Global_Kind Global_Var_Decl::kind() const { + assert(0); + return Coef_Var; +} + +Coef_Var_Decl::Coef_Var_Decl(int id, int var): + Global_Var_Decl(coef_var_name(id, var)) { + i = id; + v = var; +} + +Coef_Var_Decl *Coef_Var_Decl::really_coef_var() { + return this; +} + +int Coef_Var_Decl::stmt() const { + return i; +} + +int Coef_Var_Decl::var() const { + return v; +} + +Global_Kind Coef_Var_Decl::kind() const { + return Coef_Var; +} + +Free_Var_Decl::Free_Var_Decl(Const_String name): + Global_Var_Decl(name), _arity(0) { +} + +Free_Var_Decl::Free_Var_Decl(Const_String name, int arity): + Global_Var_Decl(name), _arity(arity) { +} + +int Free_Var_Decl::arity() const { + return _arity; +} + +Global_Kind Free_Var_Decl::kind() const { + return Free_Var; +} + + +// +// Delete variable from variable list. Does not preserve order +// +bool rm_variable(Variable_ID_Tuple &vl, Variable_ID v) { + int n = vl.size(); + int i; + for(i = 1; i<n; i++) if (vl[i] == v) break; + if (i>n) return 0; + vl[i] = vl[n]; + vl.delete_last(); + return 1; +} + + +// +// Destroy variable declarations. +// +void free_var_decls(Variable_ID_Tuple &c) { + for(Variable_ID_Iterator p = c; p; p++) { + Variable_ID v = *p; + if(v->kind()!=Global_Var) { + delete v; + } + } +} + + +Variable_ID input_var(int nth) { + assert(1 <= nth && nth <= input_vars.size()); + return input_vars[nth]; +} + +Variable_ID output_var(int nth) { + assert(1<= nth && nth <= output_vars.size()); + return output_vars[nth]; +} + +Variable_ID set_var(int nth) { + assert(1 <= nth && set_vars.size()); + return input_vars[nth]; +} + + +// +// Remap mappedVars in all conjuncts of formula. +// Uses the remap field of the Var_Decl. +// +void Formula::remap() { + for(List_Iterator<Formula*> c(children()); c; c++) + (*c)->remap(); +} + +void Conjunct::remap() { + for(Variable_Iterator VI(mappedVars); VI; VI++) { + Variable_ID v = *VI; + *VI = v->remap; + } + cols_ordered = false; +} + +// Function to reset the remap field of a Variable_ID +void reset_remap_field(Variable_ID v) { + v->remap = v; +} + +// Function to reset the remap fields of a Variable_ID_Seq +void reset_remap_field(Sequence<Variable_ID> &T) { + for(Any_Iterator<Variable_ID> VI(T.any_iterator()); VI; VI++) { + Variable_ID v = *VI; + v->remap = v; + } +} + +// Function to reset the remap fields of a Variable_ID_Tuple, +// more efficiently +void reset_remap_field(Variable_ID_Tuple &T) { + for(Variable_Iterator VI(T); VI; VI++) { + Variable_ID v = *VI; + v->remap = v; + } +} + +void reset_remap_field(Sequence<Variable_ID> &T, int var_no) { + int i=1; + for(Any_Iterator<Variable_ID> VI(T.any_iterator()); i <= var_no && VI; VI++) { + Variable_ID v = *VI; + v->remap = v; + i++; + } +} + +void reset_remap_field(Variable_ID_Tuple &T, int var_no) { + int i=1; + for(Variable_Iterator VI(T); i <= var_no && VI; VI++) { + Variable_ID v = *VI; + v->remap = v; + i++; + } +} + + +// Global input and output variable tuples. +// These Tuples must be initialized as more in/out vars are needed. +//Variable_ID_Tuple input_vars(0); +//Variable_ID_Tuple output_vars(0); +//Variable_ID_Tuple& set_vars = input_vars; +Global_Input_Output_Tuple input_vars(Input_Var); +Global_Input_Output_Tuple output_vars(Output_Var); +Global_Input_Output_Tuple &set_vars = input_vars; + +//////////////////////////////////////// +// // +// Variable and Declaration functions // +// // +//////////////////////////////////////// + +// +// Constructors and properties. +// + + +// Allocate ten variables initially. Most applications won't require more. +Global_Input_Output_Tuple::Global_Input_Output_Tuple(Var_Kind in_my_kind, int init): + my_kind(in_my_kind) { + for (int i=1; i<=(init == -1? initial_allocation: max(0,init)); i++) + this->append(new Var_Decl(Const_String(), my_kind, i)); +} + +Global_Input_Output_Tuple::~Global_Input_Output_Tuple() { + for (int i=1; i<=size(); i++) + delete data[i-1]; +} + +Variable_ID & Global_Input_Output_Tuple::operator[](int index) { + assert(index > 0); + while(size() < index) + this->append(new Var_Decl(Const_String(), my_kind, size()+1)); + return data[index-1]; +} + +const Variable_ID & Global_Input_Output_Tuple::operator[](int index) const { + assert(index > 0); + Global_Input_Output_Tuple *unconst_this = (Global_Input_Output_Tuple *) this; + while(size() < index) + unconst_this->append(new Var_Decl(Const_String(), my_kind, size()+1)); + return data[index-1]; +} + +Variable_ID Var_Decl::UF_owner() { + Variable_ID v = this; + while (v->remap != v) v = v->remap; + return v; +} + +void Var_Decl::UF_union(Variable_ID b) { + Variable_ID a = this; + while (a->remap != a) { + Variable_ID tmp = a->remap; + a->remap = tmp->remap; + a = tmp; + } + while (b->remap != a) { + Variable_ID tmp = b->remap; + b->remap = a; + b = tmp; + } +} + +} // namespace |