merge

RELEASE_NOTES

@@ -11,7 +11,7 @@ Version 4.4
 
 - Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one.
 
-- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, and Stackoverflow users user297886.
+- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, steimann, and Stackoverflow users user297886.
 
 
 Version 4.3.2

examples/c++/example.cpp

@@ -1,9 +1,11 @@
 #include<vector>
 #include"z3++.h"
 
-
 using namespace z3;
 
+
+
+
 /**
    Demonstration of how Z3 can be used to prove validity of
    De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
@@ -985,6 +987,7 @@ void extract_example() {
 }
 
 int main() {
+
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";

src/api/api_context.cpp

@@ -89,6 +89,7 @@ namespace api {
         m_bv_util(m()),
         m_datalog_util(m()),
         m_fpa_util(m()),
+	m_dtutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_replay_stack() {

src/api/api_context.h

@@ -58,6 +58,7 @@ namespace api {
         bv_util                    m_bv_util;
         datalog::dl_decl_util      m_datalog_util;
         fpa_util                   m_fpa_util;
+	datatype_util              m_dtutil;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -119,6 +120,7 @@ namespace api {
         bv_util & bvutil() { return m_bv_util; }
         datalog::dl_decl_util & datalog_util() { return m_datalog_util; }
         fpa_util & fpautil() { return m_fpa_util; }
+	datatype_util& dtutil() { return m_dtutil; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }

src/api/api_datatype.cpp

@@ -36,7 +36,7 @@ extern "C" {
         RESET_ERROR_CODE(); 
         mk_c(c)->reset_last_result();
         ast_manager& m = mk_c(c)->m();
-        datatype_util dt_util(m);
+        datatype_util& dt_util = mk_c(c)->dtutil();
 
         sort_ref_vector tuples(m);
         sort* tuple;
@@ -102,7 +102,7 @@ extern "C" {
         RESET_ERROR_CODE();
         mk_c(c)->reset_last_result();
         ast_manager& m = mk_c(c)->m();
-        datatype_util dt_util(m);
+        datatype_util& dt_util = mk_c(c)->dtutil();
 
         sort_ref_vector sorts(m);
         sort* e;
@@ -451,7 +451,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, 0);
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
@@ -470,13 +470,13 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_VALID_AST(t, 0);   
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        if (idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
@@ -499,16 +499,16 @@ extern "C" {
         LOG_Z3_get_datatype_sort_recognizer(c, t, idx);
         RESET_ERROR_CODE();   
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx >= decls->size()) {
+        if (idx >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);                        
+            return 0;
         }
         func_decl* decl = (*decls)[idx];
         decl = dt_util.get_constructor_recognizer(decl);
@@ -522,16 +522,16 @@ extern "C" {
         LOG_Z3_get_datatype_sort_constructor_accessor(c, t, idx_c, idx_a);
         RESET_ERROR_CODE();  
         sort * _t = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         
         if (!dt_util.is_datatype(_t)) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);            
         }
         ptr_vector<func_decl> const * decls = dt_util.get_datatype_constructors(_t);
-        if (!decls || idx_c >= decls->size()) {
+        if (idx_c >= decls->size()) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
-            RETURN_Z3(0);                        
+            return 0;
         }
         func_decl* decl = (*decls)[idx_c];
         if (decl->get_arity() <= idx_a) {
@@ -555,7 +555,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_mk_decl(c, t);
         RESET_ERROR_CODE();  
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
@@ -570,7 +570,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_num_fields(c, t);
         RESET_ERROR_CODE();   
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;            
@@ -593,7 +593,7 @@ extern "C" {
         LOG_Z3_get_tuple_sort_field_decl(c, t, i);
         RESET_ERROR_CODE();  
         sort * tuple = to_sort(t);
-        datatype_util dt_util(mk_c(c)->m());
+        datatype_util& dt_util = mk_c(c)->dtutil();
         if (!dt_util.is_datatype(tuple) || dt_util.is_recursive(tuple) || dt_util.get_datatype_num_constructors(tuple) != 1) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);

src/api/dotnet/EnumSort.cs

@@ -44,6 +44,16 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the inx'th constant declaration in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public FuncDecl ConstDecl(uint inx)
+        {
+            return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, inx));
+        }
+
         /// <summary>
         /// The constants in the enumeration.
         /// </summary>
@@ -61,7 +71,17 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// The test predicates for the constants in the enumeration.
+        /// Retrieves the inx'th constant in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public Expr Const(uint inx)
+        {
+            return Context.MkApp(ConstDecl(inx));
+        }
+
+        /// <summary>
+        /// The test predicates (recognizers) for the constants in the enumeration.
         /// </summary>
         public FuncDecl[] TesterDecls
         {
@@ -76,6 +96,16 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Retrieves the inx'th tester/recognizer declaration in the enumeration.
+        /// </summary>
+        /// <param name="inx"></param>
+        /// <returns></returns>
+        public FuncDecl TesterDecl(uint inx)
+        {
+            return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, inx));
+        }
+
         #region Internal
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
             : base(ctx, IntPtr.Zero)

src/api/java/EnumSort.java

@@ -35,10 +35,19 @@ public class EnumSort extends Sort
         return t;
     }
     
+    /**
+     * Retrieves the inx'th constant declaration in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl getConstDecl(int inx) throws Z3Exception
+    {
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), inx));
+    }
+
     /**
      * The constants in the enumeration.
      * @throws Z3Exception on error
-     * @return an Expr
+     * @return an Expr[]
      **/
     public Expr[] getConsts() throws Z3Exception
     {        
@@ -49,6 +58,16 @@ public class EnumSort extends Sort
         return t;
     }
     
+    /**
+     * Retrieves the inx'th constant in the enumeration.
+     * @throws Z3Exception on error
+     * @return an Expr
+     **/
+    public Expr getConst(int inx) throws Z3Exception
+    {        
+    	return getContext().mkApp(getConstDecl(inx));
+    }
+
     /**
      * The test predicates for the constants in the enumeration.
      * @throws Z3Exception on error
@@ -62,6 +81,15 @@ public class EnumSort extends Sort
         return t;
     }
     
+    /**
+     * Retrieves the inx'th tester/recognizer declaration in the enumeration.
+     * @throws Z3Exception on error
+     **/
+    public FuncDecl getTesterDecl(int inx) throws Z3Exception
+    {
+        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), inx));
+    }
+
     EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
     {
         super(ctx, 0);

src/api/ml/z3.ml

@@ -1390,11 +1390,24 @@ struct
     let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x)  i)) in
     mk_list f n
 
+  let get_const_decl ( x : sort ) ( inx : int ) =
+    func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) inx)
+
+  let get_consts ( x : sort ) =
+    let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
+    let f i = (Expr.mk_const_f (Sort.gc x) (get_const_decl x i)) in
+    mk_list f n
+
+  let get_const ( x : sort ) ( inx : int ) =
+    Expr.mk_const_f (Sort.gc x) (get_const_decl x inx)
+
   let get_tester_decls ( x : sort ) = 
     let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
     let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in
     mk_list f n
       
+  let get_tester_decl ( x : sort ) ( inx : int ) = 
+    func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) inx)
 end
 
 

src/api/ml/z3.mli

@@ -1091,8 +1091,20 @@ sig
   (** The function declarations of the constants in the enumeration. *)
   val get_const_decls : Sort.sort -> FuncDecl.func_decl list
 
+  (** Retrieves the inx'th constant declaration in the enumeration. *)
+  val get_const_decl : Sort.sort -> int -> FuncDecl.func_decl
+
+  (** The constants in the enumeration. *)
+  val get_consts : Sort.sort -> Expr.expr list
+
+  (** Retrieves the inx'th constant in the enumeration. *)
+  val get_const : Sort.sort -> int -> Expr.expr
+
   (** The test predicates for the constants in the enumeration. *)
   val get_tester_decls : Sort.sort -> FuncDecl.func_decl list
+
+  (** Retrieves the inx'th tester/recognizer declaration in the enumeration. *)
+  val get_tester_decl : Sort.sort -> int -> FuncDecl.func_decl
 end
 
 (** Functions to manipulate List expressions *)

src/ast/datatype_decl_plugin.h

@@ -169,8 +169,8 @@ class datatype_util {
     ast_ref_vector                              m_asts;
     ptr_vector<ptr_vector<func_decl> >          m_vectors;
     
-    func_decl * get_constructor(sort * ty, unsigned c_id);
     func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
+    func_decl * get_constructor(sort * ty, unsigned c_id);
 
 public:
     datatype_util(ast_manager & m);
@@ -185,7 +185,12 @@ public:
     bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); }
     bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
     ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
-    unsigned get_datatype_num_constructors(sort * ty) { return get_datatype_constructors(ty)->size(); }
+    unsigned get_datatype_num_constructors(sort * ty) { 
+        SASSERT(is_datatype(ty));
+        unsigned tid = ty->get_parameter(1).get_int();
+        unsigned o = ty->get_parameter(3 + 2 * tid).get_int();
+        return ty->get_parameter(o).get_int(); 
+    }
     unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); }
     unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); }
     func_decl * get_non_rec_constructor(sort * ty);
@@ -197,6 +202,7 @@ public:
     bool are_siblings(sort * s1, sort * s2);
     void reset();
     void display_datatype(sort *s, std::ostream& strm);
+
 };
 
 #endif /* _DATATYPE_DECL_PLUGIN_H_ */

src/ast/fpa/fpa2bv_converter.cpp

@@ -1878,6 +1878,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
     else if (num == 2 &&
              m_bv_util.is_bv(args[0]) &&
              m_bv_util.get_bv_size(args[0]) == 3 &&
+             m_arith_util.is_int(args[1]) || 
              m_arith_util.is_real(args[1])) {
         // rm + real -> float
         mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
@@ -2066,7 +2067,7 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
     TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl << 
                                     "x: " << mk_ismt2_pp(x, m) << std::endl;);
     SASSERT(m_util.is_float(s));
-    SASSERT(au().is_real(x));
+    SASSERT(au().is_real(x) || au().is_int(x));
 
     unsigned ebits = m_util.get_ebits(s);
     unsigned sbits = m_util.get_sbits(s);
@@ -2089,7 +2090,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
         }
 
         rational q;
-        m_util.au().is_numeral(x, q);
+        bool is_int;
+        m_util.au().is_numeral(x, q, is_int);
 
         scoped_mpf v(m_mpf_manager);
         m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());

src/ast/fpa_decl_plugin.cpp

@@ -521,14 +521,26 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
         symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
+    else if (arity == 2 &&
+             is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+             is_sort_of(domain[1], m_arith_fid, INT_SORT)) {
+        // Rounding + 1 Int -> 1 FP
+        if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()))
+            m_manager->raise_exception("expecting two integer parameters to to_fp");
+
+        sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
+        symbol name("to_fp");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
     else {
         m_manager->raise_exception("Unexpected argument combination for (_ to_fp eb sb). Supported argument combinations are: "
-                                   "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)),"
+                                   "((_ BitVec 1) (_ BitVec eb) (_ BitVec sb-1)), "
-                                   "(_ BitVec (eb+sb)),"
+                                   "(_ BitVec (eb+sb)), "
-                                   "(Real),"
+                                   "(Real), "
-                                   "(RoundingMode (_ BitVec (eb+sb))),"
+                                   "(RoundingMode (_ BitVec (eb+sb))), "
-                                   "(RoundingMode (_ FloatingPoint eb' sb')),"
+                                   "(RoundingMode (_ FloatingPoint eb' sb')), "
-                                   "(RoundingMode Real Int), and"
+                                   "(RoundingMode Real Int), "
+                                   "(RoundingMode Int), and "
                                    "(RoundingMode Real)."
                                    );
     }

src/muz/base/dl_context.cpp

@@ -288,7 +288,7 @@ namespace datalog {
     bool context::unbound_compressor() const { return m_params->unbound_compressor(); }
     bool context::similarity_compressor() const { return m_params->similarity_compressor(); }
     unsigned context::similarity_compressor_threshold() const { return m_params->similarity_compressor_threshold(); }
-    unsigned context::soft_timeout() const { return m_fparams.m_soft_timeout; }
+    unsigned context::timeout() const { return m_fparams.m_timeout; }
     unsigned context::initial_restart_timeout() const { return m_params->initial_restart_timeout(); } 
     bool context::generate_explanations() const { return m_params->generate_explanations(); }
     bool context::explanations_on_relation_level() const { return m_params->explanations_on_relation_level(); }

src/muz/base/dl_context.h

@@ -258,7 +258,7 @@ namespace datalog {
         bool unbound_compressor() const;
         bool similarity_compressor() const;
         unsigned similarity_compressor_threshold() const;
-        unsigned soft_timeout() const;
+        unsigned timeout() const;
         unsigned initial_restart_timeout() const;
         bool generate_explanations() const;
         bool explanations_on_relation_level() const;

src/muz/clp/clp_context.cpp

@@ -59,7 +59,7 @@ namespace datalog {
         {
             // m_fparams.m_relevancy_lvl = 0;
             m_fparams.m_mbqi = false;
-            m_fparams.m_soft_timeout = 1000;
+            m_fparams.m_timeout = 1000;
         }
 
         ~imp() {}        

src/muz/rel/rel_context.cpp

@@ -128,8 +128,8 @@ namespace datalog {
 
     lbool rel_context::saturate(scoped_query& sq) {
         m_context.ensure_closed();        
-        bool time_limit = m_context.soft_timeout()!=0;
+        bool time_limit = m_context.timeout()!=0;
-        unsigned remaining_time_limit = m_context.soft_timeout();
+        unsigned remaining_time_limit = m_context.timeout();
         unsigned restart_time = m_context.initial_restart_timeout();
                         
         instruction_block termination_code;

src/muz/tab/tab_context.cpp

@@ -1367,7 +1367,7 @@ namespace datalog {
         {
             // m_fparams.m_relevancy_lvl = 0;
             m_fparams.m_mbqi = false;
-            m_fparams.m_soft_timeout = 1000;
+            m_fparams.m_timeout = 1000;
         }
 
         ~imp() {}        

src/smt/params/smt_params.cpp

@@ -34,7 +34,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
-    m_soft_timeout = p.soft_timeout();
+    m_timeout = p.timeout();
     model_params mp(_p);
     m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))

src/smt/params/smt_params.h

@@ -202,7 +202,7 @@ struct smt_params : public preprocessor_params,
     bool                m_preprocess;  // temporary hack for disabling all preprocessing..
     bool                m_user_theory_preprocess_axioms;
     bool                m_user_theory_persist_axioms;
-    unsigned            m_soft_timeout;
+    unsigned            m_timeout;
     bool                m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
     bool                m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.    
     bool                m_dump_goal_as_smt;
@@ -270,7 +270,7 @@ struct smt_params : public preprocessor_params,
         m_preprocess(true), // temporary hack for disabling all preprocessing..
         m_user_theory_preprocess_axioms(false),
         m_user_theory_persist_axioms(false),
-        m_soft_timeout(0),
+        m_timeout(0),
         m_at_labels_cex(false),
         m_check_at_labels(false),
         m_dump_goal_as_smt(false),

src/smt/params/smt_params_helper.pyg

@@ -15,7 +15,7 @@ def_module_params(module_name='smt',
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
                           ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
-                          ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
+                          ('timeout', UINT, 0, 'timeout (0 means no timeout)'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
                           ('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),

src/smt/smt_context.cpp

@@ -3355,7 +3355,7 @@ namespace smt {
             if (m_last_search_failure != OK)
                 return true;
             
-            if (m_timer.ms_timeout(m_fparams.m_soft_timeout)) {
+            if (m_timer.ms_timeout(m_fparams.m_timeout)) {
                 m_last_search_failure = TIMEOUT;
                 return true;
             }