local changes

src/muz_qe/pdr_context.cpp

@@ -1297,6 +1297,45 @@ namespace pdr {
         }
     };
 
+    void context::validate() {
+        if (!m_params.get_bool(":validate-result", false)) {
+            return;
+        }
+        switch(m_last_result) {
+        case l_true: {
+            proof_ref pr = get_proof();
+            proof_checker checker(m);
+            expr_ref_vector side_conditions(m);
+            bool ok = check(pr, side_conditions);
+            if (!ok) {
+                IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
+            }
+            break;
+        }            
+        case l_false: {
+            expr_ref_vector refs(m);
+            model_ref model;
+            vector<relation_info> rs;
+            get_level_property(m_inductive_lvl, refs, rs);    
+            inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
+            ex.to_model(model);
+            decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+            var_subst vs(m, false);
+            for (; it != end; ++it) {
+                ptr_vector<datalog::rule> const& rules = it->m_value->rules();
+                for (unsigned i = 0; i < rules.size(); ++i) {
+                    datalog::rule* rule = rules[i];
+                    // vs(rule->get_head(), 
+                    // apply interpretation of predicates to rule.
+                    // create formula and check for unsat.
+                }
+            }
+            break;
+        }
+        default:
+            break;
+        }
+    }
 
     void context::reset_core_generalizers() {
         std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
@@ -1371,6 +1410,7 @@ namespace pdr {
             check_quantifiers();
             IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););  
             m_last_result = l_true;
+            validate();
             return l_true;
         }
         catch (inductive_exception) {
@@ -1378,6 +1418,7 @@ namespace pdr {
             m_last_result = l_false;
             TRACE("pdr",  display_certificate(tout););      
             IF_VERBOSE(1, display_certificate(verbose_stream()););
+            validate();
             return l_false;
         }
         catch (unknown_exception) {

src/muz_qe/pdr_context.h

@@ -333,6 +333,8 @@ namespace pdr {
 
         void reset_core_generalizers();
 
+        void validate();
+
     public:       
         
         /**

src/muz_qe/pdr_dl_interface.cpp

@@ -206,6 +206,7 @@ void dl_interface::collect_params(param_descrs& p) {
     p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
     p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
     p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
+    p.insert(":validate-result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
     PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
     PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
     PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););