Permalink
Browse files

Added prepare command

  • Loading branch information...
1 parent 3fa163f commit 5bd5edd4f8662ba529b999433aa0f35d5c341944 @mwolf76 committed Dec 28, 2013
@@ -18,8 +18,8 @@ INCLUDES = -I$(top_srcdir)/src/ -I$(top_srcdir)/src/dd \
AM_CPPFLAGS=@AM_CPPFLAGS@
AM_CXXFLAGS=@AM_CXXFLAGS@
-PKG_HH = base.hh
-PKG_CC = base.cc
+PKG_HH = base.hh prepare.hh
+PKG_CC = base.cc prepare.cc
PKG_SOURCES = $(PKG_H) $(PKG_CC)
View
@@ -2,9 +2,6 @@
* @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
View
@@ -0,0 +1,46 @@
+/**
+ * @file prepare.cc
+ * @brief Prepare 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 <prepare.hh>
+
+Prepare::Prepare(IModel& model)
+ : Algorithm(model)
+{}
+
+Prepare::~Prepare()
+{}
+
+void Prepare::process()
+{
+ clock_t t0 = clock(), t1;
+ double secs;
+
+ TRACE << "Phase 1" << endl;
+ prepare();
+
+ TRACE << "Phase 2" << endl;
+ compile();
+
+ t1 = clock(); secs = (double) (t1 - t0) / (double) CLOCKS_PER_SEC;
+ os () << "-- preparation completed, took " << secs
+ << " seconds" << endl;
+
+}
View
@@ -0,0 +1,40 @@
+/**
+ * @file Prepare Algorithm.hh
+ * @brief SAT Prepare Algorithm
+ *
+ * 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 PREPARE_ALGORITHM_H
+#define PREPARE_ALGORITHM_H
+
+#include <base.hh>
+
+class Prepare : public Algorithm {
+
+public:
+ Prepare(IModel& model);
+ ~Prepare();
+
+ void process();
+};
+#endif
@@ -1,6 +1,6 @@
/**
* @file MC Algorithm.hh
- * @brief SAT Simulation Algorithm
+ * @brief SAT-based BMC simulation algorithm
*
* This module contains definitions and services that implement an
* optimized storage for expressions. Expressions are stored in a
@@ -113,8 +113,8 @@ void Simulation::process()
halt = wm.eval ( witness(), em.make_main(), f_halt_cond, k);
}
}
- if (!halt) {
+ if (!halt) {
do {
t1 = clock(); secs = (double) (t1 - t0) / (double) CLOCKS_PER_SEC;
os () << "-- completed step " << 1 + k
@@ -1,10 +1,6 @@
/**
- * @file Simulation Algorithm.hh
- * @brief SAT Simulation Algorithm
- *
- * 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.
+ * @file simulation.hh
+ * @brief SAT-based BMC simulation algorithm
*
* Copyright (C) 2012 Marco Pensallorto < marco AT pensallorto DOT gmail DOT com >
*
View
@@ -52,6 +52,9 @@ public:
inline Command_ptr make_load_model(const char *filepath)
{ return new LoadModelCommand(f_interpreter, filepath); }
+ inline Command_ptr make_prepare()
+ { return new PrepareCommand(f_interpreter); }
+
inline Command_ptr make_simulate(Expr_ptr halt_cond, Expr_ptr resume_id, ExprVector& constraints)
{ return new SimulateCommand(f_interpreter, halt_cond, resume_id, constraints); }
View
@@ -50,7 +50,7 @@ Variant LoadModelCommand::operator()()
// model analysis
bool status = ModelMgr::INSTANCE().analyze();
- return Variant( status ? "OK" : "ERROR" );
+ return Variant( status ? "Ok" : "ERROR" );
}
LoadModelCommand::~LoadModelCommand()
@@ -83,6 +83,21 @@ Variant TimeCommand::operator()()
TimeCommand::~TimeCommand()
{}
+// -- Prepare -------------------------------------------------------------
+PrepareCommand::PrepareCommand(Interpreter& owner)
+ : Command(owner)
+ , f_prepare(* ModelMgr::INSTANCE().model())
+{}
+
+Variant PrepareCommand::operator()()
+{
+ f_prepare.process();
+ return Variant("Ok");
+}
+
+PrepareCommand::~PrepareCommand()
+{}
+
// -- Check -------------------------------------------------------------
CheckCommand::CheckCommand(Interpreter& owner, Expr_ptr formula)
: Command(owner)
@@ -115,8 +130,7 @@ Variant SimulateCommand::operator()()
f_sim.process();
ostringstream tmp;
- tmp << "Simulation is ";
- tmp << ((f_sim.status() == SIMULATION_SAT) ? "SAT" : "UNSAT");
+ tmp << "Simulation halted, check witness " << f_sim.witness().id();
return Variant(tmp.str());
}
View
@@ -29,6 +29,8 @@
#include <compiler/compiler.hh>
#include <sat.hh>
+/* algorithms */
+#include <prepare.hh>
#include <bmc/bmc.hh>
#include <sim/simulation.hh>
@@ -83,6 +85,17 @@ public:
Variant virtual operator()();
};
+class PrepareCommand : public Command {
+public:
+ PrepareCommand(Interpreter& owner);
+ virtual ~PrepareCommand();
+
+ Variant virtual operator()();
+
+private:
+ Prepare f_prepare;
+};
+
/* Performs a new simulation with given constraints and halting
conditions. Simulation can be resumed unless it's last status is
UNSAT. */
View
@@ -158,14 +158,17 @@ commands returns [Command_ptr res]
| c=time_command
{ $res = c; }
+ | c=prepare_command
+ { $res = c; }
+
| c=model_command
{ $res = c; }
| c=simulate_command
{ $res = c; }
| c=quit_command
- { $res = c; }
+ { $res = c; }
;
help_command returns [Command_ptr res]
@@ -177,20 +180,25 @@ help_command returns [Command_ptr res]
{ $res = cm.make_help(topic); }
;
-check_command returns [Command_ptr res]
- : 'check' expr=toplevel_expression
- { $res = cm.make_check(expr); }
- ;
-
time_command returns [Command_ptr res]
: 'time' { $res = cm.make_time(); }
;
+prepare_command returns [Command_ptr res]
+ : 'prepare' { $res = cm.make_prepare(); }
+ ;
+
model_command returns [Command_ptr res]
: 'MODEL' fp=filepath
{ $res = cm.make_load_model(fp); }
;
+
+check_command returns [Command_ptr res]
+ : 'check' expr=toplevel_expression
+ { $res = cm.make_check(expr); }
+ ;
+
simulate_command returns [Command_ptr res]
@init {
Expr_ptr halt_cond = NULL;

0 comments on commit 5bd5edd

Please sign in to comment.