Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Missing files

  • Loading branch information...
commit 4f847c0bb9ee9dc9ea6a2cef111718fe3a0ea4a2 1 parent 5a22f8d
@mwolf76 authored
Showing with 260 additions and 0 deletions.
  1. +139 −0 src/algorithms/base.cc
  2. +121 −0 src/algorithms/base.hh
View
139 src/algorithms/base.cc
@@ -0,0 +1,139 @@
+/**
+ * @file Base Algorithm.cc
+ * @brief Base Algorithm
+ *
+ * This module contains definitions and services that implement an
+ * abstract algorithm.
+ *
+ * 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 <base.hh>
+
+Algorithm::Algorithm(IModel& model)
+ : f_mm(ModelMgr::INSTANCE())
+ , f_em(ExprMgr::INSTANCE())
+ , f_tm(TypeMgr::INSTANCE())
+ , f_model(model)
+ , f_engine(* new SAT())
+{
+ set_param("alg_name", "test");
+ DEBUG << "Creating Base algoritm instance "
+ << get_param("alg_name")
+ << " @" << this
+ << endl;
+
+ /* pre-compilation */
+ prepare();
+}
+
+Algorithm::~Algorithm()
+{
+ DEBUG << "Destroying Base algoritm instance"
+ << get_param("alg_name")
+ << " @" << this
+ << endl;
+
+ delete & f_engine;
+}
+
+void Algorithm::set_param(string key, Variant value)
+{ f_params [ key ] = value; }
+
+Variant& Algorithm::get_param(const string key)
+{
+ const ParametersMap::iterator eye = f_params.find(key);
+
+ if (eye != f_params.end()) {
+ return (*eye).second;
+ }
+
+ else return NilValue;
+}
+
+void Algorithm::prepare()
+{
+ /* internal structures are empty */
+ assert( 0 == f_init_adds.size() );
+ assert( 0 == f_trans_adds.size() );
+
+ const Modules& modules = f_model.modules();
+ for (Modules::const_iterator m = modules.begin();
+ m != modules.end(); ++ m) {
+
+ Module& module = dynamic_cast <Module&> (*m->second);
+
+ /* INIT */
+ const ExprVector init = module.init();
+ for (ExprVector::const_iterator init_eye = init.begin();
+ init_eye != init.end(); ++ init_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*init_eye);
+
+ f_init_adds.push_back(f_compiler.process(ctx, body));
+ }
+
+ /* TRANS */
+ const ExprVector trans = module.trans();
+ for (ExprVector::const_iterator trans_eye = trans.begin();
+ trans_eye != trans.end(); ++ trans_eye) {
+
+ Expr_ptr ctx = module.expr();
+ Expr_ptr body = (*trans_eye);
+
+ f_trans_adds.push_back(f_compiler.process(ctx, body));
+ }
+ }
+}
+
+void Algorithm::assert_fsm_init(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_init_adds.size();
+ TRACE << "CNFizing INITs @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_init_adds.begin(); f_init_adds.end() != i; ++ i) {
+ f_engine.push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
+
+void Algorithm::assert_fsm_trans(step_t time, group_t group, color_t color)
+{
+ clock_t t0 = clock();
+ unsigned n = f_trans_adds.size();
+
+ TRACE << "CNFizing TRANSes @" << time
+ << "... (" << n << " formulas)"
+ << endl;
+
+ ADDVector::iterator i;
+ for (i = f_trans_adds.begin(); f_trans_adds.end() != i; ++ i) {
+ f_engine.push( *i, time, group, color);
+ }
+
+ clock_t elapsed = clock() - t0;
+ double secs = (double) elapsed / (double) CLOCKS_PER_SEC;
+ TRACE << "Done. (took " << secs << " seconds)" << endl;
+}
View
121 src/algorithms/base.hh
@@ -0,0 +1,121 @@
+/**
+ * @file Base Algorithm.hh
+ * @brief Base Algorithm
+ *
+ * This module contains definitions and services that implement an
+ * abstract algorithm.
+ *
+ * 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 BASE_ALGORITHM_H
+#define BASE_ALGORITHM_H
+
+#include <model.hh>
+#include <model_mgr.hh>
+
+#include <enc.hh>
+#include <enc_mgr.hh>
+
+#include <witness.hh>
+#include <variant.hh>
+
+/* SAT interface */
+#include <sat.hh>
+
+/* Model compiler */
+#include <compilers/compiler.hh>
+
+typedef unordered_map<string, Variant> ParametersMap;
+
+using Minisat::group_t;
+using Minisat::MAINGROUP;
+
+using Minisat::color_t;
+using Minisat::BACKGROUND;
+
+using Minisat::SAT;
+using Minisat::STATUS_SAT;
+using Minisat::STATUS_UNSAT;
+
+class Algorithm {
+public:
+ Algorithm(IModel& model);
+ virtual ~Algorithm();
+
+ // actual algorithm
+ virtual void process() =0;
+
+ IModel& model() const
+ { return f_model; }
+
+ // alg abstract param iface (key -> value map)
+ void set_param(string key, Variant value);
+ Variant& get_param(const string key);
+
+protected:
+ void assert_fsm_init (step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
+ void assert_fsm_trans(step_t time,
+ group_t group = MAINGROUP,
+ color_t color = BACKGROUND);
+
+ inline ModelMgr& mm()
+ { return f_mm; }
+
+ inline ExprMgr& em()
+ { return f_em; }
+
+ inline TypeMgr& tm()
+ { return f_tm; }
+
+ inline IModel& model()
+ { return f_model; }
+
+ inline SAT& engine()
+ { return f_engine; }
+
+ inline Compiler& compiler()
+ { return f_compiler; }
+
+private:
+ // managers
+ ModelMgr& f_mm;
+ ExprMgr& f_em;
+ TypeMgr& f_tm;
+
+ IModel& f_model;
+ ADDVector f_init_adds;
+ ADDVector f_trans_adds;
+
+ // services
+ void prepare();
+
+ /* Model Compiler */
+ Compiler f_compiler;
+
+ /* The Engine */
+ SAT& f_engine;
+
+ /* Parameters */
+ ParametersMap f_params;
+};
+
+#endif
Please sign in to comment.
Something went wrong with that request. Please try again.