Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/dotnet/Context.cs

@@ -303,6 +303,9 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create a new finite domain sort.
+	/// <param name="name">The name used to identify the sort</param>
+	/// <param size="size">The size of the sort</param>
+	/// <returns>The result is a sort</returns>
         /// </summary>
         public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
         {
@@ -315,6 +318,11 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create a new finite domain sort.
+	/// <param name="name">The name used to identify the sort</param>
+	/// <param size="size">The size of the sort</param>
+	/// <returns>The result is a sort</returns>
+	/// Elements of the sort are created using <seealso cref="MkNumeral"/>, 
+	/// and the elements range from 0 to <tt>size-1</tt>.
         /// </summary>
         public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
         {

src/api/z3_api.h

@@ -1721,6 +1721,8 @@ extern "C" {
        To create constants that belong to the finite domain, 
        use the APIs for creating numerals and pass a numeric
        constant together with the sort returned by this call.
+       The numeric constant should be between 0 and the less 
+       than the size of the domain.
 
        \sa Z3_get_finite_domain_sort_size
 

src/ast/dl_decl_plugin.cpp

@@ -657,7 +657,9 @@ namespace datalog {
             SASSERT(value == 1);
             return m.mk_true();
         }
-        m.raise_exception("unrecognized sort");
+        std::stringstream strm;
+        strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort";
+        m.raise_exception(strm.str().c_str());
         return 0;
     }
 

src/muz_qe/clp_context.cpp

@@ -68,9 +68,13 @@ namespace datalog {
             m_goals.reset();
             rm.mk_query(query, m_ctx.get_rules());
             m_ctx.apply_default_transformation();
-            func_decl *head_decl = m_ctx.get_rules().get_output_predicate();
+            func_decl* head_decl = m_ctx.get_rules().get_output_predicate();
-
+            rule_set& rules = m_ctx.get_rules();
-            expr_ref head(m_ctx.get_rules().get_predicate_rules(head_decl)[0]->get_head(), m);
+            rule_vector const& rv = rules.get_predicate_rules(head_decl);
+            if (rv.empty()) {
+                return l_false;
+            }
+            expr_ref head(rv[0]->get_head(), m);
             ground(head);
             m_goals.push_back(to_app(head));
             return search(20, 0);

src/muz_qe/dl_mk_array_blast.cpp

@@ -250,11 +250,11 @@ namespace datalog {
         rule_set new_rules(m_ctx);
         rm.mk_rule(fml2, p, new_rules, r.name());
 
-        TRACE("dl", new_rules.last()->display(m_ctx, tout << "new rule\n"););
         rule_ref new_rule(rm);
         if (m_simplifier.transform_rule(new_rules.last(), new_rule)) {
             rules.add_rule(new_rule.get());
             rm.mk_rule_rewrite_proof(r, *new_rule.get());
+            TRACE("dl", new_rule->display(m_ctx, tout << "new rule\n"););
         }
         return true;
     }

src/muz_qe/dl_rule.cpp

@@ -41,6 +41,7 @@ Revision History:
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
 #include"expr_safe_replace.h"
+#include"filter_model_converter.h"
 
 namespace datalog {
 
@@ -335,8 +336,14 @@ namespace datalog {
         vars.reverse();
         names.reverse();
         func_decl* qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
-        m_ctx.register_predicate(qpred, false);
+        m_ctx.register_predicate(qpred, false);        
         rules.set_output_predicate(qpred);
+        
+        if (m_ctx.get_model_converter()) {
+            filter_model_converter* mc = alloc(filter_model_converter, m);
+            mc->insert(qpred);
+            m_ctx.add_model_converter(mc);
+        }
 
         expr_ref_vector qhead_args(m);
         for (unsigned i = 0; i < vars.size(); i++) {

src/muz_qe/horn_tactic.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include"expr_replacer.h"
 #include"dl_rule_transformer.h"
 #include"dl_mk_slice.h"
+#include"filter_model_converter.h"
 
 class horn_tactic : public tactic {
     struct imp {
@@ -226,6 +227,9 @@ class horn_tactic : public tactic {
                 }
                 queries.reset();
                 queries.push_back(q);
+                filter_model_converter* mc1 = alloc(filter_model_converter, m);
+                mc1->insert(to_app(q)->get_decl());
+                mc = mc1;
             }
             SASSERT(queries.size() == 1);
             q = queries[0].get();
@@ -276,7 +280,13 @@ class horn_tactic : public tactic {
                 g->reset();
                 if (produce_models) {
                     model_ref md = m_ctx.get_model();
-                    mc = model2model_converter(&*md);
+                    model_converter_ref mc2 = model2model_converter(&*md);
+                    if (mc) {
+                        mc = concat(mc.get(), mc2.get());
+                    }
+                    else {
+                        mc = mc2;
+                    }
                 }
                 break;    
             }

src/muz_qe/pdr_context.cpp

@@ -1881,6 +1881,11 @@ namespace pdr {
     // predicate transformer (or some unfolding of it).
     // 
     lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) {
+      TRACE("pdr", 
+            tout << "expand_state: " << n.pt().head()->get_name();
+            tout << " level: " << n.level() << "\n";
+            tout << mk_pp(n.state(), m) << "\n";);
+      
         return n.pt().is_reachable(n, &result, uses_level);
     }
 

src/muz_qe/pdr_generalizers.cpp

@@ -195,13 +195,14 @@ namespace pdr {
         }
         conv1.append(eqs);
         if (m_is_closure) {
-            conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
-            conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
-        }
-        else {
             conv1.push_back(a.mk_ge(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
             conv1.push_back(a.mk_ge(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
         }
+        else {
+            // is interior:
+            conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
+            conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        }
         conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
         expr_ref fml = n.pt().get_formulas(n.level(), false);
         expr_ref_vector fmls(m);
@@ -235,7 +236,7 @@ namespace pdr {
                            verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
             }            
         }
-        if (!m_is_closure || new_cores.empty()) {
+        if (!m_is_closure || new_cores.size() == orig_size) {
             new_cores.push_back(std::make_pair(core, uses_level));
         }