Merge branch 'upstream-master' into develop

Conflicts:
	src/ast/rewriter/seq_rewriter.cpp
	src/ast/seq_decl_plugin.h

src/api/z3_api.h

@@ -1500,7 +1500,7 @@ extern "C" {
        All main interaction with Z3 happens in the context of a \c Z3_context.
 
        In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
-       are determined by the scope level of #Z3_push and #Z3_pop.
+       are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
        In other words, a Z3_ast object remains valid until there is a
        call to Z3_pop that takes the current scope below the level where
        the object was created.
@@ -3091,8 +3091,8 @@ extern "C" {
        \brief Create a numeral of a given sort.
 
        \param c logical context.
-       \param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}.
-                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
+       \param numeral A string representing the numeral value in decimal notation. The string may be of the form `[num]*[.[num]*][E[+|-][num]+]`.
+                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form `[num]* / [num]*` .
        \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
 
        \sa Z3_mk_int
@@ -3306,7 +3306,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
 
     /**
-       \brief Retrieve from \s the unit sequence positioned at position \c index.
+       \brief Retrieve from \c s the unit sequence positioned at position \c index.
 
        def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
      */

src/ast/rewriter/seq_rewriter.cpp

@@ -329,13 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     switch(f->get_decl_kind()) {
 
     case OP_SEQ_UNIT:
-        // TODO configuration param
-        if (true) {
-            SASSERT(num_args == 1);
-            return mk_seq_unit(args[0], result);
-        } else {
-            return BR_FAILED;
-        }
+        SASSERT(num_args == 1);
+        return mk_seq_unit(args[0], result);
     case OP_SEQ_EMPTY:
         return BR_FAILED;
     case OP_RE_PLUS:

src/ast/seq_decl_plugin.h

@@ -275,7 +275,7 @@ public:
 
         bool is_string_term(expr const * n) const {
             sort * s = get_sort(n);
-            return (u.is_seq(s) && u.is_string(s));
+            return u.is_string(s);
         }
 
         bool is_non_string_sequence(expr const * n) const {

src/test/cnf_backbones.cpp

@@ -50,8 +50,123 @@ static void display_model(sat::solver const & s) {
     std::cout << "\n";
 }
 
+static void display_status(lbool r) {
+    switch (r) {
+    case l_true: 
+        std::cout << "sat\n"; 
+        break;
+    case l_undef: 
+        std::cout << "unknown\n"; 
+        break;
+    case l_false: 
+        std::cout << "unsat\n"; 
+        break;
+    }
+}
 
-static void cnf_backbones(char const* file_name) {
+static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
+    for (unsigned i = 0; i < lambda.size(); ++i) {
+        if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
+            lambda[i] = lambda.back();
+            lambda.pop_back();
+            --i;
+        }
+    }
+}
+
+// Algorithm 7: Corebased Algorithm with Chunking
+
+static void back_remove(sat::literal_vector& lits, sat::literal l) {
+    for (unsigned i = lits.size(); i > 0; ) {
+        --i;
+        if (lits[i] == l) {
+            lits[i] = lits.back();
+            lits.pop_back();
+            return;
+        }
+    }
+    std::cout << "UNREACHABLE\n";
+}
+
+static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
+    for (unsigned i = 0; i < gamma.size(); ++i) {
+        sat::literal nlit = ~gamma[i];
+        lbool r = s.check(1, &nlit);
+        if (r == l_false) {
+            backbones.push_back(gamma[i]);
+        }
+    }
+}
+
+static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sat::literal_vector>& conseq, unsigned K) {
+    lbool r = s.check();
+    display_status(r);
+    if (r != l_true) {
+        return r;
+    }
+    sat::model const & m = s.get_model();
+    sat::literal_vector lambda, backbones;
+    for (unsigned i = 1; i < m.size(); i++) {
+        lambda.push_back(sat::literal(i, m[i] == l_false));
+    }
+    while (!lambda.empty()) {
+        IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << backbones.size() << ")\n";);
+        unsigned k = std::min(K, lambda.size());
+        sat::literal_vector gamma, omegaN;
+        for (unsigned i = 0; i < k; ++i) {
+            sat::literal l = lambda[lambda.size() - i - 1];
+            gamma.push_back(l);
+            omegaN.push_back(~l);
+        }
+        while (true) {
+            r = s.check(omegaN.size(), omegaN.c_ptr());
+            if (r == l_true) {
+                IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
+                prune_unfixed(lambda, s.get_model());
+                break;
+            }
+            sat::literal_vector const& core = s.get_core();
+            sat::literal_vector occurs;
+            IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";);
+            for (unsigned i = 0; i < omegaN.size(); ++i) {
+                if (core.contains(omegaN[i])) {
+                    occurs.push_back(omegaN[i]);
+                }
+            }
+            if (occurs.size() == 1) {
+                sat::literal lit = occurs.back();
+                sat::literal nlit = ~lit;
+                backbones.push_back(~lit);
+                back_remove(lambda, ~lit);
+                back_remove(gamma, ~lit);
+                s.mk_clause(1, &nlit);
+            }
+            for (unsigned i = 0; i < omegaN.size(); ++i) {
+                if (occurs.contains(omegaN[i])) {
+                    omegaN[i] = omegaN.back();
+                    omegaN.pop_back();
+                    --i;
+                }
+            }
+            if (omegaN.empty() && occurs.size() > 1) {
+                brute_force_consequences(s, gamma, backbones);
+                for (unsigned i = 0; i < gamma.size(); ++i) {
+                    back_remove(lambda, gamma[i]);
+                }
+                break;
+            }
+        }
+    }
+    for (unsigned i = 0; i < backbones.size(); ++i) {
+        sat::literal_vector cons;
+        cons.push_back(backbones[i]);
+        conseq.push_back(cons);
+    }
+    return l_true;
+}
+
+
+static void cnf_backbones(bool use_chunk, char const* file_name) {
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);
@@ -81,26 +196,23 @@ static void cnf_backbones(char const* file_name) {
         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;
+    lbool r;
+    if (use_chunk) {
+        r = core_chunking(solver, vars, conseq, 100);
     }
+    else {
+        r = solver.get_consequences(assumptions, vars, conseq);
+    }
+    std::cout << vars.size() << " " << conseq.size() << "\n";
+    display_status(r);
     display_statistics();
 }
 
 void tst_cnf_backbones(char ** argv, int argc, int& i) {
     if (i + 1 < argc) {
-        cnf_backbones(argv[i + 1]);
+        bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk"));
+        cnf_backbones(use_chunk, argv[i + 1]);
         ++i;
+        if (use_chunk) ++i;
     }
 }