Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Added missing file

  • Loading branch information...
commit f70b578f95d4e1f411b44632266e18bfa7bcf002 1 parent 5210f46
@mwolf76 authored
Showing with 305 additions and 0 deletions.
  1. +201 −0 src/model/symbol.cc
  2. +104 −0 src/model/symbol.hh
View
201 src/model/symbol.cc
@@ -0,0 +1,201 @@
+/**
+ * @file symbol.cc
+ * @brief Symbol classes
+ *
+ * This module contains definitions and services that implement an
+ * optimized storage for expressions. Expressions are stored in a
+ * Directed Acyclic Graph (DAG) for data sharing.
+ *
+ * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com >
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ *
+ **/
+
+#include <model.hh>
+#include <type_exceptions.hh>
+
+void Model::add_module(Expr_ptr name, IModule_ptr module)
+{
+ DEBUG << "Added module: '" << name << "'" << endl;
+ f_modules.insert( make_pair<Expr_ptr, IModule_ptr> (name, module));
+}
+
+bool ISymbol::is_variable(void) const
+{
+ return NULL != dynamic_cast <const IVariable_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+}
+
+IVariable& ISymbol::as_variable(void) const
+{
+ IVariable_ptr res = dynamic_cast <const IVariable_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+ assert (res);
+ return (*res);
+}
+
+bool ISymbol::is_temporary(void) const
+{
+ return NULL != dynamic_cast <const ITemporary_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+}
+
+ITemporary& ISymbol::as_temporary(void) const
+{
+ ITemporary_ptr res = dynamic_cast <const ITemporary_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+ assert (res);
+ return (*res);
+}
+
+bool ISymbol::is_define(void) const
+{
+ return NULL != dynamic_cast <const IDefine_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+}
+
+IDefine& ISymbol::as_define(void) const
+{
+ IDefine_ptr res = dynamic_cast <const IDefine_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+ assert (res);
+ return (*res);
+}
+
+bool ISymbol::is_const() const
+{
+ return NULL != dynamic_cast <const IConstant_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+}
+
+IConstant& ISymbol::as_const(void) const
+{
+ IConstant_ptr res = dynamic_cast <const IConstant_ptr>
+ (const_cast <const ISymbol_ptr> (this));
+ assert (res);
+ return (*res);
+}
+
+ostream& operator<<(ostream& os, Module& module)
+{ return os << module.expr(); }
+
+ostream& operator<<(ostream& os, AnalyzerException& ae)
+{ return os << ae.what(); }
+
+
+//
+
+Module::Module(const Expr_ptr name)
+ : f_name(name)
+
+ , f_localConsts()
+ , f_localVars()
+ , f_localDefs()
+
+ , f_init()
+ , f_trans()
+{}
+
+void Module::add_localVar(Expr_ptr name, IVariable_ptr var)
+{
+ DEBUG << "Module " << (*this)
+ << ", added local var " << var << endl;
+ f_localVars.insert(make_pair<FQExpr,
+ IVariable_ptr>(FQExpr(expr(), name), var));
+}
+
+void Module::add_localDef(Expr_ptr name, IDefine_ptr body)
+{
+ DEBUG << "Module " << (*this)
+ << ", added local def " << name << endl;
+ f_localDefs.insert(make_pair<FQExpr,
+ IDefine_ptr>(FQExpr(expr(), name), body));
+}
+
+void Module::add_localConst(Expr_ptr name, IConstant_ptr k)
+{
+ DEBUG << "Module " << (*this)
+ << ", added local const " << name << endl;
+ f_localConsts.insert(make_pair<FQExpr,
+ IConstant_ptr>(FQExpr(expr(), name), k));
+}
+
+void Module::add_init(Expr_ptr expr)
+{
+ DEBUG << "Module " << (*this)
+ << ", added INIT " << expr << endl;
+ f_init.push_back(expr);
+}
+
+void Module::add_trans(Expr_ptr expr)
+{
+ DEBUG << "Module " << (*this)
+ << ", added TRANS " << expr << endl;
+ f_trans.push_back(expr);
+}
+
+Model::Model()
+ : f_modules()
+{
+ DEBUG << "Initialized Model instance @" << this << endl;
+}
+
+Model::~Model()
+{
+ // TODO: free memory for symbols... (they've been allocated using new)
+}
+
+SymbIter::SymbIter(IModel& model, Expr_ptr formula)
+ : f_model(model)
+ , f_formula(formula)
+{
+ assert( !f_formula ); // TODO implement COI
+
+ /* Fetch modules from model */
+ const Modules& modules = f_model.modules();
+
+ for (Modules::const_iterator mi = modules.begin();
+ mi != modules.end(); ++ mi) {
+
+ IModule& module = * (*mi).second;
+
+ { /* defines */
+ Defines defs = module.get_localDefs();
+ for (Defines::const_iterator di = defs.begin();
+ di != defs.end(); ++ di) {
+
+ IDefine_ptr def = (*di).second;
+ f_symbols.push_back(def);
+ }
+ }
+
+ { /* variables */
+ Variables vars = module.get_localVars();
+ for (Variables::const_iterator vi = vars.begin();
+ vi != vars.end(); ++ vi) {
+
+ IVariable_ptr var = (*vi).second;
+ f_symbols.push_back(var);
+ }
+ }
+ }
+
+ f_iter = f_symbols.begin();
+}
+
+SymbIter::~SymbIter()
+{
+}
View
104 src/model/symbol.hh
@@ -0,0 +1,104 @@
+/**
+ * @file symbol.hh
+ * @brief Symbol interface
+ *
+ * This module contains definitions and services that implement an
+ * optimized storage for expressions. Expressions are stored in a
+ * Directed Acyclic Graph (DAG) for data sharing.
+ *
+ * Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com >
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Lesser General Public
+ * License as published by the Free Software Foundation; either
+ * version 2.1 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ * Lesser General Public License for more details.
+ *
+ * You should have received a copy of the GNU Lesser General Public
+ * License along with this library; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ *
+ **/
+
+#ifndef SYMBOL_H
+#define SYMBOL_H
+
+typedef vector<FQExpr> FQExprVector;
+
+class ISymbol;
+typedef ISymbol* ISymbol_ptr;
+typedef unordered_map<FQExpr, ISymbol_ptr, FQExprHash, FQExprEq> Symbols;
+
+class ILiteral;
+typedef ILiteral* ILiteral_ptr;
+typedef unordered_map<FQExpr, ILiteral_ptr, FQExprHash, FQExprEq> Literals;
+
+class IConstant;
+typedef IConstant* IConstant_ptr;
+typedef unordered_map<FQExpr, IConstant_ptr, FQExprHash, FQExprEq> Constants;
+
+class IVariable;
+typedef IVariable* IVariable_ptr;
+typedef unordered_map<FQExpr, IVariable_ptr, FQExprHash, FQExprEq> Variables;
+
+class ITemporary;
+typedef ITemporary* ITemporary_ptr;
+typedef unordered_map<FQExpr, ITemporary_ptr, FQExprHash, FQExprEq> Temporaries;
+
+class IDefine;
+typedef IDefine* IDefine_ptr;
+typedef unordered_map<FQExpr, IDefine_ptr, FQExprHash, FQExprEq> Defines;
+
+// -- primary decls --------------------------------------------------------------
+class ISymbol : IObject {
+public:
+ virtual const Expr_ptr ctx() const =0;
+ virtual const Expr_ptr expr() const =0;
+
+ bool is_const() const;
+ IConstant& as_const() const;
+
+ bool is_variable() const;
+ IVariable& as_variable() const;
+
+ bool is_temporary() const;
+ ITemporary& as_temporary() const;
+
+ bool is_define() const;
+ IDefine& as_define() const;
+};
+
+class ILiteral : public ISymbol {
+public:
+ virtual value_t value() const =0;
+ virtual const Type_ptr type() const =0;
+};
+
+class IConstant : public ISymbol {
+public:
+ virtual value_t value() const =0;
+ virtual const Type_ptr type() const =0;
+};
+
+class IVariable : public ISymbol {
+public:
+ // var types are used for enc building
+ virtual const Type_ptr type() const =0;
+};
+
+class ITemporary : public IVariable {
+public:
+ virtual const Type_ptr type() const =0;
+};
+
+class IDefine : public ISymbol {
+public:
+ // defines have no type, it has to be inferred.
+ virtual const Expr_ptr body() const =0;
+};
+
+#endif
Please sign in to comment.
Something went wrong with that request. Please try again.