Merge branch 'working' of //z3-1/z3 into working

lib/api_ast.cpp

@@ -964,7 +964,7 @@ extern "C" {
             case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR; 
             case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ; 
             case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA; 
-
+            case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
             default:
                 UNREACHABLE();
                 return Z3_OP_UNINTERPRETED;

lib/ast.cpp

@@ -646,7 +646,8 @@ basic_decl_plugin::basic_decl_plugin():
     m_def_intro_decl(0),
     m_iff_oeq_decl(0),
     m_skolemize_decl(0),
-    m_mp_oeq_decl(0) {
+    m_mp_oeq_decl(0),
+    m_hyper_res_decl0(0) {
 }
 
 bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const {
@@ -751,6 +752,9 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_param
         SASSERT(num_parents == 0);
         return mk_proof_decl("quant-inst", k, num_parameters, params, num_parents);
     }
+    case PR_HYPER_RESOLVE: {
+        return mk_proof_decl("hyper-res", k, num_parameters, params, num_parents);
+    }
     default:
         UNREACHABLE();
         return 0;
@@ -813,6 +817,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_SKOLEMIZE:                    return mk_proof_decl("sk", k, 0, m_skolemize_decl);
     case PR_MODUS_PONENS_OEQ:             return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
     case PR_TH_LEMMA:                     return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
+    case PR_HYPER_RESOLVE:                return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0);
     default:
         UNREACHABLE();
         return 0;
@@ -934,6 +939,7 @@ void basic_decl_plugin::finalize() {
     DEC_ARRAY_REF(m_cnf_star_decls);
 
     DEC_ARRAY_REF(m_th_lemma_decls);
+    DEC_REF(m_hyper_res_decl0);
 
 }
 
@@ -2830,6 +2836,82 @@ proof * ast_manager::mk_th_lemma(
     return mk_app(m_basic_family_id, PR_TH_LEMMA, num_params+1, parameters.c_ptr(), args.size(), args.c_ptr());
 }
 
+proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
+                                     svector<std::pair<unsigned, unsigned> > const& positions,
+                                     vector<expr_ref_vector> const& substs) {
+    ptr_vector<expr> fmls;
+    SASSERT(positions.size() + 1 == substs.size());
+    for (unsigned i = 0; i < num_premises; ++i) {
+        TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";);
+        fmls.push_back(get_fact(premises[i]));
+    }
+    SASSERT(is_bool(concl));
+    vector<parameter> params;
+    for (unsigned i = 0; i < substs.size(); ++i) {
+        expr_ref_vector const& vec = substs[i];
+        for (unsigned j = 0; j < vec.size(); ++j) {
+            params.push_back(parameter(vec[j]));
+        }
+        if (i + 1 < substs.size()) {
+            params.push_back(parameter(positions[i].first));
+            params.push_back(parameter(positions[i].second));
+        }
+    }
+    ptr_vector<sort> sorts;
+    ptr_vector<expr> args;
+    for (unsigned i = 0; i < num_premises; ++i) {
+        sorts.push_back(mk_proof_sort());
+        args.push_back(premises[i]);
+    }
+    sorts.push_back(mk_bool_sort());
+    args.push_back(concl);
+    app* result = mk_app(m_basic_family_id, PR_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr());
+    SASSERT(result->get_family_id() == m_basic_family_id);
+    SASSERT(result->get_decl_kind() == PR_HYPER_RESOLVE);
+    return result;
+}
+
+bool ast_manager::is_hyper_resolve(
+    proof* p, 
+    proof_ref_vector& premises,
+    expr_ref& conclusion,
+    svector<std::pair<unsigned, unsigned> > & positions,
+    vector<expr_ref_vector> & substs) {
+    if (!is_hyper_resolve(p)) {
+        return false;
+    }
+    unsigned sz = p->get_num_args();
+    SASSERT(sz > 0);
+    for (unsigned i = 0; i + 1 < sz; ++i) {
+        premises.push_back(to_app(p->get_arg(i)));
+    }
+    conclusion = p->get_arg(sz-1);
+    func_decl* d = p->get_decl();
+    unsigned num_p = d->get_num_parameters();
+    parameter const* params = d->get_parameters();
+    
+    substs.push_back(expr_ref_vector(*this));
+    for (unsigned i = 0; i < num_p; ++i) {
+        if (params[i].is_int()) {
+            SASSERT(i + 1 < num_p);
+            SASSERT(params[i+1].is_int());
+            unsigned x = static_cast<unsigned>(params[i].get_int());
+            unsigned y = static_cast<unsigned>(params[i+1].get_int());
+            positions.push_back(std::make_pair(x, y));
+            substs.push_back(expr_ref_vector(*this));
+            ++i;
+        }
+        else {
+            SASSERT(params[i].is_ast());
+            ast* a = params[i].get_ast();
+            SASSERT(is_expr(a));
+            substs.back().push_back(to_expr(a));                
+        }
+    }
+    
+    return true;
+}
+
 
 // -----------------------------------
 //

lib/ast.h

@@ -972,7 +972,7 @@ enum basic_op_kind {
     PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
 
     PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR, 
-    PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, LAST_BASIC_PR
+    PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
 };
 
 class basic_decl_plugin : public decl_plugin {
@@ -1034,6 +1034,7 @@ protected:
     ptr_vector<func_decl> m_cnf_star_decls;
 
     ptr_vector<func_decl> m_th_lemma_decls;
+    func_decl * m_hyper_res_decl0;
 
     static bool is_proof(decl_kind k) { return k > LAST_BASIC_OP; }
     bool check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const;
@@ -1928,6 +1929,11 @@ public:
 
     bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; }
 
+    proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
+                            svector<std::pair<unsigned, unsigned> > const& positions,
+                            vector<ref_vector<expr, ast_manager> > const& substs);
+    
+
     bool is_undef_proof(expr const * e) const { return e == m_undef_proof; }
     bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); }
     bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); }
@@ -1947,6 +1953,12 @@ public:
     bool is_lemma(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_LEMMA); }
     bool is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<expr>& binding) const;
     bool is_rewrite(expr const* e, expr*& r1, expr*& r2) const;
+    bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_basic_family_id, PR_HYPER_RESOLVE); }
+    bool is_hyper_resolve(proof* p, 
+                          ref_vector<proof, ast_manager>& premises,
+                          obj_ref<expr, ast_manager>& conclusion,
+                          svector<std::pair<unsigned, unsigned> > & positions,
+                          vector<ref_vector<expr, ast_manager> >& substs);
 
     
     bool is_def_intro(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_DEF_INTRO); }

lib/dl_bmc_engine.cpp

@@ -179,7 +179,7 @@ namespace datalog {
 
                  substs.push_back(sub1);
                  substs.push_back(sub);
-                 pr = util.mk_hyper_resolve(2, premises, concl, positions, substs);
+                 pr = m.mk_hyper_resolve(2, premises, concl, positions, substs);
                  r0 = r1;
              }
              else {
@@ -191,7 +191,7 @@ namespace datalog {
                  }
                  else {
                      substs.push_back(sub);
-                     pr = util.mk_hyper_resolve(1, &p, concl, positions, substs);
+                     pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
                  }
                  r0 = r2;
              }

lib/dl_context.cpp

@@ -54,6 +54,7 @@ Revision History:
 #include"expr_functors.h"
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
+#include"datatype_decl_plugin.h"
 
 namespace datalog {
 
@@ -1118,10 +1119,11 @@ namespace datalog {
     class context::engine_type_proc {
         ast_manager& m;
         arith_util   a;
+        datatype_util dt;
         DL_ENGINE    m_engine;
 
     public:
-        engine_type_proc(ast_manager& m): m(m), a(m), m_engine(DATALOG_ENGINE) {}
+        engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
 
         DL_ENGINE get_engine() const { return m_engine; }
         void operator()(expr* e) {
@@ -1134,6 +1136,9 @@ namespace datalog {
             else if (is_var(e) && m.is_bool(e)) {
                 m_engine = PDR_ENGINE;
             }
+            else if (dt.is_datatype(m.get_sort(e))) {
+                m_engine = PDR_ENGINE;
+            }
         }
     };
 

lib/dl_decl_plugin.cpp

@@ -489,12 +489,6 @@ namespace datalog {
         return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
     }
 
-    func_decl * dl_decl_plugin::mk_hyper_res(unsigned num_params, parameter const* params, unsigned arity, sort *const* domain) {
-        ast_manager& m = *m_manager;
-        func_decl_info info(m_family_id, OP_DL_HYPER_RESOLVE, num_params, params);
-        return m_manager->mk_func_decl(m_hyper_resolve_sym, arity, domain, m_manager->mk_proof_sort(), info);
-    }
-
     func_decl * dl_decl_plugin::mk_func_decl(
         decl_kind k, unsigned num_parameters, parameter const * parameters, 
         unsigned arity, sort * const * domain, sort * range) {
@@ -606,10 +600,6 @@ namespace datalog {
                 result = mk_compare(OP_DL_LT, m_lt_sym, domain);
                 break;                
 
-            case OP_DL_HYPER_RESOLVE:
-                result = mk_hyper_res(num_parameters, parameters, arity, domain);
-                break;
-
             default:
                 m_manager->raise_exception("operator not recognized");
                 return 0;
@@ -752,80 +742,4 @@ namespace datalog {
         return m.mk_app(f, num_args, args);
     }
 
-    proof* dl_decl_util::mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
-                                          svector<std::pair<unsigned, unsigned> > const& positions,
-                                          vector<expr_ref_vector> const& substs) {
-        ptr_vector<expr> fmls;
-        SASSERT(positions.size() + 1 == substs.size());
-        for (unsigned i = 0; i < num_premises; ++i) {
-            TRACE("dl", tout << mk_pp(premises[i], m) << "\n";);
-            fmls.push_back(m.get_fact(premises[i]));
-        }
-        SASSERT(m.is_bool(concl));
-        vector<parameter> params;
-        for (unsigned i = 0; i < substs.size(); ++i) {
-            expr_ref_vector const& vec = substs[i];
-            for (unsigned j = 0; j < vec.size(); ++j) {
-                params.push_back(parameter(vec[j]));
-            }
-            if (i + 1 < substs.size()) {
-                params.push_back(parameter(positions[i].first));
-                params.push_back(parameter(positions[i].second));
-            }
-        }
-        ptr_vector<sort> sorts;
-        ptr_vector<expr> args;
-        for (unsigned i = 0; i < num_premises; ++i) {
-            sorts.push_back(m.mk_proof_sort());
-            args.push_back(premises[i]);
-        }
-        sorts.push_back(m.mk_bool_sort());
-        args.push_back(concl);
-        app* result = m.mk_app(m_fid, OP_DL_HYPER_RESOLVE, params.size(), params.c_ptr(), args.size(), args.c_ptr());
-        SASSERT(result->get_family_id() == m_fid);
-        SASSERT(result->get_decl_kind() == OP_DL_HYPER_RESOLVE);
-        return result;
-    }
-
-    bool dl_decl_util::is_hyper_resolve(
-        proof* p, 
-        proof_ref_vector& premises,
-        expr_ref& conclusion,
-        svector<std::pair<unsigned, unsigned> > & positions,
-        vector<expr_ref_vector> & substs) const {
-        if (!is_hyper_resolve(p)) {
-            return false;
-        }
-        unsigned sz = p->get_num_args();
-        SASSERT(sz > 0);
-        for (unsigned i = 0; i + 1 < sz; ++i) {
-            premises.push_back(to_app(p->get_arg(i)));
-        }
-        conclusion = p->get_arg(sz-1);
-        func_decl* d = p->get_decl();
-        unsigned num_p = d->get_num_parameters();
-        parameter const* params = d->get_parameters();
-        
-        substs.push_back(expr_ref_vector(m));
-        for (unsigned i = 0; i < num_p; ++i) {
-            if (params[i].is_int()) {
-                SASSERT(i + 1 < num_p);
-                SASSERT(params[i+1].is_int());
-                unsigned x = static_cast<unsigned>(params[i].get_int());
-                unsigned y = static_cast<unsigned>(params[i+1].get_int());
-                positions.push_back(std::make_pair(x, y));
-                substs.push_back(expr_ref_vector(m));
-                ++i;
-            }
-            else {
-                SASSERT(params[i].is_ast());
-                ast* a = params[i].get_ast();
-                SASSERT(is_expr(a));
-                substs.back().push_back(to_expr(a));                
-            }
-        }
-
-        return true;
-    }
-
 };

lib/dl_decl_plugin.h

@@ -48,7 +48,6 @@ namespace datalog {
         OP_RA_CLONE,
         OP_DL_CONSTANT,
         OP_DL_LT,
-        OP_DL_HYPER_RESOLVE,
         LAST_RA_OP
     };
     
@@ -211,48 +210,6 @@ namespace datalog {
 
         family_id get_family_id() const { return m_fid; }
 
-        /**
-           \brief Hyper-resolution rule that works for Horn clauses (implication)
-           
-           Somewhat related to unit resolution and resolution rule from SPC, but
-           a general sledgehammer rule. 
-           The clause/implication from the first premise is the main clause.
-           One of the literals in each of the other premises is resolved with the main clause.
-           
-           The facts in the premises are closed formulas. Substitutions required for unification
-           are passed in.
-
-           positions is a vector of pairs of positions in the main clause and the side clause.
-
-           For clauses that are disjunctions the positions are indexed from 0 starting with the first
-           literal.
-
-           We use the following (Prolog style) convention for Horn implications:
-           The head of a Horn implication is position 0,
-           the first conjunct in the body of an implication is position 1
-           the second conjunct in the body of an implication is position 2
-
-           For general implications where the head is a disjunction, the
-           first n positions correspond to the n disjuncts in the head.
-           The next m positions correspond to the m conjuncts in the body.
-        */
-        proof* mk_hyper_resolve(unsigned num_premises, proof* const* premises, expr* concl,
-                                svector<std::pair<unsigned, unsigned> > const& positions,
-                                vector<expr_ref_vector> const& substs);
-
-        bool is_hyper_resolve(proof* p) const { return is_app_of(p, m_fid, OP_DL_HYPER_RESOLVE); }
-
-
-        /**
-            \brief extract components of a hyper-resolution proof rule.
-
-        */
-        bool is_hyper_resolve(proof* p, 
-                              proof_ref_vector& premises,
-                              expr_ref& conclusion,
-                              svector<std::pair<unsigned, unsigned> > & positions,
-                              vector<expr_ref_vector>& substs) const;
-
     };
     
 };

lib/dl_mk_rule_inliner.cpp

@@ -735,7 +735,7 @@ namespace datalog {
         }
         m_subst.reset();
         m_subst.reserve_vars(max_var+1);
-        m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), m_head_index.get_approx_num_regs()));
+        m_subst.reserve_offsets(std::max(m_tail_index.get_approx_num_regs(), 2+m_head_index.get_approx_num_regs()));
 
         svector<bool> valid;
         valid.reset();

lib/dl_mk_slice.cpp

@@ -181,7 +181,7 @@ namespace datalog {
             proof_ref_vector premises0(m);
             vector<expr_ref_vector> substs, substs0;
 
-            if (!util.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) {
+            if (!m.is_hyper_resolve(p, premises0, slice_concl, positions, substs0)) {
                 return false;
             }
             unsigned num_args = p->get_num_args();
@@ -240,7 +240,7 @@ namespace datalog {
                 r1 = r3;
             }
             r1->to_formula(concl);
-            proof* new_p = util.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
+            proof* new_p = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), concl, positions, substs);
             m_pinned_exprs.push_back(new_p);
             m_pinned_rules.push_back(r1.get());
             m_sliceform2rule.insert(slice_concl, r1.get());

lib/dl_util.cpp

@@ -634,7 +634,7 @@ namespace datalog {
               tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
               tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";); 
 
-        pr = util.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
+        pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
         pc->insert(pr);
     }
 

lib/pdr_context.cpp

@@ -1093,7 +1093,7 @@ namespace pdr {
                 }
                 expr_ref fml_concl(m);
                 reduced_rule->to_formula(fml_concl);                    
-                p1 = util.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
+                p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
             }
             cache.insert(n->state(), p1);
             rules.insert(n->state(), reduced_rule);

lib/z3_api.h

@@ -761,6 +761,47 @@ typedef enum
          - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.
 
 
+      - Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule.
+
+        The premises of the rules is a sequence of clauses.
+        The first clause argument is the main clause of the rule.
+        One literal from the second, third, .. clause is resolved
+        with a literal from the first (main) clause.
+
+        Premises of the rules are of the form
+        \nicebox{
+                (or l0 l1 l2 .. ln)
+        }
+        or
+        \nicebox{
+             (=> (and ln+1 ln+2 .. ln+m) l0)
+        }
+        or in the most general (ground) form:
+        \nicebox{
+             (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
+        }
+        In other words we use the following (Prolog style) convention for Horn 
+        implications:
+        The head of a Horn implication is position 0,
+        the first conjunct in the body of an implication is position 1
+        the second conjunct in the body of an implication is position 2
+
+        For general implications where the head is a disjunction, the
+        first n positions correspond to the n disjuncts in the head.
+        The next m positions correspond to the m conjuncts in the body.
+
+        The premises can be universally quantified so that the most
+        general non-ground form is:
+
+        \nicebox{
+             (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)))
+        }
+
+        The hyper-resolution rule takes a sequence of parameters.
+        The parameters are substitutions of bound variables separated by pairs
+        of literal positions from the main clause and side clause.
+
+
       - Z3_OP_RA_STORE: Insert a record into a relation.
         The function takes \c n+1 arguments, where the first argument is the relation and the remaining \c n elements 
         correspond to the \c n columns of the relation.
@@ -982,6 +1023,7 @@ typedef enum {
     Z3_OP_PR_SKOLEMIZE,
     Z3_OP_PR_MODUS_PONENS_OEQ, 
     Z3_OP_PR_TH_LEMMA, 
+    Z3_OP_PR_HYPER_RESOLVE,
 
     // Sequences
     Z3_OP_RA_STORE = 0x600,
@@ -5039,7 +5081,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Backtrack one backtracking point.
        
-       \sa Z3_fixedpoing_push
+       \sa Z3_fixedpoint_push
 
        \pre The number of calls to pop cannot exceed calls to push.
     */