tuning and fixing consequence finding, adding dimacs evaluation

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

contrib/cmake/src/test/CMakeLists.txt

@@ -23,6 +23,7 @@ add_executable(test-z3
   bv_simplifier_plugin.cpp
   chashtable.cpp
   check_assumptions.cpp
+  cnf_backbones.cpp
   datalog_parser.cpp
   ddnf.cpp
   diff_logic.cpp

src/sat/sat_solver.cpp

@@ -3284,13 +3284,17 @@ namespace sat {
             checkpoint();
             literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
             unsigned num_resolves = 0;
+            unsigned num_fixed = 0;
+            unsigned num_assigned = 0;
             lbool is_sat = l_true;
             for (; it != end; ++it) {
-                literal lit = *it;
+                literal lit = *it;                
                 if (value(lit) != l_undef) {
+                    ++num_fixed;
                     continue;
                 }
                 push();
+                ++num_assigned;
                 assign(~lit, justification());
                 propagate(false);
                 while (inconsistent()) {
@@ -3307,8 +3311,18 @@ namespace sat {
                     break;
                 }
             }
+            if (scope_lvl() == 1) {
+                it = unfixed_lits.begin();
+                for (; it != end; ++it) {
+                    literal lit = *it;
+                    if (value(lit) == l_true) {
+                        VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
+                    }
+                }
+            }
             if (is_sat == l_true) {
                 if (scope_lvl() == 1 && num_resolves > 0) {
+                    IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
                     is_sat = l_undef;
                 }
                 else {
@@ -3331,6 +3345,8 @@ namespace sat {
                        << " iterations: " << num_iterations
                        << " variables: " << unfixed_lits.size()
                        << " fixed: " << conseq.size()
+                       << " status: " << is_sat 
+                       << " pre-assigned: " << num_fixed                        
                        << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
                        << ")\n";);
 

src/sat/sat_solver.h

@@ -247,6 +247,7 @@ namespace sat {
         unsigned num_clauses() const;
         unsigned num_restarts() const { return m_restarts; }
         bool is_external(bool_var v) const { return m_external[v] != 0; }
+        void set_external(bool_var v) { m_external[v] = true; }
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
         lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }

src/test/cnf_backbones.cpp

@@ -0,0 +1,106 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+--*/
+#include<iostream>
+#include<time.h>
+#include<signal.h>
+#include"timeout.h"
+#include"rlimit.h"
+#include"dimacs.h"
+#include"sat_solver.h"
+#include"gparams.h"
+
+static sat::solver * g_solver = 0;
+static clock_t       g_start_time;
+
+static void display_statistics() {
+    clock_t end_time = clock();
+    if (g_solver) {
+        std::cout.flush();
+        std::cerr.flush();
+        
+        statistics st;
+        g_solver->collect_statistics(st);
+        st.update("total time", ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
+        st.display_smt2(std::cout);
+    }
+}
+
+static void on_timeout() {
+    display_statistics();
+    exit(0);
+}
+
+static void STD_CALL on_ctrl_c(int) {
+    signal (SIGINT, SIG_DFL);
+    display_statistics();
+    raise(SIGINT);
+}
+
+static void display_model(sat::solver const & s) {
+    sat::model const & m = s.get_model();
+    for (unsigned i = 1; i < m.size(); i++) {
+        switch (m[i]) {
+        case l_false: std::cout << "-" << i << " ";  break;
+        case l_undef: break;
+        case l_true: std::cout << i << " ";  break;
+        }
+    }
+    std::cout << "\n";
+}
+
+
+static void cnf_backbones(char const* file_name) {
+    g_start_time = clock();
+    register_on_timeout_proc(on_timeout);
+    signal(SIGINT, on_ctrl_c);
+    params_ref p = gparams::get_module("sat");
+    p.set_bool("produce_models", true);
+    reslimit limit;
+    sat::solver solver(p, limit, 0);
+    g_solver = &solver;
+
+    if (file_name) {
+        std::ifstream in(file_name);
+        if (in.bad() || in.fail()) {
+            std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
+            exit(ERR_OPEN_FILE);
+        }
+        parse_dimacs(in, solver);
+    }
+    else {
+        parse_dimacs(std::cin, solver);
+    }
+    IF_VERBOSE(20, solver.display_status(verbose_stream()););
+    
+    vector<sat::literal_vector> conseq;
+    sat::bool_var_vector vars;
+    sat::literal_vector assumptions;
+    for (unsigned i = 1; i < solver.num_vars(); ++i) {
+        vars.push_back(i);        
+        solver.set_external(i);
+    }
+    lbool r = solver.get_consequences(assumptions, vars, conseq);
+    
+    switch (r) {
+    case l_true: 
+        std::cout << "sat\n"; 
+        std::cout << vars.size() << " " << conseq.size() << "\n";
+        break;
+    case l_undef: 
+        std::cout << "unknown\n"; 
+        break;
+    case l_false: 
+        std::cout << "unsat\n"; 
+        break;
+    }
+    display_statistics();
+}
+
+void tst_cnf_backbones(char ** argv, int argc, int& i) {
+    if (i + 1 < argc) {
+        cnf_backbones(argv[i + 1]);
+        ++i;
+    }
+}

src/test/ddnf.cpp

@@ -1,4 +1,3 @@
-
 /*++
 Copyright (c) 2015 Microsoft Corporation
 

src/test/main.cpp

@@ -229,6 +229,7 @@ int main(int argc, char ** argv) {
     TST(model_evaluator);
     TST(get_consequences);
     TST(pb2bv);
+    TST_ARGV(cnf_backbones);
     //TST_ARGV(hs);
 }