some more fixes

src/uclid/builder.py

@@ -63,6 +63,7 @@ class DeclTypes(Enum):
     CONST = 6
     PROCEDURE = 7
     CONSTRAINTS = 8
+    IMPORT = 9
 
 # Base class for (all sorts of) uclid declarations
 class UclidDecl(UclidElement):
@@ -90,6 +91,8 @@ def __inject__(self) -> str:
             return self.__declstring__
         elif self.decltype == DeclTypes.CONSTRAINTS:
             return self.__declstring__
+        elif self.decltype == DeclTypes.IMPORT:
+            return self.__declstring__
         else:
             _logger.error(f"Declaration for decltype {self.decltype} is not permitted")
             exit(1)
@@ -178,13 +181,13 @@ def __init__(self, instancename, module, argmap):
         self.argmap = argmap
     @property
     def __declstring__(self):
-        if self.modulename not in UclidContext.modules:
-            _logger.error("Module {} not found in UclidContext.modules".format(self.modulename))
+        if self.module.name not in UclidContext.modules:
+            _logger.error("Module {} not found in UclidContext.modules".format(self.module.name))
             _logger.debug("Available modules: {}".format(UclidContext.modules.keys()))
             exit(1)
         argmapstr = ', '.join([
             "{} : ({})".format(port.name, self.argmap[port.name].__inject__())
-            for port in self.module.ip_var_decls + self.module.op_var_decls
+            for k, port in {**self.module.ip_var_decls, **self.module.op_var_decls}.items()
         ])
         return "{}({})".format(self.module.name, argmapstr)
 
@@ -213,13 +216,17 @@ def __init__(self, decltype, name, modulename, refname) -> None:
             modulename (Module/str): Module (or its name) from which to import
             refname (str): Name of object in the module
         """
-        super().__init__(decltype)
+        super().__init__(DeclTypes.IMPORT)
         self.name = name
         self.modulename = modulename if isinstance(modulename, str) else modulename.name
         self.refname = refname
+        self.decltype = decltype
     @property
     def __declstring__(self):
-        return f"{self.modulename}.{self.refname}"
+        if self.decltype == DeclTypes.FUNCTION:
+            return f"function {self.name} = {self.modulename}.{self.refname};"
+        else:
+            return f"{self.modulename}.{self.refname}"
 class UclidWildcardImportDecl(UclidImportDecl):
     def __init__(self, decltype, modulename) -> None:
         super().__init__(decltype, "*", modulename, "*")
@@ -319,6 +326,8 @@ def __init__(self, typestring):
         self.typestring = typestring
     def __inject__(self) -> str:
         return self.typestring
+    def __eq__(self, other) -> bool:
+        return self.typestring == other.typestring
 
 class UclidBooleanType(UclidType):
     def __init__(self):
@@ -966,7 +975,7 @@ def __init__(self, instance: UclidInstance):
         super().__init__()
         self.instance = instance
     def __inject__(self) -> str:
-        return "next ({});".format(self.instance.__inject__())
+        return "next ({});".format(self.instance.instancename)
 class UclidAssumeStmt(UclidStmt):
     def __init__(self, body: UclidExpr):
         """Assumption statement: this assumes that the body expression is true 
@@ -1070,6 +1079,17 @@ def __init__(self, name: str, depth: int):
     def __inject__(self) -> str:
         return "{} = bmc({});".format(self.name, self.depth)
 
+class UclidInductionCommand(UclidControlCommand):
+    def __init__(self, name: str):
+        """Induction proof command
+
+        Args:
+            name (str): Name of proof object
+        """
+        self.name = name
+    def __inject__(self) -> str:
+        return "{} = induction;".format(self.name)
+
 class UclidCheckCommand(UclidControlCommand):
     def __init__(self):
         """Uclid check command to execute the proof"""
@@ -1504,6 +1524,10 @@ def __instance_decls__(self):
     def __define_decls__(self):
         return "\n".join([textwrap.indent(decl.__inject__(), "\t") 
             for k, decl in self.define_decls.items()])
+
+    def __function_decls__(self):
+        return "\n".join([textwrap.indent(decl.__inject__(), "\t") 
+            for k, decl in self.function_decls.items()])
 
     def __import_decls__(self):
         return "\n".join([textwrap.indent(decl.__inject__(), "\t") 
@@ -1547,7 +1571,10 @@ def __inject__(self) -> str:
 
             \t// Defines
             {}
-
+            
+            \t// Functions
+            {}
+                                     
             \t// Procedures
             {}
 
@@ -1563,6 +1590,7 @@ def __inject__(self) -> str:
                 self.__const_decls__(),
                 self.__instance_decls__(),
                 self.__define_decls__(),
+                self.__function_decls__(),
                 self.__procedure_defns__(),
                 self.__module_assumes__(),
                 self.__module_properties__()

src/uclid/builder_sugar.py

@@ -1,6 +1,6 @@
 
 
-from .builder import UclidContext, UclidBooleanType, UclidIntegerType, PortType, UclidOpExpr, UclidCheckCommand, UclidPrintResultsCommand
+from .builder import UclidContext, UclidBooleanType, UclidIntegerType, PortType, UclidOpExpr, UclidCheckCommand, UclidPrintResultsCommand, UclidControlBlock, UclidBMCCommand, UclidPrintCexJSONCommand, UclidInductionCommand
 
 # Variable creation sugaring
 def mkUclidVar(varname, typ, porttype):
@@ -81,3 +81,19 @@ def Uconcat(args):
 
 CMD_check = UclidCheckCommand()
 CMD_print = UclidPrintResultsCommand()
+
+def mkBMCBlock(enginename: str, depth: int, is_json: bool = True):
+    return UclidControlBlock([
+            UclidBMCCommand(enginename, depth), 
+            CMD_check, 
+            UclidPrintCexJSONCommand(enginename) if is_json else None, 
+            CMD_print
+        ])
+
+def mkInductionBlock(enginename: str, is_json: bool = True):
+    return UclidControlBlock([
+            UclidInductionCommand(enginename), 
+            CMD_check, 
+            UclidPrintCexJSONCommand(enginename) if is_json else None, 
+            CMD_print
+        ])