clean

src/smvlang/Makefile

@@ -0,0 +1,30 @@
+SRC = smv_language.cpp smv_parser.cpp smv_typecheck.cpp expr2smv.cpp \
+      y.tab.cpp lex.yy.cpp smv_parse_tree.cpp
+
+include ../config.inc
+
+INCLUDES= -I $(CBMC)/src -I $(CBMC)/src/util
+
+CLEANFILES = smvlang$(LIBEXT) y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output
+
+all: smvlang$(LIBEXT)
+
+###############################################################################
+
+smvlang$(LIBEXT): $(OBJ)
+	$(LINKLIB)
+
+y.tab.cpp: parser.y
+	$(YACC) $(YFLAGS) $$flags -pyysmv -d parser.y -o y.tab.cpp
+
+y.tab.h: y.tab.cpp
+	if [ -e y.tab.hpp ] ; then mv y.tab.hpp y.tab.h ; else \
+        mv y.tab.cpp.h y.tab.h ; fi
+
+lex.yy.cpp: scanner.l
+	$(LEX) -Pyysmv -olex.yy.cpp scanner.l
+
+# extra dependencies
+y.tab$(OBJEXT): y.tab.cpp y.tab.h
+lex.yy$(OBJEXT): y.tab.cpp lex.yy.cpp y.tab.h
+

src/smvlang/expr2smv.cpp

@@ -0,0 +1,578 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <string.h>
+
+#include <lispexpr.h>
+#include <lispirep.h>
+#include <i2string.h>
+#include <std_expr.h>
+
+#include "expr2smv.h"
+
+class expr2smvt
+{
+public:
+  bool convert_nondet_choice(const exprt &src, std::string &dest, unsigned precedence);
+
+  bool convert_binary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence);
+
+  bool convert_unary(const exprt &src, std::string &dest, const std::string &symbol, unsigned precedence);
+
+  bool convert_index(const exprt &src, std::string &dest, unsigned precedence);
+
+  bool convert(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert(const exprt &src, std::string &dest);
+
+  bool convert_symbol(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_next_symbol(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_constant(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert_cond(const exprt &src, std::string &dest);
+
+  bool convert_norep(const exprt &src, std::string &dest, unsigned &precedence);
+
+  bool convert(const typet &src, std::string &dest);
+};
+
+/* SMV Operator Precedences:
+
+ 1 %left  COMMA
+ 2 %right IMPLIES
+ 3 %left  IFF
+ 4 %left  OR XOR XNOR
+ 5 %left  AND
+ 6 %left  NOT
+ 7 %left  EX AX EF AF EG AG EE AA SINCE UNTIL TRIGGERED RELEASES EBF EBG ABF ABG BUNTIL MMIN MMAX
+ 8 %left  OP_NEXT OP_GLOBAL OP_FUTURE
+ 9 %left  OP_PREC OP_NOTPRECNOT OP_HISTORICAL OP_ONCE
+10 %left  APATH EPATH
+11 %left  EQUAL NOTEQUAL LT GT LE GE
+12 %left  UNION
+13 %left  SETIN
+14 %left  MOD
+15 %left  PLUS MINUS
+16 %left  TIMES DIVIDE
+17 %left  UMINUS
+18 %left  NEXT SMALLINIT
+19 %left  DOT
+20        [ ]
+21 = max
+
+*/
+
+#define SMV_MAX_PRECEDENCE 21
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_nondet_choice
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_nondet_choice(
+  const exprt &src,
+  std::string &dest,
+  unsigned precedence)
+{
+  dest="{ ";
+
+  bool first=true;
+
+  forall_operands(it, src)
+  {
+    if(first)
+      first=false;
+    else
+      dest+=", ";
+
+    std::string tmp;
+    if(convert(*it, tmp)) return true;
+    dest+=tmp;
+  }
+
+  dest+=" }";
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_cond
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_cond(
+  const exprt &src,
+  std::string &dest)
+{
+  dest="case ";
+
+  bool condition=true;
+
+  forall_operands(it, src)
+  {
+    std::string tmp;
+    if(convert(*it, tmp)) return true;
+    dest+=tmp;
+
+    if(condition)
+      dest+=": ";
+    else
+      dest+="; ";
+    
+    condition=!condition;
+  }
+
+  dest+="esac";
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_binary(
+  const exprt &src,
+  std::string &dest,
+  const std::string &symbol,
+  unsigned precedence)
+{
+  if(src.operands().size()<2)
+    return convert_norep(src, dest, precedence);
+
+  bool first=true;
+
+  forall_operands(it, src)
+  {
+    if(first)
+      first=false;
+    else
+    {
+      dest+=' ';
+      dest+=symbol;
+      dest+=' ';
+    }
+
+    std::string op;
+    unsigned p;
+
+    if(convert(*it, op, p)) return true;
+
+    if(precedence>p) dest+='(';
+    dest+=op;
+    if(precedence>p) dest+=')';
+  }
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_unary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_unary(
+  const exprt &src, std::string &dest,
+  const std::string &symbol,
+  unsigned precedence)
+{
+  if(src.operands().size()!=1)
+    return convert_norep(src, dest, precedence);
+    
+  std::string op;
+  unsigned p;
+
+  if(convert(src.op0(), op, p)) return true;
+
+  dest+=symbol;
+  if(precedence>p) dest+='(';
+  dest+=op;
+  if(precedence>p) dest+=')';
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_index
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_index(
+  const exprt &src,
+  std::string &dest,
+  unsigned precedence)
+{
+  if(src.operands().size()!=2)
+    return convert_norep(src, dest, precedence);
+
+  std::string op;
+  unsigned p;
+
+  if(convert(src.op0(), op, p)) return true;
+
+  if(precedence>p) dest+='(';
+  dest+=op;
+  if(precedence>p) dest+=')';
+
+  if(convert(src.op1(), op, p)) return true;
+
+  dest+='[';
+  dest+=op;
+  dest+=']';
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_norep
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_norep(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+  dest=src.to_string();
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_symbol(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+  dest=src.get_string(ID_identifier);
+ 
+  if(strncmp(dest.c_str(), "smv::", 5)==0)
+    dest.erase(0, 5);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_next_symbol
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_next_symbol(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  std::string tmp;
+  convert_symbol(src, tmp, precedence);
+
+  dest="next("+tmp+")";
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert_constant(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+
+  const typet &type=src.type();
+  const std::string &value=src.get_string(ID_value);
+
+  if(type.id()==ID_bool)
+  {
+    if(src.is_true())
+      dest+="TRUE";
+    else
+      dest+="FALSE";
+  }
+  else if(type.id()==ID_integer ||
+          type.id()==ID_natural ||
+          type.id()==ID_range)
+    dest=value;
+  else
+    return convert_norep(src, dest, precedence);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert(
+  const exprt &src,
+  std::string &dest,
+  unsigned &precedence)
+{
+  precedence=SMV_MAX_PRECEDENCE;
+
+  if(src.id()==ID_plus)
+    return convert_binary(src, dest, "+", precedence=15);
+
+  else if(src.id()==ID_minus)
+  {
+    if(src.operands().size()<2)
+      return convert_norep(src, dest, precedence);
+    else     
+      return convert_binary(src, dest, "-", precedence=15);
+  }
+
+  else if(src.id()==ID_unary_minus)
+  {
+    if(src.operands().size()!=1)
+      return convert_norep(src, dest, precedence);
+    else     
+      return convert_unary(src, dest, "-", precedence=17);
+  }
+
+  else if(src.id()==ID_index)
+    return convert_index(src, dest, precedence=20);
+
+  else if(src.id()==ID_mult || src.id()==ID_div)
+    return convert_binary(src, dest, src.id_string(), precedence=16);
+
+  else if(src.id()==ID_lt || src.id()==ID_gt ||
+          src.id()==ID_le || src.id()==ID_ge)
+    return convert_binary(src, dest, src.id_string(), precedence=11);
+
+  else if(src.id()==ID_equal)
+    return convert_binary(src, dest, "=", precedence=11);
+
+  else if(src.id()==ID_not)
+    return convert_unary(src, dest, "!", precedence=6);
+
+  else if(src.id()==ID_and)
+    return convert_binary(src, dest, "&", precedence=5);
+
+  else if(src.id()==ID_or)
+    return convert_binary(src, dest, "|", precedence=4);
+
+  else if(src.id()==ID_implies)
+    return convert_binary(src, dest, "->", precedence=2);
+
+  else if(src.id()=="<=>")
+    return convert_binary(src, dest, "<->", precedence=3);
+
+  else if(src.id()==ID_AG || src.id()==ID_EG ||
+          src.id()==ID_AX || src.id()==ID_EX)
+    return convert_unary(src, dest, src.id_string()+" ", precedence=7);
+
+  else if(src.id()==ID_symbol)
+    return convert_symbol(src, dest, precedence);
+
+  else if(src.id()==ID_next_symbol)
+    return convert_next_symbol(src, dest, precedence);
+
+  else if(src.id()==ID_constant)
+    return convert_constant(src, dest, precedence);
+
+  else if(src.id()=="smv_nondet_choice")
+    return convert_nondet_choice(src, dest, precedence);
+
+  else if(src.id()==ID_nondet_bool)
+  {
+    exprt nondet_choice_expr("smv_nondet_choice");
+    nondet_choice_expr.operands().clear();
+    nondet_choice_expr.operands().push_back(false_exprt());
+    nondet_choice_expr.operands().push_back(true_exprt());
+    return convert_nondet_choice(nondet_choice_expr, dest, precedence);
+  }
+
+  else if(src.id()==ID_cond)
+    return convert_cond(src, dest);
+
+  else // no SMV language expression for internal representation 
+    return convert_norep(src, dest, precedence);
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: expr2smvt::convert
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smvt::convert(const exprt &src, std::string &dest)
+{
+  unsigned precedence;
+  return convert(src, dest, precedence);
+}
+
+/*******************************************************************\
+
+Function: expr2smv
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool expr2smv(const exprt &expr, std::string &code)
+{
+  expr2smvt expr2smv;
+  return expr2smv.convert(expr, code);
+}
+
+/*******************************************************************\
+
+Function: type2smv
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool type2smv(const typet &type, std::string &code)
+{
+  if(type.id()==ID_bool)
+    code="boolean";
+  else if(type.id()==ID_array)
+  {
+    std::string tmp;
+    if(type2smv(type.subtype(), tmp)) return true;
+    code="array ";
+    code+="..";
+    code+=" of ";
+    code+=tmp;
+  }
+  else if(type.id()==ID_enum)
+  {
+    const irept &elements=type.find("elements");
+    code="{ ";
+    bool first=true;
+    forall_irep(it, elements.get_sub())
+    {
+      if(first) first=false; else code+=", ";
+      code+=it->id_string();
+    }
+    code+=" }";
+  }
+  else if(type.id()==ID_range)
+  {
+    code=type.get_string(ID_from)+".."+type.get_string(ID_to);
+  }
+  else if(type.id()=="submodule")
+  {
+    code=type.get_string(ID_identifier);
+    const exprt &e=(exprt &)type;
+    if(e.has_operands())
+    {
+      code+='(';
+      bool first=true;
+      forall_operands(it, e)
+      {
+        if(first) first=false; else code+=", ";
+        std::string tmp;
+        expr2smv(*it, tmp);
+        code+=tmp;
+      }
+      code+=')';
+    }
+  }
+  else
+    return true;
+
+  return false;
+}

src/smvlang/expr2smv.h

@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "expr.h"
+
+bool expr2smv(const exprt &expr, std::string &code);
+bool type2smv(const typet &type, std::string &code);
+

src/smvlang/parser.y

@@ -0,0 +1,551 @@
+%{
+#include <i2string.h>
+
+#include "smv_parser.h"
+#include "smv_typecheck.h"
+
+#define YYSTYPE unsigned
+#define PARSER smv_parser
+
+#include "y.tab.h"
+
+#define YYMAXDEPTH 200000
+#define YYSTYPE_IS_TRIVIAL 1
+
+/*------------------------------------------------------------------------*/
+
+#define yylineno yysmvlineno
+#define yytext yysmvtext
+
+#define yyerror yysmverror
+int yysmverror(const std::string &error);
+int yylex();
+extern char *yytext;
+
+/*------------------------------------------------------------------------*/
+
+#define mto(x, y) stack(x).move_to_operands(stack(y))
+#define binary(x, y, id, z) { init(x, id); \
+  stack(x).move_to_operands(stack(y), stack(z)); }
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(exprt &expr)
+{
+  expr.clear();
+  PARSER.set_location(expr);
+}
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(YYSTYPE &expr)
+{
+  newstack(expr);
+  init(stack(expr));
+}
+
+/*******************************************************************\
+
+Function: init
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void init(YYSTYPE &expr, const irep_idt &id)
+{
+  init(expr);
+  stack(expr).id(id);
+}
+
+/*******************************************************************\
+
+Function: j_binary
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void j_binary(YYSTYPE &dest, YYSTYPE &op1,
+                     const irep_idt &id, YYSTYPE &op2)
+{
+  if(stack(op1).id()==id)
+  {
+    dest=op1;
+    mto(dest, op2);
+  }
+  else if(stack(op2).id()==id)
+  {
+    dest=op2;
+    mto(dest, op1);
+  }
+  else
+    binary(dest, op1, id, op2);
+}
+
+/*******************************************************************\
+
+Function: new_module
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void new_module(YYSTYPE &module)
+{
+  const std::string name=smv_module_symbol(stack(module).id_string());
+  PARSER.module=&PARSER.parse_tree.modules[name];
+  PARSER.module->name=name;
+  PARSER.module->base_name=stack(module).id_string();
+  PARSER.module->used=true;
+}
+
+/*------------------------------------------------------------------------*/
+
+%}
+
+%token AG_Token AX_Token AF_Token
+
+%token INIT_Token TRANS_Token SPEC_Token VAR_Token DEFINE_Token ASSIGN_Token
+%token INVAR_Token FAIRNESS_Token MODULE_Token ARRAY_Token OF_Token
+%token DOTDOT_Token BOOLEAN_Token EXTERN_Token
+
+%token NEXT_Token INC_Token DEC_Token CASE_Token ESAC_Token BECOMES_Token
+%token ADD_Token SUB_Token SWITCH_Token init_Token PLUS_Token
+
+%token STRING_Token QSTRING_Token QUOTE_Token
+%token NUMBER_Token
+
+%right IMPLIES_Token
+%left  UNION_Token
+%left  EQUIV_Token
+%left  XOR_Token
+%left  OR_Token
+%left  AND_Token
+%left  NOT_Token
+%left  EX_Token AX_Token EF_Token AF_Token EG_Token AG_Token E_Token A_Token UNTIL_Token
+%left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
+%left  PLUS_Token MINUS_Token
+%left  TIMES_Token DIVIDE_Token
+%left  UMINUS           /* supplies precedence for unary minus */
+%left  DOT_Token
+
+%%
+
+start      : modules
+           | formula { PARSER.module->add_spec(stack($1));
+                       PARSER.module->used=true; }
+           ;
+
+modules    : module
+           | modules module
+           ;
+
+module     : module_head sections
+           ;
+
+module_name: STRING_Token
+           | QUOTE_Token
+           ;
+
+module_head: MODULE_Token module_name { new_module($2); }
+           | MODULE_Token module_name { new_module($2); } '(' module_argument_list_opt ')'
+           ;
+
+sections   : /* epsilon */
+           | section sections
+           ;
+           
+semi_opt   :    /* empty */
+           | ';'
+           ;
+
+section    : VAR_Token vardecls
+           | VAR_Token
+           | INIT_Token formula semi_opt { PARSER.module->add_init(stack($2), stack($1).location()); }
+           | INIT_Token
+           | TRANS_Token formula semi_opt { PARSER.module->add_trans(stack($2), stack($1).location()); }
+           | TRANS_Token
+           | SPEC_Token formula semi_opt { PARSER.module->add_spec(stack($2), stack($1).location()); }
+           | SPEC_Token
+           | ASSIGN_Token assignments
+           | ASSIGN_Token
+           | DEFINE_Token defines
+           | DEFINE_Token
+           | INVAR_Token formula semi_opt { PARSER.module->add_invar(stack($2), stack($1).location()); }
+           | INVAR_Token
+           | FAIRNESS_Token formula semi_opt { PARSER.module->add_fairness(stack($2), stack($1).location()); }
+           | FAIRNESS_Token
+           | EXTERN_Token extern_var semi_opt
+           | EXTERN_Token
+           ;
+ 
+extern_var : variable_name EQUAL_Token QUOTE_Token
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  if(var.identifier!="")
+  {
+    yyerror("variable `"+id2string(identifier)+"' already declared extern");
+    YYERROR;
+  }
+  else
+    var.identifier=stack($3).id_string();
+}
+           ;
+
+vardecls   : vardecl
+           | vardecl vardecls
+           ;
+
+module_argument: variable_name
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+  var.var_class=smv_parse_treet::mc_vart::ARGUMENT;
+  PARSER.module->ports.push_back(identifier);
+}
+           ;
+
+module_argument_list: module_argument
+           | module_argument_list ',' module_argument
+           ;
+
+module_argument_list_opt: /* empty */
+           | module_argument_list
+           ;
+
+type       : ARRAY_Token NUMBER_Token DOTDOT_Token NUMBER_Token OF_Token type
+{
+  init($$, ID_array);
+  int start=atoi(stack($2).id().c_str());
+  int end=atoi(stack($4).id().c_str());
+
+  if(end < start)
+  {
+    yyerror("array must end with number >= `"+i2string(start)+"'");
+    YYERROR;
+  }
+
+  stack($$).set(ID_size, end-start+1);
+  stack($$).set(ID_offset, start);
+  stack($$).set(ID_subtype, stack($6));
+}
+           | BOOLEAN_Token { init($$, ID_bool); }
+           | '{' enum_list '}' { $$=$2; }
+           | NUMBER_Token DOTDOT_Token NUMBER_Token
+            {
+              init($$, ID_range);
+              stack($$).set(ID_from, stack($1));
+              stack($$).set(ID_to, stack($3));
+            }
+           | usertype
+           ;
+
+usertype   : module_name
+            {
+              init($$, "submodule");
+              stack($$).set(ID_identifier,
+                            smv_module_symbol(stack($1).id_string()));
+            }
+           | module_name '(' formula_list ')'
+            {
+              init($$, "submodule");
+              stack($$).set(ID_identifier,
+                            smv_module_symbol(stack($1).id_string()));
+              stack($$).operands().swap(stack($3).operands());
+            }
+           ;
+
+enum_list  : enum_element
+              {
+               init($$, ID_enum);
+               stack($$).add("elements").get_sub().push_back(irept(stack($1).id()));
+              }
+           | enum_list ',' enum_element
+              {
+               $$=$1;
+               stack($$).add("elements").get_sub().push_back(irept(stack($3).id())); 
+              }
+           ;
+
+enum_element: STRING_Token
+              {
+                $$=$1;
+                PARSER.module->enum_set.insert(stack($1).id_string());
+              }
+            ;
+
+vardecl    : variable_name ':' type ';'
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  switch(var.var_class)
+  {
+  case smv_parse_treet::mc_vart::UNKNOWN:
+    var.type=(typet &)stack($3);
+    var.var_class=smv_parse_treet::mc_vart::DECLARED;
+    break;
+
+  case smv_parse_treet::mc_vart::DEFINED:
+    yyerror("variable `"+id2string(identifier)+"' already defined");
+    YYERROR;
+    break;
+
+  case smv_parse_treet::mc_vart::DECLARED:
+    yyerror("variable `"+id2string(identifier)+"' already declared as variable");
+    YYERROR;
+    break;
+  
+  case smv_parse_treet::mc_vart::ARGUMENT:
+    yyerror("variable `"+id2string(identifier)+"' already declared as argument");
+    YYERROR;
+    break;
+  
+  default:
+    assert(false);
+  }
+}
+           ;
+
+assignments: assignment
+           | assignment assignments
+           | define
+           | define assignments
+           ;
+
+assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
+{
+  binary($$, $3, ID_equal, $6);
+
+  if(stack($1).id()=="next")
+  {
+    exprt &op=stack($$).op0();
+    exprt tmp("smv_next");
+    tmp.operands().resize(1);
+    tmp.op0().swap(op);
+    tmp.swap(op);
+    PARSER.module->add_trans(stack($$));
+  }
+  else
+    PARSER.module->add_init(stack($$));
+}
+;
+
+assignment_var: variable_name
+              ;
+
+assignment_head: init_Token { init($$, ID_init); }
+               | NEXT_Token { init($$, "next"); }
+               ;
+
+defines: define
+       | define defines
+       ;
+
+define : assignment_var BECOMES_Token formula ';'
+{
+  const irep_idt &identifier=stack($1).get(ID_identifier);
+  smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
+
+  switch(var.var_class)
+  {
+  case smv_parse_treet::mc_vart::UNKNOWN:
+    var.type.make_nil();
+    var.var_class=smv_parse_treet::mc_vart::DEFINED;
+    break;
+
+  case smv_parse_treet::mc_vart::DECLARED:
+    var.var_class=smv_parse_treet::mc_vart::DEFINED;
+    break;
+
+  case smv_parse_treet::mc_vart::DEFINED:
+    yyerror("variable `"+id2string(identifier)+"' already defined");
+    YYERROR;
+    break;
+  
+  case smv_parse_treet::mc_vart::ARGUMENT:
+    yyerror("variable `"+id2string(identifier)+"' already declared as argument");
+    YYERROR;
+    break;
+  
+  default:
+    assert(false);
+  }
+
+  binary($$, $1, ID_equal, $3);
+  PARSER.module->add_define(stack($$));
+}
+;
+
+formula : term
+        ;
+
+term: variable_name
+    | NEXT_Token '(' term ')' { init($$, "smv_next"); mto($$, $3); }
+    | '(' formula ')' { $$=$2; }
+    | '{' formula_list '}' { $$=$2; stack($$).id("smv_nondet_choice"); }
+    | INC_Token '(' term ')' { init($$, "inc"); mto($$, $3); }
+    | DEC_Token '(' term ')' { init($$, "dec"); mto($$, $3); }
+    | ADD_Token '(' term ',' term ')' { j_binary($$, $3, ID_plus, $5); }
+    | SUB_Token '(' term ',' term ')' { init($$, ID_minus); mto($$, $3); mto($$, $5); }
+    | NUMBER_Token { init($$, "number_constant"); stack($$).set(ID_value, stack($1).id()); }
+    | CASE_Token cases ESAC_Token { $$=$2; }
+    | SWITCH_Token '(' variable_name ')' '{' switches '}' { init($$, "switch"); mto($$, $3); mto($$, $6); }
+    | MINUS_Token term %prec UMINUS { init($$, ID_unary_minus); mto($$, $2); }
+    | term PLUS_Token term    { j_binary($$, $1, ID_plus, $3); }
+    | term MINUS_Token term   { j_binary($$, $1, ID_minus, $3); }
+    | term EQUIV_Token term   { binary($$, $1, ID_equal, $3); }
+    | term IMPLIES_Token term { binary($$, $1, ID_implies, $3); }
+    | term XOR_Token term     { j_binary($$, $1, ID_xor, $3); }
+    | term OR_Token term      { j_binary($$, $1, ID_or, $3); }
+    | term AND_Token term     { j_binary($$, $1, ID_and, $3); }
+    | NOT_Token term          { init($$, ID_not); mto($$, $2); }
+    | AX_Token  term          { init($$, ID_AX);  mto($$, $2); }
+    | AF_Token  term          { init($$, ID_AF);  mto($$, $2); }
+    | AG_Token  term          { init($$, ID_AG);  mto($$, $2); }
+    | term EQUAL_Token    term { binary($$, $1, ID_equal,  $3); }
+    | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
+    | term LT_Token       term { binary($$, $1, ID_lt,  $3); }
+    | term LE_Token       term { binary($$, $1, ID_le, $3); }
+    | term GT_Token       term { binary($$, $1, ID_gt,  $3); }
+    | term GE_Token       term { binary($$, $1, ID_ge, $3); }
+    | term UNION_Token    term { binary($$, $1, "smv_union", $3); }
+    ;
+
+formula_list: formula { init($$); mto($$, $1); }
+            | formula_list ',' formula { $$=$1; mto($$, $3); }
+            ;
+
+variable_name: qstring_list
+		{
+                 const irep_idt &id=stack($1).id();
+
+                 bool is_enum=(PARSER.module->enum_set.find(id)!=
+                               PARSER.module->enum_set.end());
+                 bool is_var=(PARSER.module->vars.find(id)!=
+                              PARSER.module->vars.end());
+
+                 if(is_var && is_enum)
+                  {
+                   yyerror("identifier `"+id2string(id)+"' is ambiguous");
+                   YYERROR;
+                  }
+                 else if(is_enum)
+                  {
+                   init($$, "enum_constant");
+                   stack($$).type()=typet(ID_enum);
+                   stack($$).set(ID_value, stack($1).id());
+                  }
+                 else // not an enum, probably a variable
+                  {
+                   init($$, ID_symbol);
+                   stack($$).set(ID_identifier, stack($1).id());
+                   //PARSER.module->vars[stack($1).id()];
+                  }
+                }
+             | QUOTE_Token
+		{
+                 const irep_idt &id=stack($1).id();
+
+                 init($$, ID_symbol);
+                 stack($$).set(ID_identifier, id);
+                 PARSER.module->vars[id];
+                }
+             ;
+
+qstring_list: QSTRING_Token
+              {
+                init($$, std::string(stack($1).id_string(), 1)); // remove backslash
+              }
+            | STRING_Token
+            | qstring_list DOT_Token QSTRING_Token
+              {
+                std::string id(stack($1).id_string());
+                id+=".";
+                id+=std::string(stack($3).id_string(), 1); // remove backslash
+                init($$, id);
+              }
+            | qstring_list DOT_Token STRING_Token
+              {
+                std::string id(stack($1).id_string());
+                id+=".";
+                id+=stack($3).id_string();
+                init($$, id);
+              }
+            | qstring_list '[' NUMBER_Token ']'
+              {
+                std::string id(stack($1).id_string());
+                id+="[";
+                id+=stack($3).id_string();
+                id+="]";
+                init($$, id);
+              }
+            | qstring_list '(' NUMBER_Token ')'
+              {
+                std::string id(stack($1).id_string());
+                id+="(";
+                id+=stack($3).id_string();
+                id+=")";
+                init($$, id);
+              }
+            ;
+
+cases   : { init($$, "smv_cases"); }
+        | cases case { $$=$1; mto($$, $2); }
+        ;
+
+case    : formula ':' formula ';' { binary($$, $1, ID_case, $3); }
+        ;
+
+switches: { init($$, "switches"); }
+        | switches switch { $$=$1; mto($$, $2); }
+        ;
+
+switch  : NUMBER_Token ':' term ';' { init($$, "switch"); mto($$, $1); mto($$, $3); }
+        ;
+
+%%
+
+int yysmverror(const std::string &error)
+{
+  PARSER.parse_error(error, yytext);
+  return 0;
+}
+
+#undef yyerror
+

src/smvlang/scanner.l

@@ -0,0 +1,133 @@
+%option nounput
+
+%{
+#ifdef _WIN32
+#define YY_NO_UNISTD_H
+static int isatty(int) { return 0; }
+#endif
+
+#include <stdio.h>
+#include <string.h>
+
+#include <expr.h>
+
+#define PARSER smv_parser
+#define YYSTYPE unsigned
+
+#include "smv_parser.h"
+#include "y.tab.h"
+
+int yysmverror(const std::string &error);
+
+void newlocation(YYSTYPE &x)
+{
+  newstack(x);
+  PARSER.set_location(stack(x));
+}
+
+%}
+
+%pointer
+
+%%
+
+"/*"		{
+		  int c;
+
+		  for(;;)
+		    {
+		      while((c = yyinput()) != '*' && c != EOF)
+			;
+
+		      if(c == '*')
+                        {
+			  while((c = yyinput()) == '*')
+                            ;
+
+			  if( c == '/' ) break;
+                        }
+
+		      if (c == EOF)
+                        {
+			  yysmverror("EOF in comment");
+			  break;
+                        }
+                    }
+                }
+
+"//".*          ;
+"--".*          ;
+"#".*		{ /* preprocessor */ }
+
+[ \t\n]+	;
+
+"INIT"		{ newlocation(yysmvlval); return INIT_Token; }
+"TRANS"		{ newlocation(yysmvlval); return TRANS_Token; }
+"SPEC"		{ newlocation(yysmvlval); return SPEC_Token; }
+"INVAR"		{ newlocation(yysmvlval); return INVAR_Token; }
+"VAR"		{ newlocation(yysmvlval); return VAR_Token; }
+"ASSIGN"	{ newlocation(yysmvlval); return ASSIGN_Token; }
+"DEFINE"	{ newlocation(yysmvlval); return DEFINE_Token; }
+"FAIRNESS"	{ newlocation(yysmvlval); return FAIRNESS_Token; }
+"MODULE"	{ newlocation(yysmvlval); return MODULE_Token; }
+"EXTERN"	{ newlocation(yysmvlval); return EXTERN_Token; }
+
+"AG"		return AG_Token;
+"AF"		return AF_Token;
+"AX"		return AX_Token;
+"next"		return NEXT_Token;
+"init"		return init_Token;
+"case"		return CASE_Token;
+"esac"		return ESAC_Token;
+"switch"	return SWITCH_Token;
+"array"		return ARRAY_Token;
+"of"		return OF_Token;
+"boolean"	return BOOLEAN_Token;
+"union"		return UNION_Token;
+".."		return DOTDOT_Token;
+"XOR"		return XOR_Token;
+
+[\$A-Za-z_][A-Za-z0-9_\$#-]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return STRING_Token;
+		}
+\\[A-Za-z0-9_\$#-]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return QSTRING_Token;
+		}
+[0-9][0-9]*	{
+                  newstack(yysmvlval);
+                  stack(yysmvlval).id(yytext);
+		  return NUMBER_Token;
+		}
+\"[^\"]*\"      {
+                  newstack(yysmvlval);
+                  std::string tmp(yytext);
+                  stack(yysmvlval).id(std::string(tmp, 1, tmp.size()-2));
+                  return QUOTE_Token;
+                }
+
+"~"		return NOT_Token;
+"!"		return NOT_Token;
+"+"		return PLUS_Token;
+"-"		return MINUS_Token;
+"|"		return OR_Token;
+"&"		return AND_Token;
+"->"		return IMPLIES_Token;
+"<->"		return EQUIV_Token;
+"="		return EQUAL_Token;
+"<="		return LE_Token;
+">="		return GE_Token;
+"<"		return LT_Token;
+">"		return GT_Token;
+"!="		return NOTEQUAL_Token;
+":="		return BECOMES_Token;
+"."		return DOT_Token;
+
+.		return yytext[0];
+
+%%
+
+int yywrap() { return 1; }

src/smvlang/smv_language.cpp

@@ -0,0 +1,265 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_language.h"
+#include "smv_typecheck.h"
+#include "smv_parser.h"
+#include "expr2smv.h"
+
+/*******************************************************************\
+
+Function: smv_languaget::parse
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::parse(
+  std::istream &instream,
+  const std::string &path,
+  message_handlert &message_handler)
+{
+  smv_parser.clear();
+
+  const std::string main_name=smv_module_symbol("main");
+  smv_parser.module=&smv_parser.parse_tree.modules[main_name];
+  smv_parser.module->name=main_name;
+  smv_parser.module->base_name="main";
+
+  smv_parser.filename=path;
+  smv_parser.in=&instream;
+  smv_parser.set_message_handler(message_handler);
+
+  bool result=smv_parser.parse();
+
+  // see if we used main
+
+  if(!smv_parser.parse_tree.modules[main_name].used)
+    smv_parser.parse_tree.modules.erase(main_name);
+
+  smv_parse_tree.swap(smv_parser.parse_tree);
+
+  // save some memory
+  smv_parser.clear();
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::dependencies
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_languaget::dependencies(
+  const std::string &module, 
+  std::set<std::string> &module_set)
+{
+  smv_parse_treet::modulest::const_iterator
+    m_it=smv_parse_tree.modules.find(module);
+
+  if(m_it==smv_parse_tree.modules.end()) return;
+
+  const smv_parse_treet::modulet &smv_module=m_it->second;
+
+  for(smv_parse_treet::mc_varst::const_iterator it=smv_module.vars.begin();
+      it!=smv_module.vars.end(); it++)
+    if(it->second.type.id()=="submodule")
+      module_set.insert(it->second.type.get_string("identifier"));
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::modules_provided
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_languaget::modules_provided(std::set<std::string> &module_set)
+{
+  for(smv_parse_treet::modulest::const_iterator
+      it=smv_parse_tree.modules.begin();
+      it!=smv_parse_tree.modules.end(); it++)
+    module_set.insert(id2string(it->second.name));
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::typecheck
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::typecheck(
+  contextt &context,
+  const std::string &module,
+  message_handlert &message_handler)
+{
+  return smv_typecheck(smv_parse_tree, context, module, message_handler);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::show_parse
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+  
+void smv_languaget::show_parse(std::ostream &out)
+{
+  for(smv_parse_treet::modulest::const_iterator
+      it=smv_parse_tree.modules.begin();
+      it!=smv_parse_tree.modules.end(); it++)
+  {
+    const smv_parse_treet::modulet &module=it->second;
+    out << "Module: " << module.name << std::endl << std::endl;
+
+    out << "  VARIABLES:" << std::endl;
+
+    for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin();
+        it!=module.vars.end(); it++)
+      if(it->second.type.id()!="submodule")
+      {
+        std::string msg;
+        type2smv(it->second.type, msg);
+        out << "    " << it->first << ": " 
+            << msg << ";" << std::endl;
+      }
+
+    out << std::endl;
+
+    out << "  SUBMODULES:" << std::endl;
+
+    for(smv_parse_treet::mc_varst::const_iterator
+        it=module.vars.begin();
+        it!=module.vars.end(); it++)
+      if(it->second.type.id()=="submodule")
+      {
+        std::string msg;
+        type2smv(it->second.type, msg);
+        out << "    " << it->first << ": " 
+            << msg << ";" << std::endl;
+      }
+
+    out << std::endl;
+
+    out << "  ITEMS:" << std::endl;
+
+    forall_item_list(it, module.items)
+    {
+      out << "    TYPE: " << to_string(it->item_type) << std::endl;
+      out << "    EXPR: " << it->expr << std::endl;
+      out << std::endl;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::from_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::from_expr(const exprt &expr, std::string &code,
+                              const namespacet &ns)
+{
+  return expr2smv(expr, code);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::from_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::from_type(
+  const typet &type,
+  std::string &code,
+  const namespacet &ns)
+{
+  return type2smv(type, code);
+}
+
+/*******************************************************************\
+
+Function: smv_languaget::to_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool smv_languaget::to_expr(
+  const std::string &code,
+  const std::string &module,
+  exprt &expr,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  messaget message(message_handler);
+  message.error("not yet implemented");
+  return true;
+}
+
+/*******************************************************************\
+
+Function: new_smv_language
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+  
+languaget *new_smv_language()
+{
+  return new smv_languaget;
+}
+

src/smvlang/smv_language.h

@@ -0,0 +1,75 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_LANGUAGE_H
+#define CPROVER_SMV_LANGUAGE_H
+
+/*! \defgroup gr_smvlang SMV front-end */
+
+#include <language.h>
+
+#include "smv_parse_tree.h"
+
+/*! \brief TO_BE_DOCUMENTED
+    \ingroup gr_smvlang
+*/
+class smv_languaget:public languaget
+{
+public:
+  virtual bool parse(
+    std::istream &instream,
+    const std::string &path,
+    message_handlert &message_handler);
+
+  virtual void dependencies(
+    const std::string &module,
+    std::set<std::string> &module_set);
+
+  virtual void modules_provided(
+    std::set<std::string> &module_set);
+                 
+  virtual bool typecheck(
+    contextt &context,
+    const std::string &module,
+    message_handlert &message_handler);
+  
+  virtual void show_parse(std::ostream &out);
+  
+  virtual ~smv_languaget() { }
+  
+  virtual bool from_expr(
+    const exprt &expr,
+    std::string &code,
+    const namespacet &ns);
+
+  virtual bool from_type(
+    const typet &type,
+    std::string &code,
+    const namespacet &ns);
+
+  virtual bool to_expr(
+    const std::string &code,
+    const std::string &module,
+    exprt &expr,
+    message_handlert &message_handler,
+    const namespacet &ns);
+                       
+  virtual std::string id() const { return "SMV"; }
+  virtual std::string description() const { return "SMV"; }
+  virtual std::set<std::string> extensions() const
+  { std::set<std::string> s; s.insert("smv"); return s; }
+  
+  virtual languaget *new_language()
+  { return new smv_languaget; }
+     
+  smv_parse_treet smv_parse_tree;
+};
+
+languaget *new_smv_language();
+ 
+#endif

src/smvlang/smv_parse_tree.cpp

@@ -0,0 +1,72 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_parse_tree.h"
+
+/*******************************************************************\
+
+Function: smv_parse_treet::swap
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
+{
+  smv_parse_tree.modules.swap(modules);
+}
+
+/*******************************************************************\
+
+Function: smv_parse_treet::clear
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_parse_treet::clear()
+{
+  modules.clear();
+}
+
+/*******************************************************************\
+
+Function: operator <<
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string to_string(smv_parse_treet::modulet::itemt::item_typet i)
+{
+  switch(i)
+  {
+  case smv_parse_treet::modulet::itemt::INVAR:    return "INVAR";
+  case smv_parse_treet::modulet::itemt::TRANS:    return "TRANS";
+  case smv_parse_treet::modulet::itemt::INIT:     return "INIT";
+  case smv_parse_treet::modulet::itemt::SPEC:     return "SPEC";
+  case smv_parse_treet::modulet::itemt::FAIRNESS: return "FAIRNESS";
+  case smv_parse_treet::modulet::itemt::DEFINE:    return "DEFINE";  
+  
+  default:;
+  }
+  
+  return "";
+}

src/smvlang/smv_parse_tree.h

@@ -0,0 +1,175 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_PARSE_TREE_H
+#define CPROVER_SMV_PARSE_TREE_H
+
+#include <hash_cont.h>
+#include <string_hash.h>
+#include <expr.h>
+
+class smv_parse_treet
+{
+public:
+
+  struct mc_vart
+  {
+    typedef enum { UNKNOWN, DECLARED, DEFINED, ARGUMENT } var_classt;
+    var_classt var_class;
+    typet type;
+    irep_idt identifier;
+    
+    mc_vart():var_class(UNKNOWN), type(typet(ID_bool))
+    {
+    }
+  };
+   
+  typedef hash_map_cont<irep_idt, mc_vart, irep_id_hash> mc_varst;
+  typedef hash_set_cont<irep_idt, irep_id_hash> enum_sett;
+
+  struct modulet
+  {
+    irep_idt name, base_name;
+    
+    struct itemt
+    {
+      enum item_typet { SPEC, INIT, TRANS, DEFINE, INVAR, FAIRNESS };
+      
+      friend std::string to_string(item_typet i);
+      
+      item_typet item_type;
+      exprt expr;
+      locationt location;
+
+      bool is_spec() const
+      {
+        return item_type==SPEC;
+      }
+      
+      bool is_define() const
+      {
+        return item_type==DEFINE;
+      }
+      
+      bool is_invar() const
+      {
+        return item_type==INVAR;
+      }
+      
+      bool is_trans() const
+      {
+        return item_type==TRANS;
+      }
+      
+      bool is_init() const
+      {
+        return item_type==INIT;
+      }
+      
+    };
+    
+    typedef std::list<itemt> item_listt;
+    item_listt items;
+    
+    void add_item(
+      itemt::item_typet item_type,
+      const exprt &expr,
+      const locationt &location)
+    {
+      items.push_back(itemt());
+      items.back().item_type=item_type;
+      items.back().expr=expr;
+      items.back().location=location;
+    }
+    
+    void add_invar(const exprt &expr)
+    {
+      add_item(itemt::INVAR, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_spec(const exprt &expr)
+    {
+      add_item(itemt::SPEC, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_define(const exprt &expr)
+    {
+      add_item(itemt::DEFINE, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_fairness(const exprt &expr)
+    {
+      add_item(itemt::FAIRNESS, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_init(const exprt &expr)
+    {
+      add_item(itemt::INIT, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_trans(const exprt &expr)
+    {
+      add_item(itemt::TRANS, expr, static_cast<const locationt &>(get_nil_irep()));
+    }
+    
+    void add_invar(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::INVAR, expr, location);
+    }
+    
+    void add_spec(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::SPEC, expr, location);
+    }
+    
+    void add_define(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::DEFINE, expr, location);
+    }
+    
+    void add_fairness(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::FAIRNESS, expr, location);
+    }
+    
+    void add_init(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::INIT, expr, location);
+    }
+    
+    void add_trans(const exprt &expr, const locationt &location)
+    {
+      add_item(itemt::TRANS, expr, location);
+    }
+    
+    mc_varst vars;
+    enum_sett enum_set;
+    bool used;
+    
+    std::list<irep_idt> ports;
+    
+    modulet():used(false) { }
+  };
+   
+  typedef hash_map_cont<irep_idt, modulet, irep_id_hash> modulest;
+  
+  modulest modules;
+  
+  void swap(smv_parse_treet &smv_parse_tree);
+  void clear();
+};
+
+#define forall_item_list(it, expr) \
+  for(smv_parse_treet::modulet::item_listt::const_iterator it=(expr).begin(); \
+      it!=(expr).end(); it++)
+
+#define Forall_item_list(it, expr) \
+  for(smv_parse_treet::modulet::item_listt::iterator it=(expr).begin(); \
+      it!=(expr).end(); it++)
+
+#endif

src/smvlang/smv_parser.cpp

@@ -0,0 +1,12 @@
+/*******************************************************************\
+
+Module: SMV Parse Tree
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "smv_parser.h"
+
+smv_parsert smv_parser;
+

src/smvlang/smv_parser.h

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: SMV Parser
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_PARSER_H
+#define CPROVER_SMV_PARSER_H
+
+#include <parser.h>
+
+#include "smv_parse_tree.h"
+
+int yysmvparse();
+
+class smv_parsert:public parsert
+{
+ public:
+  smv_parse_treet parse_tree;
+  smv_parse_treet::modulet *module;
+  
+  virtual bool parse()
+  {
+    return yysmvparse();
+  }
+  
+  virtual void clear()
+  {
+    parsert::clear();
+    parse_tree.clear();
+    module=NULL;
+  }
+};
+
+extern smv_parsert smv_parser;
+
+#endif

src/smvlang/smv_typecheck.h

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: SMV Typechecking
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_SMV_TYPECHECK_H
+#define CPROVER_SMV_TYPECHECK_H
+
+#include <context.h>
+#include <message.h>
+
+#include "smv_parse_tree.h"
+
+bool smv_typecheck(
+  smv_parse_treet &smv_parse_tree,
+  contextt &context,
+  const std::string &module,
+  message_handlert &message_handler,
+  bool do_spec=true);
+
+std::string smv_module_symbol(const std::string &module);
+
+#endif