add feature to display benchmark in format seen by SAT solver

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

src/cmd_context/cmd_context.cpp

@@ -1545,6 +1545,20 @@ void cmd_context::reset_assertions() {
 }
 
 
+void cmd_context::display_dimacs() {
+    if (m_solver) {
+        try {
+            gparams::set("sat.dimacs.display", "true");
+            m_solver->check_sat(0, nullptr);
+        }
+        catch (...) {
+            gparams::set("sat.dimacs.display", "false");        
+            throw;
+        }
+        gparams::set("sat.dimacs.display", "false");        
+    }
+}
+
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
         model_params p;

src/cmd_context/cmd_context.h

@@ -419,6 +419,7 @@ public:
 
     void display_assertions();
     void display_statistics(bool show_total_time = false, double total_time = 0.0);
+    void display_dimacs();
     void reset(bool finalize = false);
     void assert_expr(expr * t);
     void assert_expr(symbol const & name, expr * t);

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -31,7 +31,6 @@ Notes:
 #include "ast/rewriter/var_subst.h"
 #include "util/gparams.h"
 
-#ifndef _EXTERNAL_RELEASE
 
 BINARY_SYM_CMD(get_quantifier_body_cmd,
                "dbg-get-qbody",
@@ -343,10 +342,19 @@ public:
     }
 };
 
-#endif
+class print_dimacs_cmd : public cmd {
+public:
+    print_dimacs_cmd():cmd("display-dimacs") {}
+    virtual char const * get_usage() const { return ""; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "print benchmark in DIMACS format"; }
+    virtual unsigned get_arity() const { return 0; }
+    virtual void prepare(cmd_context & ctx) {}
+    virtual void execute(cmd_context & ctx) { ctx.display_dimacs(); }
+};
+
 
 void install_dbg_cmds(cmd_context & ctx) {
-#ifndef _EXTERNAL_RELEASE
+    ctx.insert(alloc(print_dimacs_cmd));
     ctx.insert(alloc(get_quantifier_body_cmd));
     ctx.insert(alloc(set_cmd));
     ctx.insert(alloc(pp_var_cmd));
@@ -369,5 +377,4 @@ void install_dbg_cmds(cmd_context & ctx) {
     ctx.insert(alloc(instantiate_cmd));
     ctx.insert(alloc(instantiate_nested_cmd));
     ctx.insert(alloc(set_next_id));
-#endif
 }

src/sat/sat_config.cpp

@@ -35,7 +35,7 @@ namespace sat {
         m_glue("glue"),
         m_glue_psm("glue_psm"),
         m_psm_glue("psm_glue") {
-        m_num_parallel = 1;
+        m_num_parallel = 1;        
         updt_params(p); 
     }
 
@@ -114,6 +114,7 @@ namespace sat {
         m_core_minimize   = p.core_minimize();
         m_core_minimize_partial   = p.core_minimize_partial();
         m_dyn_sub_res     = p.dyn_sub_res();
+        m_dimacs_display  = p.dimacs_display();
     }
 
     void config::collect_param_descrs(param_descrs & r) {

src/sat/sat_config.h

@@ -74,6 +74,7 @@ namespace sat {
         bool               m_core_minimize;
         bool               m_core_minimize_partial;
 
+        bool               m_dimacs_display;
 
         symbol             m_always_true;
         symbol             m_always_false;

src/sat/sat_params.pyg

@@ -23,4 +23,5 @@ def_module_params('sat',
                           ('core.minimize', BOOL, False, 'minimize computed core'),
                           ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('parallel_threads', UINT, 1, 'number of parallel threads to use'),
-                          ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))
+                          ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
+                          ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving')))

src/sat/sat_solver.cpp

@@ -724,6 +724,13 @@ namespace sat {
         pop_to_base_level();
         IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
         SASSERT(scope_lvl() == 0);
+        if (m_config.m_dimacs_display) {
+            display_dimacs(std::cout);
+            for (unsigned i = 0; i < num_lits; ++lits) {
+                std::cout << dimacs_lit(lits[i]) << " 0\n";
+            }
+            return l_undef;
+        }
         if (m_config.m_num_parallel > 1 && !m_par) {
             return check_par(num_lits, lits);
         }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -105,7 +105,6 @@ public:
 
     virtual void set_progress_callback(progress_callback * callback) {}
 
-
     void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
         if (weights != 0) {
             for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);

src/tactic/portfolio/enum2bv_solver.cpp

@@ -97,7 +97,6 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
-    
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         datatype_util dt(m);
         bv_util bv(m);