exposed subresultants aka psc-chain procedure

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

scripts/mk_project.py

@@ -58,11 +58,11 @@ def init_project_def():
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
+    API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h']
     add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
-            includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h', 'z3_algebraic.h'])
+            includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
     add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
     add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
-    API_files = ['z3_api.h', 'z3_algebraic.h']
     add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', 
             reexports=['api'], 
             dll_name='libz3', 

src/api/api_algebraic.cpp

@@ -21,11 +21,11 @@ Notes:
 #include"z3.h"
 #include"api_log_macros.h"
 #include"api_context.h"
+#include"api_ast_vector.h"
 #include"algebraic_numbers.h"
 #include"expr2polynomial.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
-#include"api_ast_vector.h"
 
 extern "C" {
 

src/api/api_polynomial.cpp

@@ -16,7 +16,16 @@ Author:
 Notes:
     
 --*/
+#include<iostream>
+#include"z3.h"
+#include"api_log_macros.h"
+#include"api_context.h"
 #include"api_polynomial.h"
+#include"api_ast_vector.h"
+#include"expr2polynomial.h"
+#include"cancel_eh.h"
+#include"scoped_timer.h"
+#include"expr2var.h"
 
 namespace api {
 
@@ -32,3 +41,44 @@ namespace api {
     }
 
 };
+
+extern "C" {
+
+    Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x) {
+        Z3_TRY;
+        LOG_Z3_polynomial_subresultants(c, p, q, x);
+        RESET_ERROR_CODE();
+        polynomial::manager & pm = mk_c(c)->pm();
+        polynomial_ref _p(pm), _q(pm);
+        polynomial::scoped_numeral d(pm.m());
+        default_expr2polynomial converter(mk_c(c)->m(), pm);
+        if (!converter.to_polynomial(to_expr(p), _p, d) ||
+            !converter.to_polynomial(to_expr(q), _q, d)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        mk_c(c)->save_object(result);
+        if (converter.is_var(to_expr(x))) {
+            expr2var const & mapping = converter.get_mapping();
+            unsigned v_x = mapping.to_var(to_expr(x));
+            polynomial_ref_vector rs(pm);
+            polynomial_ref r(pm);
+            expr_ref _r(mk_c(c)->m());
+            {
+                cancel_eh<polynomial::manager> eh(pm);
+                api::context::set_interruptable(*(mk_c(c)), eh);
+                scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
+                pm.psc_chain(_p, _q, v_x, rs);
+            }
+            for (unsigned i = 0; i < rs.size(); i++) {
+                r = rs.get(i);
+                converter.to_expr(r, true, _r);
+                result->m_ast_vector.push_back(_r);
+            }
+        }
+        RETURN_Z3(of_ast_vector(result));
+        Z3_CATCH_RETURN(0);
+    }
+
+};

src/api/python/z3poly.py

@@ -0,0 +1,37 @@
+############################################
+# Copyright (c) 2012 Microsoft Corporation
+# 
+# Z3 Python interface for Z3 polynomials
+#
+# Author: Leonardo de Moura (leonardo)
+############################################
+from z3 import *
+
+def subresultants(p, q, x):
+    """
+    Return the non-constant subresultants of 'p' and 'q' with respect to the "variable" 'x'.
+
+    'p', 'q' and 'x' are Z3 expressions where 'p' and 'q' are arithmetic terms.
+    Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
+    Example: f(a) is a considered to be a variable b in the polynomial       
+
+    f(a)*f(a) + 2*f(a) + 1 
+    
+    >>> x, y = Reals('x y')
+    >>> subresultants(2*x + y, 3*x - 2*y + 2, x)
+    [-7*y + 4]
+    >>> r = subresultants(3*y*x**2 + y**3 + 1, 2*x**3 + y + 3, x)
+    >>> r[0]
+    4*y**9 + 12*y**6 + 27*y**5 + 162*y**4 + 255*y**3 + 4
+    >>> r[1]
+    -6*y**4 + -6*y
+    """
+    return AstVector(Z3_polynomial_subresultants(p.ctx_ref(), p.as_ast(), q.as_ast(), x.as_ast()), p.ctx)
+
+if __name__ == "__main__":
+    import doctest
+    if doctest.testmod().failed:
+        exit(1)
+
+
+    

src/api/z3.h

@@ -25,6 +25,7 @@ Notes:
 #include"z3_macros.h"
 #include"z3_api.h"
 #include"z3_algebraic.h"
+#include"z3_polynomial.h"
 
 #undef __in
 #undef __out

src/api/z3_polynomial.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_polynomial.h
+
+Abstract:
+
+    Additional APIs for polynomials.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-12-09
+
+Notes:
+    
+--*/
+
+#ifndef _Z3_POLYNOMIAL_H_
+#define _Z3_POLYNOMIAL_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /**
+       \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
+       
+       \pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms.
+       Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
+       Example: f(a) is a considered to be a variable in the polynomial   
+                  
+       f(a)*f(a) + 2*f(a) + 1 
+
+       def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
+    */
+    Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
+
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif

src/math/polynomial/polynomial.h

@@ -219,6 +219,7 @@ namespace polynomial {
         void set_zp(uint64 p);
 
         void set_cancel(bool f);
+        void cancel() { set_cancel(true); }
 
         /**
            \brief Abstract event handler.