working on symbolic execution for PDR

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

lib/api_ast.cpp

@@ -16,7 +16,7 @@ Revision History:
 
 --*/
 #include<iostream>
-#include"z3.h"
+#include"z3_internal.h"
 #include"api_log_macros.h"
 #include"api_context.h"
 #include"api_util.h"

lib/api_poly.cpp

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_poly.cpp
+
+Abstract:
+
+    External API for polynomial package
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18.
+
+Revision History:
+
+--*/
+#include"z3.h"
+#include"z3_internal.h"
+#include"api_context.h"
+#include"api_poly.h"
+#include"api_util.h"
+#include"api_log_macros.h"
+
+Z3_polynomial_manager Z3_mk_polynomial_manager(Z3_context c) {
+    Z3_TRY;
+    LOG_Z3_mk_polynomial_manager(c);
+    RESET_ERROR_CODE();
+    _Z3_polynomial_manager * m = alloc(_Z3_polynomial_manager);
+    RETURN_Z3(of_poly_manager(m));
+    Z3_CATCH_RETURN(0);
+}
+
+void Z3_del_polynomial_manager(Z3_context c, Z3_polynomial_manager m) {
+    Z3_TRY;
+    LOG_Z3_del_polynomial_manager(c, m);
+    RESET_ERROR_CODE();
+    dealloc(to_poly_manager(m));
+    Z3_CATCH;
+}
+
+Z3_polynomial Z3_mk_zero_polynomial(Z3_context c, Z3_polynomial_manager m) {
+    Z3_TRY;
+    LOG_Z3_mk_zero_polynomial(c, m);
+    RESET_ERROR_CODE();
+    polynomial::polynomial * r = to_poly_manager(m)->m_manager.mk_zero();
+    to_poly_manager(m)->m_result = r;
+    RETURN_Z3(of_poly(r));
+    Z3_CATCH_RETURN(0);
+}
+
+void Z3_polynomial_inc_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_inc_ref(c, m, p);
+    RESET_ERROR_CODE();
+    to_poly_manager(m)->m_manager.inc_ref(to_poly(p));
+    Z3_CATCH;
+}
+
+void Z3_polynomial_dec_ref(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_inc_ref(c, m, p);
+    RESET_ERROR_CODE();
+    to_poly_manager(m)->m_manager.dec_ref(to_poly(p));
+    Z3_CATCH;
+}
+
+Z3_string Z3_polynomial_to_string(Z3_context c, Z3_polynomial_manager m, Z3_polynomial p) {
+    Z3_TRY;
+    LOG_Z3_polynomial_to_string(c, m, p);
+    RESET_ERROR_CODE();
+    std::ostringstream buffer;
+    to_poly_manager(m)->m_manager.display(buffer, to_poly(p));
+    return mk_c(c)->mk_external_string(buffer.str());
+    Z3_CATCH_RETURN("");
+}
+

lib/api_poly.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    api_poly.h
+
+Abstract:
+    External API for polynomial package
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18.
+
+Revision History:
+
+--*/
+#ifndef _API_POLY_H_
+#define _API_POLY_H_
+
+#include"polynomial.h"
+
+struct _Z3_polynomial_manager {
+    unsynch_mpz_manager m_num_manager;
+    polynomial::manager m_manager;
+    polynomial_ref      m_result;
+
+    _Z3_polynomial_manager():
+        m_manager(m_num_manager),
+        m_result(m_manager) {
+    }
+};
+
+inline _Z3_polynomial_manager * to_poly_manager(Z3_polynomial_manager m) { return reinterpret_cast<_Z3_polynomial_manager*>(m); }
+inline Z3_polynomial_manager of_poly_manager(_Z3_polynomial_manager * m) { return reinterpret_cast<Z3_polynomial_manager>(m); }
+
+inline polynomial::polynomial * to_poly(Z3_polynomial p) { return reinterpret_cast<polynomial::polynomial*>(p); }
+inline Z3_polynomial of_poly(polynomial::polynomial * p) { return reinterpret_cast<Z3_polynomial>(p); }
+
+#endif

lib/api_util.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include"params.h"
 #include"lbool.h"
+#include"ast.h"
 
 #define Z3_TRY try {
 #define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }

lib/lib.vcxproj

@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
 <Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
   <ItemGroup Label="ProjectConfigurations">
     <ProjectConfiguration Include="commercial|Win32">
@@ -443,6 +443,7 @@
     <ClCompile Include="api_numeral.cpp" />
     <ClCompile Include="api_params.cpp" />
     <ClCompile Include="api_parsers.cpp" />
+    <ClCompile Include="api_poly.cpp" />
     <ClCompile Include="api_quant.cpp" />
     <ClCompile Include="api_solver_old.cpp" />
     <ClCompile Include="api_solver.cpp" />

lib/pdr_context.cpp

@@ -1737,7 +1737,6 @@ namespace pdr {
         datalog::flatten_and(forms);        
         ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
         expr_ref_vector Phi = mev.minimize_literals(forms1, M);
-
         ptr_vector<func_decl> preds;
         pt.find_predecessors(r, preds);
         pt.remove_predecessors(Phi);

lib/pdr_util.h

@@ -239,6 +239,13 @@ public:
     */
     expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
 
+    /**
+       \brief extract literals from formulas that satisfy formulas.
+
+       \pre model satisfies formulas
+    */
+    expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, expr_ref_vector const & model);
+
     // for_each_expr visitor.
     void operator()(expr* e) {} 
 };

lib/z3.h

@@ -24,6 +24,7 @@ Notes:
 #include<stdio.h>
 #include"z3_macros.h"
 #include"z3_api.h"
+#include"z3_internal_types.h"
 
 #undef __in
 #undef __out

lib/z3_internal.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_internal.h
+
+Abstract:
+
+    Z3 internal API for C and Python.
+    It provides access to internal Z3 components.
+    It should only be used by advanced users.
+    We used it to build regression tests in Python.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_INTERNAL_H_
+#define _Z3_INTERNAL_H_
+
+#include"z3_macros.h"
+#include"z3_api.h"
+#include"z3_internal_types.h"
+#include"z3_poly.h"
+
+#undef __in
+#undef __out
+#undef __inout
+#undef __in_z
+#undef __out_z
+#undef __ecount
+#undef __in_ecount
+#undef __out_ecount
+#undef __inout_ecount
+
+#endif

lib/z3_internal_types.h

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_internal_types.h
+
+Abstract:
+
+    Z3 internal API type declarations.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_INTERNAL_TYPES_H_
+#define _Z3_INTERNAL_TYPES_H_
+
+DEFINE_TYPE(Z3_polynomial_manager);
+DEFINE_TYPE(Z3_polynomial);
+DEFINE_TYPE(Z3_monomial);
+
+/*
+  Definitions for update_api.py
+  
+  def_Type('POLYNOMIAL_MANAGER',           'Z3_polynomial_manager',           'PolynomialManagerObj')
+  def_Type('POLYNOMIAL',                   'Z3_polynomial',                   'PolynomialObj')
+  def_Type('MONOMIAL',                     'Z3_monomial',                     'MonomialObj')
+*/
+
+#endif

lib/z3_poly.h

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    z3_poly.h
+
+Abstract:
+
+    Z3 multivariate polynomial API.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-18
+
+Notes:
+    
+--*/
+#ifndef _Z3_POLY_H_
+#define _Z3_POLY_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif // __cplusplus
+
+    /**
+       \brief Create a new polynomial manager.
+
+       def_API('Z3_mk_polynomial_manager', POLYNOMIAL_MANAGER, (_in(CONTEXT),))
+    */
+    Z3_polynomial_manager Z3_API Z3_mk_polynomial_manager(__in Z3_context c);
+    
+    /**
+       \brief Delete the given polynomial manager.
+       
+       def_API('Z3_del_polynomial_manager', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER)))
+    */
+    void Z3_API Z3_del_polynomial_manager(__in Z3_context c, __in Z3_polynomial_manager m);
+
+    /**
+       \brief Return the zero polynomial.
+
+       def_API('Z3_mk_zero_polynomial', POLYNOMIAL, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER)))
+    */
+    Z3_polynomial Z3_API Z3_mk_zero_polynomial(__in Z3_context c, __in Z3_polynomial_manager m);
+
+    /**
+       \brief Increment p's reference counter
+
+       def_API('Z3_polynomial_inc_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    void Z3_API Z3_polynomial_inc_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+
+    /**
+       \brief Decrement p's reference counter.
+
+       def_API('Z3_polynomial_dec_ref', VOID, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    void Z3_API Z3_polynomial_dec_ref(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+    
+    /**
+       \brief Convert the given polynomial into a string.
+
+       def_API('Z3_polynomial_to_string', STRING, (_in(CONTEXT), _in(POLYNOMIAL_MANAGER), _in(POLYNOMIAL)))
+    */
+    Z3_string Z3_API Z3_polynomial_to_string(__in Z3_context c, __in Z3_polynomial_manager m, __in Z3_polynomial p);
+
+#ifdef __cplusplus
+};
+#endif // __cplusplus
+
+#endif