+ // constructors
+public:
+ realsymbol();
+ explicit realsymbol(const std::string & initname, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, const std::string & texname, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, unsigned rt, unsigned rtt, unsigned domain = domain::real);
+ realsymbol(const std::string & initname, const std::string & texname, unsigned rt, unsigned rtt, unsigned domain = domain::real);
+};