print certificate for #2202, enable CTL-C for API fix #2203

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

src/api/api_datalog.cpp

@@ -24,6 +24,7 @@ Revision History:
 #include "api/api_stats.h"
 #include "muz/fp/datalog_parser.h"
 #include "util/cancel_eh.h"
+#include "util/scoped_ctrl_c.h"
 #include "util/scoped_timer.h"
 #include "muz/fp/dl_cmds.h"
 #include "cmd_context/cmd_context.h"
@@ -280,11 +281,13 @@ extern "C" {
         lbool r = l_undef;
         unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit  = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_fixedpoint(d)->m_params.get_bool("ctrl_c", true);
         {
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             cancel_eh<reslimit> eh(mk_c(c)->m().limit());
             api::context::set_interruptable si(*(mk_c(c)), eh);        
             scoped_timer timer(timeout, &eh);
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             try {
                 r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
             }

src/api/api_opt.cpp

@@ -18,6 +18,7 @@ Revision History:
 #include<iostream>
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
+#include "util/scoped_ctrl_c.h"
 #include "util/file_path.h"
 #include "parsers/smt2/smt2parser.h"
 #include "opt/opt_context.h"
@@ -148,8 +149,10 @@ extern "C" {
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit = to_optimize_ptr(o)->get_params().get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true);
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {

src/api/api_solver.cpp

@@ -31,9 +31,6 @@ Revision History:
 #include "api/api_stats.h"
 #include "api/api_ast_vector.h"
 #include "solver/tactic2solver.h"
-#include "util/scoped_ctrl_c.h"
-#include "util/cancel_eh.h"
-#include "util/scoped_timer.h"
 #include "util/file_path.h"
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
@@ -465,7 +462,7 @@ extern "C" {
         expr * const * _assumptions = to_exprs(assumptions);
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
-        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", true);
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         api::context::set_interruptable si(*(mk_c(c)), eh);
         lbool result;
@@ -656,7 +653,7 @@ extern "C" {
         lbool result = l_undef;
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
-        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", true);
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {
@@ -698,7 +695,7 @@ extern "C" {
         }
         unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
         unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
-        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", true);
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {

src/muz/base/dl_context.cpp

@@ -730,6 +730,7 @@ namespace datalog {
     void context::collect_params(param_descrs& p) {
         fp_params::collect_param_descrs(p);
         insert_timeout(p);
+        insert_ctrl_c(p);
     }
 
     void context::updt_params(params_ref const& p) {
@@ -854,7 +855,11 @@ namespace datalog {
             UNREACHABLE();
         }
         ensure_engine();
-        return m_engine->query(query);
+        lbool r = m_engine->query(query);
+        if (r != l_undef && get_params().print_certificate()) {
+            display_certificate(std::cout) << "\n";
+        }
+        return r;
     }
 
     lbool context::query_from_lvl (expr* query, unsigned lvl) {
@@ -951,9 +956,10 @@ namespace datalog {
         }
     }
 
-    void context::display_certificate(std::ostream& out) {
+    std::ostream& context::display_certificate(std::ostream& out) {
         ensure_engine();
         m_engine->display_certificate(out);
+        return out;
     }
 
     void context::display(std::ostream & out) const {

src/muz/base/dl_context.h

@@ -581,7 +581,7 @@ namespace datalog {
         /**
            \brief Display a certificate for reachability and/or unreachability.
         */
-        void display_certificate(std::ostream& out);
+        std::ostream& display_certificate(std::ostream& out);
 
         /**
            \brief query result if it contains fact.

src/opt/opt_context.cpp

@@ -1487,6 +1487,8 @@ namespace opt {
 
     void context::collect_param_descrs(param_descrs & r) {
         opt_params::collect_param_descrs(r);
+        insert_timeout(r);
+        insert_ctrl_c(r);
     }
     
     void context::updt_params(params_ref const& p) {

src/sat/sat_model_converter.cpp

@@ -144,20 +144,30 @@ namespace sat {
             DEBUG_CODE({
                 // all clauses must be satisfied
                 bool sat = false;
-                for (literal l : it->m_clauses) {
+                bool undef = false;
+                for (literal const& l : it->m_clauses) {
                     if (l == null_literal) {
                         CTRACE("sat", !sat, 
+                               if (m_solver) m_solver->display(tout);
                                display(tout);
                                for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n";
+                               for (literal const& l2 : it->m_clauses) {
+                                   if (l2 == null_literal) tout << "\n"; else tout << l2 << " ";
+                                   if (&l == &l2) break;
+                               }
                                );
-                        SASSERT(sat);
+                        SASSERT(sat || undef);
                         sat = false;
+                        undef = false;
                         continue;
                     }
                     if (sat)
                         continue;
-                    if (value_at(l, m) == l_true)
+                    switch (value_at(l, m)) {
-                        sat = true;
+                    case l_undef: undef = true; break;
+                    case l_true: sat = true; break;
+                    default: break;
+                    }
                 }
             });
         }

src/solver/solver.cpp

@@ -223,9 +223,6 @@ void solver::assert_expr(expr* f, expr* t) {
     assert_expr_core2(fml, a);    
 }
 
-static void insert_ctrl_c(param_descrs & r) {
-    r.insert("ctrl_c", CPK_BOOL, "enable interrupts from ctrl-c", "false");
-}
 
 
 void solver::collect_param_descrs(param_descrs & r) {

src/util/params.cpp

@@ -305,6 +305,9 @@ void insert_rlimit(param_descrs & r) {
     r.insert("rlimit", CPK_UINT, "default resource limit used for solvers. Unrestricted when set to 0.", "0");
 }
 
+void insert_ctrl_c(param_descrs & r) {
+    r.insert("ctrl_c", CPK_BOOL, "enable interrupts from ctrl-c", "true");
+}
 
 class params {
     friend class params_ref;

src/util/params.h

@@ -140,5 +140,6 @@ void insert_produce_models(param_descrs & r);
 void insert_produce_proofs(param_descrs & r);
 void insert_timeout(param_descrs & r);
 void insert_rlimit(param_descrs & r);
+void insert_ctrl_c(param_descrs & r);
 
 #endif