Merge branch 'master' of https://github.com/z3prover/z3 into polysat

contrib/ci/README.md

@@ -42,7 +42,7 @@ the future.
 * `Z3_BUILD_TYPE` - CMake build type (`RelWithDebInfo`, `Release`, `Debug`, or `MinSizeRel`)
 * `Z3_CMAKE_GENERATOR` - CMake generator (`Ninja` or `Unix Makefiles`)
 * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
-* `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`)
+* `Z3_BUILD_LIBZ3_SHARED` - Build Z3 binaries and libraries dynamically/statically (`0` or `1`)
 * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used.
 * `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
 

scripts/mk_nuget_release.py

@@ -48,7 +48,7 @@ os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
            'x64-win' : ('dll', 'win-x64'),
 # Skip x86 as I can't get dotnet build to produce AnyCPU TargetPlatform           
 #          'x86-win' : ('dll', 'win-x86'),
-           'osx' : ('dylib', 'macos'),
+           'osx' : ('dylib', 'osx-x64'),
            'debian' : ('so', 'debian.8-x64') }
 
 def classify_package(f):
@@ -69,7 +69,7 @@ def unpack():
     #    +- ubuntu.16.04-x64
     #    +- ubuntu.14.04-x64
     #    +- debian.8-x64
-    #    +- macos
+    #    +- osx-x64
     # +
     for f in os.listdir("packages"):
         print(f)

scripts/mk_nuget_task.py

@@ -28,7 +28,7 @@ os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
            'glibc-2.31' : ('so', 'glibc-x64'),
            'x64-win' : ('dll', 'win-x64'),
            'x86-win' : ('dll', 'win-x86'),
-           'osx' : ('dylib', 'macos'),
+           'osx' : ('dylib', 'osx-x64'),
            'debian' : ('so', 'debian.8-x64') }
 
 def classify_package(f):
@@ -52,7 +52,7 @@ def unpack(packages, symbols):
     #    +- win-x64
     #    +- win-x86
     #    +- ubuntu-x64
-    #    +- macos
+    #    +- osx-x64
     # +
     tmp = "tmp" if not symbols else "tmpsym"
     for f in os.listdir(packages):

scripts/nightly.yaml

@@ -74,7 +74,7 @@ stages:
       vmImage: "Ubuntu-18.04"
     container: "quay.io/pypa/manylinux2010_x86_64:latest"
     variables:
-      python: "/opt/python/cp35-cp35m/bin/python"
+      python: "/opt/python/cp37-cp37m/bin/python"
     steps:
     - script: $(python) scripts/mk_unix_dist.py --nodotnet --nojava
     - script: git clone https://github.com/z3prover/z3test z3test

src/api/api_config_params.cpp

@@ -47,15 +47,13 @@ extern "C" {
         env_params::updt_params();
     }
     
-    static std::string g_Z3_global_param_get_buffer;
-    
     Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
         memory::initialize(UINT_MAX);
         LOG_Z3_global_param_get(param_id, param_value);
         *param_value = nullptr;
         try {
-            g_Z3_global_param_get_buffer = gparams::get_value(param_id);
+            gparams::g_buffer() = gparams::get_value(param_id);
-            *param_value = g_Z3_global_param_get_buffer.c_str();
+            *param_value = gparams::g_buffer().c_str();
             return true;
         }
         catch (z3_exception & ex) {

src/api/c++/z3++.h

@@ -511,9 +511,11 @@ namespace z3 {
             return *this;
         }
         ast & operator=(ast && s) noexcept {
+            if (this != &s) {
                 object::operator=(std::forward<object>(s));
                 m_ast = s.m_ast;
                 s.m_ast = nullptr;
+            }
             return *this;
         }
         Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }

src/api/dotnet/Microsoft.Z3.csproj.in

@@ -84,7 +84,7 @@ ${Z3_DOTNET_COMPILE_ITEMS}
       <PackagePath>runtimes\linux-x64\native</PackagePath>
     </Content>
     <Content Include="${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dylib" Condition="Exists('${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libz3.dylib')">
-      <PackagePath>runtimes\macos\native</PackagePath>
+      <PackagePath>runtimes\osx-x64\native</PackagePath>
     </Content>
   </ItemGroup>
 

src/api/julia/z3jl.cpp

@@ -451,7 +451,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .method("add", static_cast<void (optimize::*)(expr const &)>(&optimize::add))
         .method("add", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add))
         .method("add", static_cast<void (optimize::*)(expr const &, expr const &)>(&optimize::add))
-        .method("add",      static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
+        .method("add", static_cast<void (optimize::*)(expr const &, char const *)>(&optimize::add))
         .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
         .method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add_soft))
         .MM(optimize, maximize)

src/ast/datatype_decl_plugin.cpp

@@ -645,7 +645,6 @@ namespace datatype {
             return false;
         func_decl* c = get_accessor_constructor(f);
         SASSERT(n == 1);
-        std::cout << f->get_name() << " " << mk_pp(args[0], m) << "\n";
         if (is_constructor(args[0])) 
             return to_app(args[0])->get_decl() != c;
         return false;

src/ast/datatype_decl_plugin.h

@@ -103,9 +103,9 @@ namespace datatype {
 
     namespace param_size {
         class size {
-            unsigned m_ref;
+            unsigned m_ref{ 0 };
         public:
-            size(): m_ref(0) {}
+            size() {}
             virtual ~size() { }
             void inc_ref() { ++m_ref; }
             void dec_ref();
@@ -197,7 +197,7 @@ namespace datatype {
         sort_ref_vector const& params() const { return m_params; }
         util& u() const { return m_util; }
         param_size::size* sort_size() { return m_sort_size; }
-        void set_sort_size(param_size::size* p) { m_sort_size = p; if (p) p->inc_ref(); m_sort = nullptr; }
+        void set_sort_size(param_size::size* p) { auto* q = m_sort_size;  m_sort_size = p; if (p) p->inc_ref(); if (q) q->dec_ref(); m_sort = nullptr; }
         def* translate(ast_translation& tr, util& u);
     };
 

src/ast/expr_substitution.h

@@ -51,7 +51,7 @@ public:
     void reset();
     void cleanup();
 
-    obj_map<expr, expr*> const sub() const { return m_subst; }
+    obj_map<expr, expr*> const & sub() const { return m_subst; }
 
     std::ostream& display(std::ostream& out);
 };

src/ast/macros/quantifier_macro_info.cpp

@@ -25,14 +25,16 @@ quantifier_macro_info::quantifier_macro_info(ast_manager& m, quantifier* q) :
     m_is_auf(true),
     m_has_x_eq_y(false),
     m_the_one(m) {
-    SASSERT(is_forall(q));
     collect_macro_candidates(q);
 }
 
 void quantifier_macro_info::collect_macro_candidates(quantifier* q) {
     macro_util mutil(m);
     macro_util::macro_candidates candidates(m);
-    mutil.collect_macro_candidates(q, candidates);
+    quantifier_ref qa(q, m);
+    if (is_exists(q))
+        qa = m.update_quantifier(q, quantifier_kind::forall_k, m.mk_not(q->get_expr()));
+    mutil.collect_macro_candidates(qa, candidates);
     unsigned num_candidates = candidates.size();
     for (unsigned i = 0; i < num_candidates; i++) {
         cond_macro* mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),

src/ast/normal_forms/nnf.cpp

@@ -72,6 +72,7 @@ class skolemizer {
     cache         m_cache;
     cache         m_cache_pr;
     bool          m_proofs_enabled;
+    used_vars     m_uv;
 
 
     void process(quantifier * q, expr_ref & r, proof_ref & p) {
@@ -81,14 +82,14 @@ class skolemizer {
             p = nullptr;
             return;
         }
-        used_vars uv;
+        m_uv.reset();
-        uv(q);
+        m_uv(q);
         SASSERT(is_well_sorted(m, q));
-        unsigned sz = uv.get_max_found_var_idx_plus_1();
+        unsigned sz = m_uv.get_max_found_var_idx_plus_1();
         ptr_buffer<sort> sorts;
         expr_ref_vector args(m);
         for (unsigned i = 0; i < sz; i++) {
-            sort * s = uv.get(i);
+            sort * s = m_uv.get(i);
             if (s != nullptr) {
                 sorts.push_back(s);
                 args.push_back(m.mk_var(i, s));
@@ -111,7 +112,7 @@ class skolemizer {
         // (VAR num_decls-1) is in the last position.
         //
         for (unsigned i = 0; i < sz; i++) {
-            sort * s = uv.get(i);
+            sort * s = m_uv.get(i);
             if (s != nullptr)
                 substitution.push_back(m.mk_var(i, s));
             else

src/ast/rewriter/bool_rewriter.cpp

@@ -62,7 +62,7 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
         return BR_DONE;
     case OP_XOR:
         switch (num_args) {
-        case 0: return BR_FAILED;
+        case 0: result = m().mk_false(); return BR_DONE;
         case 1: result = args[0]; return BR_DONE;
         case 2: mk_xor(args[0], args[1], result); return BR_DONE;
         default: UNREACHABLE(); return BR_FAILED;

src/ast/rewriter/th_rewriter.cpp

@@ -51,6 +51,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     recfun_rewriter     m_rec_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
+    expr_safe_replace   m_rep;
+    bool                m_new_subst { false };
     expr_ref_vector     m_pinned;
     unsigned long long  m_max_memory; // in bytes
     unsigned            m_max_steps;    
@@ -685,12 +687,17 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     void apply_subst(ptr_buffer<expr>& patterns) {
         if (!m_subst)
             return;
-        expr_ref tmp(m());
+        if (patterns.empty())
-        expr_safe_replace rep(m());
+            return;
+        if (m_new_subst) {
+            m_rep.reset();
             for (auto kv : m_subst->sub())
-            rep.insert(kv.m_key, kv.m_value);
+                m_rep.insert(kv.m_key, kv.m_value);
+            m_new_subst = false;
+        }
+        expr_ref tmp(m());
         for (unsigned i = 0; i < patterns.size(); ++i) {
-            rep(patterns[i], tmp);
+            m_rep(patterns[i], tmp);
             m_pinned.push_back(tmp);
             patterns[i] = tmp;
         }
@@ -796,6 +803,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_rec_rw(m),
         m_a_util(m),
         m_bv_util(m),
+        m_rep(m),
         m_pinned(m),
         m_used_dependencies(m),
         m_subst(nullptr) {
@@ -805,6 +813,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     void set_substitution(expr_substitution * s) {
         reset();
         m_subst = s;
+        m_new_subst = true;
     }
 
     void reset() {

src/ast/rewriter/var_subst.cpp

@@ -79,7 +79,9 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
         result = q;
         return result;
     }
+    unsigned num_decls = q->get_num_decls();
     m_used.reset();
+    m_used.set_num_decls(num_decls);
     m_used.process(q->get_expr());
     unsigned num_patterns = q->get_num_patterns();
     for (unsigned i = 0; i < num_patterns; i++)
@@ -88,7 +90,7 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
     for (unsigned i = 0; i < num_no_patterns; i++)
         m_used.process(q->get_no_pattern(i));
 
-    unsigned num_decls = q->get_num_decls();
+    
     if (m_used.uses_all_vars(num_decls)) {
         q->set_no_unused_vars();
         result = q;

src/ast/seq_decl_plugin.cpp

@@ -1480,7 +1480,7 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
             // unsigned ite_min_length = std::min(min_length, i.min_length);
             // lbool ite_nullable = (nullable == i.nullable ? nullable : l_undef);
             // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
-            return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, min_length, std::max(star_height, i.star_height));
+            return info(false, false, false, false, normalized && i.normalized, monadic && i.monadic, singleton && i.singleton, nullable, std::min(min_length, i.min_length), std::max(star_height, i.star_height));
         }
         else
             return i;

src/ast/used_vars.cpp

@@ -22,6 +22,9 @@ Revision History:
 void used_vars::process(expr * n, unsigned delta) {
     unsigned j, idx;
 
+    if (m_num_found_vars == m_num_decls)
+        return;
+
     m_cache.reset();
     m_todo.reset();
     m_todo.push_back(expr_delta_pair(n, delta));
@@ -58,8 +61,16 @@ void used_vars::process(expr * n, unsigned delta) {
             if (idx >= delta) {
                 idx = idx - delta;
                 if (idx >= m_found_vars.size())
-                    m_found_vars.resize(idx + 1);
+                    m_found_vars.resize(idx + 1, nullptr);
+                if (!m_found_vars[idx]) {
                     m_found_vars[idx] = to_var(n)->get_sort();
+                    if (idx < m_num_decls)
+                        m_num_found_vars++;
+                    if (m_num_found_vars == m_num_decls) {
+                        m_todo.reset();
+                        return;
+                    }
+                }
             }
             break;
         case AST_QUANTIFIER:

src/ast/used_vars.h

@@ -26,18 +26,26 @@ class used_vars {
     typedef hashtable<expr_delta_pair, obj_hash<expr_delta_pair>, default_eq<expr_delta_pair> > cache;
     cache                    m_cache;
     svector<expr_delta_pair> m_todo;
+    unsigned                 m_num_decls{ UINT_MAX };
+    unsigned                 m_num_found_vars{ 0 };
 
     void process(expr * n, unsigned delta);
 
 public:
     
     void operator()(expr * n) {
-        m_found_vars.reset();
+        reset();
         process(n, 0);
     }
 
     void reset() {
         m_found_vars.reset();
+        m_num_decls = UINT_MAX;
+        m_num_found_vars = 0;
+    }
+
+    void set_num_decls(unsigned n) {
+        m_num_decls = n;
     }
 
     void process(expr * n) {

src/cmd_context/cmd_context.cpp

@@ -879,8 +879,9 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
 void cmd_context::insert(symbol const & s, psort_decl * p) {
     pm().inc_ref(p);
     if (m_psort_decls.contains(s)) {
+        symbol _s = s;
         pm().dec_ref(p);
-        throw cmd_exception("sort already defined ", s);
+        throw cmd_exception("sort already defined ", _s);
     }
     m_psort_decls.insert(s, p);
     if (!m_global_decls) {

src/math/lp/lar_solver.cpp

@@ -162,7 +162,7 @@ namespace lp {
                 continue;
             if (!m_terms[k]->contains(basis_j))
                 continue;
-            m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row);
+            m_terms[k]->subst_in_row(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row);
         }
     }
 
@@ -1717,6 +1717,27 @@ namespace lp {
         return true;
     }
 
+    void lar_solver::subst_known_terms(lar_term* t) {
+        std::set<unsigned> seen_terms;
+        for (const auto&p : *t) {
+            auto j = p.column();
+            if (this->column_corresponds_to_term(j)) {
+                seen_terms.insert(j);
+            }
+        }
+        while (!seen_terms.empty()) {
+            unsigned j = *seen_terms.begin();
+            seen_terms.erase(j);
+            auto tj = this->m_var_register.local_to_external(j);
+            auto& ot = this->get_term(tj);
+            for(const auto&  p : ot){
+              if (this->column_corresponds_to_term(p.column())) {
+                 seen_terms.insert(p.column());
+              }   
+            }
+            t->subst_by_term(ot, j);
+        }
+    }
     // do not register in m_var_register this term if ext_i == UINT_MAX
     var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i) {
         TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
@@ -1726,6 +1747,7 @@ namespace lp {
         if (strategy_is_undecided())
             return add_term_undecided(coeffs);
         lar_term* t = new lar_term(coeffs);
+        subst_known_terms(t);
         push_term(t);
         SASSERT(m_terms.size() == m_term_register.size());
         unsigned adjusted_term_index = m_terms.size() - 1;

src/math/lp/lar_solver.h

@@ -585,6 +585,8 @@ public:
         return out;
     }
     
+    void subst_known_terms(lar_term*);
+
     inline std::ostream& print_column_bound_info(unsigned j, std::ostream& out) const {
         return m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, out);
     }

src/math/lp/lar_term.h

@@ -57,6 +57,16 @@ public:
         return m_coeffs;
     }
     
+    void subst_by_term(const lar_term& t, unsigned term_column) {
+        auto it = this->m_coeffs.find_core(term_column);
+        if (it == nullptr) return;
+        mpq a = it->get_data().m_value;
+        this->m_coeffs.erase(term_column);
+        for (const auto & p : t) {
+            this->add_monomial(a * p.coeff(), p.column());
+        }
+    }
+
     lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
         for (const auto & p : coeffs) {
             add_monomial(p.first, p.second);
@@ -94,7 +104,7 @@ public:
     }
 
     // j is the basic variable to substitute
-    void subst(unsigned j, indexed_vector<mpq> & li) {
+    void subst_in_row(unsigned j, indexed_vector<mpq> & li) {
         auto* it = m_coeffs.find_core(j);
         if (it == nullptr) return;
         const mpq & b = it->get_data().m_value;

src/math/lp/var_register.h

@@ -39,7 +39,7 @@ public:
 };
 
 class var_register {
-    svector<ext_var_info> m_local_to_external;
+    vector<ext_var_info> m_local_to_external;
     std::unordered_map<unsigned, unsigned> m_external_to_local;
     unsigned m_locals_mask;
     unsigned m_locals_mask_inverted;

src/model/model_evaluator.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/arith_rewriter.h"
@@ -266,6 +267,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             func_interp * fi = m_model.get_func_interp(g);
             if (fi && (result = fi->get_array_interp(g))) {
                 model_evaluator ev(m_model, m_params);
+                ev.set_model_completion(false);
                 result = ev(result);
                 m_pinned.push_back(result);
                 m_def_cache.insert(g, result);
@@ -373,6 +375,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
             var_subst vs(m, false);
             result = vs(fi->get_interp(), num, args);
+            if (!is_ground(result.get()) && recfun::util(m).is_defined(f))
+                return BR_DONE;
             return BR_REWRITE_FULL;
         }
 

src/opt/opt_context.cpp

@@ -1714,23 +1714,8 @@ namespace opt {
             objective const& obj = m_objectives[i];
             switch(obj.m_type) {
             case O_MINIMIZE:
-            case O_MAXIMIZE: {
+            case O_MAXIMIZE: 
-                inf_eps n = m_optsmt.get_lower(obj.m_index);
-                if (false && // theory_lra doesn't produce infinitesimals
-                    m_optsmt.objective_is_model_valid(obj.m_index) && 
-                    n.get_infinity().is_zero() &&
-                    n.get_infinitesimal().is_zero() &&
-                    is_numeral((*m_model)(obj.m_term), r1)) {
-                    rational r2 = n.get_rational();
-                    if (obj.m_type == O_MINIMIZE) {
-                        r1.neg();
-                    }
-                    CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";);
-                    CTRACE("opt", r1 != r2, tout << *m_model;);
-                    SASSERT(r1 == r2);
-                }
                 break;
-            }
             case O_MAXSMT: {
                 rational value(0);
                 for (unsigned i = 0; i < obj.m_terms.size(); ++i) {

src/opt/opt_solver.cpp

@@ -244,23 +244,46 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         m_last_model = nullptr;
+        //
+        // compute an optimization hint.
+        // The hint is valid if there are no shared symbols (a pure LP).
+        // Generally, the hint is not necessarily valid and has to be checked
+        // relative to other theories.
+        // 
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
         m_context.get_model(m_last_model);
         inf_eps val2;
-        m_valid_objectives[i] = true;
         has_shared = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";
               if (m_last_model) tout << *m_last_model << "\n";);
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
 
-        auto decrement = [&]() {
+        //
+        // retrieve value of objective from current model and update 
+        // current optimal.
+        // 
+        auto update_objective = [&]() {
+            rational r;
+            expr_ref value = (*m_last_model)(m_objective_terms.get(i));
+            if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i])
+                m_objective_values[i] = inf_eps(r);            
+        };
+
+        update_objective();
+                        
+
+        // 
+        // check that "val" obtained from optimization hint is a valid bound.
+        // 
+        auto check_bound = [&]() {
             SASSERT(has_shared);
-            decrement_value(i, val);
+            bool ok = bound_value(i, val);
             if (l_true != m_context.check(0, nullptr))  
                 return false;
             m_context.get_model(m_last_model);   
-            return true;
+            update_objective();
+            return ok;
         };
 
         if (!val.is_finite()) {
@@ -270,19 +293,16 @@ namespace opt {
             TRACE("opt", tout << "updated\n";);
             m_last_model = nullptr;
             m_context.get_model(m_last_model);
-            if (has_shared && val != current_objective_value(i)) {
+            if (!has_shared || val == current_objective_value(i))
-                if (!decrement())
+                m_models.set(i, m_last_model.get());
+            else if (!check_bound())
                 return false;
         }
-            else {
+        else if (!check_bound())
-                m_models.set(i, m_last_model.get());
-            }
-        }
-        else if (!decrement())
             return false;
         m_objective_values[i] = val;
         TRACE("opt", { 
-                tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
+                tout << "objective:     " << mk_pp(m_objective_terms.get(i), m) << "\n";
                 tout << "maximal value: " << val << "\n"; 
                 tout << "new condition: " << blocker << "\n";
                 if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); 
@@ -291,10 +311,9 @@ namespace opt {
         return true;
     }
 
-    lbool opt_solver::decrement_value(unsigned i, inf_eps& val) {
+    bool opt_solver::bound_value(unsigned i, inf_eps& val) {
         push_core();
         expr_ref ge = mk_ge(i, val);
-        TRACE("opt", tout << ge << "\n";);
         assert_expr(ge);
         lbool is_sat = m_context.check(0, nullptr);
         is_sat = adjust_result(is_sat);
@@ -303,19 +322,7 @@ namespace opt {
             m_models.set(i, m_last_model.get());
         }
         pop_core(1);
-        TRACE("opt", tout << is_sat << "\n";);
+        return is_sat == l_true;
-        if (is_sat != l_true) {
-            // cop-out approximation
-            if (arith_util(m).is_real(m_objective_terms.get(i))) {
-                val -= inf_eps(inf_rational(rational(0), true));
-            }
-            else {
-                val -= inf_eps(inf_rational(rational(1)));
-            }
-            m_valid_objectives[i] = false;
-        }
-        return is_sat;
-
     }
 
     lbool opt_solver::adjust_result(lbool r) {
@@ -338,10 +345,12 @@ namespace opt {
         for (unsigned i = m_models.size(); i-- > 0; ) {
             auto* mdl = m_models[i];
             if (mdl) {
+                TRACE("opt", tout << "get " << i << "\n" << *mdl << "\n";);
                 m = mdl;
                 return;
             }
         }        
+        TRACE("opt", tout << "get last\n";);
         m = m_last_model.get();
     }
     
@@ -384,7 +393,6 @@ namespace opt {
         m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational::minus_one(), inf_rational()));
         m_objective_terms.push_back(term);
-        m_valid_objectives.push_back(true);
         m_models.push_back(nullptr);
         return v;
     }
@@ -486,7 +494,6 @@ namespace opt {
         m_objective_vars.reset();
         m_objective_values.reset();
         m_objective_terms.reset();
-        m_valid_objectives.reset();
     }
 
     opt_solver& opt_solver::to_opt(solver& s) {

src/opt/opt_solver.h

@@ -77,7 +77,6 @@ namespace opt {
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;
         expr_ref_vector     m_objective_terms;
-        bool_vector       m_valid_objectives;
         bool                m_dump_benchmarks;
         static unsigned     m_dump_count;
         statistics          m_stats;
@@ -124,9 +123,6 @@ namespace opt {
         inf_eps const & saved_objective_value(unsigned obj_index);
         inf_eps current_objective_value(unsigned obj_index);
         model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }
-        bool objective_is_model_valid(unsigned obj_index) const {
-            return m_valid_objectives[obj_index];
-        }
 
         bool was_unknown() const { return m_was_unknown; }
 
@@ -147,7 +143,7 @@ namespace opt {
                                symbol const& logic = symbol::null, char const * status = "unknown", char const * attributes = "");
 
     private:
-        lbool decrement_value(unsigned i, inf_eps& val);
+        bool bound_value(unsigned i, inf_eps& val);
         void set_model(unsigned i);
         lbool adjust_result(lbool r);
     };

src/opt/optsmt.cpp

@@ -195,24 +195,25 @@ namespace opt {
     lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
         TRACE("opt", tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";);
         arith_util arith(m);
-        bool is_int = arith.is_int(m_objs[obj_index].get());
+        bool is_int = arith.is_int(m_objs.get(obj_index));
         lbool is_sat = l_true;
         expr_ref bound(m), last_bound(m);
 
-        for (unsigned i = 0; i < obj_index; ++i) {
+        for (unsigned i = 0; i < obj_index; ++i) 
             commit_assignment(i);
-        }
 
         unsigned steps = 0;
         unsigned step_incs = 0;
         rational delta_per_step(1);
         unsigned num_scopes = 0;
+        inf_eps last_objective = inf_eps(rational(-1), inf_rational(0));
 
         while (m.inc()) {
             SASSERT(delta_per_step.is_int());
             SASSERT(delta_per_step.is_pos());
             is_sat = m_s->check_sat(0, nullptr);
             TRACE("opt", tout << "check " << is_sat << "\n";
+                  tout << "last bound: " << last_bound << "\n";
                   tout << "lower: " << m_lower[obj_index] << "\n";
                   tout << "upper: " << m_upper[obj_index] << "\n";
                   );
@@ -221,6 +222,7 @@ namespace opt {
                 m_s->get_model(m_model);
                 SASSERT(m_model);
                 inf_eps obj = m_s->saved_objective_value(obj_index);
+                TRACE("opt", tout << "saved objective: " << obj << "\n";);
                 update_lower_lex(obj_index, obj, is_maximize);
                 if (!is_int || !m_lower[obj_index].is_finite()) {
                     delta_per_step = rational(1);
@@ -233,12 +235,12 @@ namespace opt {
                 else {
                     ++steps;
                 }
-                if (delta_per_step > rational::one()) {
+                if (delta_per_step > rational::one() || (obj == last_objective && is_int)) {
                     m_s->push();
                     ++num_scopes;
                     bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
                 }
-                TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";);
+                last_objective = obj;
                 if (bound == last_bound) {
                     break;
                 }
@@ -357,6 +359,7 @@ namespace opt {
     }
 
     void optsmt::update_lower_lex(unsigned idx, inf_eps const& v, bool is_maximize) {
+        TRACE("opt", tout << v << " lower: " << m_lower[idx] << "\n";);
         if (v > m_lower[idx]) {
             m_lower[idx] = v;                
             IF_VERBOSE(1, 
@@ -368,6 +371,7 @@ namespace opt {
             for (unsigned i = idx+1; i < m_vars.size(); ++i) {
                 m_lower[i] = m_s->saved_objective_value(i);
             }
+            TRACE("opt", tout << "update best model " << *m_model << "\n";);
             m_best_model = m_model;
             m_s->get_labels(m_labels);
             m_context.set_model(m_model);
@@ -532,10 +536,6 @@ namespace opt {
         return m_lower[i];
     }
 
-    bool optsmt::objective_is_model_valid(unsigned index) const {
-        return m_s->objective_is_model_valid(index);
-    }
-
     inf_eps optsmt::get_upper(unsigned i) const {
         if (i >= m_upper.size()) return inf_eps();
         return m_upper[i];
@@ -543,6 +543,7 @@ namespace opt {
 
     void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {        
         mdl = m_best_model.get();
+        TRACE("opt", tout << *mdl << "\n";);
         labels = m_labels;
     }
 

src/opt/optsmt.h

@@ -61,7 +61,6 @@ namespace opt {
         void commit_assignment(unsigned index);
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
-        bool objective_is_model_valid(unsigned index) const;
         void    get_model(model_ref& mdl, svector<symbol>& labels);
         model*  get_model(unsigned index) const { return m_models[index]; }
 

src/qe/mbp/mbp_arith.cpp

@@ -194,17 +194,19 @@ namespace mbp {
 
             else if (m.is_ite(t, t1, t2, t3)) {
                 val = eval(t1);
-                SASSERT(m.is_true(val) || m.is_false(val));
                 TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
                 if (m.is_true(val)) {
                     linearize(mbo, eval, mul, t2, c, fmls, ts, tids);
                     fmls.push_back(t1);
                 }
-                else {
+                else if (m.is_false(val)) {
                     expr_ref not_t1(mk_not(m, t1), m);
                     fmls.push_back(not_t1);
                     linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
                 }
+                else {
+                    throw default_exception("mbp evaluation didn't produce a truth value");
+                }
             }
             else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
                 rational r;
@@ -372,6 +374,8 @@ namespace mbp {
                     ts.push_back(var2expr(index2expr, v));                
                 if (!d.m_coeff.is_zero())
                     ts.push_back(a.mk_numeral(d.m_coeff, is_int));
+                if (ts.empty())
+                    ts.push_back(a.mk_numeral(rational(0), is_int));
                 t = mk_add(ts);
                 if (!d.m_div.is_one() && is_int) 
                     t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int));                

src/qe/qe_lite.cpp

@@ -2316,7 +2316,7 @@ public:
         if (is_exists(tmp) && to_quantifier(tmp)->get_qid() == qe_lite) {
             used_vars used;
             tmp = to_quantifier(tmp)->get_expr();
-            used.process(tmp);
+            used(tmp);
             var_subst vs(m, true);
             fml = vs(tmp, vars.size(), (expr*const*)vars.data());
             // collect set of variables that were used.

src/sat/sat_types.h

@@ -27,6 +27,7 @@ Revision History:
 #include "util/uint_set.h"
 #include "util/stopwatch.h"
 #include "util/symbol.h"
+#include "util/sat_literal.h"
 
 class params_ref;
 class reslimit;
@@ -35,89 +36,11 @@ class statistics;
 namespace sat {
 #define SAT_VB_LVL 10
 
-    // TODO: there is some duplication in the sat and smt namespaces.
-    // The sat namespace should be the base.
-    // I should cleanup the smt namespace later.
-
-    /**
-       \brief A boolean variable is just an integer.
-    */
-    typedef unsigned bool_var;
-
-    typedef svector<bool_var> bool_var_vector;
-
-    const bool_var null_bool_var  = UINT_MAX >> 1;
-
-    /**
-       \brief The literal b is represented by the value 2*b, and
-       the literal (not b) by the value 2*b + 1
-    */
-    class literal {
-        unsigned  m_val;
-        explicit literal(unsigned v):m_val(v) {}
-    public:
-        literal():m_val(null_bool_var << 1) {
-            SASSERT(var() == null_bool_var && !sign());
-        }
-
-        literal(bool_var v, bool _sign):
-            m_val((v << 1) + static_cast<unsigned>(_sign)) {
-            SASSERT(var() == v);
-            SASSERT(sign() == _sign);
-        }
-
-        bool_var var() const {
-            return m_val >> 1;
-        }
-
-        bool sign() const {
-            return m_val & 1;
-        }
-
-        literal unsign() const {
-            return literal(m_val & ~1);
-        }
-
-        unsigned index() const {
-            return m_val;
-        }
-
-        void neg() {
-            m_val = m_val ^ 1;
-        }
-
-        friend literal operator~(literal l) {
-            return literal(l.m_val ^ 1);
-        }
-
-        unsigned to_uint() const { return m_val; }
-
-        unsigned hash() const { return to_uint(); }
-
-        friend literal to_literal(unsigned x);
-        friend bool operator<(literal const & l1, literal const & l2);
-        friend bool operator==(literal const & l1, literal const & l2);
-        friend bool operator!=(literal const & l1, literal const & l2);
-    };
-
-    const literal null_literal;
-    struct literal_hash : obj_hash<literal> {};
-
-    inline literal to_literal(unsigned x) { return literal(x); }
-    inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val;  }
-    inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; }
-    inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; }
-
-    inline std::ostream & operator<<(std::ostream & out, literal l) { if (l == null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; }
-
-    typedef svector<literal> literal_vector;
-    typedef std::pair<literal, literal> literal_pair;
 
     typedef size_t clause_offset;
     typedef size_t ext_constraint_idx;
     typedef size_t ext_justification_idx;
 
-    struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } };
 
     typedef approx_set_tpl<literal, literal2unsigned, unsigned> literal_approx_set;
 
@@ -141,7 +64,6 @@ namespace sat {
 
     typedef svector<lbool> model;
 
-    inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
     inline lbool value_at(bool_var v, model const & m) { return  m[v]; }
     inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; }
 
@@ -155,88 +77,6 @@ namespace sat {
         return out;
     }
 
-    typedef tracked_uint_set uint_set;
-
-    typedef uint_set bool_var_set;
-
-    class literal_set {
-        uint_set m_set;
-    public:
-        literal_set(literal_vector const& v) {
-            for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
-        }
-        literal_set() {}
-        literal_vector to_vector() const {
-            literal_vector result;
-            for (literal lit : *this) result.push_back(lit);
-            return result;
-        }
-        literal_set& operator=(literal_vector const& v) {
-            reset();
-            for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
-            return *this;
-        }
-
-        void insert(literal l) { m_set.insert(l.index()); }
-        void remove(literal l) { m_set.remove(l.index()); }
-        literal pop() { return to_literal(m_set.erase()); }
-        bool contains(literal l) const { return m_set.contains(l.index()); }
-        bool empty() const { return m_set.empty(); }
-        unsigned size() const { return m_set.size(); }
-        void reset() { m_set.reset(); }
-        void finalize() { m_set.finalize(); }
-        class iterator {
-            uint_set::iterator m_it;
-        public:
-            iterator(uint_set::iterator it):m_it(it) {}
-            literal operator*() const { return to_literal(*m_it); }
-            iterator& operator++() { ++m_it; return *this; }
-            iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }
-            bool operator==(iterator const& it) const { return m_it == it.m_it; }
-            bool operator!=(iterator const& it) const { return m_it != it.m_it; }
-        };
-        iterator begin() const { return iterator(m_set.begin()); }
-        iterator end() const { return iterator(m_set.end()); }
-        literal_set& operator&=(literal_set const& other) {
-            m_set &= other.m_set;
-            return *this;
-        }
-        literal_set& operator|=(literal_set const& other) {
-            m_set |= other.m_set;
-            return *this;
-        }
-    };
-
-    struct dimacs_lit {
-        literal m_lit;
-        dimacs_lit(literal l):m_lit(l) {}
-    };
-
-    inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) {
-        literal l = dl.m_lit;
-        if (l.sign()) out << "-" << (l.var() + 1);
-        else out << (l.var() + 1);
-        return out;
-    }
-
-    struct mk_lits_pp {
-        unsigned        m_num;
-        literal const * m_lits;
-        mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {}
-    };
-
-    inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) {
-        for (unsigned i = 0; i < ls.m_num; i++) {
-            if (i > 0) out << " ";
-            out << ls.m_lits[i];
-        }
-        return out;
-    }
-
-    inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) {
-        return out << mk_lits_pp(ls.size(), ls.data());
-    }
-
     class i_local_search {
     public:
         virtual ~i_local_search() {}

src/sat/smt/arith_solver.cpp

@@ -580,6 +580,7 @@ namespace arith {
                        verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
                        verbose_stream() << *b << "\n";);
             IF_VERBOSE(0, ctx.display(verbose_stream()));
+            IF_VERBOSE(0, verbose_stream() << mdl << "\n");
             UNREACHABLE();
         }
     }
@@ -1438,4 +1439,12 @@ namespace arith {
         ctx.get_antecedents(l, jst, r, probing);
     }
 
+    bool solver::include_func_interp(func_decl* f) const {
+        return 
+            a.is_div0(f) ||
+            a.is_idiv0(f) ||
+            a.is_power0(f) ||
+            a.is_rem0(f) ||
+            a.is_mod0(f);        
+    }
 }

src/sat/smt/arith_solver.h

@@ -444,6 +444,7 @@ namespace arith {
         void apply_sort_cnstr(euf::enode* n, sort* s) override {}
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
+        bool include_func_interp(func_decl* f) const override;
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }

src/sat/smt/bv_internalize.cpp

@@ -162,7 +162,7 @@ namespace bv {
 
 #define internalize_bin(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
 #define internalize_un(F) un = [&](unsigned sz, expr* const* xs, expr_ref_vector& bits) { m_bb.F(sz, xs, bits);}; internalize_unary(a, un);
-#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_ac_binary(a, bin);
+#define internalize_ac(F) bin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits) { m_bb.F(sz, xs, ys, bits); }; internalize_binary(a, bin);
 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
 #define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
@@ -284,7 +284,6 @@ namespace bv {
     }
 
     void solver::register_true_false_bit(theory_var v, unsigned idx) {
-        SASSERT(s().value(m_bits[v][idx]) != l_undef);
         sat::literal l = m_bits[v][idx];
         SASSERT(l == mk_true() || ~l == mk_true());
         bool is_true = l == mk_true();
@@ -369,7 +368,7 @@ namespace bv {
     sat::literal solver::mk_true() {
         if (m_true == sat::null_literal) {
             ctx.push(value_trail<sat::literal>(m_true));
-            m_true = ctx.internalize(m.mk_true(), false, false, false);
+            m_true = ctx.internalize(m.mk_true(), false, true, false);
         }
         return m_true;
     }
@@ -559,27 +558,19 @@ namespace bv {
         init_bits(n, bits);
     }
 
-    void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
-        SASSERT(e->get_num_args() == 2);
-        expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
-        get_arg_bits(e, 0, arg1_bits);
-        get_arg_bits(e, 1, arg2_bits);
-        SASSERT(arg1_bits.size() == arg2_bits.size());
-        fn(arg1_bits.size(), arg1_bits.data(), arg2_bits.data(), bits);
-        init_bits(e, bits);
-    }
 
-    void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
+    void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
         SASSERT(e->get_num_args() >= 1);
         expr_ref_vector bits(m), new_bits(m), arg_bits(m);
+        
         unsigned i = e->get_num_args() - 1;
-        get_arg_bits(e, i, bits);
+        get_arg_bits(e, 0, bits);
-        for (; i-- > 0; ) {
+        for (unsigned i = 1; i < e->get_num_args(); ++i) {
             arg_bits.reset();
             get_arg_bits(e, i, arg_bits);
             SASSERT(arg_bits.size() == bits.size());
             new_bits.reset();
-            fn(arg_bits.size(), arg_bits.data(), bits.data(), new_bits);
+            fn(bits.size(), bits.data(), arg_bits.data(), new_bits);
             bits.swap(new_bits);
         }        
         init_bits(e, bits);

src/sat/smt/bv_solver.cpp

@@ -95,6 +95,11 @@ namespace bv {
         result.reset();
         unsigned i = 0;
         for (literal b : m_bits[v]) {
+            if (b == ~m_true) 
+                ;
+            else if (b == m_true) 
+                result += power2(i);
+            else {
                 switch (ctx.s().value(b)) {
                 case l_false:
                     break;
@@ -104,6 +109,7 @@ namespace bv {
                     result += power2(i);
                     break;
                 }
+            }
             ++i;
         }
         return true;

src/sat/smt/bv_solver.h

@@ -239,7 +239,6 @@ namespace bv {
         bool internalize_circuit(app* a);
         void internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn);
         void internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
-        void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
         void internalize_par_unary(app* n, std::function<void(unsigned, expr* const*, unsigned p, expr_ref_vector&)>& fn);
         void internalize_novfl(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref&)>& fn);
         void internalize_interp(app* n, std::function<expr*(expr*, expr*)>& ibin, std::function<expr*(expr*)>& un);

src/sat/smt/dt_solver.cpp

@@ -249,7 +249,7 @@ namespace dt {
         SASSERT(!d->m_constructor);
         SASSERT(!recognizer || ctx.value(recognizer) == l_false || !is_final);
         
-        TRACE("dt", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
+        TRACE("dt", tout << ctx.bpp(n) << " non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
 
         if (!recognizer && non_rec_c->get_arity() == 0) {
             sat::literal eq = eq_internalize(n->get_expr(), m.mk_const(non_rec_c));
@@ -469,12 +469,12 @@ namespace dt {
 
     void solver::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
         // v1 is the new root
-        TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n";);
         SASSERT(v1 == static_cast<int>(m_find.find(v1)));
         var_data* d1 = m_var_data[v1];
         var_data* d2 = m_var_data[v2];
         auto* con1 = d1->m_constructor;
         auto* con2 = d2->m_constructor;
+        TRACE("dt", tout << "merging v" << v1 << " v" << v2 << "\n" << ctx.bpp(var2enode(v1)) << " == " << ctx.bpp(var2enode(v2)) << " " << ctx.bpp(con1) << " " << ctx.bpp(con2) << "\n";);
         if (con1 && con2 && con1->get_decl() != con2->get_decl())
             ctx.set_conflict(euf::th_explain::conflict(*this, con1, con2));
         else if (con2 && !con1) {
@@ -721,6 +721,19 @@ namespace dt {
         return true;
     }
 
+    bool solver::include_func_interp(func_decl* f) const {
+        if (!dt.is_accessor(f))
+            return false;
+        func_decl* con = dt.get_accessor_constructor(f);
+        for (enode* app : ctx.get_egraph().enodes_of(f)) {
+            enode* arg = app->get_arg(0)->get_root();
+            if (is_constructor(arg) && arg->get_decl() != con) 
+                return true;
+        }
+        return false; 
+    }
+
+
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
         if (!visit_rec(m, e, sign, root, redundant)) 
             return sat::null_literal;        
@@ -769,7 +782,6 @@ namespace dt {
                 }
             }
             mk_var(n);
-
         }
         else if (is_recognizer(term)) {
             mk_var(n);
@@ -781,6 +793,8 @@ namespace dt {
             SASSERT(is_accessor(term));
             SASSERT(n->num_args() == 1);
             mk_var(n->get_arg(0));
+            if (is_datatype(n))
+                mk_var(n);
         }
 
         return true;

src/sat/smt/dt_solver.h

@@ -60,7 +60,7 @@ namespace dt {
             stats() { reset(); }
         };
 
-        datatype_util         dt;
+        mutable datatype_util dt;
         array_util            m_autil;
         stats                 m_stats;
         ptr_vector<var_data>  m_var_data;
@@ -150,6 +150,7 @@ namespace dt {
         bool unit_propagate() override { return false; }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
+        bool include_func_interp(func_decl* f) const override;
         sat::literal internalize(expr* e, bool sign, bool root, bool redundant) override;
         void internalize(expr* e, bool redundant) override;
         euf::theory_var mk_var(euf::enode* n) override;

src/sat/smt/euf_ackerman.cpp

@@ -34,6 +34,7 @@ namespace euf {
             m.dec_ref(inf->a);
             m.dec_ref(inf->b);
             m.dec_ref(inf->c);
+            dealloc(inf);
         }
         m_table.reset();
         m_queue = nullptr;        

src/sat/smt/euf_model.cpp

@@ -208,7 +208,6 @@ namespace euf {
                     fi = alloc(func_interp, m, arity);
                     mdl->register_decl(f, fi);
                 }
-                TRACE("euf", tout << f->get_name() << "\n";);
                 args.reset();                
                 for (enode* arg : enode_args(n)) 
                     args.push_back(m_values.get(arg->get_root_id()));                
@@ -216,6 +215,10 @@ namespace euf {
                 SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.data()))
                     fi->insert_new_entry(args.data(), v);
+                TRACE("euf", tout << f->get_name() << "\n";
+                      for (expr* arg : args) tout << mk_pp(arg, m) << " ";
+                      tout << "\n -> " << mk_pp(v, m) << "\n";);
+
             }
         }
     }

src/sat/smt/q_ematch.cpp

@@ -166,9 +166,9 @@ namespace q {
         todo.push_back(e);
         while (!todo.empty()) {
             expr* t = todo.back();
+            todo.pop_back();
             if (m_mark.is_marked(t))
                 continue;
-            todo.pop_back();
             m_mark.mark(t);
             if (is_ground(t)) {
                 add_watch(ctx.get_egraph().find(t), clause_idx);

src/sat/smt/q_mam.cpp

@@ -1224,16 +1224,10 @@ namespace q {
                 m_mp_already_processed[first_idx] = true;
                 linearise_multi_pattern(first_idx);
             }
+            for (unsigned i = 0; i < m_qa->get_num_decls(); i++) 
+                if (m_vars[i] == -1)
+                    return;
             
-#ifdef Z3DEBUG
-            for (unsigned i = 0; i < m_qa->get_num_decls(); i++) {
-                CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n";
-                       tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n";
-                       tout << "tree:\n" << *m_tree << "\n";
-                       );
-                SASSERT(m_vars[i] >= 0);
-            }
-#endif
             SASSERT(head->m_next == 0);
             m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
 

src/sat/smt/q_solver.cpp

@@ -148,8 +148,10 @@ namespace q {
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
         SASSERT(is_forall(e) || is_exists(e));
         sat::bool_var v = ctx.get_si().add_bool_var(e);
-        sat::literal lit = ctx.attach_lit(sat::literal(v, sign), e);
+        sat::literal lit = ctx.attach_lit(sat::literal(v, false), e);
         mk_var(ctx.get_egraph().find(e));
+        if (sign)
+            lit.neg();
         return lit;
     }
 

src/sat/smt/sat_dual_solver.cpp

@@ -147,6 +147,7 @@ namespace sat {
             if (m_solver.value(r) == l_true)
                 lits.push_back(r);
         out << "roots: " << lits << "\n";
+        m_solver.display(out);
 
         return out;
     }

src/sat/tactic/goal2sat.cpp

@@ -75,7 +75,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     expr_ref_vector             m_trail;
     func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
-    bool                        m_xor_solver { false };
     bool                        m_euf { false };
     bool                        m_drat { false };
     bool                        m_is_redundant { false };
@@ -108,7 +107,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat_params sp(p);
         m_ite_extra  = p.get_bool("ite_extra", true);
         m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-        m_xor_solver = p.get_bool("xor_solver", false);
         m_euf = sp.euf();
         m_drat = sp.drat_file().is_non_empty_string();
     }
@@ -576,7 +574,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    void convert_iff2(app * t, bool root, bool sign) {
+    void convert_iff(app * t, bool root, bool sign) {
+        if (t->get_num_args() != 2)
+            throw default_exception("unexpected number of arguments to xor");
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
@@ -609,13 +609,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    void convert_iff(app * t, bool root, bool sign) {
-        if (!m_euf && is_xor(t))
-            convert_ba(t, root, sign);
-        else               
-            convert_iff2(t, root, sign);
-    }
-
     func_decl_ref_vector const& interpreted_funs() {
         auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
         if (ext)
@@ -721,10 +714,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
-    bool is_xor(app* t) const {
-        return m_xor_solver && m.is_iff(t) && m.is_iff(t->get_arg(1));
-    }
-
     struct scoped_stack {
         imp& i;
         sat::literal_vector& r;
@@ -782,11 +771,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 visit(t->get_arg(0), root, !sign);
                 continue;
             }
-            if (!m_euf && is_xor(t)) {
-                convert_ba(t, root, sign);
-                m_frame_stack.pop_back();
-                continue;
-            }
             unsigned num = t->get_num_args();
             while (m_frame_stack[fsz-1].m_idx < num) {
                 expr * arg = t->get_arg(m_frame_stack[fsz-1].m_idx);

src/shell/dimacs_frontend.cpp

@@ -66,6 +66,7 @@ static void STD_CALL on_ctrl_c(int) {
 
 static void display_model(sat::solver const & s) {
     sat::model const & m = s.get_model();
+    std::cout << "v ";
     for (unsigned i = 1; i < m.size(); i++) {
         switch (m[i]) {
         case l_false: std::cout << "-" << i << " ";  break;
@@ -77,7 +78,7 @@ static void display_model(sat::solver const & s) {
 }
 
 static void display_core(sat::solver const& s, vector<sat::literal_vector> const& tracking_clauses) {
-    std::cout << "core\n";
+    std::cout << "v core\n";
     sat::literal_vector const& c = s.get_core();
     for (unsigned i = 0; i < c.size(); ++i) {
         sat::literal_vector const& cls = tracking_clauses[c[i].var()];
@@ -264,15 +265,15 @@ unsigned read_dimacs(char const * file_name) {
     }
     switch (r) {
     case l_true: 
-        std::cout << "sat\n"; 
+        std::cout << "s SATISFIABLE\n"; 
         if (file_name && gparams::get_ref().get_bool("model_validate", false)) verify_solution(file_name);
         display_model(*g_solver);
         break;
     case l_undef: 
-        std::cout << "unknown\n"; 
+        std::cout << "s UNKNOWN\n"; 
         break;
     case l_false: 
-        std::cout << "unsat\n"; 
+        std::cout << "s UNSATISFIABLE\n"; 
         if (p.get_bool("dimacs.core", false)) {
             display_core(*g_solver, tracking_clauses);
         }

src/shell/main.cpp

@@ -46,7 +46,6 @@ Revision History:
 
 typedef enum { IN_UNSPECIFIED, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS, IN_DRAT } input_kind;
 
-static std::string  g_aux_input_file;
 static char const * g_input_file          = nullptr;
 static char const * g_drat_input_file     = nullptr;
 static bool         g_standard_input      = false;
@@ -124,7 +123,7 @@ void display_usage() {
     std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
 }
    
-static void parse_cmd_line_args(int argc, char ** argv) {
+static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) {
     long timeout = 0;
     int i = 1;
     char * eq_pos = nullptr;
@@ -134,19 +133,18 @@ static void parse_cmd_line_args(int argc, char ** argv) {
         if (arg[0] == '-' && arg[1] == '-' && arg[2] == 0) {
             // Little hack used to read files with strange names such as -foo.smt2
             // z3 -- -foo.smt2
-            i++;
-            g_aux_input_file = "";
-            for (; i < argc; i++) {
-                g_aux_input_file += argv[i];
-                if (i < argc - 1)
-                    g_aux_input_file += " ";
-            }
             if (g_input_file) {
                 warning_msg("input file was already specified.");
+                break;
             }
-            else {
+            i++;
-                g_input_file = g_aux_input_file.c_str();
+            input_file = "";
+            for (; i < argc; i++) {
+                input_file += argv[i];
+                if (i < argc - 1)
+                    input_file += " ";
             }
+            g_input_file = input_file.c_str();
             break;
         }
         
@@ -325,7 +323,8 @@ int STD_CALL main(int argc, char ** argv) {
         unsigned return_value = 0;
         memory::initialize(0);
         memory::exit_when_out_of_memory(true, "ERROR: out of memory");
-        parse_cmd_line_args(argc, argv);
+        std::string input_file;
+        parse_cmd_line_args(input_file, argc, argv);
         env_params::updt_params();
 
         if (g_input_file && g_standard_input) {

src/smt/mam.cpp

@@ -1218,15 +1218,11 @@ namespace {
                 linearise_multi_pattern(first_idx);
             }
 
-#ifdef Z3DEBUG
+            // check that all variables are captured by pattern.
-            for (unsigned i = 0; i < m_qa->get_num_decls(); i++) {
+            for (unsigned i = 0; i < m_qa->get_num_decls(); i++) 
-                CTRACE("mam_new_bug", m_vars[i] < 0, tout << mk_ismt2_pp(m_qa, m) << "\ni: " << i << " m_vars[i]: " << m_vars[i] << "\n";
+                if (m_vars[i] == -1) 
-                       tout << "m_mp:\n" << mk_ismt2_pp(m_mp, m) << "\n";
+                    return;
-                       tout << "tree:\n" << *m_tree << "\n";
+
-                       );
-                SASSERT(m_vars[i] >= 0);
-            }
-#endif
             SASSERT(head->m_next == 0);
             m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
 
@@ -1843,7 +1839,7 @@ namespace {
         enode_vector        m_bindings;
         enode_vector        m_args;
         backtrack_stack     m_backtrack_stack;
-        unsigned            m_top;
+        unsigned            m_top { 0 };
         const instruction * m_pc;
 
         // auxiliary temporary variables
@@ -2210,8 +2206,13 @@ namespace {
             if (curr->get_num_args() == expected_num_args && m_context.is_relevant(curr))
                 break;
         }
-        if (bp.m_it == bp.m_end)
+        if (bp.m_it == bp.m_end) {
+            if (best_v) {
+                bp.m_to_recycle = nullptr; 
+                recycle_enode_vector(best_v);
+            }
             return nullptr;
+        }
         m_top++;
         update_max_generation(*(bp.m_it), nullptr);
         return *(bp.m_it);

src/smt/smt_clause.cpp

@@ -101,7 +101,7 @@ namespace smt {
         out << "(clause";
         for (unsigned i = 0; i < m_num_literals; i++) {
             out << " ";
-            m_lits[i].display(out, m, bool_var2expr_map);
+            smt::display(out, m_lits[i], m, bool_var2expr_map);
         }
         return out << ")";
     }
@@ -110,7 +110,7 @@ namespace smt {
         out << "(clause";
         for (unsigned i = 0; i < m_num_literals; i++) {
             out << " ";
-            m_lits[i].display_compact(out, bool_var2expr_map);
+            smt::display_compact(out, m_lits[i], bool_var2expr_map);
         }
         return out << ")";
     }

src/smt/smt_consequences.cpp

@@ -385,10 +385,10 @@ namespace smt {
                 expr* e = kv.m_key;
                 expr* val = kv.m_value;
                 literal lit = mk_diseq(e, val);
-                mark_as_relevant(lit);
                 if (get_assignment(lit) != l_undef) {
                     continue;
                 }
+                mark_as_relevant(lit);
                 ++num_vars;
                 push_scope();
                 assign(lit, b_justification::mk_axiom(), true);

src/smt/smt_context.cpp

@@ -3081,7 +3081,7 @@ namespace smt {
                     literal l2 = *set_it;
                     if (l2 != l) {
                         b_justification js(l);
-                        TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m, m_bool_var2expr.data()); tout << std::endl;);
+                        TRACE("theory_case_split", tout << "case split literal "; smt::display(tout, l2, m, m_bool_var2expr.data()); tout << std::endl;);
                         if (l2 == true_literal || l2 == false_literal || l2 == null_literal) continue;
                         assign(~l2, js);
                         if (inconsistent()) {
@@ -4188,7 +4188,7 @@ namespace smt {
                   for (unsigned i = 0; i < num_lits; i++) {
                       display_literal(tout, v[i]);
                       tout << "\n";
-                      v[i].display(tout, m, m_bool_var2expr.data());
+                      smt::display(tout, v[i], m, m_bool_var2expr.data());
                       tout << "\n\n";
                   }
                   tout << "\n";);

src/smt/smt_context.h

@@ -1357,7 +1357,7 @@ namespace smt {
 
         std::ostream& display_literal(std::ostream & out, literal l) const;
 
-        std::ostream& display_detailed_literal(std::ostream & out, literal l) const { l.display(out, m, m_bool_var2expr.data()); return out; }
+        std::ostream& display_detailed_literal(std::ostream & out, literal l) const { return smt::display(out, l, m, m_bool_var2expr.data()); }
 
         void display_literal_info(std::ostream & out, literal l) const;
 

src/smt/smt_context_pp.cpp

@@ -89,7 +89,7 @@ namespace smt {
     }
 
     std::ostream& context::display_literal(std::ostream & out, literal l) const {
-        l.display_compact(out, m_bool_var2expr.data()); return out;
+        smt::display_compact(out, l, m_bool_var2expr.data()); return out;
     }
 
     std::ostream& context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
@@ -120,7 +120,7 @@ namespace smt {
     }
 
     void context::display_literal_info(std::ostream & out, literal l) const {
-        l.display_compact(out, m_bool_var2expr.data());
+        smt::display_compact(out, l, m_bool_var2expr.data());
         display_literal_smt2(out, l);
         out << "relevant: " << is_relevant(bool_var2expr(l.var())) << ", val: " << get_assignment(l) << "\n";
     }

src/smt/smt_literal.cpp

@@ -22,41 +22,44 @@ Revision History:
 
 namespace smt {
 
-    void literal::display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
+    std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) {
-        if (*this == true_literal)
+        if (lit == true_literal)
             out << "true";
-        else if (*this == false_literal)
+        else if (lit == false_literal)
             out << "false";
-        else if (*this == null_literal)
+        else if (lit == null_literal)
             out << "null";
-        else if (sign())
+        else if (lit.sign())
-            out << "(not " << mk_bounded_pp(bool_var2expr_map[var()], m, 3) << ")";
+            out << "(not " << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3) << ")";
         else
-            out << mk_bounded_pp(bool_var2expr_map[var()], m, 3);
+            out << mk_bounded_pp(bool_var2expr_map[lit.var()], m, 3);
+        return out;
     }
 
-    void literal::display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const {
+    std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map) {
-        if (*this == true_literal)
+        if (lit == true_literal)
             out << "true";
-        else if (*this == false_literal)
+        else if (lit == false_literal)
             out << "false";
-        else if (*this == null_literal)
+        else if (lit == null_literal)
             out << "null";
-        else if (sign())
+        else if (lit.sign())
-            out << "(not " << mk_pp(bool_var2expr_map[var()], m, 3) << ")";
+            out << "(not " << mk_pp(bool_var2expr_map[lit.var()], m, 3) << ")";
         else
-            out << mk_pp(bool_var2expr_map[var()], m, 3);
+            out << mk_pp(bool_var2expr_map[lit.var()], m, 3);
+        return out;
     }
 
-    void literal::display_compact(std::ostream & out, expr * const * bool_var2expr_map) const {
+    std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map) {
-        if (*this == true_literal)
+        if (lit == true_literal)
             out << "true";
-        else if (*this == false_literal)
+        else if (lit == false_literal)
             out << "false";
-        else if (sign())
+        else if (lit.sign())
-            out << "(not #" << bool_var2expr_map[var()]->get_id() << ")";
+            out << "(not #" << bool_var2expr_map[lit.var()]->get_id() << ")";
         else
-            out << "#" << bool_var2expr_map[var()]->get_id();
+            out << "#" << bool_var2expr_map[lit.var()]->get_id();
+        return out;
     }
 
     std::ostream & operator<<(std::ostream & out, literal l) {
@@ -72,24 +75,26 @@ namespace smt {
     }
 
     std::ostream & operator<<(std::ostream & out, const literal_vector & v) {
-        display(out, v.begin(), v.end());
+        ::display(out, v.begin(), v.end());
         return out;
     }
 
-    void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) {
+    std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map) {
         for (unsigned i = 0; i < num_lits; i++) {
             if (i > 0)
                 out << " ";
-            lits[i].display_compact(out, bool_var2expr_map);
+            display_compact(out, lits[i], bool_var2expr_map);
         }
+        return out;
     }
 
-    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) {
+    std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep) {
         for (unsigned i = 0; i < num_lits; i++) {
             if (i > 0)
                 out << sep;
-            lits[i].display(out, m, bool_var2expr_map);
+            display(out, lits[i], m, bool_var2expr_map);
         }
+        return out;
     }
 
     /**

src/smt/smt_literal.h

@@ -21,77 +21,13 @@ Revision History:
 #include "ast/ast.h"
 #include "smt/smt_types.h"
 #include "util/approx_set.h"
+#include "util/sat_literal.h"
 
 namespace smt {
-    /**
-       \brief The literal b is represented by the value 2*b, and
-       the literal (not b) by the value 2*b + 1
 
-    */
+    typedef sat::literal literal;
-    class literal {
-        int  m_val;
     
-    public:
+    inline literal to_literal(int x) { return sat::to_literal(x); }
-        literal():m_val(-2) {
-            SASSERT(var() == null_bool_var && !sign());
-        }
-        
-        explicit literal(bool_var v, bool sign = false):
-            m_val((v << 1) + static_cast<int>(sign)) {
-        }
-        
-        bool_var var() const { 
-            return m_val >> 1; 
-        }
-        
-        bool sign() const {
-            return m_val & 1; 
-        }
-        
-        int index() const {
-            return m_val;
-        }
-        
-        void neg() {
-            m_val = m_val ^ 1;
-        }
-        
-        friend literal operator~(literal l);
-        
-        friend literal to_literal(int x);
-
-        void display(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
-
-        void display_smt2(std::ostream & out, ast_manager & m, expr * const * bool_var2expr_map) const;
-
-        void display_compact(std::ostream & out, expr * const * bool_var2expr_map) const;
-
-        unsigned hash() const { return m_val; }
-    };
-
-    inline bool operator==(literal l1, literal l2) {
-        return l1.index() == l2.index();
-    }
-    
-    inline bool operator!=(literal l1, literal l2) {
-        return l1.index() != l2.index();
-    }
-    
-    inline bool operator<(literal l1, literal l2) {
-        return l1.index() < l2.index();
-    }
-    
-    inline literal operator~(literal l) {
-        literal r;
-        r.m_val = l.m_val ^ 1;
-        return r;
-    }
-    
-    inline literal to_literal(int x) {
-        literal l;
-        l.m_val = x;
-        return l;
-    }
 
     const literal null_literal;
     const literal true_literal(true_bool_var, false); 
@@ -99,12 +35,16 @@ namespace smt {
 
     typedef svector<literal> literal_vector;
     typedef sbuffer<literal> literal_buffer;
-    std::ostream & operator<<(std::ostream & out, literal l);
-    std::ostream & operator<<(std::ostream & out, const literal_vector & v);
 
-    void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
+    std::ostream& display(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map);
     
-    void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n");
+    std::ostream& display_smt2(std::ostream & out, literal lit, ast_manager & m, expr * const * bool_var2expr_map);
+    
+    std::ostream& display_compact(std::ostream & out, literal lit, expr * const * bool_var2expr_map);
+
+    std::ostream& display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map);
+
+    std::ostream& display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n");
 
     template<typename T>
     void neg_literals(unsigned num_lits, literal const * lits, T & result) {
@@ -112,9 +52,6 @@ namespace smt {
             result.push_back(~lits[i]);
     }
 
-    struct literal2unsigned { unsigned operator()(literal l) const { return l.index(); } };
-
-    typedef approx_set_tpl<literal, literal2unsigned> literal_approx_set;
 
     bool backward_subsumption(unsigned num_lits1, literal const * lits1, unsigned num_lits2, literal const * lits2);
 };

src/smt/smt_model_checker.cpp

@@ -319,7 +319,14 @@ namespace smt {
     struct scoped_ctx_push {
         context* c;
         scoped_ctx_push(context* c): c(c) { c->push(); }
-        ~scoped_ctx_push() { c->pop(1); }
+        ~scoped_ctx_push() { 
+            try {
+                c->pop(1);
+            }
+            catch (...) {
+                ;
+            }
+        }
     };
 
     /**

src/smt/smt_parallel.cpp

@@ -193,15 +193,26 @@ namespace smt {
 
             }
             catch (z3_error & err) {
+                if (finished_id == UINT_MAX) {
                     error_code = err.error_code();
                     ex_kind = ERROR_EX;
                     done = true;
                 }
+            }
             catch (z3_exception & ex) {
+                if (finished_id == UINT_MAX) {
                     ex_msg = ex.msg();
                     ex_kind = DEFAULT_EX;
                     done = true;
                 }
+            }
+            catch (...) {
+                if (finished_id == UINT_MAX) {
+                    ex_msg = "unknown exception";
+                    ex_kind = ERROR_EX;
+                    done = true;
+                }
+            }
         };
 
         // for debugging:  num_threads = 1;

src/smt/smt_relevancy.cpp

@@ -333,6 +333,7 @@ namespace smt {
                 if (e != nullptr) {
                     enode * curr = e;
                     do {
+                        if (!is_relevant_core(curr->get_expr()))
                             set_relevant(curr->get_expr());
                         curr = curr->get_next();
                     }

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -190,6 +190,8 @@ protected:
             parent_pos = todo.back().m_parent;
             self_idx   = todo.back().m_idx;
             n = names.back();
+            bool found = false;
+
             
             if (cache.contains(e)) {
                 goto done;
@@ -213,23 +215,34 @@ protected:
             sz = a->get_num_args();            
             n2 = nullptr;
 
-            for (unsigned i = 0; i < sz; ++i) {
+
-                expr* arg = a->get_arg(i);
-                if (cache.find(arg, path_r)) {
             //
             // This is a single traversal version of the context
             // simplifier. It simplifies only the first occurrence of 
             // a sub-term with respect to the context.
             //                                        
 
-                    if (path_r.m_parent == self_pos && path_r.m_idx == i) {
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* arg = a->get_arg(i);
+                if (cache.find(arg, path_r) &&
+                    path_r.m_parent == self_pos && path_r.m_idx == i) {
                     args.push_back(path_r.m_expr);
+                    found = true;
+                    continue;
                 }
-                    else {
                 args.push_back(arg);
             }
-                }
+
-                else if (!n2 && !m.is_value(arg)) {
+            //
+            // the context is not equivalent to top-level 
+            // if it is already simplified.
+            // Bug exposes such a scenario #5256
+            // 
+            if (!found) {
+                args.reset();            
+                for (unsigned i = 0; i < sz; ++i) {
+                    expr* arg = a->get_arg(i);
+                    if (!n2 && !m.is_value(arg)) {
                         n2 = mk_fresh(id, arg->get_sort());
                         trail.push_back(n2);
                         todo.push_back(expr_pos(self_pos, ++child_id, i, arg));
@@ -240,10 +253,12 @@ protected:
                         args.push_back(arg);
                     }
                 }
+            }
             m_mk_app(a->get_decl(), args.size(), args.data(), res);
             trail.push_back(res);
             // child needs to be visited.
             if (n2) {
+                SASSERT(!found);
                 m_solver.push();
                 tmp = m.mk_eq(res, n);
                 m_solver.assert_expr(tmp);

src/smt/theory_lra.cpp

@@ -976,17 +976,14 @@ public:
     }
         
     void internalize_eq_eh(app * atom, bool_var) {
-        if (!ctx().get_fparams().m_arith_eager_eq_axioms)
-            return;
         expr* lhs = nullptr, *rhs = nullptr;
         VERIFY(m.is_eq(atom, lhs, rhs));
         enode * n1 = get_enode(lhs);
         enode * n2 = get_enode(rhs);
         TRACE("arith_verbose", tout << mk_pp(atom, m) << " " << is_arith(n1) << " " << is_arith(n2) << "\n";);
-        if (is_arith(n1) && is_arith(n2) && n1 != n2) {
+        if (is_arith(n1) && is_arith(n2) && n1 != n2) 
             m_arith_eq_adapter.mk_axioms(n1, n2);
     }
-    }
 
     void assign_eh(bool_var v, bool is_true) {
         TRACE("arith", tout << mk_pp(ctx().bool_var2expr(v), m) << " " << (literal(v, !is_true)) << "\n";);
@@ -1085,7 +1082,6 @@ public:
     }
 
     void relevant_eh(app* n) {
-        TRACE("arith", tout << mk_pp(n, m) << "\n";);
         expr* n1, *n2;
         if (a.is_mod(n, n1, n2)) 
             mk_idiv_mod_axioms(n1, n2);
@@ -2083,7 +2079,7 @@ public:
             bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
             m_to_check.push_back(bv);
             api_bound* b = nullptr;
-            TRACE("arith", tout << "propagate: " << bv << "\n";);
+            TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n";);
             if (m_bool_var2bound.find(bv, b)) {
                 assert_bound(bv, is_true, *b);
             }
@@ -2642,14 +2638,14 @@ public:
             if (sign)
                 lit2.neg();
         }
-        TRACE("arith", 
-              ctx().display_literal_verbose(tout, lit1);
-              ctx().display_literal_verbose(tout << " => ", lit2);
-              tout << "\n";);
         updt_unassigned_bounds(v, -1);
         ++m_stats.m_bound_propagations2;
         reset_evidence();
         m_core.push_back(lit1);
+        TRACE("arith", 
+              ctx().display_literals_verbose(tout, m_core);
+              ctx().display_literal_verbose(tout << " => ", lit2);
+              tout << "\n";);
         m_params.push_back(parameter(m_farkas));
         m_params.push_back(parameter(rational(1)));
         m_params.push_back(parameter(rational(1)));

src/smt/theory_str.h

@@ -107,54 +107,6 @@ public:
     }
 };
 
-struct c_hash { unsigned operator()(char u) const { return (unsigned)u; } };
-struct c_eq { bool operator()(char u1, char u2) const { return u1 == u2; } };
-
-class nfa {
-protected:
-    bool m_valid;
-    unsigned m_next_id;
-
-    unsigned next_id() {
-        unsigned retval = m_next_id;
-        ++m_next_id;
-        return retval;
-    }
-
-    unsigned m_start_state;
-    unsigned m_end_state;
-
-    std::map<unsigned, std::map<char, unsigned> > transition_map;
-    std::map<unsigned, std::set<unsigned> > epsilon_map;
-
-    void make_transition(unsigned start, char symbol, unsigned end) {
-        transition_map[start][symbol] = end;
-    }
-
-    void make_epsilon_move(unsigned start, unsigned end) {
-        epsilon_map[start].insert(end);
-    }
-
-    // Convert a regular expression to an e-NFA using Thompson's construction
-    void convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u);
-
-public:
-    nfa(seq_util & u, expr * e)
-: m_valid(true), m_next_id(0), m_start_state(0), m_end_state(0) {
-        convert_re(e, m_start_state, m_end_state, u);
-    }
-
-    nfa() : m_valid(false), m_next_id(0), m_start_state(0), m_end_state(0) {}
-
-    bool is_valid() const {
-        return m_valid;
-    }
-
-    void epsilon_closure(unsigned start, std::set<unsigned> & closure);
-
-    bool matches(zstring input);
-};
-
 class regex_automaton_under_assumptions {
 protected:
     expr * re_term;
@@ -489,7 +441,6 @@ protected:
     obj_hashtable<expr> regex_terms;
     obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]
     obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
-    obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
     obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
     obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
     obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
@@ -718,15 +669,14 @@ protected:
     void check_consistency_contains(expr * e, bool is_true);
 
     int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
-            std::map<expr*, std::set<expr*> > & unrollGroupMap, std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
+            std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
     void trace_ctx_dep(std::ofstream & tout,
             std::map<expr*, expr*> & aliasIndexMap,
             std::map<expr*, expr*> & var_eq_constStr_map,
             std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
             std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
             std::map<expr*, expr*> & concat_eq_constStr_map,
-            std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map,
+            std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map);
-            std::map<expr*, std::set<expr*> > & unrollGroupMap);
 
     bool term_appears_as_subterm(expr * needle, expr * haystack);
     void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,

src/tactic/arith/pb2bv_tactic.cpp

@@ -657,13 +657,14 @@ private:
                         SASSERT(pos);                        
                         r = m.mk_true();
                     }
-                    else {
+                    else if ((c.is_zero() && k == GE) ||
-                        SASSERT((c.is_zero() && k == GE) ||
+                             (c.is_one() && k == LE)) {
-                                (c.is_one() && k == LE));
                         // unit 0 >= x, 1 <= x
                         SASSERT(pos);
                         r = mk_unit(rhs, k == GE);
                     }
+                    else 
+                        throw_non_pb(t);
                     return;
                 }
                 throw_non_pb(t);
@@ -985,7 +986,7 @@ private:
 
         void throw_tactic(expr* e) {
             std::stringstream strm;
-            strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m);
+            strm << "goal is in a fragment not supported by pb2bv. Offending expression: " << mk_pp(e, m);
             throw tactic_exception(strm.str());
         }
     };

src/test/finder.cpp

@@ -13,7 +13,7 @@ static void _init_solver(sat::solver& s)
     s.mk_var();
 }
 
-static void _mk_clause4(sat::solver& s, sat::literal w, sat::literal x, sat::literal y, sat::literal z)
+static void _mk_clause4(sat::solver& s, sat::literal const & w, sat::literal const& x, sat::literal const& y, sat::literal const& z)
 {
     sat::literal lits[] = {w, x, y, z};
     s.mk_clause(4, lits);
@@ -41,10 +41,10 @@ static void tst_single_mux() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({ 0, true }, { 1, true }, { 3, false });
+    s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false));
-    s.mk_clause({ 0, true }, { 1, false }, { 3, true });
+    s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true));
-    s.mk_clause({ 0, false }, { 2, true }, { 3, false });
+    s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false));
-    s.mk_clause({ 0, false }, { 2, false }, { 3, true });
+    s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_mux), "mux", 7, 0, 3, 5);
 }
@@ -54,12 +54,12 @@ static void tst_single_maj() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({ 0, false }, { 1, false }, { 3, true });
+    s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, true));
-    s.mk_clause({ 0, false }, { 2, false }, { 3, true });
+    s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({ 1, false }, { 2, false }, { 3, true });
+    s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({ 0, true }, { 1, true }, { 3, false });
+    s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false));
-    s.mk_clause({ 0, true }, { 2, true }, { 3, false });
+    s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false));
-    s.mk_clause({ 1, true }, { 2, true }, { 3, false });
+    s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_maj), "maj", 6, 0, 2, 4);
 }
@@ -69,10 +69,10 @@ static void tst_single_orand() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, false}, {3, true});
+    s.mk_clause(sat::literal(0, false), sat::literal(3, true));
-    s.mk_clause({1, false}, {2, false}, {3, true});
+    s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({0, true}, {1, true}, {3, false});
+    s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, false));
-    s.mk_clause({0, true}, {2, true}, {3, false});
+    s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_orand), "orand", 6, 0, 2, 4);
 }
@@ -82,11 +82,11 @@ static void tst_single_and() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    sat::literal ls1[] = {{0, true}, {1, true}, {2, true}, {3, false}};
+    sat::literal ls1[] = {sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false)};
     s.mk_clause(4, ls1);
-    s.mk_clause({0, false}, {3, true});
+    s.mk_clause(sat::literal(0, false), sat::literal(3, true));
-    s.mk_clause({1, false}, {3, true});
+    s.mk_clause(sat::literal(1, false), sat::literal(3, true));
-    s.mk_clause({2, false}, {3, true});
+    s.mk_clause(sat::literal(2, false), sat::literal(3, true));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_and), "and", 6, 0, 2, 4);
 }
@@ -96,14 +96,14 @@ static void tst_single_xor() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true));
-    _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, true});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, true});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xor), "xor", 1, 3, 4, 6);
 }
@@ -113,12 +113,12 @@ static void tst_single_andxor() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, true}, {1, false}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true));
-    s.mk_clause({0, true}, {2, false}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(2, false), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false));
-    s.mk_clause({0, false}, {1, false}, {3, false});
+    s.mk_clause(sat::literal(0, false), sat::literal(1, false), sat::literal(3, false));
-    s.mk_clause({0, false}, {2, false}, {3, false});
+    s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, true}, {2, true}, {3, true});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, true), sat::literal(3, true));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_andxor), "andxor", 0, 6, 2, 4);
 }
@@ -128,11 +128,11 @@ static void tst_single_xorand() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, false}, {3, true});
+    s.mk_clause(sat::literal(0, false), sat::literal(3, true));
-    s.mk_clause({1, false}, {2, false}, {3, true});
+    s.mk_clause(sat::literal(1, false), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({1, true}, {2, true}, {3, true});
+    s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, true}, {1, false}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_xorand), "xorand", 6, 0, 3, 5);
 }
@@ -142,11 +142,11 @@ static void tst_single_gamble() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, true}, {1, false}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(1, false), sat::literal(3, true));
-    s.mk_clause({1, true}, {2, false}, {3, true});
+    s.mk_clause(sat::literal(1, true), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({0, false}, {2, true}, {3, true});
+    s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, true));
-    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, true}, {1, true}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, true), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_gamble), "gamble", 6, 0, 2, 4);
 }
@@ -156,13 +156,13 @@ static void tst_single_onehot() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, true}, {1, true}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true));
-    s.mk_clause({0, true}, {2, true}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true));
-    s.mk_clause({1, true}, {2, true}, {3, true});
+    s.mk_clause(sat::literal(1, true), sat::literal(2, true), sat::literal(3, true));
-    _mk_clause4(s, {0, false}, {1, false}, {2, false}, {3, true});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, false), sat::literal(3, true));
-    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, true}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, true), sat::literal(2, false), sat::literal(3, false));
-    _mk_clause4(s, {0, false}, {1, false}, {2, true}, {3, false});
+    _mk_clause4(s, sat::literal(0, false), sat::literal(1, false), sat::literal(2, true), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_onehot), "onehot", 6, 0, 2, 4);
 }
@@ -172,11 +172,11 @@ static void tst_single_dot() {
     sat::solver s({}, r);
     _init_solver(s);
 
-    s.mk_clause({0, false}, {2, false}, {3, true});
+    s.mk_clause(sat::literal(0, false), sat::literal(2, false), sat::literal(3, true));
-    s.mk_clause({0, true}, {1, true}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(1, true), sat::literal(3, true));
-    s.mk_clause({0, true}, {2, true}, {3, true});
+    s.mk_clause(sat::literal(0, true), sat::literal(2, true), sat::literal(3, true));
-    s.mk_clause({0, false}, {2, true}, {3, false});
+    s.mk_clause(sat::literal(0, false), sat::literal(2, true), sat::literal(3, false));
-    _mk_clause4(s, {0, true}, {1, false}, {2, false}, {3, false});
+    _mk_clause4(s, sat::literal(0, true), sat::literal(1, false), sat::literal(2, false), sat::literal(3, false));
 
     _check_finder(s, std::mem_fn(&sat::npn3_finder::set_on_dot), "dot", 6, 0, 2, 4);
 }

src/util/gparams.cpp

@@ -137,6 +137,7 @@ struct gparams::imp {
     smap<params_ref* >   m_module_params;
     params_ref           m_params;
     region               m_region;
+    std::string          m_buffer;
 
     void check_registered() {
         if (m_modules_registered)
@@ -651,3 +652,8 @@ void gparams::finalize() {
     dealloc(g_imp);
     DEALLOC_MUTEX(gparams_mux);
 }
+
+std::string& gparams::g_buffer() {
+    SASSERT(g_imp);
+    return g_imp->m_buffer;
+}

src/util/gparams.h

@@ -26,6 +26,9 @@ class gparams {
 public:
     typedef default_exception exception;
 
+    static std::string& g_buffer();
+
+
     /**
        \brief Reset all global and module parameters.
     */

src/util/sat_literal.h

@@ -0,0 +1,194 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_literal.h
+
+Abstract:
+
+    Literal datatype
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-05-21.
+
+--*/
+#pragma once
+
+#include "util/lbool.h"
+#include "util/vector.h"
+#include "util/uint_set.h"
+
+namespace sat {
+
+    /**
+       \brief A boolean variable is just an integer.
+    */
+    typedef unsigned bool_var;
+
+    typedef svector<bool_var> bool_var_vector;
+
+    const bool_var null_bool_var  = UINT_MAX >> 1;
+
+    /**
+       \brief The literal b is represented by the value 2*b, and
+       the literal (not b) by the value 2*b + 1
+    */
+    class literal {
+        unsigned  m_val;
+    public:
+        literal():m_val(null_bool_var << 1) {
+            SASSERT(var() == null_bool_var && !sign());
+        }
+
+        explicit literal(bool_var v, bool _sign = false):
+            m_val((v << 1) + static_cast<unsigned>(_sign)) {
+            SASSERT(var() == v);
+            SASSERT(sign() == _sign);
+        }
+
+        bool_var var() const {
+            return m_val >> 1;
+        }
+
+        bool sign() const {
+            return m_val & 1ul;
+        }
+
+        literal unsign() const {
+            literal l;
+            l.m_val = m_val & ~1;
+            return l;
+        }
+
+        unsigned index() const {
+            return m_val;
+        }
+
+        void neg() {
+            m_val = m_val ^ 1;
+        }
+
+        friend literal operator~(literal l) {
+            l.m_val = l.m_val ^1;
+            return l;
+        }
+
+        unsigned to_uint() const { return m_val; }
+
+        unsigned hash() const { return to_uint(); }
+
+        friend literal to_literal(unsigned x);
+        friend bool operator<(literal const & l1, literal const & l2);
+        friend bool operator==(literal const & l1, literal const & l2);
+        friend bool operator!=(literal const & l1, literal const & l2);
+    };
+
+    const literal null_literal;
+    struct literal_hash : obj_hash<literal> {};
+
+    inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; }
+    inline bool operator<(literal const & l1, literal const & l2) { return l1.m_val < l2.m_val;  }
+    inline bool operator==(literal const & l1, literal const & l2) { return l1.m_val == l2.m_val; }
+    inline bool operator!=(literal const & l1, literal const & l2) { return l1.m_val != l2.m_val; }
+
+
+    typedef svector<literal> literal_vector;
+    typedef std::pair<literal, literal> literal_pair;
+
+    struct literal2unsigned { unsigned operator()(literal l) const { return l.to_uint(); } };
+
+    typedef approx_set_tpl<literal, literal2unsigned, unsigned> literal_approx_set;
+
+    typedef approx_set_tpl<bool_var, u2u, unsigned> var_approx_set;
+
+
+    inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
+
+    typedef tracked_uint_set uint_set;
+
+    typedef uint_set bool_var_set;
+
+    class literal_set {
+        uint_set m_set;
+    public:
+        literal_set(literal_vector const& v) {
+            for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
+        }
+        literal_set() {}
+        literal_vector to_vector() const {
+            literal_vector result;
+            for (literal lit : *this) result.push_back(lit);
+            return result;
+        }
+        literal_set& operator=(literal_vector const& v) {
+            reset();
+            for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
+            return *this;
+        }
+
+        void insert(literal l) { m_set.insert(l.index()); }
+        void remove(literal l) { m_set.remove(l.index()); }
+        literal pop() { return to_literal(m_set.erase()); }
+        bool contains(literal l) const { return m_set.contains(l.index()); }
+        bool empty() const { return m_set.empty(); }
+        unsigned size() const { return m_set.size(); }
+        void reset() { m_set.reset(); }
+        void finalize() { m_set.finalize(); }
+        class iterator {
+            uint_set::iterator m_it;
+        public:
+            iterator(uint_set::iterator it):m_it(it) {}
+            literal operator*() const { return to_literal(*m_it); }
+            iterator& operator++() { ++m_it; return *this; }
+            iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }
+            bool operator==(iterator const& it) const { return m_it == it.m_it; }
+            bool operator!=(iterator const& it) const { return m_it != it.m_it; }
+        };
+        iterator begin() const { return iterator(m_set.begin()); }
+        iterator end() const { return iterator(m_set.end()); }
+        literal_set& operator&=(literal_set const& other) {
+            m_set &= other.m_set;
+            return *this;
+        }
+        literal_set& operator|=(literal_set const& other) {
+            m_set |= other.m_set;
+            return *this;
+        }
+    };
+
+    struct dimacs_lit {
+        literal m_lit;
+        dimacs_lit(literal l):m_lit(l) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, dimacs_lit const & dl) {
+        literal l = dl.m_lit;
+        if (l.sign()) out << "-" << (l.var() + 1);
+        else out << (l.var() + 1);
+        return out;
+    }
+
+    struct mk_lits_pp {
+        unsigned        m_num;
+        literal const * m_lits;
+        mk_lits_pp(unsigned num, literal const * ls):m_num(num), m_lits(ls) {}
+    };
+
+    inline std::ostream & operator<<(std::ostream & out, mk_lits_pp const & ls) {
+        for (unsigned i = 0; i < ls.m_num; i++) {
+            if (i > 0) out << " ";
+            out << ls.m_lits[i];
+        }
+        return out;
+    }
+
+    inline std::ostream & operator<<(std::ostream & out, literal_vector const & ls) {
+        return out << mk_lits_pp(ls.size(), ls.data());
+    }
+
+};
+
+inline std::ostream & operator<<(std::ostream & out, sat::literal l) { if (l == sat::null_literal) out << "null"; else out << (l.sign() ? "-" : "") << l.var(); return out; }
+

src/util/scoped_timer.cpp

@@ -153,4 +153,5 @@ void scoped_timer::finalize() {
         }
     }
     num_workers = 0;
+    available_workers.clear();
 }