better proof mining for Farkas

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

lib/ast.cpp

@@ -1370,10 +1370,11 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
           decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();            
           register_plugin(fid, new_p);
           SASSERT(new_p->get_family_id() == fid);
+          SASSERT(has_plugin(fid));
       }
       SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
       SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
-      SASSERT(from.has_plugin(fid) == has_plugin(fid));      
+      SASSERT(!from.has_plugin(fid) || has_plugin(fid));      
     }
 }
 

lib/pdr_context.cpp

@@ -1354,16 +1354,18 @@ namespace pdr {
             m_core_generalizers.push_back(alloc(core_multi_generalizer, *this));
         }
         if (m_params.get_bool(":use-farkas", true) && !is_bool(rules)) {
-            // TBD: 
+            if (m_params.get_bool(":use-proofs", true)) {
-            m.toggle_proof_mode(PGM_FINE);
+                m.toggle_proof_mode(PGM_FINE);
-            m_fparams.m_proof_mode = PGM_FINE;
+                m_fparams.m_proof_mode = PGM_FINE;
-            m_fparams.m_arith_bound_prop = BP_NONE;
+                m_fparams.m_arith_bound_prop = BP_NONE;
-            m_fparams.m_arith_auto_config_simplex = true;
+                m_fparams.m_arith_auto_config_simplex = true;
-            m_fparams.m_arith_propagate_eqs = false;
+                m_fparams.m_arith_propagate_eqs = false;
-            m_fparams.m_arith_eager_eq_axioms = false;
+                m_fparams.m_arith_eager_eq_axioms = false;
-            m_fparams.m_arith_eq_bounds = false;
+                m_fparams.m_arith_eq_bounds = false;
-
+            }
-            // m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
+            else {
+                m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
+            }
         }
         if (m_params.get_bool(":use-farkas-properties", false)) {
             m_core_generalizers.push_back(alloc(core_farkas_properties_generalizer, *this));

lib/pdr_farkas_learner.cpp

@@ -512,12 +512,10 @@ namespace pdr {
             for_each_expr(collect_proc, *it);
         }
 
-        proof_ref tmp(root, m);
-        proof_utils::reduce_hypotheses(tmp);
-        IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(tmp, m) << "\n";);
-
         proof_ref pr(root, m);
-        permute_unit_resolution(pr);
+        proof_utils::reduce_hypotheses(pr);
+        IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";);
+        proof_utils::permute_unit_resolution(pr);
         
         ptr_vector<expr_set> hyprefs;
         obj_map<expr, expr_set*> hypmap;
@@ -751,94 +749,6 @@ namespace pdr {
         }
     }
 
-    // permute unit resolution over Theory lemmas to track premises.
-    void farkas_learner::permute_unit_resolution(proof_ref& pr) {
-        expr_ref_vector refs(pr.get_manager());
-        obj_map<proof,proof*> cache;
-        permute_unit_resolution(refs, cache, pr);
-    }
-
-    void farkas_learner::permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
-        ast_manager& m = pr.get_manager();
-        proof* pr2 = 0;
-        proof_ref_vector parents(m);
-        proof_ref prNew(pr); 
-        if (cache.find(pr, pr2)) {
-            pr = pr2;
-            return;
-        }
-
-        for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
-            prNew = m.get_parent(pr, i);
-            permute_unit_resolution(refs, cache, prNew);
-            parents.push_back(prNew);
-        }
-
-        prNew = pr;
-        if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
-            parents[0]->get_decl_kind() == PR_TH_LEMMA) { 
-                /*
-                Unit resolution:
-                    T1:      (or l_1 ... l_n l_1' ... l_m')
-                    T2:      (not l_1)
-                    ...
-                    T(n+1):  (not l_n)
-                    [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
-                Th lemma:
-                    T1:      (not l_1)
-                    ...
-                    Tn:      (not l_n)
-                    [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
-
-                    Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
-
-                Implement conversion:
-
-                    T1 |- not l_1 ... Tn |- not l_n  
-                    -------------------------------  TH_LEMMA
-                           (or k_1 .. k_m j_1 ... j_m)    S1 |- not k_1 ... Sm |- not k_m
-                           -------------------------------------------------------------- UNIT_RESOLUTION
-                                         (or j_1 .. j_m)
-
-
-                    |-> 
-
-                    T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
-                    ---------------------------------------------------------------- TH_LEMMA
-                                        (or j_1 .. j_m)
-
-                */
-                proof_ref_vector premises(m);
-                proof* thLemma = parents[0].get();
-                for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
-                    premises.push_back(m.get_parent(thLemma, i));
-                }
-                for (unsigned i = 1; i < parents.size(); ++i) {
-                    premises.push_back(parents[i].get());
-                }
-                parameter const* params = thLemma->get_decl()->get_parameters();
-                unsigned num_params = thLemma->get_decl()->get_num_parameters();
-                SASSERT(params[0].is_symbol());
-                family_id tid = m.get_family_id(params[0].get_symbol());
-                SASSERT(tid != null_family_id);
-                prNew = m.mk_th_lemma(tid, m.get_fact(pr), 
-                                      premises.size(), premises.c_ptr(), num_params-1, params+1);
-        }
-        else {
-            ptr_vector<expr> args;
-            for (unsigned i = 0; i < parents.size(); ++i) {
-                args.push_back(parents[i].get());
-            }
-            if (m.has_fact(pr)) {
-                args.push_back(m.get_fact(pr));
-            }
-            prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
-        }    
-      
-        cache.insert(pr, prNew);
-        refs.push_back(prNew);
-        pr = prNew;
-    }	
 
     bool farkas_learner::is_farkas_lemma(ast_manager& m, expr* e) {
         app * a;

lib/pdr_farkas_learner.h

@@ -69,10 +69,6 @@ class farkas_learner {
    
     void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, expr_ref_vector& lemmas);
 
-    void permute_unit_resolution(proof_ref& pr);
-
-    void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr);
-
     bool is_pure_expr(func_decl_set const& symbs, expr* e) const;
 
     static void test();

lib/proof_utils.cpp

@@ -196,19 +196,18 @@ public:
             }
             m_hypmap.insert(result, new_hyps);
             m_hyprefs.push_back(new_hyps);
-            TRACE("proof_utils",
+            TRACE("proof_utils",            
-            {
                     tout << "New lemma: " << mk_pp(m.get_fact(p), m) 
                       << "\n==>\n" 
                       << mk_pp(m.get_fact(result), m) << "\n";
                 if (hyps) {
-                    expr_set::iterator it = hyps->begin(), end = hyps->end();
+                    expr_set::iterator it = hyps->begin();
+                    expr_set::iterator end = hyps->end();
                     for (; it != end; ++it) {
                         tout << "Hypothesis: " << mk_pp(*it, m) << "\n";
                     }
-                }
+                });                               
-            });
+            
-            }
             break;
         }
         case PR_UNIT_RESOLUTION: {
@@ -387,3 +386,94 @@ bool proof_utils::is_closed(ast_manager& m, proof* p) {
     proof_is_closed checker(m);
     return checker(p);
 }
+
+
+static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
+    ast_manager& m = pr.get_manager();
+    proof* pr2 = 0;
+    proof_ref_vector parents(m);
+    proof_ref prNew(pr); 
+    if (cache.find(pr, pr2)) {
+        pr = pr2;
+        return;
+    }
+    
+    for (unsigned i = 0; i < m.get_num_parents(pr); ++i) {
+        prNew = m.get_parent(pr, i);
+        permute_unit_resolution(refs, cache, prNew);
+        parents.push_back(prNew);
+    }
+    
+    prNew = pr;
+    if (pr->get_decl_kind() == PR_UNIT_RESOLUTION &&
+        parents[0]->get_decl_kind() == PR_TH_LEMMA) { 
+        /*
+          Unit resolution:
+          T1:      (or l_1 ... l_n l_1' ... l_m')
+          T2:      (not l_1)
+          ...
+          T(n+1):  (not l_n)
+                   [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')
+          Th lemma:
+          T1:      (not l_1)
+          ...
+          Tn:      (not l_n)
+          [th-lemma T1 ... Tn]: (or l_{n+1} ... l_m)
+                    
+          Such that (or l_1 .. l_n l_{n+1} .. l_m) is a theory axiom.
+                    
+          Implement conversion:
+                    
+                 T1 |- not l_1 ... Tn |- not l_n  
+                 -------------------------------  TH_LEMMA
+                          (or k_1 .. k_m j_1 ... j_m)    S1 |- not k_1 ... Sm |- not k_m
+                          -------------------------------------------------------------- UNIT_RESOLUTION
+                                        (or j_1 .. j_m)
+
+
+            |-> 
+
+                    T1 |- not l_1 ... Tn |- not l_n S1 |- not k_1 ... Sm |- not k_m
+                    ---------------------------------------------------------------- TH_LEMMA
+                                        (or j_1 .. j_m)
+
+        */
+        proof_ref_vector premises(m);
+        proof* thLemma = parents[0].get();
+        for (unsigned i = 0; i < m.get_num_parents(thLemma); ++i) {
+            premises.push_back(m.get_parent(thLemma, i));
+        }
+        for (unsigned i = 1; i < parents.size(); ++i) {
+            premises.push_back(parents[i].get());
+        }
+        parameter const* params = thLemma->get_decl()->get_parameters();
+        unsigned num_params = thLemma->get_decl()->get_num_parameters();
+        SASSERT(params[0].is_symbol());
+        family_id tid = m.get_family_id(params[0].get_symbol());
+        SASSERT(tid != null_family_id);
+        prNew = m.mk_th_lemma(tid, m.get_fact(pr), 
+                              premises.size(), premises.c_ptr(), num_params-1, params+1);
+    }
+    else {
+        ptr_vector<expr> args;
+        for (unsigned i = 0; i < parents.size(); ++i) {
+            args.push_back(parents[i].get());
+        }
+        if (m.has_fact(pr)) {
+            args.push_back(m.get_fact(pr));
+        }
+        prNew = m.mk_app(pr->get_decl(), args.size(), args.c_ptr());
+    }    
+    
+    cache.insert(pr, prNew);
+    refs.push_back(prNew);
+    pr = prNew;
+}	
+
+
+// permute unit resolution over Theory lemmas to track premises.
+void proof_utils::permute_unit_resolution(proof_ref& pr) {
+    expr_ref_vector refs(pr.get_manager());
+    obj_map<proof,proof*> cache;
+    ::permute_unit_resolution(refs, cache, pr);
+}

lib/proof_utils.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Utilities for proofs.
+    Utilities for transforming proofs.
 
 Author:
 
@@ -31,6 +31,11 @@ public:
     */
     static bool is_closed(ast_manager& m, proof* p);
 
+    /**
+       \brief Permute unit resolution rule with th-lemma
+    */
+    static void permute_unit_resolution(proof_ref& pr);
+
 };
 
 #endif _PROOF_UTILS_H_