Issue #127: Arithmetic translation support

 - Implemented handling of tarski ```Interval``` sorts
 - Expression translator: implemented support for simple terms

pyfs/notebooks/auv.ipynb

@@ -0,0 +1,233 @@
+{
+ "cells": [
+  {
+   "cell_type": "code",
+   "execution_count": 1,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": [
+    "import logging"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 2,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": [
+    "import tarski\n",
+    "from tarski.theories import Theory\n",
+    "from tarski.syntax import *\n",
+    "from tarski.model import Model\n",
+    "from tarski.evaluators.simple import evaluate\n",
+    "from tarski.syntax.arithmetic import *"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 3,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "import pyfs\n",
+    "import pyfs.extension as cext\n",
+    "import pyfs.translations as trans"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Automatic Underwater Vehicle"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "ScottyActivity: Mixed Discrete Continuous Planning with Convex Optimization\n",
+    "\n",
+    "E. Fernandez Gonzalez, B. Williams, E. Karpas\n",
+    "\n",
+    "Journal of Artificial Intelligence Research, 62 (2018)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Language translation"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 4,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "L = tarski.language('auv', [Theory.EQUALITY, Theory.ARITHMETIC])"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": [
+    "vehicle = L.sort('vehicle', L.Object)\n",
+    "auv = L.sort('auv', vehicle)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 6,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": [
+    "auv1 = L.constant('auv1', auv)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 7,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": [
+    "x = L.function('x', vehicle, L.Real)\n",
+    "y = L.function('y', vehicle, L.Real)\n",
+    "b = L.function('b', auv, L.Real)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 8,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "vx = L.function('vx', vehicle, L.Real)\n",
+    "vy = L.function('vy', vehicle, L.Real)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Now we cross into the C++ boundary"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 9,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "FSTYPE:  5\n",
+      "get_typename(0):  bool\n",
+      "get_typename(1):  Integer\n",
+      "get_object_name(2o): auv1\n",
+      "Symbol vy/1 registered with ID 0 (vy)\n",
+      "Symbol ite/2 registered with ID 1 (ite)\n",
+      "Symbol y/1 registered with ID 2 (y)\n",
+      "Symbol vx/1 registered with ID 3 (vx)\n",
+      "Symbol x/1 registered with ID 4 (x)\n",
+      "Symbol b/1 registered with ID 5 (b)\n"
+     ]
+    }
+   ],
+   "source": [
+    "info = trans.tarski.create_language_info(L)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "## Terms"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 10,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "X = [x(auv1), y(auv1), b(auv1)]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 11,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "expr_trans = trans.tarski.ExpressionTranslator(info)\n",
+    "    "
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "name": "stdout",
+     "output_type": "stream",
+     "text": [
+      "<pyfs.extension._pyfs.CompositeTerm object at 0x7f82c012cda0>\n",
+      "<pyfs.extension._pyfs.CompositeTerm object at 0x7f82c012cad0>\n",
+      "<pyfs.extension._pyfs.CompositeTerm object at 0x7f82c012cda0>\n"
+     ]
+    }
+   ],
+   "source": [
+    "Xt = []\n",
+    "\n",
+    "for x in X:\n",
+    "    Xt += [expr_trans.translate(x)]"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {
+    "collapsed": true
+   },
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "Python 3",
+   "language": "python",
+   "name": "python3"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3",
+   "version": "3.5.2"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}

pyfs/src/pyfs/translations/tarski.py

@@ -27,6 +27,14 @@ def create_language_info(language):
     # Declare language sorts
     for sort in language.sorts:
         if isinstance(sort, tsk.Interval):
+            if sort.name == 'Real':
+                tid = info.add_fstype(sort.name, cext.type_id.float_t)
+                type_idxs[sort] = tid
+                continue
+            elif sort.name == 'Integer' or sort.name == 'Natural':
+                tid = info.add_fstype(sort.name, cext.type_id.int_t)
+                type_idxs[sort] = tid
+                continue
             # TODO TODO TODO
             # assert 0, "To implement"
             print("\n\nWARNING: WE'RE IGNORING INTERVAL TYPES AT THE MOMENT. FIX THIS.\n\n")
@@ -75,8 +83,7 @@ def translate_problem(problem):
 
     return None, None, None, None, goal
 
-
-class FormulaTranslator(object):
+class Translator(object):
     def __init__(self, language_info_wrapper):
         self.language_info_wrapper = language_info_wrapper
 
@@ -97,6 +104,39 @@ def get_object_id(self, obj):
         return self.language_info_wrapper.obj_idxs[obj]
         # return cext.make_object(True)
 
+    def translate_term(self, term):
+        assert isinstance(term, tsk.Term)
+        if isinstance(term, tsk.Variable):
+            varid = self.get_variable_id(term.symbol)
+            typeid = self.get_type_id(term.sort)
+            return cext.LogicalVariable(varid, term.symbol, typeid)
+
+        elif isinstance(term, tsk.CompoundTerm):
+            symbol_id = self.get_symbol_id(term.symbol)
+            return cext.create_composite_term(symbol_id, self.translate_term_list(term.subterms))
+
+        elif isinstance(term, tsk.Constant):
+            oid = self.get_object_id(term)
+            typeid = self.get_type_id(term.sort)
+            return cext.Constant(oid, typeid)
+
+        raise RuntimeError("Unexpected Tarski element type: {}".format(term))
+
+    def translate_term_list(self, terms):
+        return [self.translate_term(t) for t in terms]
+
+class ExpressionTranslator(Translator):
+
+    def __init__(self, info):
+        super().__init__(info)
+
+    def translate(self, expr):
+        return self.translate_term(expr)
+
+class FormulaTranslator(Translator):
+    def __init__(self, language_info_wrapper):
+        super().__init__(language_info_wrapper)
+
     def translate_formula(self, formula):
         assert isinstance(formula, tsk.Formula)
 
@@ -129,26 +169,6 @@ def translate_formula(self, formula):
 
         raise RuntimeError("Unexpected Tarski element type: {}".format(formula))
 
-    def translate_term(self, term):
-        assert isinstance(term, tsk.Term)
-        if isinstance(term, tsk.Variable):
-            varid = self.get_variable_id(term.symbol)
-            typeid = self.get_type_id(term.sort)
-            return cext.LogicalVariable(varid, term.symbol, typeid)
-
-        elif isinstance(term, tsk.CompoundTerm):
-            symbol_id = self.get_symbol_id(term.symbol)
-            return cext.CompositeTerm(symbol_id, self.translate_term_list(term.subterms))
-
-        elif isinstance(term, tsk.Constant):
-            oid = self.get_object_id(term)
-            typeid = self.get_type_id(term.sort)
-            return cext.Constant(oid, typeid)
-
-        raise RuntimeError("Unexpected Tarski element type: {}".format(term))
-
-    def translate_term_list(self, terms):
-        return [self.translate_term(t) for t in terms]
 
     def translate_connective(self, connective):
         return {