Nearing a good way point.

Author: ianamason

.gitignore

@@ -1 +1,6 @@
-.cache
+build
+dist
+yices.egg-info
+.pytest_cache
+**/*.cache
+**/*.pyc

Makefile

@@ -42,7 +42,7 @@ install:
 	pip install
 
 clean:
-	rm -rf  *.pyc *~ __pycache__ */*.pyc */*~ */__pycache__ */*/*.pyc */*/*~ */*/__pycache__
+	rm -rf  *.pyc *~ __pycache__ */*.pyc */*~ */__pycache__ */*/*.pyc */*/*~ */*/__pycache__ examples/mcsat/mcsat
 
 
 

TODO.txt

@@ -1,14 +1,14 @@
 
-[] 1. Move exceptions out of yices_api and into yices. yices_api should not throw exceptions.
+[X] 1. Move exceptions out of yices_api and into yices. yices_api should not throw exceptions.
 yices should throw them instead.
 
 [] 2. doc strings in yices to reflect this. do the yices_api doc strings need TLC?
 
 [] 3. Solve the gmp and libpoly conundrums, maybe ask Dejan?
 
-[] 4. Add tests for the yices package.
+[X] 4. Add tests for the yices package.
 
-[] 5. Fix the `lint_all` complaints.
+[X] 5. Fix the `lint_all` complaints.
 
 [] 6. Investigate the new type annotation mechanism.
 

examples/functions.py

@@ -0,0 +1,67 @@
+#! /usr/bin/env python
+
+
+from yices import *
+
+
+def define_const(name, ytype, defn=None):
+    '''Tries to emulate yices define_term
+    (see eval_define_term in yices2/src/parser_utils/term_stack2)
+    '''
+    if defn is None:
+        term = Terms.new_uninterpreted_term(ytype)
+        Terms.set_name(term, name)
+        return term
+    # Have a defn
+    if isinstance(defn, basestring):
+        term = Terms.parse_term(defn)
+    else:
+        term = defn
+        term_type = Terms.type_of_term(term)
+    if not Types.is_subtype(term_type, ytype):
+        raise YicesException(msg='incompatible sort in definition')
+    Terms.set_name(term, name)
+    return term
+
+def assert_formula(formula, ctx):
+    if isinstance(formula, basestring):
+        formula = Terms.parse_term(formula)
+    ctx.assert_formula(formula)
+
+
+
+cfg = Config()
+ctx = Context(cfg)
+param = Parameters()
+param.default_params_for_context(ctx)
+global bool_t, int_t, real_t
+bool_t = Types.bool_type()
+int_t = Types.int_type()
+real_t = Types.real_type()
+
+
+funtype = Types.new_function_type([int_t, bool_t, real_t], real_t)
+ftystr = Types.to_string(funtype, 100, 80, 0)
+Types.print_to_fd(1, funtype, 100, 80, 0)
+#assertEqual(ftystr, '(-> int bool real real)')
+fun1 = define_const('fun1', funtype)
+b1 = define_const('b1', bool_t)
+i1 = define_const('i1', int_t)
+r1 = define_const('r1', real_t)
+assert_formula('(> (fun1 i1 b1 r1) (fun1 (+ i1 1) (not b1) (- r1 i1)))', ctx)
+print(ctx.check_context(param) == Status.SAT)
+mdl = Model.from_context(ctx, 1)
+mdlstr = mdl.to_string(80, 100, 0)
+print(mdlstr)
+print('(= b1 false)\n(= i1 1463)\n(= r1 -579)\n(function fun1\n (type (-> int bool real real))\n (= (fun1 1463 false -579) 1)\n (= (fun1 1464 true -2042) 0)\n (default 2))')
+fun1val = mdl.get_value(fun1)
+print(fun1val((1463, False, -579)))
+print(fun1val((1464, True, -2042)))
+print(fun1val((1462, True, -2041)))
+
+
+
+cfg.dispose()
+ctx.dispose()
+param.dispose()
+Yices.exit()

yices/Terms.py

@@ -1,3 +1,4 @@
+import ctypes
 import yices_api as yapi
 
 from .YicesException import YicesException
@@ -994,15 +995,57 @@ def proj_arg(term):
         return retval
 
 
-#FIXME finish these
-#yices_bool_const_value(term)
-#yices_bv_const_value(term)
-#yices_scalar_const_value(term)
+    @staticmethod
+    def bool_const_value(term):
+        value = ctypes.c_int32()
+        errcode =  yapi.yices_bool_const_value(term, value)
+        if errcode == 0:
+            return value.value
+        raise YicesException('yices_bool_const_value')
+
+    @staticmethod
+    def bv_const_value(term):
+        bitsize = Terms.bitsize(term)
+        bvarray = yapi.make_empty_int32_array(bitsize)
+        errcode =  yapi.yices_bv_const_value(term, bvarray)
+        if errcode == 0:
+            return [ bvarray[i] for i in range(0, bitsize) ]
+        raise YicesException('yices_bool_const_value')
+
+    @staticmethod
+    def scalar_const_value(term):
+        value = ctypes.c_int32()
+        errcode =  yapi.yices_scalar_const_value(term, value)
+        if errcode == 0:
+            return value.value
+        raise YicesException('yices_scalar_const_value')
+
+    @staticmethod
+    def bvsum_component(term, i):
+        bitsize = Terms.bitsize(term)
+        if i >= bitsize:
+            raise YicesException('bvsum_component', 'index {0} too big >= bitsize {1}'.format(i, bitsize))
+        bvarray = yapi.make_empty_int32_array(bitsize)
+        termv = ctypes.c_int32()
+        errcode =  yapi.yices_bvsum_component(term, i, bvarray, termv)
+        if errcode == 0:
+            return ([ bvarray[i] for i in range(0, bitsize) ], termv.value)
+        raise YicesException('yices_bvsum_component')
+
+    @staticmethod
+    def product_component(term, i):
+        expv = ctypes.c_uint32()
+        termv = ctypes.c_int32()
+        errcode =  yapi.yices_bvsum_component(term, i, termv, expv)
+        if errcode == 0:
+            return (termv.value, expv.value)
+        raise YicesException('yices_bvsum_component')
+
+
+
+# TBD: gmp issues
 #yices_rational_const_value
 #yices_sum_component
-#yices_bvsum_component(term)
-#yices_product_component(term)
-
 
     # names
 

yices_api.py

@@ -95,15 +95,16 @@ def yices_python_info_main():
 # 1.0.6    -  2.5.3    -  9/28/2017      -  LD_LIBRARY_PATH hackery, III.                      #
 # 1.0.7    -  2.5.4    -  9/29/2017      -  patch level version bump for PPA goodness          #
 # 1.0.8    -  2.5.4    -  10/4/2017      -  improving the user experience  (less SIGSEGVs)     #
-# 1.1.0    -  2.6.0    -  10/8/2018      -  major changes (addition of pythonesque api)        #
+# 1.1.0    -  2.6.0    -  10/8/2018      -  major changes (addition of pythonesque API)        #
+# 1.1.1    -  2.6.0    -  10/9/2018      -  tweaks and finish the pythonesque API              #
 ################################################################################################
 
 #
 # when the dust settles we can synch this with the library, but
 # while the bindings are moving so fast we should keep them separate.
 #
 #
-yices_python_version = '1.1.0'
+yices_python_version = '1.1.1'
 
 #
 # 1.0.1 needs yices_has_mcsat