00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019 #include <sstream>
00020 #include "Sym.h"
00021 #include "FunDef.h"
00022 #include <LanguageTable.h>
00023
00024 using namespace std;
00025 using namespace boost::numeric;
00026
00027 vector<const FunDef*> language;
00028
00029 token_t add_function(FunDef* function) {
00030 language.push_back(function);
00031 return token_t(language.size()-1);
00032 }
00033
00034 const FunDef& get_element(token_t token) { return *language[token]; }
00035
00036
00037
00038 string c_print(const Sym& sym) {
00039 return c_print(sym, vector<string>());
00040 }
00041
00042 string c_print(const Sym& sym, const vector<string>& vars) {
00043 const SymVec& args = sym.args();
00044 vector<string> names(args.size());
00045 for (unsigned i = 0; i < args.size(); ++i) {
00046 names[i] = c_print(args[i], vars);
00047 }
00048 return language[sym.token()]->c_print(names, vars);
00049 }
00050
00051
00052
00053
00054 double eval(const Sym& sym, const std::vector<double>& inputs) {
00055 return language[sym.token()]->eval(sym.args(), inputs);
00056 }
00057
00058
00059
00060 Interval eval(const Sym& sym, const vector<Interval>& inputs) {
00061 const SymVec& args = sym.args();
00062 vector<Interval> interv(args.size());
00063 for (unsigned i = 0; i < args.size(); ++i) {
00064 interv[i] = eval(args[i], inputs);
00065
00066 if (!valid(interv[i])) throw interval_error();
00067 }
00068 return language[sym.token()]->eval(interv, inputs);
00069 }
00070
00071
00072 void add_function_to_table(LanguageTable& table, token_t token) {
00073 const FunDef& fundef = *language[token];
00074
00075 if (fundef.has_varargs() == false) {
00076 table.add_function(token, fundef.min_arity());
00077 } else {
00078 table.add_function(token, 2);
00079 }
00080 }
00081
00082
00083
00084 double FunDef::eval(const SymVec& args, const vector<double>& inputs) const {
00085 vector<double> values(args.size());
00086 for (unsigned i = 0; i < args.size(); ++i) {
00087 values[i] = ::eval(args[i], inputs);
00088 }
00089
00090 return eval(values, inputs);
00091 }
00092
00093
00094 FunDef* make_var(int idx);
00095 static vector<token_t> var_token;
00096
00097 Sym SymVar(unsigned idx) {
00098 if (var_token.size() <= idx) {
00099
00100 var_token.resize(idx+1, token_t(-1));
00101 var_token[idx] = add_function( make_var(idx) );
00102 } else if (var_token[idx] == token_t(-1)) {
00103 var_token[idx] = add_function( make_var(idx) );
00104 }
00105 return Sym(var_token[idx]);
00106 }
00107
00108
00109
00110
00111 struct HashDouble{
00112 size_t operator()(double val) const {
00113 unsigned long h = 0;
00114 char* s = (char*)&val;
00115 for (unsigned i=0 ; i<sizeof(double); ++i)
00116 h = 5*h + s[i];
00117 return size_t(h);
00118 }
00119 };
00120
00121 #if USE_TR1
00122 typedef std::tr1::unordered_map<double, token_t> DoubleSet;
00123 typedef std::tr1::unordered_map<Sym, token_t> LambdaSet;
00124 #else
00125 typedef hash_map<double, token_t, HashDouble> DoubleSet;
00126 typedef hash_map<Sym, token_t, HashSym> LambdaSet;
00127 #endif
00128
00129 static DoubleSet doubleSet;
00130 static vector<double> token_value;
00131
00132 static LambdaSet lambdaSet;
00133 static vector<Sym> token_lambda;
00134
00135 static std::vector<token_t> free_list;
00136
00137 void delete_val(token_t token) {
00138
00139 if (is_constant(token)) {
00140
00141 double value = token_value[token];
00142 doubleSet.erase(value);
00143
00144 delete language[token];
00145 language[token] = 0;
00146 free_list.push_back(token);
00147 }
00148 else if (is_lambda(token)) {
00149
00150
00151 Sym expression = token_lambda[token];
00152 lambdaSet.erase(expression);
00153
00154 delete language[token];
00155 language[token] = 0;
00156 free_list.push_back(token);
00157 }
00158 }
00159
00160
00161 FunDef* make_const(double value);
00162
00163 void extend_free_list();
00164
00165 Sym SymConst(double value) {
00166
00167 DoubleSet::iterator it = doubleSet.find(value);
00168
00169 if (it != doubleSet.end()) {
00170 return Sym(it->second);
00171 }
00172
00173
00174 if (free_list.empty()) {
00175 extend_free_list();
00176 }
00177
00178 token_t token = free_list.back();
00179 free_list.pop_back();
00180
00181 assert(language[token] == 0);
00182
00183 language[token] = make_const(value);
00184
00185 doubleSet[value] = token;
00186 if (token_value.size() < token) token_value.resize(token+1);
00187 token_value[token] = value;
00188
00189 return Sym(token);
00190 }
00191
00192
00193 #include <utils/eoRNG.h>
00194 extern Sym default_const() { return SymConst(rng.normal()); }
00195
00196
00197 namespace {
00198
00199 class Var : public FunDef {
00200 public :
00201 unsigned idx;
00202 string default_str;
00203
00204 Var(unsigned _idx) : idx(_idx) {
00205 ostringstream os;
00206 os << "x[" << idx << ']';
00207 default_str = os.str();
00208 }
00209
00210 double eval(const vector<double>& _, const vector<double>& inputs) const { return inputs[idx]; }
00211 double eval(const SymVec& _, const vector<double>& inputs) const { return inputs[idx]; }
00212 string c_print(const vector<string>& _, const vector<string>& names) const {
00213 if (names.empty()) {
00214 return default_str;
00215 }
00216 return names[idx];
00217 }
00218
00219 Interval eval(const vector<Interval>& _, const vector<Interval>& inputs) const {
00220 return inputs[idx];
00221 }
00222
00223 unsigned min_arity() const { return 0; }
00224
00225 string name() const { return "var"; }
00226
00227 };
00228
00229 class Const : public FunDef {
00230 public:
00231 double value;
00232 string value_str;
00233
00234 Const(double _value) : value(_value) {
00235 ostringstream os;
00236 os.precision(17);
00237 os.setf(ios::showpoint);
00238 os << '(' << value << ')';
00239 value_str = os.str();
00240 }
00241
00242
00243 double eval(const vector<double>& _, const vector<double>& inputs) const { return value; }
00244 double eval(const SymVec& _, const vector<double>& inputs) const { return value; }
00245 string c_print(const vector<string>& _, const vector<string>& names) const {
00246 return value_str;
00247 }
00248
00249 Interval eval(const vector<Interval>& _, const vector<Interval>& inputs) const {
00250 return Interval(value);
00251 }
00252
00253 unsigned min_arity() const { return 0; }
00254
00255 string name() const { return "parameter"; }
00256 };
00257
00258 }
00259
00260 void get_constants(Sym sym, vector<double>& ret) {
00261 token_t token = sym.token();
00262 if (is_constant(token)) {
00263 double val = static_cast<const Const*>(language[token])->value;
00264 ret.push_back(val);
00265 }
00266
00267 const SymVec& args = sym.args();
00268 for (unsigned i = 0; i < args.size(); ++i) {
00269 get_constants(args[i], ret);
00270 }
00271
00272 }
00273
00274 double get_constant_value(token_t token) {
00275 return static_cast<const Const*>(language[token])->value;
00276 }
00277
00279 vector<double> get_constants(Sym sym) {
00280 vector<double> retval;
00281 get_constants(sym, retval);
00282 return retval;
00283 }
00284
00287 Sym set_constants(Sym sym, vector<double>::const_iterator& it) {
00288
00289 token_t token = sym.token();
00290 if (is_constant(token)) {
00291 return SymConst(*it++);
00292 }
00293
00294 SymVec args = sym.args();
00295 for (unsigned i = 0; i < args.size(); ++i) {
00296 args[i] = set_constants(args[i], it);
00297 }
00298
00299 return Sym(token, args);
00300 }
00301
00302 Sym set_constants(Sym sym, const vector<double>& constants) {
00303 vector<double>::const_iterator it = constants.begin();
00304 return set_constants(sym, it);
00305 }
00306
00307
00308 vector<const FunDef*> get_defined_functions() {
00309 vector<const FunDef*> res;
00310 for (unsigned i = 0; i < language.size(); ++i) {
00311 res.push_back(language[i]);
00312
00313 if (is_constant(i) || is_variable(i)) {
00314 res.back() = 0;
00315 }
00316 }
00317
00318 return res;
00319 }
00320
00321 FunDef* make_var(int idx) { return new Var(idx); }
00322 FunDef* make_const(double value) { return new Const(value); }
00323
00324 bool is_constant(token_t token) {
00325 const Const* cnst = dynamic_cast<const Const*>( language[token] );
00326 return cnst != 0;
00327 }
00328
00329 bool is_variable(token_t token) {
00330 const Var* var = dynamic_cast<const Var*>( language[token] );
00331 return var != 0;
00332 }
00333
00334 unsigned get_variable_index(token_t token) {
00335 const Var* var = static_cast<const Var*>( language[token] );
00336 return var->idx;
00337 }
00338
00339 namespace {
00340 class Lambda : public FunDef {
00341 public:
00342 Sym expression;
00343 int arity;
00344
00345 Lambda(Sym expr, int arity_) : expression(expr), arity(arity_) {}
00346
00347 double eval(const vector<double>& vals, const vector<double>& _) const {
00348 return ::eval(expression, vals);
00349 }
00350
00351 string c_print(const vector<string>& args, const vector<string>& _) const {
00352 return string("/*f*/") + ::c_print(expression, args) + string("/*eof*/");
00353 }
00354
00355 Interval eval(const vector<Interval>& args, const vector<Interval>& _) const {
00356 return ::eval(expression, args);
00357 }
00358
00359 unsigned min_arity() const { return arity; }
00360 string name() const { return "F"; }
00361
00362 };
00363 Sym normalize(Sym sym, SymVec& args) {
00364
00365 token_t token = sym.token();
00366 const Var* var = dynamic_cast< const Var*>(language[token]);
00367
00368 if (var != 0) {
00369 for (unsigned i = 0; i < args.size(); ++i) {
00370 if (sym == args[i]) {
00371 return SymVar(i);
00372 }
00373 }
00374
00375
00376 args.push_back(sym);
00377 return SymVar(args.size()-1);
00378
00379 }
00380
00381 SymVec a = sym.args();
00382 for (unsigned i = 0; i < a.size(); ++i) {
00383 a[i] = normalize(a[i], args);
00384 }
00385
00386 return Sym(token, a);
00387 }
00388 }
00389
00390 bool is_lambda(token_t token) {
00391 const Lambda* lambda = dynamic_cast<const Lambda*>( language[token]);
00392 return lambda != 0;
00393 }
00394
00395 std::ostream& print_list(Sym sym, ostream& os) {
00396 os << sym.token() << ' ';
00397
00398 const SymVec& args = sym.args();
00399 for (unsigned i = 0; i < args.size(); ++i) {
00400 print_list(args[i], os);
00401 }
00402 return os;
00403 }
00404
00405 token_t new_lambda(Sym sym, int arity) {
00406
00407
00408 LambdaSet::iterator it = lambdaSet.find(sym);
00409 if (it != lambdaSet.end()) {
00410 return it->second;
00411 }
00412
00413
00414
00415 Lambda* lambda = new Lambda(sym, arity);
00416
00417 if (free_list.empty()) {
00418 extend_free_list();
00419 }
00420
00421 token_t token = free_list.back();
00422 free_list.pop_back();
00423 language[token] = lambda;
00424
00425 lambdaSet[sym] = token;
00426 if (token_lambda.size() <= token) token_lambda.resize(token+1);
00427 token_lambda[token] = sym;
00428
00429 return token;
00430 }
00431
00432
00433 typedef hash_map<Sym, unsigned, HashSym> OccMap;
00434
00435 void count_occurances(Sym sym, OccMap& occ) {
00436 occ[sym]++;
00437 const SymVec& args = sym.args();
00438 for (unsigned i = 0; i < args.size(); ++i) {
00439 count_occurances(args[i], occ);
00440 }
00441 }
00442
00443 Sym create_lambda(Sym sym, OccMap& occ, unsigned nvars, vector<Sym>& args) {
00444 unsigned o = occ[sym];
00445 unsigned sz = sym.size();
00446
00447 if (o * sz > o + sz + nvars || is_variable(sym.token()) ) {
00448
00449 for (unsigned i = 0; i < args.size(); ++i) {
00450 if (args[i] == sym) {
00451 return SymVar(i);
00452 }
00453 }
00454
00455 args.push_back(sym);
00456 return SymVar(args.size()-1);
00457 }
00458
00459 SymVec sym_args = sym.args();
00460 for (unsigned i = 0; i < sym_args.size(); ++i) {
00461 sym_args[i] = create_lambda(sym_args[i], occ, nvars, args);
00462 }
00463
00464 return Sym(sym.token(), sym_args);
00465
00466 }
00467
00468 Sym compress(Sym sym) {
00469 OccMap occ(sym.size());
00470 count_occurances(sym, occ);
00471
00472 unsigned nvars = 0;
00473 for (OccMap::iterator it = occ.begin(); it != occ.end(); ++it) {
00474 if (is_variable(it->first.token())) nvars++;
00475 }
00476
00477 SymVec args;
00478 Sym body = create_lambda(sym, occ, nvars, args);
00479
00480
00481 if (body.size() < sym.size()) {
00482
00483 body = compress(body);
00484
00485 token_t token = new_lambda(body, args.size());
00486
00487 for (unsigned i = 0; i < args.size(); ++i) {
00488 args[i] = compress(args[i]);
00489 }
00490
00491 Sym result = Sym(token, args);
00492 return compress(result);
00493 }
00494
00495 return sym;
00496 }
00497
00498 Sym SymLambda(Sym expr) { return compress(expr); }
00499
00500 Sym expand(Sym expr, const SymVec& args) {
00501
00502 const Var* var = dynamic_cast<const Var*>( language[expr.token()] );
00503 if (var != 0) {
00504 return args[var->idx];
00505 }
00506
00507 SymVec expr_args = expr.args();
00508 for (unsigned i = 0; i < expr_args.size(); ++i) {
00509 expr_args[i] = expand(expr_args[i], args);
00510 }
00511
00512 return Sym(expr.token(), expr_args);
00513 }
00514
00515 Sym SymUnlambda(Sym sym) {
00516 Sym retval = sym;
00517 const Lambda* lambda = dynamic_cast<const Lambda*>( language[sym.token()] );
00518 if (lambda != 0) {
00519 retval = expand(lambda->expression, sym.args());
00520 }
00521
00522 return retval;
00523 }
00524
00525 Sym expand_all(Sym sym) {
00526 SymVec args = sym.args();
00527 for (unsigned i = 0; i < args.size(); ++i) {
00528 args[i] = expand_all(args[i]);
00529 }
00530
00531 Sym nw = SymUnlambda( Sym(sym.token(), args) );
00532
00533 if (nw != sym) {
00534 nw = expand_all(nw);
00535 }
00536
00537 return nw;
00538 }
00539
00540 namespace {
00541
00542 class Sum : public FunDef {
00543
00544 public :
00545
00546 double eval(const vector<double>& vals, const vector<double>& _) const {
00547 double res = 0;
00548 for (unsigned i = 0; i < vals.size(); ++i) res += vals[i];
00549 return res;
00550 }
00551
00552 string c_print(const vector<string>& args, const vector<string>& _) const {
00553 if (args.empty()) { return "0.0"; }
00554
00555 ostringstream os;
00556 os << "(" << args[0];
00557 for (unsigned i = 1; i < args.size(); ++i) {
00558 os << "+" << args[i];
00559 }
00560 os << ")";
00561 return os.str();
00562 }
00563
00564 Interval eval(const vector<Interval>& args, const vector<Interval>& inputs) const {
00565 Interval interv(0.0);
00566 for (unsigned i = 0; i < args.size(); ++i) {
00567 interv += args[i];
00568 }
00569 return interv;
00570 }
00571
00572 unsigned min_arity() const { return 0; }
00573 bool has_varargs() const { return true; }
00574
00575 string name() const { return "sum"; }
00576 };
00577
00578
00579 class Prod : public FunDef {
00580
00581 public :
00582
00583 double eval(const vector<double>& vals, const vector<double>& _) const {
00584 double res = 1;
00585 for (unsigned i = 0; i < vals.size(); ++i) res *= vals[i];
00586 return res;
00587 }
00588
00589 string c_print(const vector<string>& args, const vector<string>& _) const {
00590 if (args.empty()) { return "1.0"; }
00591
00592 ostringstream os;
00593 os << "(" << args[0];
00594 for (unsigned i = 1; i < args.size(); ++i) {
00595 os << "*" << args[i];
00596 }
00597 os << ")";
00598
00599 return os.str();
00600 }
00601
00602 Interval eval(const vector<Interval>& args, const vector<Interval>& inputs) const {
00603 Interval interv(1.0);
00604 for (unsigned i = 0; i < args.size(); ++i) {
00605 interv *= args[i];
00606 }
00607 return interv;
00608 }
00609
00610 unsigned min_arity() const { return 0; }
00611 bool has_varargs() const { return true; }
00612
00613 string name() const { return "prod"; }
00614 };
00615
00616
00617 class Power : public FunDef {
00618 public :
00619 double eval(const vector<double>& vals, const vector<double>& _) const {
00620 return pow(vals[0], vals[1]);
00621 }
00622
00623 string c_print(const vector<string>& args, const vector<string>& _) const {
00624 return "pow(" + args[0] + ',' + args[1] + ')';
00625 }
00626
00627 Interval eval(const vector<Interval>& args, const vector<Interval>& _) const {
00628 Interval first = args[0];
00629 Interval second = args[1];
00630 Interval lg = log(first);
00631 if (!valid(lg)) throw interval_error();
00632 return exp(second * lg);
00633 }
00634
00635 unsigned min_arity() const { return 2; }
00636
00637 string name() const { return "pow"; }
00638 };
00639
00640 class IsNeg : public FunDef {
00641
00642 public:
00643 double eval(const vector<double>& vals, const vector<double>& _) const {
00644 if (vals[0] < 0.0) return vals[1];
00645 return vals[2];
00646 }
00647
00648 double eval(const Sym& sym, const vector<double>& inputs) const {
00649 const SymVec& args = sym.args();
00650 double arg0 = ::eval(args[0], inputs);
00651 if (arg0 < 0.0) {
00652 return ::eval(args[1], inputs);
00653 }
00654 return ::eval(args[2], inputs);
00655 }
00656
00657 string c_print(const vector<string>& args, const vector<string>& _) const {
00658 return "((" + args[0] + "<0.0)?" + args[1] + ":" + args[2]+")";
00659 }
00660
00661 Interval eval(const vector<Interval>& args, const vector<Interval>& _) const {
00662 Interval a0 = args[0];
00663 if (a0.upper() < 0.0) return args[1];
00664 if (a0.lower() >= 0.0) return args[2];
00665
00666 return Interval( std::min(args[1].lower(), args[2].lower()), std::max(args[1].upper(), args[2].upper()));
00667 }
00668
00669 unsigned min_arity() const { return 3; }
00670
00671 string name() const { return "ifltz"; }
00672 };
00673
00674 template <typename Func>
00675 class Unary : public FunDef {
00676
00677 Func un;
00678
00679 double eval(const vector<double>& vals, const vector<double>& _) const {
00680 return un(vals[0]);
00681 }
00682
00683 string c_print(const vector<string>& args, const vector<string>& _) const {
00684 return un(args[0]);
00685 }
00686
00687 Interval eval(const vector<Interval>& args, const vector<Interval>& _) const {
00688 return un(args[0]);
00689 }
00690
00691 unsigned min_arity() const { return 1; }
00692
00693 string name() const { return un.name(); }
00694
00695 };
00696
00697 struct Inv {
00698 double operator()(double val) const { return 1.0 / val; }
00699 string operator()(string v) const { return "(1./" + v + ")"; }
00700 Interval operator()(Interval v) const { return 1.0 / v; }
00701
00702 string name() const { return "inv"; }
00703 };
00704
00705 struct Min {
00706 double operator()(double val) const { return -val; }
00707 string operator()(string v) const { return "(-" + v + ")"; }
00708 Interval operator()(Interval v) const { return -v; }
00709
00710 string name() const { return "min"; }
00711 };
00712
00713 }
00714
00715 string prototypes = "double pow(double, double);";
00716 string get_prototypes() { return prototypes; }
00717 unsigned add_prototype(string str) { prototypes += string("double ") + str + "(double);"; return prototypes.size(); }
00718
00719 token_t add_function(FunDef* function, token_t where) {
00720 if (language.size() <= where) language.resize(where+1);
00721 language[where] = function;
00722 return 0;
00723 }
00724
00725 namespace {
00726
00727 #define FUNCDEF(funcname) struct funcname##_struct { \
00728 double operator()(double val) const { return funcname(val); }\
00729 string operator()(string val) const { return string(#funcname) + '(' + val + ')'; }\
00730 Interval operator()(Interval val) const { return funcname(val); }\
00731 string name() const { return string(#funcname); }\
00732 };\
00733 static const token_t funcname##_token_static = add_function( new Unary<funcname##_struct>, funcname##_token);\
00734 unsigned funcname##_size = add_prototype(#funcname);
00735
00736 static token_t ssum_token = add_function( new Sum , sum_token);
00737 static token_t sprod_token = add_function( new Prod, prod_token);
00738 static token_t sinv_token = add_function( new Unary<Inv>, inv_token);
00739 static token_t smin_token = add_function( new Unary<Min>, min_token);
00740 static token_t spow_token = add_function( new Power, pow_token);
00741 static token_t sifltz_token = add_function( new IsNeg, ifltz_token);
00742
00743 FUNCDEF(sin);
00744 FUNCDEF(cos);
00745 FUNCDEF(tan);
00746 FUNCDEF(asin);
00747 FUNCDEF(acos);
00748 FUNCDEF(atan);
00749
00750 FUNCDEF(sinh);
00751 FUNCDEF(cosh);
00752 FUNCDEF(tanh);
00753 FUNCDEF(asinh);
00754 FUNCDEF(acosh);
00755 FUNCDEF(atanh);
00756
00757 FUNCDEF(exp);
00758 FUNCDEF(log);
00759 }
00760
00761 double sqr(double x) { return x*x; }
00762
00763 namespace {
00764 FUNCDEF(sqr);
00765 FUNCDEF(sqrt);
00766
00767 const int buildInFunctionOffset = language.size();
00768 }
00769
00770 void add_tokens() {
00771 unsigned sz = language.size();
00772 language.resize(sz + sz+1);
00773
00774 for (unsigned i = sz; i < language.size(); ++i) {
00775 free_list.push_back(i);
00776 }
00777 }
00778
00779 void extend_free_list() {
00780
00781 const vector<unsigned>& refcount = Sym::token_refcount();
00782 for (unsigned i = buildInFunctionOffset; i < refcount.size(); ++i) {
00783 if (language[i] == 0) continue;
00784
00785 bool c = is_constant(i);
00786 bool l = is_lambda(i);
00787
00788 if (refcount[i] == 0 && (c || l)) {
00789
00790 if (c) {
00791 doubleSet.erase(token_value[i]);
00792 }
00793
00794 if (l) {
00795 lambdaSet.erase(token_lambda[i]);
00796 }
00797
00798 delete language[i];
00799 language[i] = 0;
00800 free_list.push_back(i);
00801 }
00802 }
00803
00804
00805 if (free_list.empty()) {
00806 add_tokens();
00807 }
00808 }
00809
00810
00811
00812 void write_raw(ostream& os, const Sym& sym) {
00813 token_t token = sym.token();
00814 const SymVec& args = sym.args();
00815
00816 if (is_constant(token)) {
00817 os << "c" << language[token]->c_print(vector<string>(), vector<string>());
00818 } else {
00819
00820 const Var* var = dynamic_cast<const Var*>( language[token] );
00821
00822 if (var != 0) {
00823 os << "v" << var->idx;
00824 } else {
00825 os << "f" << token << ' ' << args.size();
00826 }
00827 }
00828
00829 for (unsigned i = 0; i < args.size(); ++i) {
00830 write_raw(os, args[i]);
00831 }
00832 }
00833
00834 string write_raw(const Sym& sym) {
00835
00836 ostringstream os;
00837 write_raw(os, sym);
00838
00839 return os.str();
00840 }
00841
00842 Sym read_raw(istream& is) {
00843 char id = is.get();
00844
00845 switch (id) {
00846 case 'c' :
00847 {
00848 double val;
00849 is.get();
00850 is >> val;
00851 is.get();
00852 return SymConst(val);
00853 }
00854 case 'v' :
00855 {
00856 unsigned idx;
00857 is >> idx;
00858 return SymVar(idx);
00859 }
00860 case 'f' :
00861 {
00862 token_t token;
00863 unsigned arity;
00864 is >> token;
00865 is >> arity;
00866 SymVec args(arity);
00867 for (unsigned i = 0; i < arity; ++i) {
00868 args[i] = read_raw(is);
00869 }
00870
00871 return Sym(token, args);
00872 }
00873 default : {
00874 cerr << "Character = " << id << " Could not read formula from stream" << endl;
00875 exit(1);
00876 }
00877
00878 }
00879
00880 return Sym();
00881 }
00882
00883 Sym read_raw(string str) {
00884 istringstream is(str);
00885 return read_raw(is);
00886 }
00887
00888 void read_raw(istream& is, Sym& sym) {
00889 sym = read_raw(is);
00890 }
00891