fix for unsound results reported in #313

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

src/ast/ast_util.cpp

@@ -166,6 +166,11 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
         return m.mk_and(num_args, args);
 }
 
+app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
+    return to_app(mk_and(m, num_args, (expr* const*) args));
+}
+
+
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
     if (num_args == 0)
         return m.mk_false();
@@ -175,6 +180,10 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
         return m.mk_or(num_args, args);
 }
 
+app* mk_or(ast_manager & m, unsigned num_args, app * const * args) {
+    return to_app(mk_or(m, num_args, (expr* const*) args));
+}
+
 expr * mk_not(ast_manager & m, expr * arg) {
     expr * atom;
     if (m.is_not(arg, atom))

src/ast/ast_util.h

@@ -107,6 +107,9 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
    Return true                               if num_args == 0
  */
 expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
+app  * mk_and(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
 
 /**
    Return (or args[0] ... args[num_args-1]) if num_args >= 2
@@ -114,6 +117,10 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
    Return false                             if num_args == 0
  */
 expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
+app  * mk_or(ast_manager & m, unsigned num_args, app * const * args);
+inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
+
 
 /**
    Return a          if arg = (not a)

src/muz/pdr/pdr_context.cpp

@@ -50,6 +50,7 @@ Notes:
 #include "blast_term_ite_tactic.h"
 #include "model_implicant.h"
 #include "expr_safe_replace.h"
+#include "ast_util.h"
 
 namespace pdr {
 
@@ -448,6 +449,7 @@ namespace pdr {
         else if (is_sat == l_false) {
             uses_level = m_solver.assumes_level();
         }
+        m_solver.set_model(0);
         return is_sat;
     }
 
@@ -481,6 +483,7 @@ namespace pdr {
         prop_solver::scoped_level _sl(m_solver, level);
         m_solver.set_core(&core);
         m_solver.set_subset_based_core(true);
+        m_solver.set_model(0);
         lbool res = m_solver.check_assumptions_and_formula(lits, fml);
         if (res == l_false) {
             lits.reset();
@@ -775,6 +778,13 @@ namespace pdr {
         }
         // only initial states are not set by the PDR search.
         SASSERT(m_model.get());
+        if (!m_model.get()) {
+            std::stringstream msg;
+            msg << "no model for node " << state();
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }
+
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -793,15 +803,23 @@ namespace pdr {
             }
         }
         SASSERT(!tags.empty());
-        ini_tags = m.mk_or(tags.size(), tags.c_ptr());
+        ini_tags = ::mk_or(tags);
         ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
         model_ref mdl;
         pt().get_solver().set_model(&mdl);
-        TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
+        TRACE("pdr", tout << ini_state << "\n";);
-        VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
+        if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) {
+            std::stringstream msg;
+            msg << "Unsatisfiable initial state: " << ini_state << "\n";
+            display(msg, 2);
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }
+        SASSERT(mdl.get());
         datalog::rule const& rl2 = pt().find_rule(*mdl);
         SASSERT(is_ini(rl2));
         set_rule(&rl2);
+        pt().get_solver().set_model(0);
         return const_cast<datalog::rule*>(m_rule);                        
     }
 
@@ -830,7 +848,7 @@ namespace pdr {
         }
         r0 = get_rule();
         app_ref_vector& inst = pt().get_inst(r0);
-        TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
+        TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";);
         for (unsigned i = 0; i < inst.size(); ++i) {
             expr* v;
             if (model.find(inst[i].get(), v)) {
@@ -852,7 +870,7 @@ namespace pdr {
         for (unsigned i = 0; i < indent; ++i) out << " ";
         out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n";
         for (unsigned i = 0; i < indent; ++i) out << " ";
-        out << "  " << mk_pp(m_state, m_state.get_manager(), indent) << "\n";
+        out << "  " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n";
         for (unsigned i = 0; i < children().size(); ++i) {
             children()[i]->display(out, indent + 1);
         }
@@ -925,17 +943,6 @@ namespace pdr {
         }
     }
 
-    bool model_search::is_repeated(model_node& n) const {
-        model_node* p = n.parent();
-        while (p) {
-            if (p->state() == n.state()) {
-                TRACE("pdr", tout << n.state() << "repeated\n";);
-                return true;
-            }
-            p = p->parent();
-        }
-        return false;
-    }
 
     void model_search::add_leaf(model_node& n) {
         SASSERT(n.children().empty());
@@ -1012,11 +1019,11 @@ namespace pdr {
         nodes.erase(&n);
         bool is_goal = n.is_goal();
         remove_goal(n);
-        if (!nodes.empty() && is_goal && backtrack) {
+        // TBD: siblings would also fail if n is not a goal.
+        if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) {
             TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2););
             model_node* n1 = nodes[0];
             n1->set_open();            
-            SASSERT(n1->children().empty());
             enqueue_leaf(n1);
         }
 
@@ -1702,7 +1709,15 @@ namespace pdr {
 
     void context::validate_search() {
         expr_ref tr = m_search.get_trace(*this);
-        // TBD: tr << "\n";
+        smt::kernel solver(m, get_fparams());
+        solver.assert_expr(tr);
+        lbool res = solver.check();
+        if (res != l_true) {
+            std::stringstream msg;
+            msg << "rule validation failed when checking: " << tr;
+            IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
+            throw default_exception(msg.str());
+        }                                
     }
 
     void context::validate_model() {
@@ -1938,11 +1953,11 @@ namespace pdr {
         proof_ref proof(m);
         SASSERT(m_last_result == l_true);
         proof = m_search.get_proof_trace(*this);
-        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
         apply(m, m_pc.get(), proof);
-        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
+        TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
         // proof_utils::push_instantiations_up(proof);
-        // TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
+        // TRACE("pdr", tout << "PDR up: " << proof << "\n";);
         return proof;
     }
 

src/muz/pdr/pdr_context.h

@@ -268,7 +268,6 @@ namespace pdr {
         void enqueue_leaf(model_node* n); // add leaf to priority queue.
         void update_models();
         void set_leaf(model_node& n); // Set node as leaf, remove children.
-        bool is_repeated(model_node& n) const;
         unsigned num_goals() const; 
 
     public: