smt: support equation solving

py2many/smt.py

@@ -1,2 +1,6 @@
 def check_sat():
     pass
+
+
+def get_model():
+    pass

pysmt/clike.py

@@ -3,6 +3,7 @@
 from .inference import SMT_TYPE_MAP, SMT_WIDTH_RANK
 
 from py2many.clike import CLikeTranspiler as CommonCLikeTranspiler
+from py2many.analysis import is_global
 
 
 # allowed as names in Python but treated as keywords in Smt
@@ -12,7 +13,7 @@
     ast.Eq: "=",
     ast.Is: "==",
     ast.NotEq: "!=",
-    ast.Pass: "discard",
+    ast.Pass: "",
     ast.Mult: "*",
     ast.Add: "+",
     ast.Sub: "-",
@@ -56,7 +57,7 @@ def visit(self, node):
             return super().visit(node)
 
     def visit_Ellipsis(self, node):
-        return "discard"
+        return ""
 
     def visit_UnaryOp(self, node):
         return "({0} {1})".format(self.visit(node.op), self.visit(node.operand))
@@ -111,3 +112,10 @@ def visit_In(self, node):
         if left_type == "string":
             self._usings.add("strutils")
         return f"{left} in {right}"
+
+    def visit_Expr(self, node) -> str:
+        """Writing assert x > 3 is tedious"""
+        ret = super().visit_Expr(node)
+        if is_global(node) and isinstance(node.value, ast.Compare):
+            return f"(assert {ret})"
+        return ret

pysmt/transpiler.py

@@ -16,7 +16,11 @@
 from py2many.analysis import get_id, is_mutable, is_void_function
 from py2many.clike import class_for_typename
 from py2many.declaration_extractor import DeclarationExtractor
-from py2many.exceptions import AstClassUsedBeforeDeclaration, AstTypeNotSupported
+from py2many.exceptions import (
+    AstClassUsedBeforeDeclaration,
+    AstNotImplementedError,
+    AstTypeNotSupported,
+)
 from py2many.tracer import is_list, defined_before
 
 from typing import List
@@ -463,10 +467,10 @@ def visit_Assert(self, node):
 
     def visit_AnnAssign(self, node):
         target, type_str, val = super().visit_AnnAssign(node)
-        kw = "var" if is_mutable(node.scopes, target) else "let"
-        if type_str == self._default_type:
-            return f"{kw} {target} = {val}"
-        return f"{kw} {target}: {type_str} = {val}"
+        if val == None:
+            return f"(declare-const {target} {type_str})"
+        else:
+            raise AstNotImplementedError(f"{val} can't be assigned", node)
 
     def visit_Assign(self, node):
         lines = [self._visit_AssignOne(node, target) for target in node.targets]

tests/cases/equations.py

@@ -0,0 +1,9 @@
+x: int
+y: int
+
+x > 2
+y < 10
+x + 2 * y == 7
+
+check_sat()
+get_model()

tests/expected/equations.smt

@@ -0,0 +1,7 @@
+(declare-const x Int)
+(declare-const y Int)
+(assert (> x 2))
+(assert (< y 10))
+(assert (= (+ x (* 2 y)) 7))
+(check-sat)
+(get-model)