From 83add2bd9bfcd3dab8917b0baf25a75c33f0b343 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Apr 2013 13:39:11 -0700
Subject: [PATCH] fix bugs reported by Filip Konecny <filip.konecny@epfl.ch> in
 PDR

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt_pp.cpp                        |  5 +-
 src/muz_qe/dl_mk_rule_inliner.cpp             | 26 ++++--
 src/muz_qe/dl_mk_rule_inliner.h               |  2 +-
 src/muz_qe/dl_mk_subsumption_checker.cpp      |  6 +-
 src/muz_qe/dl_rule.cpp                        |  8 +-
 src/muz_qe/horn_tactic.cpp                    | 16 ++--
 src/muz_qe/pdr_context.cpp                    | 14 ++-
 src/muz_qe/pdr_context.h                      |  1 +
 src/muz_qe/pdr_util.cpp                       | 30 +++++-
 src/muz_qe/pdr_util.h                         |  2 +
 src/muz_qe/proof_utils.cpp                    | 91 +++++++++++++++++++
 src/muz_qe/proof_utils.h                      |  6 ++
 src/parsers/smt2/smt2parser.cpp               |  2 +-
 src/tactic/portfolio/smt_strategic_solver.cpp |  1 -
 14 files changed, 176 insertions(+), 34 deletions(-)

diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 5819e3930..f684879ae 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -260,6 +260,7 @@ class smt_printer {
         else {
             m_out << sym << "[";
         }
+
         for (unsigned i = 0; i < num_params; ++i) {
             parameter const& p = params[i];
             if (p.is_ast()) {
@@ -642,9 +643,7 @@ class smt_printer {
             m_out << m_var_names[m_num_var_names - idx - 1];
         }
         else {
-            if (!m_is_smt2) {
-                m_out << "?" << idx;
-            }
+            m_out << "?" << idx;
         }
     }
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index 8428d9049..5bbeb2378 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -709,8 +709,7 @@ namespace datalog {
 
 #define PRT(_x_) ((_x_)?"T":"F")
 
-    bool mk_rule_inliner::inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules) {
-        scoped_ptr<rule_set> res = alloc(rule_set, m_context);
+    bool mk_rule_inliner::inline_linear(scoped_ptr<rule_set>& rules) {
         bool done_something = false;        
         unsigned sz = rules->get_num_rules();
 
@@ -731,7 +730,7 @@ namespace datalog {
         svector<bool>& can_expand = m_head_visitor.can_expand();
 
         for (unsigned i = 0; i < sz; ++i) {
-            add_rule(source, acc[i].get(), i);
+            add_rule(*rules, acc[i].get(), i);
         }
 
         // initialize substitution.
@@ -808,7 +807,7 @@ namespace datalog {
                 TRACE("dl", r->display(m_context, tout); r2->display(m_context, tout); rl_res->display(m_context, tout); );
 
                 del_rule(r, i);
-                add_rule(source, rl_res.get(), i);
+                add_rule(*rules, rl_res.get(), i);
                 
 
                 r = rl_res;
@@ -828,13 +827,15 @@ namespace datalog {
             }
         }
         if (done_something) {
-            rules = alloc(rule_set, m_context);
+            scoped_ptr<rule_set> res = alloc(rule_set, m_context);
             for (unsigned i = 0; i < sz; ++i) {
                 if (valid.get(i)) {
-                    rules->add_rule(acc[i].get());
+                    res->add_rule(acc[i].get());
                 }
             }
-            TRACE("dl", rules->display(tout););
+            res->inherit_predicates(*rules);
+            TRACE("dl", res->display(tout););
+            rules = res.detach();
         }        
         return done_something;
     }
@@ -871,11 +872,17 @@ namespace datalog {
             // try eager inlining
             if (do_eager_inlining(res)) {
                 something_done = true;
-            }
+            }            
             TRACE("dl", res->display(tout << "after eager inlining\n"););
+        }    
+        if (something_done) {
+            res->inherit_predicates(source);
+        }
+        else {
+            res = alloc(rule_set, source);
         }
 
-        if (m_context.get_params().inline_linear() && inline_linear(source, res)) {
+        if (m_context.get_params().inline_linear() && inline_linear(res)) {
             something_done = true;
         }
 
@@ -883,7 +890,6 @@ namespace datalog {
             res = 0;
         }
         else {
-            res->inherit_predicates(source);
             m_context.add_model_converter(hsmc.get());
         }
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index 476c6b4b0..3a933f990 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -172,7 +172,7 @@ namespace datalog {
         /**
            Inline predicates that are known to not be join-points.
          */
-        bool inline_linear(rule_set const& source, scoped_ptr<rule_set>& rules);
+        bool inline_linear(scoped_ptr<rule_set>& rules);
 
         void add_rule(rule_set const& rule_set, rule* r, unsigned i);
         void del_rule(rule* r, unsigned i);
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp
index 0e94ba3b9..8c9e7e69f 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.cpp
+++ b/src/muz_qe/dl_mk_subsumption_checker.cpp
@@ -241,6 +241,7 @@ namespace datalog {
             tgt.add_rule(new_rule);
             subs_index.add(new_rule);
         }
+        tgt.inherit_predicates(orig);
         TRACE("dl",
             tout << "original set size: "<<orig.get_num_rules()<<"\n"
                  << "reduced set size: "<<tgt.get_num_rules()<<"\n"; );
@@ -338,7 +339,7 @@ namespace datalog {
         rule_set * res = alloc(rule_set, m_context);
         bool modified = transform_rules(source, *res);
 
-        if(!m_have_new_total_rule && !modified) {
+        if (!m_have_new_total_rule && !modified) {
             dealloc(res);
             return 0;
         }
@@ -347,7 +348,7 @@ namespace datalog {
         //During the construction of the new set we may discover new total relations
         //(by quantifier elimination on the uninterpreted tails).
         SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
-        while(m_have_new_total_rule) {
+        while (m_have_new_total_rule) {
             m_have_new_total_rule = false;
 
             rule_set * old = res;
@@ -355,7 +356,6 @@ namespace datalog {
             transform_rules(*old, *res);
             dealloc(old);
         }
-        res->inherit_predicates(source);
 
         return res;
     }
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 92f504bcc..32f3a5fe8 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -1004,16 +1004,14 @@ namespace datalog {
         }
         svector<symbol> names;
         used_symbols<> us;
-        
-        us(fml);
-        sorts.reverse();
-        
         for (unsigned i = 0; i < sorts.size(); ++i) {
             if (!sorts[i]) {
                 sorts[i] = m.mk_bool_sort();
             }
         }
-
+               
+        us(fml);
+        sorts.reverse();
         for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
             for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
                 func_decl_ref f(m);
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 1a8f562d9..5db4f1a00 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -125,12 +125,13 @@ class horn_tactic : public tactic {
         enum formula_kind { IS_RULE, IS_QUERY, IS_NONE };
 
         formula_kind get_formula_kind(expr_ref& f) {
-            normalize(f);
+            expr_ref tmp(f);
+            normalize(tmp);
             ast_mark mark;
             expr_ref_vector args(m), body(m);
             expr_ref head(m);
             expr* a = 0, *a1 = 0;
-            datalog::flatten_or(f, args);
+            datalog::flatten_or(tmp, args);
             for (unsigned i = 0; i < args.size(); ++i) {
                 a = args[i].get(); 
                 check_predicate(mark, a);
@@ -147,12 +148,12 @@ class horn_tactic : public tactic {
                     body.push_back(m.mk_not(a));
                 }
             }
-            f = m.mk_and(body.size(), body.c_ptr());
             if (head) {
-                f = m.mk_implies(f, head);
+                // f = m.mk_implies(f, head);
                 return IS_RULE;
             }
             else {
+                f = m.mk_and(body.size(), body.c_ptr());
                 return IS_QUERY;
             }
         }
@@ -171,7 +172,7 @@ class horn_tactic : public tactic {
             tactic_report report("horn", *g);
             bool produce_proofs = g->proofs_enabled();
 
-            if (produce_proofs) {
+            if (produce_proofs) {                
                 if (!m_ctx.get_params().generate_proof_trace()) {
                     params_ref params = m_ctx.get_params().p;
                     params.set_bool("generate_proof_trace", true);
@@ -239,10 +240,13 @@ class horn_tactic : public tactic {
             switch (is_reachable) {
             case l_true: {
                 // goal is unsat
-                g->assert_expr(m.mk_false());
                 if (produce_proofs) {
                     proof_ref proof = m_ctx.get_proof();
                     pc = proof2proof_converter(m, proof);
+                    g->assert_expr(m.mk_false(), proof, 0);
+                }
+                else {
+                    g->assert_expr(m.mk_false());
                 }
                 break;    
             }
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index a240a9aef..62b119538 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -43,6 +43,7 @@ Notes:
 #include "ast_ll_pp.h"
 #include "proof_checker.h"
 #include "smt_value_sort.h"
+#include "proof_utils.h"
 
 namespace pdr {
 
@@ -275,7 +276,7 @@ namespace pdr {
                 src.pop_back();
             }
             else if (is_invariant(tgt_level, curr, false, assumes_level)) {
-                
+
                 add_property(curr, assumes_level?tgt_level:infty_level);
                 TRACE("pdr", tout << "is invariant: "<< pp_level(tgt_level) << " " << mk_pp(curr, m) << "\n";);              
                 src[i] = src.back();
@@ -1225,6 +1226,7 @@ namespace pdr {
           m_search(m_params.bfs_model_search()),
           m_last_result(l_undef),
           m_inductive_lvl(0),
+          m_expanded_lvl(0),
           m_cancel(false)
     {
     }
@@ -1680,6 +1682,9 @@ namespace pdr {
         proof = m_search.get_proof_trace(*this);
         TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
         apply(m, m_pc.get(), proof);
+        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        // proof_utils::push_instantiations_up(proof);
+        // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
         return proof;
     }
 
@@ -1711,6 +1716,7 @@ namespace pdr {
         bool reachable;
         while (true) {
             checkpoint();
+            m_expanded_lvl = lvl;
             reachable = check_reachability(lvl);
             if (reachable) {
                 throw model_exception();
@@ -1769,6 +1775,10 @@ namespace pdr {
     void context::expand_node(model_node& n) {
         SASSERT(n.is_open());
         expr_ref_vector cube(m);
+        
+        if (n.level() < m_expanded_lvl) {
+            m_expanded_lvl = n.level();
+        }
 
         if (n.pt().is_reachable(n.state())) {
             TRACE("pdr", tout << "reachable\n";);
@@ -1835,7 +1845,7 @@ namespace pdr {
         if (m_params.simplify_formulas_pre()) {
             simplify_formulas();
         }
-        for (unsigned lvl = 0; lvl <= max_prop_lvl; lvl++) {
+        for (unsigned lvl = m_expanded_lvl; lvl <= max_prop_lvl; lvl++) {
             checkpoint();
             bool all_propagated = true;
             decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 6aa02ef10..b5652d1b6 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -303,6 +303,7 @@ namespace pdr {
         mutable model_search m_search;
         lbool                m_last_result;
         unsigned             m_inductive_lvl;
+        unsigned             m_expanded_lvl;
         ptr_vector<core_generalizer>  m_core_generalizers;
         stats                m_stats;
         volatile bool        m_cancel;
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 237cf9415..62185f1d2 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -1081,6 +1081,7 @@ namespace pdr {
         arith_util a;
         bv_util    bv;
         bool m_is_dl;
+        bool m_test_for_utvpi;
 
         bool is_numeric(expr* e) const {
             if (a.is_numeral(e)) {
@@ -1115,6 +1116,16 @@ namespace pdr {
                 }
                 return false;
             }
+            if (m_test_for_utvpi) {
+                if (a.is_mul(e, e1, e2)) {
+                    if (is_minus_one(e1)) {
+                        return is_offset(e2);
+                    }
+                    if (is_minus_one(e2)) {
+                        return is_offset(e1);
+                    }
+                }
+            }
             return !is_arith_expr(e);
         }
 
@@ -1140,6 +1151,9 @@ namespace pdr {
             if (!a.is_add(lhs, arg1, arg2)) 
                 return false;    
             // x
+            if (m_test_for_utvpi) {
+                return is_offset(arg1) && is_offset(arg2);
+            }
             if (is_arith_expr(arg1)) 
                 std::swap(arg1, arg2);
             if (is_arith_expr(arg1))
@@ -1209,8 +1223,10 @@ namespace pdr {
         }
 
     public:
-        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true) {}
-        
+        test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
+       
+        void test_for_utvpi() { m_test_for_utvpi = true; }
+
         void operator()(expr* e) {
             if (!m_is_dl) {
                 return;
@@ -1248,6 +1264,16 @@ namespace pdr {
         return test.is_dl();
     }  
 
+    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
+        test_diff_logic test(m);
+        test.test_for_utvpi();
+        expr_fast_mark1 mark;
+        for (unsigned i = 0; i < num_fmls; ++i) {
+            quick_for_each_expr(test, mark, fmls[i]);
+        } 
+        return test.is_dl();
+    }  
+
 }
 
 template class rewriter_tpl<pdr::ite_hoister_cfg>;
diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h
index ddbf0d122..5f2d22b76 100644
--- a/src/muz_qe/pdr_util.h
+++ b/src/muz_qe/pdr_util.h
@@ -151,6 +151,8 @@ namespace pdr {
 
     bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
 
+    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
+
 }
 
 #endif
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index 369c3aae6..36e721b5c 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -1,6 +1,7 @@
 #include "dl_util.h"
 #include "proof_utils.h"
 #include "ast_smt2_pp.h"
+#include "var_subst.h"
 
 class reduce_hypotheses {
     typedef obj_hashtable<expr> expr_set;
@@ -517,3 +518,93 @@ void proof_utils::permute_unit_resolution(proof_ref& pr) {
     obj_map<proof,proof*> cache;
     ::permute_unit_resolution(refs, cache, pr);
 }
+
+class push_instantiations_up_cl {
+    ast_manager& m;
+public:
+    push_instantiations_up_cl(ast_manager& m): m(m) {}
+
+    void operator()(proof_ref& p) {
+        expr_ref_vector s0(m);
+        p = push(p, s0);
+    }
+
+private:
+
+    proof* push(proof* p, expr_ref_vector const& sub) {
+        proof_ref_vector premises(m);
+        expr_ref conclusion(m);
+        svector<std::pair<unsigned, unsigned> >  positions;
+        vector<expr_ref_vector> substs;
+
+        if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
+            for (unsigned i = 0; i < premises.size(); ++i) {
+                compose(substs[i], sub);
+                premises[i] = push(premises[i].get(), substs[i]);
+                substs[i].reset();
+            }
+            instantiate(sub, conclusion);
+            return 
+                m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, 
+                                   positions, 
+                                   substs);
+        }        
+        if (sub.empty()) {
+            return p;
+        }
+        if (m.is_modus_ponens(p)) {
+            SASSERT(m.get_num_parents(p) == 2);
+            proof* p0 = m.get_parent(p, 0);
+            proof* p1 = m.get_parent(p, 1);
+            if (m.get_fact(p0) == m.get_fact(p)) {
+                return push(p0, sub);
+            }
+            expr* e1, *e2;
+            if (m.is_rewrite(p1, e1, e2) && 
+                is_quantifier(e1) && is_quantifier(e2) &&
+                to_quantifier(e1)->get_num_decls() == to_quantifier(e2)->get_num_decls()) {
+                expr_ref r1(e1,m), r2(e2,m);
+                instantiate(sub, r1);
+                instantiate(sub, r2);
+                p1 = m.mk_rewrite(r1, r2);
+                return m.mk_modus_ponens(push(p0, sub), p1);
+            }
+        }
+        premises.push_back(p);
+        substs.push_back(sub);
+        conclusion = m.get_fact(p);
+        instantiate(sub, conclusion);
+        return m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
+    }
+
+    void compose(expr_ref_vector& sub, expr_ref_vector const& s0) {
+        for (unsigned i = 0; i < sub.size(); ++i) {
+            expr_ref e(m);
+            var_subst(m, false)(sub[i].get(), s0.size(), s0.c_ptr(), e);
+            sub[i] = e;            
+        }
+    }
+
+    void instantiate(expr_ref_vector const& sub, expr_ref& fml) {
+        if (sub.empty()) {
+            return;
+        }
+        if (!is_forall(fml)) {
+            return;
+        }
+        quantifier* q = to_quantifier(fml);
+        if (q->get_num_decls() != sub.size()) {
+            TRACE("proof_utils", tout << "quantifier has different number of variables than substitution";
+                  tout << mk_pp(q, m) << "\n";
+                  tout << sub.size() << "\n";);
+            return;
+        }
+        var_subst(m, false)(q->get_expr(), sub.size(), sub.c_ptr(), fml);
+    }
+
+};
+
+void proof_utils::push_instantiations_up(proof_ref& pr) {
+    push_instantiations_up_cl push(pr.get_manager());
+    push(pr);
+}
diff --git a/src/muz_qe/proof_utils.h b/src/muz_qe/proof_utils.h
index 53a38592e..dc3cdc3ef 100644
--- a/src/muz_qe/proof_utils.h
+++ b/src/muz_qe/proof_utils.h
@@ -36,6 +36,12 @@ public:
     */
     static void permute_unit_resolution(proof_ref& pr);
 
+    /**
+       \brief Push instantiations created in hyper-resolutions up to leaves.
+       This produces a "ground" proof where leaves are annotated by instantiations.
+    */
+    static void push_instantiations_up(proof_ref& pr);
+
 };
 
 #endif
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 0698f4eaf..b5af6353e 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1159,7 +1159,7 @@ namespace smt2 {
             m_num_expr_frames++;
             unsigned num_vars = parse_sorted_vars();
             if (num_vars == 0)
-                throw parser_exception("invalied quantifier, list of sorted variables is empty");
+                throw parser_exception("invalid quantifier, list of sorted variables is empty");
         }
 
         symbol parse_indexed_identifier_core() {
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 55512f677..ae79446e3 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -94,7 +94,6 @@ public:
     smt_strategic_solver_factory(symbol const & logic):m_logic(logic) {}
     
     virtual ~smt_strategic_solver_factory() {}
-    
     virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) {
         symbol l;
         if (m_logic != symbol::null)