Integrated structured branch into unstable branch (the official 'working in progress' branch)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/dead/assertion_stack.cpp

@@ -0,0 +1,314 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    assertion_stack.cpp
+
+Abstract:
+    
+    Assertion stacks
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-17
+
+Revision History:
+
+--*/
+#include"assertion_stack.h"
+#include"well_sorted.h"
+#include"ast_smt2_pp.h"
+#include"ref_util.h"
+
+assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled):
+    m_manager(m),
+    m_forbidden(m),
+    m_csubst(m, core_enabled),
+    m_fsubst(m, core_enabled) {
+    init(m.proofs_enabled(), models_enabled, core_enabled);
+}
+
+assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
+    m_manager(m),
+    m_forbidden(m),
+    m_csubst(m, core_enabled, proofs_enabled),
+    m_fsubst(m, core_enabled, proofs_enabled) {
+    init(proofs_enabled, models_enabled, core_enabled);
+}
+
+void assertion_stack::init(bool proofs_enabled, bool models_enabled, bool core_enabled) {
+    m_ref_count      = 0;
+    m_models_enabled = models_enabled;
+    m_proofs_enabled = proofs_enabled;
+    m_core_enabled   = core_enabled;
+    m_inconsistent   = false;
+    m_form_qhead     = 0;
+}
+
+assertion_stack::~assertion_stack() {
+    reset();
+}
+
+void assertion_stack::reset() {
+    m_inconsistent = false;
+    m_form_qhead   = 0;
+    m_mc_qhead     = 0;
+    dec_ref_collection_values(m_manager, m_forms);
+    dec_ref_collection_values(m_manager, m_proofs);
+    dec_ref_collection_values(m_manager, m_deps);
+    m_forbidden_set.reset();
+    m_forbidden.reset();
+    m_csubst.reset();
+    m_fsubst.reset();
+    m_mc.reset();
+    m_scopes.reset();
+}
+
+void assertion_stack::expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) {
+    // TODO: expand definitions
+    new_f   = f;
+    new_pr  = pr;
+    new_dep = dep;
+}
+
+void assertion_stack::push_back(expr * f, proof * pr, expr_dependency * d) {
+    if (m().is_true(f))
+        return;
+    if (m().is_false(f)) {
+        m_inconsistent = true;
+    }
+    else {
+        SASSERT(!m_inconsistent);
+    }
+    m().inc_ref(f);
+    m_forms.push_back(f);
+    if (proofs_enabled()) {
+        m().inc_ref(pr);
+        m_proofs.push_back(pr);
+    }
+    if (unsat_core_enabled()) {
+        m().inc_ref(d);
+        m_deps.push_back(d);
+    }
+}
+
+void assertion_stack::quick_process(bool save_first, expr * & f, expr_dependency * d) {
+    if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
+        if (!save_first) {
+            push_back(f, 0, d);
+        }
+        return; 
+    }
+    typedef std::pair<expr *, bool> expr_pol;
+    sbuffer<expr_pol, 64> todo;
+    todo.push_back(expr_pol(f, true));
+    while (!todo.empty()) {
+        if (m_inconsistent)
+            return;
+        expr_pol p  = todo.back();
+        expr * curr = p.first;
+        bool   pol  = p.second;
+        todo.pop_back();
+        if (pol && m().is_and(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), true));
+            }
+        }
+        else if (!pol && m().is_or(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), false));
+            }
+        }
+        else if (m().is_not(curr)) {
+            todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
+        }
+        else {
+            if (!pol) 
+                curr = m().mk_not(curr);
+            if (save_first) {
+                f  = curr;
+                save_first = false;
+            }
+            else {
+                push_back(curr, 0, d);
+            }
+        }
+    }
+}
+
+void assertion_stack::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr);
+    }
+}
+
+void assertion_stack::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        expr * child = f->get_arg(i);
+        if (m().is_not(child)) {
+            expr * not_child = to_app(child)->get_arg(0);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+        else {
+            expr_ref not_child(m());
+            not_child = m().mk_not(child);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+    }
+}
+
+void assertion_stack::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    if (m().is_and(f)) 
+        process_and(save_first, to_app(f), pr, d, out_f, out_pr);
+    else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) 
+        process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
+    else if (save_first) {
+        out_f  = f;
+        out_pr = pr;
+    }
+    else {
+        push_back(f, pr, d);
+    }
+}
+
+void assertion_stack::slow_process(expr * f, proof * pr, expr_dependency * d) {
+    expr_ref out_f(m());
+    proof_ref out_pr(m());
+    slow_process(false, f, pr, d, out_f, out_pr);
+}
+
+
+void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
+    expand(f, pr, d, new_f, new_pr, new_d);
+    if (proofs_enabled())
+        slow_process(f, pr, d);
+    else
+        quick_process(false, f, d);
+}
+
+#ifdef Z3DEBUG
+// bool assertion_stack::is_expanded(expr * f) {
+// }
+#endif
+
+void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(i >= m_form_qhead);
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    if (proofs_enabled()) {
+        expr_ref out_f(m());
+        proof_ref out_pr(m());
+        slow_process(true, f, pr, d, out_f, out_pr);
+        if (!m_inconsistent) {
+            if (m().is_false(out_f)) {
+                push_back(out_f, out_pr, d);
+            }
+            else {
+                m().inc_ref(out_f);
+                m().dec_ref(m_forms[i]);
+                m_forms[i] = out_f;
+
+                m().inc_ref(out_pr);
+                m().dec_ref(m_proofs[i]);
+                m_proofs[i] = out_pr;
+
+                if (unsat_core_enabled()) {
+                    m().inc_ref(d);
+                    m().dec_ref(m_deps[i]);
+                    m_deps[i] = d;
+                }
+            }
+        }
+    }
+    else {
+        quick_process(true, f, d);
+        if (!m_inconsistent) {
+            if (m().is_false(f)) {
+                push_back(f, 0, d);
+            }
+            else {
+                m().inc_ref(f);
+                m().dec_ref(m_forms[i]);
+                m_forms[i] = f;
+
+                if (unsat_core_enabled()) {
+                    m().inc_ref(d);
+                    m().dec_ref(m_deps[i]);
+                    m_deps[i] = d;
+                }
+            }
+        }
+    }
+}
+
+void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(i >= m_form_qhead);
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
+    expand(f, pr, d, new_f, new_pr, new_d);
+    update(i, new_f, new_pr, new_d);
+}
+
+void assertion_stack::push() {
+}
+
+void assertion_stack::pop(unsigned num_scopes) {
+}
+
+void assertion_stack::commit() {
+}
+
+void assertion_stack::add_filter(func_decl * f) const {
+}
+
+void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) {
+    
+}
+
+void assertion_stack::add_definition(func_decl * f, quantifier * q, proof * pr, expr_dependency * dep) {
+}
+
+void assertion_stack::convert(model_ref & m) {
+}
+
+void assertion_stack::display(std::ostream & out) const {
+    out << "(assertion-stack";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  ";
+        if (i == m_form_qhead) 
+            out << "==>\n";
+        out << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << ")" << std::endl;
+}
+
+bool assertion_stack::is_well_sorted() const {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * t = form(i);
+        if (!::is_well_sorted(m(), t))
+            return false;
+    }
+    return true;
+}

src/dead/assertion_stack.h

@@ -0,0 +1,141 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    assertion_stack.h
+
+Abstract:
+
+    It should be viewed as the "goal" object for incremental solvers.
+    The main difference is the support of push/pop operations.  Like a
+    goal, an assertion_stack contains expressions, their proofs (if
+    proof generation is enabled), and dependencies (if unsat core
+    generation is enabled).
+
+    The assertions on the stack are grouped by scope levels. Scoped
+    levels are created using push, and removed using pop. 
+
+    Assertions may be "committed". Whenever a push is executed, all
+    "uncommitted" assertions are automatically committed. 
+    Only uncommitted assertions can be simplified/reduced.
+
+    An assertion set has a limited model converter that only supports
+    definitions (for variable/function elimination) and filters (for fresh
+    symbols introduced by tactics).
+
+    Some tactics support assertion_stacks and can be applied to them.
+    However, a tactic can only access the assertions on the top level.
+    The assertion stack also informs the tactic which declarations 
+    can't be eliminated since they occur in the already committed part. 
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-17
+
+Revision History:
+
+--*/
+#ifndef _ASSERTION_STACK_H_
+#define _ASSERTION_STACK_H_
+
+#include"ast.h"
+#include"model.h"
+#include"expr_substitution.h"
+#include"macro_substitution.h"
+
+class assertion_stack {
+    ast_manager &                m_manager;
+    unsigned                     m_ref_count;
+    bool                         m_models_enabled;  // model generation is enabled.
+    bool                         m_proofs_enabled;  // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true
+    bool                         m_core_enabled;    // unsat core extraction is enabled.
+    bool                         m_inconsistent; 
+    ptr_vector<expr>             m_forms;
+    ptr_vector<proof>            m_proofs;
+    ptr_vector<expr_dependency>  m_deps;
+    unsigned                     m_form_qhead; // position of first uncommitted assertion
+    unsigned                     m_mc_qhead;
+
+    // Set of declarations that can't be eliminated
+    obj_hashtable<func_decl>     m_forbidden_set;
+    func_decl_ref_vector         m_forbidden;
+    
+    // Limited model converter support, it supports only extensions
+    // and filters.
+    // It should be viewed as combination of extension_model_converter and 
+    // filter_model_converter for goals.
+    expr_substitution            m_csubst;  // substitution for eliminated constants
+    macro_substitution           m_fsubst;  // substitution for eliminated functions
+
+    // Model converter is just a sequence of tagged pointers.
+    // Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst.
+    // Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model.
+    ptr_vector<func_decl>        m_mc;      
+    
+    struct scope {
+        unsigned                 m_forms_lim;
+        unsigned                 m_forbidden_vars_lim;
+        unsigned                 m_mc_lim;
+        bool                     m_inconsistent_old;
+    };
+    
+    svector<scope>               m_scopes;
+
+    void init(bool proofs_enabled, bool models_enabled, bool core_enabled);
+    void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep);
+    void push_back(expr * f, proof * pr, expr_dependency * d);
+    void quick_process(bool save_first, expr * & f, expr_dependency * d);
+    void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(expr * f, proof * pr, expr_dependency * d);
+
+public:
+    assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true);
+    assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled);
+    ~assertion_stack();
+
+    void reset();
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
+    
+    ast_manager & m() const { return m_manager; }
+    
+    bool models_enabled() const { return m_models_enabled; }
+    bool proofs_enabled() const { return m_proofs_enabled; }
+    bool unsat_core_enabled() const { return m_core_enabled; }
+    bool inconsistent() const { return m_inconsistent; }
+    
+    unsigned size() const { return m_forms.size(); }
+    unsigned qhead() const { return m_form_qhead; }
+    expr * form(unsigned i) const { return m_forms[i]; }
+    proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m_proofs[i]) : 0; }
+    expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m_deps[i] : 0; }
+    
+    void assert_expr(expr * f, proof * pr, expr_dependency * d);
+    void assert_expr(expr * f) {
+        assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
+    }
+    void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
+    void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0);
+    
+    void commit();
+    void push();
+    void pop(unsigned num_scopes);
+    unsigned scope_lvl() const { return m_scopes.size(); }
+  
+    bool is_well_sorted() const;
+
+    bool is_forbidden(func_decl * f) const { return m_forbidden_set.contains(f); }
+    void add_filter(func_decl * f) const;
+    void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep);
+    void add_definition(func_decl * f, quantifier * q, proof * pr, expr_dependency * dep);
+
+    void convert(model_ref & m);
+
+    void display(std::ostream & out) const;
+};
+
+#endif

src/dead/big_rational.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    big_rational.h
+
+Abstract:
+
+    Big rational numbers
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-09-18.
+
+Revision History:
+
+--*/
+#ifndef _BIG_RATIONAL_H_
+#define _BIG_RATIONAL_H_
+
+#ifdef _WINDOWS
+#include"..\msbig_rational\msbig_rational.h"
+#else
+#ifdef NO_GMP
+#include"dummy_big_rational.h"
+#else
+#include"gmp_big_rational.h"
+#endif
+#endif
+
+#endif /* _BIG_RATIONAL_H_ */
+

src/dead/configure.in

@@ -0,0 +1,168 @@
+AC_PREREQ(2.50)
+AC_INIT(lib/util.h)
+
+ARITH="internal"
+AC_ARG_WITH([gmp], [AS_HELP_STRING([--with-gmp], [Use GMP for multi-precision naturals (default=no)])], [use_gmp=yes], [use_gmp=no])
+AS_IF([test "$use_gmp" = "yes"],[
+  ARITH="gmp"
+  CPPFLAGS="$CPPFLAGS -D_MP_GMP"
+],[
+  CPPFLAGS="$CPPFLAGS -D_MP_INTERNAL"
+])
+AC_SUBST(EXTRA_LIB_SRCS)
+
+AC_ARG_WITH(python,
+[AS_HELP_STRING([--with-python=PYTHON_PATH],
+		[specify the location of the python 2.x executable.])])
+
+PYTHON="python"
+if test "x$with_python" != x; then
+  PYTHON="$with_python"
+fi
+
+AC_SUBST(PYTHON)
+
+AC_PATH_PROG([D2U], [dos2unix], [no], [~/bin$PATH_SEPARATOR$PATH])
+AS_IF([test "$D2U" = "no"], [AC_MSG_ERROR(dos2unix not found)])
+AC_SUBST(D2U)
+
+AC_PROG_CXX(g++)
+AC_PROG_MAKE_SET
+
+AC_LANG_CPLUSPLUS
+
+host_os=`uname -s`
+
+AS_IF([test "$host_os" = "Darwin"], [
+  PLATFORM=osx
+  SO_EXT=dylib
+  SLIBFLAGS="-dynamiclib -fopenmp"
+  COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)"
+  STATIC_FLAGS=
+  CPPFLAGS+=""
+], [test "$host_os" = "Linux"], [
+  PLATFORM=linux
+  SO_EXT=so
+  LDFLAGS=-lrt
+  SLIBFLAGS="-shared -fopenmp"
+  COMP_VERSIONS=
+  STATIC_FLAGS=-static
+], [test "${host_os:0:6}" = "CYGWIN"], [
+   PLATFORM=win
+   SO_EXT=dll
+   LDFLAGS=
+   SLIBFLAGS="-shared -fopenmp"
+   COMP_VERSIONS=
+   STATIC_FLAGS=-static
+   CPPFLAGS+=" -D_CYGWIN"
+],
+[
+  AC_MSG_ERROR([Unknown host platform: $host_os])
+])
+AC_SUBST(PLATFORM)
+AC_SUBST(SO_EXT)
+AC_SUBST(SLIBFLAGS)
+AC_SUBST(COMP_VERSIONS)
+AC_SUBST(STATIC_FLAGS)
+
+cat > tst_python.py <<EOF
+from sys import version
+if version >= "3":
+   exit(1)
+exit(0)
+EOF
+
+if $PYTHON tst_python.py; then
+  HAS_PYTHON="1"
+  HAS_PYTHON_MSG="yes"
+cat > get_py_dir.py << EOF
+import distutils.sysconfig
+print distutils.sysconfig.get_python_lib()
+EOF
+  if $PYTHON get_py_dir.py > dir.txt; then
+    PYTHON_PACKAGE_DIR=`cat dir.txt`
+  else
+    HAS_PYTHON="0"
+    HAS_PYTHON_MSG="no"
+  fi
+  rm -f dir.txt
+  rm -f get_py_dir.py
+else
+  HAS_PYTHON="0"
+  HAS_PYTHON_MSG="no"
+fi
+AC_SUBST(PYTHON_PACKAGE_DIR)
+AC_SUBST(HAS_PYTHON)
+rm -f tst_python.py
+
+cat > tst64.c <<EOF
+    int main() {
+    	return sizeof(unsigned) == sizeof(void*);
+    }
+EOF
+
+AC_SUBST(EXTRA_LIBS)
+
+g++ $CPPFLAGS tst64.c -o tst64
+if ./tst64; then
+   dnl In 64-bit systems we have to compile using -fPIC
+   CPPFLAGS="$CPPFLAGS -D_AMD64_"
+   dnl Only enable use of thread local storage for 64-bit Linux. It is disabled for OSX and 32-bit Linux
+   if test $PLATFORM = "linux"; then
+      CPPFLAGS="$CPPFLAGS -D_USE_THREAD_LOCAL" 
+   fi
+   CXXFLAGS="-fPIC"
+   EXTRA_LIBS=""
+   dnl Rewrite -lz3-gmp to -lz3 in the files:
+   dnl  - test_capi/build-external-linux.sh 
+   dnl  - test_user_theory/build-external-linux.sh
+   dnl Reason: the library libz3-gmp.so is not available in 64-bit systems
+   dnl sed 's|lz3-gmp|lz3|' test_capi/build-external-linux.sh > tmp.sh
+   dnl mv tmp.sh test_capi/build-external-linux.sh
+   dnl sed 's|lz3-gmp|lz3|' test_user_theory/build-external-linux.sh > tmp.sh
+   dnl mv tmp.sh test_user_theory/build-external-linux.sh
+else
+   CXXFLAGS=""
+   dnl In 64-bit systems it is not possible to build a dynamic library using static gmp.
+   dnl EXTRA_LIBS="\$(BIN_DIR)/lib\$(Z3)-gmp.so"
+fi
+rm -f tst64.c
+rm -f tst64
+
+AC_SUBST(GMP_STATIC_LIB)
+GMP_STATIC_LIB=""
+
+if test "$ARITH" = "gmp"; then
+   AC_CHECK_HEADER([gmp.h], GMP='gmp', AC_MSG_ERROR([GMP include file not found]))
+   AC_SUBST(LIBS)
+   AC_CHECK_LIB(gmp, __gmpz_cmp, LIBS="-lgmp $LIBS", AC_MSG_ERROR([GMP library not found]))
+   dnl Look for libgmp.a at /usr/local/lib and /usr/lib
+   dnl TODO: make the following test more robust...
+   if test -e /usr/local/lib/libgmp.a; then
+      GMP_STATIC_LIB="/usr/local/lib/libgmp.a"
+   else if test -e /usr/lib/libgmp.a; then
+      GMP_STATIC_LIB="/usr/lib/libgmp.a"
+   else if test -e /usr/lib/libgmp.dll.a; then
+      GMP_STATIC_LIB="/usr/lib/libgmp.dll.a"
+   else
+      AC_MSG_ERROR([Failed to find libgmp.a])   
+   fi fi fi
+fi
+
+AC_PROG_CXXCPP
+
+AC_OUTPUT(Makefile)
+
+cat <<EOF
+
+Z3 was configured with success.
+Host platform:  $PLATFORM
+Arithmetic:     $ARITH
+Python Support: $HAS_PYTHON_MSG
+Python:         $PYTHON 
+Prefix:         $prefix
+
+Type 'make' to compile Z3.
+Type 'sudo make install' to install Z3.
+Type 'sudo make install-z3py' to install Z3 Python (Z3Py) bindings.
+EOF

src/dead/contains_var.h

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    contains_var.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-06-12.
+
+Revision History:
+
+--*/
+#ifndef _CONTAINS_VAR_H_
+#define _CONTAINS_VAR_H_
+
+class ast;
+
+bool contains_var(ast * n);
+
+#endif /* _CONTAINS_VAR_H_ */
+

src/dead/dl_simplifier_plugin.cpp

@@ -0,0 +1,64 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_simplifier_plugin.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-08-10
+
+Revision History:
+
+--*/
+
+#include"dl_simplifier_plugin.h"
+
+namespace datalog {
+
+    dl_simplifier_plugin::dl_simplifier_plugin(ast_manager& m) 
+        : simplifier_plugin(symbol("datalog_relation"), m),
+          m_util(m)
+    {}
+        
+    bool dl_simplifier_plugin::reduce(
+        func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) {
+        uint64 v1, v2;
+        switch(f->get_decl_kind()) {
+        case OP_DL_LT:
+            if (m_util.try_get_constant(args[0], v1) &&
+                m_util.try_get_constant(args[1], v2)) {
+                result = (v1 < v2)?m_manager.mk_true():m_manager.mk_false();
+                return true;
+            }
+            // x < x <=> false
+            if (args[0] == args[1]) {
+                result = m_manager.mk_false();
+                return true;
+            }
+            // x < 0 <=> false
+            if (m_util.try_get_constant(args[1], v2) && v2 == 0) {
+                result = m_manager.mk_false();
+                return true;
+            }
+            // 0 < x <=> 0 != x
+            if (m_util.try_get_constant(args[1], v1) && v1 == 0) {
+                result = m_manager.mk_not(m_manager.mk_eq(args[0], args[1]));
+                return true;
+            }
+            break;
+
+        default:
+            break;
+        }
+        return false;
+    }
+    
+};
+
+

src/dead/dl_simplifier_plugin.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_simplifier_plugin.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-08-10
+
+Revision History:
+
+--*/
+#ifndef _DL_SIMPLIFIER_PLUGIN_H_
+#define _DL_SIMPLIFIER_PLUGIN_H_
+
+#include"dl_decl_plugin.h"
+#include "simplifier_plugin.h"
+
+namespace datalog {
+
+    class dl_simplifier_plugin : public simplifier_plugin {
+        dl_decl_util  m_util;
+    public:
+        dl_simplifier_plugin(ast_manager& m);
+        
+        virtual bool reduce(func_decl * f, unsigned num_args, expr* const* args, expr_ref& result);
+        
+    };
+    
+};
+#endif /* _DL_SIMPLIFIER_PLUGIN_H_ */
+

src/dead/dummy_big_rational.h

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    dummy_big_rational.h
+
+Abstract:
+
+    Dummy big rational
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-09-26.
+
+Revision History:
+
+--*/
+
+#ifndef _DUMMY_BIG_RATIONAL_H_
+#define _DUMMY_BIG_RATIONAL_H_
+
+#include<string>
+#include"debug.h"
+
+class big_rational {
+public:
+    big_rational() { }
+    big_rational(int n) {}
+    ~big_rational() {}
+    void reset() {}
+    unsigned hash() const { return 0; }
+    void set(int num, int den) { UNREACHABLE(); }
+    void set(const char * str) { UNREACHABLE(); }
+    bool is_int() const { UNREACHABLE(); return false; }
+    long get_int() const { UNREACHABLE(); return 0; }
+    void neg() { UNREACHABLE(); }
+    big_rational & operator=(const big_rational & r) { UNREACHABLE(); return *this; }
+    bool operator==(const big_rational & r) const { UNREACHABLE(); return false; }
+    bool operator<(const big_rational & r) const { UNREACHABLE(); return false; }
+    big_rational & operator+=(const big_rational & r) { UNREACHABLE(); return *this; }
+    big_rational & operator-=(const big_rational & r) { UNREACHABLE(); return *this; }
+    big_rational & operator*=(const big_rational & r) { UNREACHABLE(); return *this; }
+    big_rational & operator/=(const big_rational & r) { UNREACHABLE(); return *this; }
+    big_rational & operator%=(const big_rational & r) { UNREACHABLE(); return *this; }
+    friend void div(const big_rational & r1, const big_rational & r2, big_rational & result) { UNREACHABLE(); }
+    void get_numerator(big_rational & result) { UNREACHABLE(); }
+    void get_denominator(big_rational & result) { UNREACHABLE(); }
+    void get_floor(big_rational & result) { UNREACHABLE(); }
+    std::string to_string() const { UNREACHABLE(); return std::string(""); }
+};
+
+#endif /* _DUMMY_BIG_RATIONAL_H_ */
+

src/dead/expr_weight.cpp

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    expr_weight.cpp
+
+Abstract:
+
+    Functor for computing the weight of an expression.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-11
+
+Notes:
+
+--*/
+#include"expr_weight.h"
+#include"recurse_expr_def.h"
+
+template class recurse_expr<weight, expr_weight_visitor, true>;
+
+weight expr_weight_visitor::visit(app const * n, weight const * args) {
+    weight r(1);
+    unsigned j = n->get_num_args();
+    while (j > 0) {
+        --j;
+        r += args[j];
+    }
+    return r;
+}

src/dead/expr_weight.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    expr_weight.h
+
+Abstract:
+
+    Functor for computing the weight of an expression.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-11
+
+Notes:
+
+--*/
+#ifndef _EXPR_WEIGHT_H_
+#define _EXPR_WEIGHT_H_
+
+#include"recurse_expr.h"
+#include"approx_nat.h"
+
+typedef approx_nat weight;
+
+struct expr_weight_visitor {
+    weight visit(var * n) { return weight(1); }
+    weight visit(app const * n, weight const * args);
+    weight visit(quantifier * n, weight body, weight *, weight *) { body += 1; return body; } 
+};
+
+typedef recurse_expr<weight, expr_weight_visitor, true> expr_weight;
+
+#endif /* _EXPR_WEIGHT_H_ */

src/dead/gl_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    gl_tactic.h
+
+Abstract:
+
+    A T-function/Goldreich Levin-based heuristic.
+
+Author:
+
+    Nikolaj (nbjorner) 2011-12-18
+
+Notes:
+
+--*/
+
+#ifndef _GL_TACTIC_H_
+#define _GL_TACTIC_H_
+
+#include"tactic.h"
+
+namespace gl {
+    tactic * mk_tactic(ast_manager& m, params_ref const& p);
+};
+
+#endif

src/dead/gmp_big_rational.cpp

@@ -0,0 +1,117 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    gmp_big_rational.cpp
+
+Abstract:
+
+    Big rationals using GMP
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-09-26.
+
+Revision History:
+
+--*/
+#include<limits.h>
+
+#include"gmp_big_rational.h"
+#include"trace.h"
+#include"buffer.h"
+
+#ifndef NO_GMP
+mpz_t big_rational::m_tmp;
+bool  big_rational::m_tmp_initialized = false;
+mpz_t big_rational::m_int_min;
+mpz_t big_rational::m_int_max;
+mpz_t big_rational::m_uint_max;
+mpz_t big_rational::m_two32;
+mpz_t big_rational::m_int64_min;
+mpz_t big_rational::m_int64_max;
+mpz_t big_rational::m_uint64_max;
+bool  big_rational::m_has_limits = false;
+
+void big_rational::init_limits() {
+    mpz_init(m_int_min);
+    mpz_init(m_int_max);
+    mpz_init(m_uint_max);
+    mpz_init(m_two32);
+    mpz_init(m_int64_min);
+    mpz_init(m_int64_max);
+    mpz_init(m_uint64_max);
+    mpz_set_si(m_int_min,  INT_MIN);
+    mpz_set_si(m_int_max,  INT_MAX);
+    mpz_set_ui(m_uint_max, UINT_MAX);
+    mpz_set_ui(m_two32, UINT_MAX);
+    mpz_t & tmp = get_tmp();
+    mpz_set_si(tmp, 1);
+    mpz_add(m_two32, m_two32, tmp);
+    unsigned max_l = static_cast<unsigned>(INT64_MAX % static_cast<int64>(UINT_MAX));
+    unsigned max_h = static_cast<unsigned>(INT64_MAX / static_cast<int64>(UINT_MAX));
+    mpz_set_ui(m_int64_max, max_h);
+    mpz_mul(m_int64_max, m_uint_max, m_int64_max);
+    mpz_set_ui(tmp, max_l);
+    mpz_add(m_int64_max, tmp, m_int64_max);
+    mpz_neg(m_int64_min, m_int64_max);
+    mpz_set_si(tmp, -1);
+    mpz_add(m_int64_min, m_int64_min, tmp);
+    mpz_set(m_uint64_max, m_int64_max);
+    mpz_set_si(tmp, 2);
+    mpz_mul(m_uint64_max, m_uint64_max, tmp);
+    mpz_set_si(tmp, 1);
+    mpz_add(m_uint64_max, m_uint64_max, tmp);
+    m_has_limits = true;
+}
+
+std::string big_rational::to_string() const {
+    size_t sz = mpz_sizeinbase(mpq_numref(m_data), 10) + mpz_sizeinbase(mpq_numref(m_data), 10) + 3;
+    buffer<char> b(sz, 0);
+    mpq_get_str(b.c_ptr(), 10, m_data);
+    std::string result(b.c_ptr());
+    return result;
+}
+
+int64 big_rational::get_int64() const {
+    if (!m_has_limits) {
+        init_limits();
+    }
+    SASSERT(is_int64());
+    mpz_t & tmp = get_tmp();
+    mpq_get_num(tmp, m_data);
+    if (sizeof(int64) == sizeof(long) || mpz_fits_slong_p(tmp)) {
+        return mpz_get_si(tmp);
+    }
+    else {
+        mpz_mod(tmp, tmp, two32());
+        int64 r = static_cast<int64>(mpz_get_ui(tmp));
+        mpq_get_num(tmp, m_data);
+        mpz_div(tmp, tmp, two32());
+        r += static_cast<int64>(mpz_get_si(tmp)) << static_cast<int64>(32);
+        return r;
+    }
+}
+
+uint64 big_rational::get_uint64() const {
+    if (!m_has_limits) {
+        init_limits();
+    }
+    SASSERT(is_uint64());
+    mpz_t & tmp = get_tmp();
+    mpq_get_num(tmp, m_data);
+    if (sizeof(uint64) == sizeof(unsigned long) || mpz_fits_ulong_p(tmp)) {
+        return mpz_get_ui(tmp);
+    }
+    else {
+        mpz_mod(tmp, tmp, two32());
+        uint64 r = static_cast<uint64>(mpz_get_ui(tmp));
+        mpq_get_num(tmp, m_data);
+        mpz_div(tmp, tmp, two32());
+        r += static_cast<uint64>(mpz_get_ui(tmp)) << static_cast<uint64>(32);
+        return r;
+    }
+}
+
+#endif

src/dead/gmp_big_rational.h

@@ -0,0 +1,193 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    gmp_big_rational.h
+
+Abstract:
+
+    Big rationals using gmp
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-09-26.
+
+Revision History:
+
+--*/
+#ifndef _GMP_BIG_RATIONAL_H_
+#define _GMP_BIG_RATIONAL_H_
+
+#ifndef NO_GMP
+
+#include<string>
+#include<gmp.h>
+#include"util.h"
+#include"debug.h"
+#include"trace.h"
+
+class big_rational {
+    mpq_t        m_data;
+    static mpz_t m_tmp;
+    static bool  m_tmp_initialized;
+    static mpz_t & get_tmp() { 
+        if (!m_tmp_initialized) {
+            mpz_init(m_tmp);
+            m_tmp_initialized = true;
+        }
+        return m_tmp;
+    }
+    static mpz_t m_int_min;
+    static mpz_t m_int_max;
+    static mpz_t m_uint_max;
+    static mpz_t m_two32;
+    static mpz_t m_int64_min;
+    static mpz_t m_int64_max;
+    static mpz_t m_uint64_max;
+    static bool  m_has_limits;
+    static void init_limits();
+
+    static mpz_t & int64_min() {
+        if (!m_has_limits) {
+            init_limits();
+        }
+        return m_int64_min;
+    }
+
+    static mpz_t & int64_max() {
+        if (!m_has_limits) {
+            init_limits();
+        }
+        return m_int64_max;
+    }
+
+    static mpz_t & uint64_max() {
+        if (!m_has_limits) {
+            init_limits();
+        }
+        return m_uint64_max;
+    }
+    
+    static mpz_t & uint_max() {
+        if (!m_has_limits) {
+            init_limits();
+        }
+        return m_uint_max;
+    }
+
+    static mpz_t & two32() {
+        if (!m_has_limits) {
+            init_limits();
+        }
+        return m_two32;
+    }
+    
+public:
+    big_rational() { mpq_init(m_data); reset(); }
+    big_rational(int n) { mpq_init(m_data); mpq_set_si(m_data, n, 1); }
+    ~big_rational() { mpq_clear(m_data); }
+    void reset() { mpq_set_si(m_data, 0, 1); }
+    unsigned hash() const { return mpz_get_si(mpq_numref(m_data)); }
+    void set(int num, int den) { 
+        mpq_set_si(m_data, num, den);
+        mpq_canonicalize(m_data);
+    }
+    void setu(unsigned num) {
+        mpq_set_ui(m_data, num, 1);
+        mpq_canonicalize(m_data);
+    }
+    void set(const char * str) {
+        mpq_set_str(m_data, str, 10);
+    }
+    bool is_int() const {
+        return mpz_cmp_ui(mpq_denref(m_data), 1) == 0;
+    }
+    bool is_even() const {
+        if (!is_int()) {
+            return false;
+        }
+        mpz_t & tmp = get_tmp();
+        mpq_get_num(tmp, m_data);
+        return mpz_even_p(tmp) != 0;
+    }
+    bool is_int64() const {
+        if (!is_int()) {
+            return false;
+        }
+        mpz_t & tmp = get_tmp();
+        mpq_get_num(tmp, m_data);
+        return mpz_fits_slong_p(tmp) || 
+            (mpz_cmp(tmp, int64_min()) >= 0 && mpz_cmp(tmp, int64_max()) <= 0);
+    }
+    bool is_uint64() const {
+        if (!is_int()) {
+            return false;
+        }
+        mpz_t & tmp = get_tmp();
+        mpq_get_num(tmp, m_data);
+        return mpz_sgn(tmp) >= 0 && (mpz_fits_ulong_p(tmp) || mpz_cmp(tmp, uint64_max()) <= 0);
+    }
+    int64 get_int64() const;
+    uint64 get_uint64() const;
+    void neg() { mpq_neg(m_data, m_data); }
+    big_rational & operator=(const big_rational & r) {
+        mpq_set(m_data, r.m_data);
+        return *this;
+    }
+    bool operator==(const big_rational & r) const { return mpq_equal(m_data, r.m_data) != 0; }
+    bool operator<(const big_rational & r) const { return mpq_cmp(m_data, r.m_data) < 0; }
+    big_rational & operator+=(const big_rational & r) {
+        mpq_add(m_data, m_data, r.m_data);
+        return *this;
+    }
+    big_rational & operator-=(const big_rational & r) {
+        mpq_sub(m_data, m_data, r.m_data);
+        return *this;
+    }
+    big_rational & operator*=(const big_rational & r) {
+        mpq_mul(m_data, m_data, r.m_data);
+        return *this;
+    }
+    big_rational & operator/=(const big_rational & r) {
+        mpq_div(m_data, m_data, r.m_data);
+        return *this;
+    }
+    big_rational & operator%=(const big_rational & r) {
+        mpz_t & tmp = get_tmp();
+        mpz_tdiv_r(tmp, mpq_numref(m_data), mpq_numref(r.m_data));
+        mpq_set_z(m_data, tmp);
+        return *this;
+    }
+    friend void div(const big_rational & r1, const big_rational & r2, big_rational & result) {
+        mpz_t & tmp = get_tmp();
+        mpz_tdiv_q(tmp, mpq_numref(r1.m_data), mpq_numref(r2.m_data));
+        mpq_set_z(result.m_data, tmp);
+    }
+    void get_numerator(big_rational & result) {
+        mpz_t & tmp = get_tmp();
+        mpq_get_num(tmp, m_data);
+        mpq_set_z(result.m_data, tmp);
+    }
+    void get_denominator(big_rational & result) {
+        mpz_t & tmp = get_tmp();
+        mpq_get_den(tmp, m_data);
+        mpq_set_z(result.m_data, tmp);
+    }
+    void get_floor(big_rational & result) {
+        mpz_t & tmp = get_tmp();
+        mpz_fdiv_q(tmp, mpq_numref(m_data), mpq_denref(m_data));
+        mpq_set_z(result.m_data, tmp);
+    }
+    std::string to_string() const;
+#ifdef Z3DEBUG
+    static void test() {
+        init_limits();
+    }
+#endif
+};
+
+#endif 
+
+#endif /* _GMP_BIG_RATIONAL_H_ */
+

src/dead/lru_cache.cpp

@@ -0,0 +1,424 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    lru_cache.cpp
+
+Abstract:
+
+    expr -> expr LRU cache
+
+Author:
+
+    Leonardo (leonardo) 2011-04-12
+
+Notes:
+
+--*/
+#include"lru_cache.h"
+#include"ast_ll_pp.h"
+
+#define MIN_MAX_SIZE     1024
+#define INITIAL_CAPACITY 128
+
+lru_cache::cell * lru_cache::allocate(unsigned capacity) {
+    cell * mem = static_cast<cell*>(memory::allocate(sizeof(cell) * capacity));
+    memset(mem, 0, sizeof(cell)*capacity);
+    return mem;
+}
+
+void lru_cache::deallocate(cell * table) {
+    memory::deallocate(table);
+}
+
+lru_cache::cell * lru_cache::copy_table(cell * old_head, cell * new_table, unsigned new_capacity) {
+    SASSERT(old_head);
+    cell * it = old_head;
+    cell * new_head = 0;
+    cell * prev = 0;
+    do {
+        expr * k       = it->m_key;
+        unsigned h     = k->hash();
+        unsigned mask  = new_capacity - 1;
+        unsigned idx   = h & mask;
+        
+        cell * begin = new_table + idx;
+        cell * end   = new_table + new_capacity;
+        cell * curr  = begin;
+
+        for (; curr != end; ++curr) {
+            if (curr->m_key == 0) {
+                curr->m_key   = k;
+                curr->m_value = it->m_value;
+                LCS_CODE(curr->m_hits = it->m_hits;);
+                LCS_CODE(curr->m_birthday = it->m_birthday;);
+                if (prev == 0) {
+                    new_head = curr;
+                }
+                else {
+                    prev->m_next = curr;
+                    curr->m_prev = prev;
+                }
+                goto end;
+            }
+        }
+        for (curr = new_table; curr != begin; ++curr) {
+            if (curr->m_key == 0) {
+                curr->m_key   = k;
+                curr->m_value = it->m_value;
+                SASSERT(prev != 0);
+                prev->m_next = curr;
+                curr->m_prev = prev;
+            }
+            goto end;
+        }
+        UNREACHABLE();
+    end:
+        prev = curr;
+        it = it->m_next;
+    }
+    while (it != old_head);
+    prev->m_next     = new_head;
+    new_head->m_prev = prev;
+    return new_head;
+}
+
+void lru_cache::expand_table() {
+    SASSERT(m_head);
+    unsigned new_capacity = m_capacity * 2;
+    TRACE("lru_cache", tout << "expanding table new_capacity: " << new_capacity << "\n";);
+    cell *   new_table    = allocate(new_capacity);
+    m_head     = copy_table(m_head, new_table, new_capacity);
+    deallocate(m_table);
+    m_table    = new_table;
+    m_capacity = new_capacity;
+    m_num_deleted = 0;
+    SASSERT(check_invariant());
+}
+
+void lru_cache::remove_deleted() {
+    SASSERT(m_head);
+    TRACE("lru_cache", tout << "removing deleted entries\n";);
+    cell *   new_table    = allocate(m_capacity);
+    m_head     = copy_table(m_head, new_table, m_capacity);
+    deallocate(m_table);
+    m_table    = new_table;
+    m_num_deleted = 0;
+    SASSERT(check_invariant());
+}
+
+void lru_cache::init() {
+    if (m_max_size < MIN_MAX_SIZE)
+        m_max_size = MIN_MAX_SIZE;
+    m_size = 0;
+    m_capacity = INITIAL_CAPACITY;
+    m_table = allocate(m_capacity);
+    m_head  = 0;
+    m_num_deleted = 0;
+}
+
+lru_cache::lru_cache(ast_manager & m):
+    m_manager(m),
+    m_max_size(m.get_num_asts() * 100) {
+    init();
+    TRACE("lru_cache", tout << "new lru cache, max-size: " << m_max_size << "\n";);
+}
+ 
+lru_cache::lru_cache(ast_manager & m, unsigned max_size):
+    m_manager(m),
+    m_max_size(max_size) {
+    init();
+}
+
+void lru_cache::dec_refs() {
+    if (m_head) {
+        cell * curr = m_head;
+#ifdef Z3DEBUG
+        unsigned sz = 0;
+#endif
+        do {
+            m_manager.dec_ref(curr->m_key);
+            m_manager.dec_ref(curr->m_value);
+            curr = curr->m_next;
+            DEBUG_CODE(sz++;);
+        }
+        while (curr != m_head);
+        SASSERT(sz == m_size);
+    }
+}
+ 
+lru_cache::~lru_cache() {
+    TRACE("lru_cache", tout << "destructor invoked size: " << m_size << ", m_head: " << m_head << "\n";);
+    LCS_CODE({
+        if (m_head) {
+            unsigned used = 0;
+            cell * curr = m_head;
+            do {
+                if (curr->m_hits > 0)
+                    used++;
+                curr = curr->m_next;
+            }
+            while (curr != m_head);
+            verbose_stream() << "[lru_cache] num-used: " << used << " size: " << m_size << "\n";
+        }
+    });
+    SASSERT(check_invariant());
+    dec_refs();
+    deallocate(m_table);
+}
+
+void lru_cache::del_least_used() {
+    SASSERT(m_head);
+    SASSERT(m_size >= 2);
+    cell * c = m_head->m_prev;
+    TRACE("lru_cache", tout << "del least used: " << mk_bounded_pp(c->m_key, m_manager, 3) << "\n";);
+    LCS_CODE({
+        static unsigned non_zero = 0;
+        static unsigned long long total_hits;
+        static unsigned counter = 0;
+        if (c->m_hits > 0) {
+            counter++;
+            total_hits += c->m_hits;
+            non_zero++;
+            if (non_zero % 1000 == 0)
+                verbose_stream() << "[lru_cache] cell with non-zero hits was deleted: " << non_zero << " avg: " << ((double)total_hits/(double) counter) << std::endl;
+        }
+    });
+    SASSERT(c->m_prev != c);
+    SASSERT(c->m_next != c);
+    m_manager.dec_ref(c->m_key);
+    m_manager.dec_ref(c->m_value);
+    c->m_prev->m_next = c->m_next;
+    c->m_next->m_prev = c->m_prev;
+    SASSERT(m_head->m_prev == c->m_prev);
+    c->m_key  = reinterpret_cast<expr*>(1);
+    c->m_prev = 0;
+    c->m_next = 0;
+    m_size--;
+    m_num_deleted++;
+    CASSERT("lru_cache", check_invariant());
+    if (m_num_deleted * 3 > m_capacity)
+        remove_deleted();
+}
+
+void lru_cache::add_front(cell * c) {
+    SASSERT(c->m_next == 0);
+    SASSERT(c->m_prev == 0);
+    if (m_head == 0) {
+        c->m_next = c;
+        c->m_prev = c;
+        m_head    = c;
+    }
+    else {
+        c->m_prev = m_head->m_prev;
+        c->m_next = m_head;
+        m_head->m_prev->m_next = c;
+        m_head->m_prev = c;
+        m_head = c;
+    }
+    CASSERT("lru_cache", check_invariant());
+    SASSERT(m_head == c);
+}
+
+void lru_cache::move_front(cell * c) {
+    SASSERT(m_head);
+    SASSERT(c->m_next);
+    SASSERT(c->m_prev);
+    if (m_head != c) {
+        c->m_prev->m_next = c->m_next;
+        c->m_next->m_prev = c->m_prev;
+        
+        c->m_prev = m_head->m_prev;
+        c->m_next = m_head;
+        
+        m_head->m_prev->m_next = c;
+        m_head->m_prev         = c;
+        
+        m_head = c;
+    }
+    CASSERT("lru_cache", check_invariant());
+    SASSERT(m_head == c);
+}
+
+void lru_cache::insert(expr * k, expr * v) {
+    LCS_CODE(m_time++;);
+    if (m_size == m_max_size)
+        del_least_used();
+    else if (m_size * 2 > m_capacity)
+        expand_table();
+    SASSERT(m_size < m_max_size);
+    unsigned h     = k->hash();
+    unsigned mask  = m_capacity - 1;
+    unsigned idx   = h & mask;
+
+    cell * begin = m_table + idx;
+    cell * end   = m_table + m_capacity;
+    cell * curr  = begin;
+    cell * del_cell = 0;
+
+#define INSERT_LOOP()                                           \
+        if (curr->m_key == 0) {                                 \
+            cell * new_cell;                                    \
+            if (del_cell) {                                     \
+                new_cell = del_cell;                            \
+                m_num_deleted--;                                \
+            }                                                   \
+            else {                                              \
+                new_cell = curr;                                \
+            }                                                   \
+            m_manager.inc_ref(k);                               \
+            m_manager.inc_ref(v);                               \
+            new_cell->m_key   = k;                              \
+            new_cell->m_value = v;                              \
+            LCS_CODE(new_cell->m_hits = 0;);                    \
+            LCS_CODE(new_cell->m_birthday = m_time;);           \
+            m_size++;                                           \
+            add_front(new_cell);                                \
+            return;                                             \
+        }                                                       \
+        if (curr->m_key == reinterpret_cast<expr*>(1)) {        \
+            del_cell = curr;                                    \
+            continue;                                           \
+        }                                                       \
+        if (curr->m_key == k) {                                 \
+            m_manager.inc_ref(v);                               \
+            m_manager.dec_ref(curr->m_value);                   \
+            curr->m_value = v;                                  \
+            LCS_CODE(curr->m_hits = 0;);                        \
+            LCS_CODE(curr->m_birthday = m_time;);               \
+            move_front(curr);                                   \
+            return;                                             \
+        }
+
+    for (; curr != end; ++curr) {
+        INSERT_LOOP();
+    }
+    for (curr = m_table; curr != begin; ++curr) {
+        INSERT_LOOP();
+    } 
+    UNREACHABLE();
+}
+
+expr * lru_cache::find(expr * k) {
+    unsigned h     = k->hash();
+    unsigned mask  = m_capacity - 1;
+    unsigned idx   = h & mask;
+
+#ifdef LRU_CACHE_STATISTICS
+    static unsigned long long total_age = 0;
+    static unsigned long long max_time = 0;
+    static unsigned counter = 0;
+#define COLLECT()                                                                                                                                       \
+    if (curr->m_hits == 0) {                                                                                                                            \
+        counter ++;                                                                                                                                     \
+        unsigned age = m_time - curr->m_birthday;                                                                                                       \
+        if (age > max_time)                                                                                                                             \
+            max_time = age;                                                                                                                             \
+        total_age += age;                                                                                                                               \
+        if (counter % 1000 == 0)                                                                                                                        \
+            verbose_stream() << "[lru_cache] avg time for first hit: " << ((double) total_age / (double) counter) << " max time: " << max_time << "\n";        \
+    }
+#endif    
+
+    cell * begin = m_table + idx;
+    cell * end   = m_table + m_capacity;
+    cell * curr  = begin;
+    for (; curr != end; ++curr) {
+        if (curr->m_key == k) {
+            // LCS_CODE(COLLECT());
+            LCS_CODE(if (curr->m_hits == 0 && m_time - curr->m_birthday >= 5000) return 0;)
+            LCS_CODE(curr->m_hits++;);
+            move_front(curr);
+            return curr->m_value;
+        }
+        if (curr->m_key == 0) 
+            return 0;
+    }
+    for (curr = m_table; curr != begin; ++curr) {
+        if (curr->m_key == k) {
+            // LCS_CODE(COLLECT());
+            LCS_CODE(curr->m_hits++;);
+            LCS_CODE(if (curr->m_hits == 0 && m_time - curr->m_birthday >= 5000) return 0;);
+            move_front(curr);
+            return curr->m_value;
+        }
+        if (curr->m_key == 0) 
+            return 0;
+    }
+    return 0;
+}
+
+void lru_cache::reset() {
+    TRACE("lru_cache", tout << "reset... m_size: " << m_size << "\n";);
+    LCS_CODE(m_time = 0;);
+    if (m_head) {
+        cell * curr = m_head;
+#ifdef Z3DEBUG
+        unsigned sz = 0;
+#endif
+        do {
+            m_manager.dec_ref(curr->m_key);
+            m_manager.dec_ref(curr->m_value);
+            cell * next = curr->m_next;
+            curr->m_key   = 0;
+            curr->m_value = 0;
+            curr->m_next  = 0;
+            curr->m_prev  = 0;
+            LCS_CODE(curr->m_hits = 0;);
+            LCS_CODE(curr->m_birthday = 0;);
+            curr = next;
+            DEBUG_CODE(sz++;);
+        }
+        while (curr != m_head);
+        SASSERT(sz == m_size);
+        m_head = 0;
+        m_size = 0;
+        SASSERT(check_invariant());
+    }
+}
+ 
+void lru_cache::cleanup() {
+    dec_refs();
+    deallocate(m_table);
+    m_capacity    = INITIAL_CAPACITY;
+    m_table       = allocate(m_capacity); 
+    m_head        = 0;
+    m_size        = 0;
+    m_num_deleted = 0;
+}
+
+bool lru_cache::check_invariant() const {
+    SASSERT(m_size <= m_max_size);
+    cell * begin         = m_table;
+    cell * end           = m_table + m_capacity;
+    unsigned sz          = 0;
+    if (m_head) {
+        cell * curr  = m_head;
+        do {
+            sz++;
+            SASSERT(curr->m_key != 0 && curr->m_key != reinterpret_cast<expr*>(1));
+            SASSERT(curr->m_next->m_prev == curr);
+            SASSERT(curr->m_prev->m_next == curr);
+            SASSERT(curr < end);
+            SASSERT(curr >= begin);
+            curr = curr->m_next;
+        }
+        while (curr != m_head);
+    }
+    SASSERT(m_size == sz);
+    sz = 0;
+    unsigned num_deleted = 0;
+    for (cell * it = begin; it != end; it++) {
+        if (it->m_key == reinterpret_cast<expr*>(1)) {
+            num_deleted++;
+            continue;
+        }
+        if (it->m_key != 0) {
+            sz++;
+        }
+    }
+    SASSERT(m_size == sz);
+    SASSERT(m_num_deleted == num_deleted);
+    return true;
+}

src/dead/lru_cache.h

@@ -0,0 +1,80 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    lru_cache.h
+
+Abstract:
+
+    expr -> expr LRU cache
+
+Author:
+
+    Leonardo (leonardo) 2011-04-12
+
+Notes:
+
+--*/
+#ifndef _LRU_CACHE_H_
+#define _LRU_CACHE_H_
+
+#include"ast.h"
+
+// #define LRU_CACHE_STATISTICS
+
+#ifdef LRU_CACHE_STATISTICS
+#define LCS_CODE(CODE) { CODE }
+#else
+#define LCS_CODE(CODE)
+#endif
+
+class lru_cache {
+    struct cell {
+        expr *  m_key;
+        expr *  m_value;
+        cell *  m_prev;
+        cell *  m_next;
+#ifdef LRU_CACHE_STATISTICS
+        unsigned m_hits;
+        unsigned m_birthday;
+#endif
+    };
+
+    ast_manager & m_manager;
+    cell *        m_table;
+    cell *        m_head;
+    unsigned      m_size;
+    unsigned      m_max_size;
+    unsigned      m_capacity;
+    unsigned      m_num_deleted;
+#ifdef LRU_CACHE_STATISTICS
+    unsigned      m_time;
+#endif
+
+    static cell * allocate(unsigned capacity);
+    static void deallocate(cell * table);
+    static cell * copy_table(cell * old_head, cell * new_table, unsigned new_capacity);
+
+    void del_least_used();
+    void add_front(cell * c);
+    void move_front(cell * c);
+    void expand_table();
+    void remove_deleted();
+    void init();
+    void dec_refs();
+public:
+    lru_cache(ast_manager & m);
+    lru_cache(ast_manager & m, unsigned max_size);
+    ~lru_cache();
+    void insert(expr * k, expr * v);
+    expr * find(expr * k);
+    void reset();
+    void cleanup();
+    unsigned size() const { return m_size; }
+    unsigned capacity() const { return m_capacity; }
+    bool empty() const { return m_size == 0; }
+    bool check_invariant() const;
+};
+
+#endif

src/dead/parameters.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    parameters.h
+
+Abstract:
+
+    Settings and parameters supplied to pre-processing and solver
+    modules.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-18.
+    Nikolaj Bjorner (nbjorner) 2007-02-15
+
+Revision History:
+    2007-02-15, nbjorner.
+    Hoisted out from simplify_parser.h and core_theory_types.h
+    in order to share functionality with SMTLIB and other
+    front-ends without bringing in the simplifier and core_theory.
+
+--*/
+#ifndef _PARAMETERS_H_
+#define _PARAMETERS_H_
+
+#include"sat_params.h"
+#include"core_theory_params.h"
+#include"front_end_params.h"
+
+#endif

src/dead/simple_sat.cpp

@@ -0,0 +1,118 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    simple_sat.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-10.
+
+Revision History:
+
+--*/
+#include<fstream>
+#include<time.h>
+#include"front_end_params.h"
+#include"sat_def.h"
+#include"dimacs_parser.h"
+#include"timeit.h"
+#include"mem_stat.h"
+
+class simple_sat_solver : public no_extension {
+    const front_end_params &         m_params;
+    sat_solver<simple_sat_solver> *  m_sat;
+    unsigned                         m_num_vars;
+    svector<lbool>                   m_model;
+public:
+    simple_sat_solver(const front_end_params & p):
+        m_params(p),
+        m_sat(new sat_solver<simple_sat_solver>(*this, p)),
+        m_num_vars(0) {
+    }
+
+    ~simple_sat_solver() {
+        delete m_sat;
+    }
+
+    static bool enable_ref_counters() {
+        return false; 
+    }
+
+    void mk_var() {
+	m_sat->mk_var();
+	m_num_vars++;
+    }
+
+    void mk_clause(const literal_vector & lits) {
+	m_sat->mk_main_clause(lits);
+    }
+
+    unsigned get_num_vars() const {
+	return m_num_vars;
+    }
+
+    lbool check() {
+	return m_sat->check();
+    }
+    
+    void mk_model() {
+        if (m_params.m_build_model) {
+            m_sat->save_assignment(m_model);
+        }
+    }
+
+    void display_model(std::ostream & out) const {
+        int sz = m_model.size();
+        for (int i = 1; i < sz; i++) {
+            if (m_model[i] == l_true) {
+                out << i << " ";
+            }
+            else if (m_model[i] == l_false) {
+                out << -i << " ";
+            }
+        }
+        out << "\n";
+    }
+
+    void display_statistics(std::ostream & out) const {
+	m_sat->display_statistics(out);
+    }
+};
+
+extern bool g_display_statistics;
+extern front_end_params g_front_end_params;
+
+void solve_cnf(const char * file) {
+    clock_t start_time = clock();
+    simple_sat_solver solver(g_front_end_params);
+    std::ifstream in(file);
+    parse_dimacs(in, solver);
+    lbool r = solver.check();
+    clock_t end_time   = clock();
+    switch(r) {
+    case l_false:
+        std::cout << "unsat\n";
+	break;
+    case l_undef:
+	std::cout << "unknown\n";
+	break;
+    case l_true:
+	std::cout << "sat\n";
+        if (g_front_end_params.m_build_model) {
+            solver.display_model(std::cout);
+        }
+	break;
+    }
+    if (g_display_statistics) {
+	solver.display_statistics(std::cerr);
+        memory::display_max_usage(std::cerr);
+        std::cerr << "time:               " << ((static_cast<double>(end_time) - static_cast<double>(start_time)) / CLOCKS_PER_SEC) << "\n";
+    }
+}
+

src/dead/simple_sat.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    simple_sat.h
+
+Abstract:
+
+    Simple SAT solver using the Z3 SAT template.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-10.
+
+Revision History:
+
+--*/
+
+#ifndef _SIMPLE_SAT_H_
+#define _SIMPLE_SAT_H_
+
+void solve_cnf(const char * file);
+
+#endif /* _SIMPLE_SAT_H_ */
+

src/dead/smt_classifier.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_classifier.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-24.
+
+Revision History:
+
+--*/
+#ifndef _SMT_CLASSIFIER_H_
+#define _SMT_CLASSIFIER_H_
+
+#include"static_features.h"
+
+namespace smt {
+
+    class classifier {
+        context     &     m_context;
+        ast_manager &     m_manager;
+        static_features   m_static_features;
+        symbol            m_logic;
+    public:
+        classifier(context & c);
+        /**
+           \brief Give a hint by specifying the logic used to describe a problem.
+        */
+        void set_logic(symbol & s);
+        /**
+           \brief Setup the logical context for solving the following formulas.
+        */
+        void setup(unsigned num_formulas, expr * const * fs);
+    };
+    
+};
+
+#endif /* _SMT_CLASSIFIER_H_ */
+

src/dead/smt_euf.cpp

@@ -0,0 +1,187 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_euf.cpp
+
+Abstract:
+
+    Equality and uninterpreted functions
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-14.
+
+Revision History:
+
+--*/
+#include"smt_euf.h"
+#include"smt_context.h"
+#include"ast_smt2_pp.h"
+
+namespace smt {
+
+    struct euf_manager::imp {
+        context &                   m_context;
+        ast_manager &               m_manager;
+        region &                    m_region;
+        expr_ref_vector             m_e_internalized_stack; // stack of the expressions already internalized as enodes. 
+        ptr_vector<enode>           m_app2enode;    // app -> enode
+        ptr_vector<enode>           m_enodes;
+        vector<enode_vector>        m_decl2enodes;  // decl -> enode (for decls with arity > 0)
+        cg_table                    m_cg_table; 
+        dyn_ack_manager             m_dyn_ack_manager;
+        struct new_eq {
+            enode *                 m_lhs;
+            enode *                 m_rhs;
+            eq_justification        m_justification;
+            new_eq() {}
+            new_eq(enode * lhs, enode * rhs, eq_justification const & js):
+                m_lhs(lhs), m_rhs(rhs), m_justification(js) {}
+        };
+        svector<new_eq>             m_eq_propagation_queue;
+        struct new_th_eq {
+            theory_id  m_th_id;
+            theory_var m_lhs;
+            theory_var m_rhs;
+            new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {}
+            new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {}
+        };
+        svector<new_th_eq>          m_th_eq_propagation_queue;
+        svector<new_th_eq>          m_th_diseq_propagation_queue;
+        enode *                     m_is_diseq_tmp; // auxiliary enode used to find congruent equality atoms.
+        tmp_enode                   m_tmp_enode;
+        ptr_vector<almost_cg_table> m_almost_cg_tables; // temporary field for is_ext_diseq
+        obj_map<expr, unsigned>     m_cached_generation;
+        obj_hashtable<expr>         m_cache_generation_visited;
+        friend class mk_enode_trail;
+        class mk_enode_trail : public trail<context> {
+            imp & m_owner;
+        public:
+            mk_enode_trail(imp & o):m_owner(o) {}
+            virtual void undo(context & ctx) { m_owner.undo_mk_enode(); }
+        };
+        mk_enode_trail              m_mk_enode_trail;
+        volatile bool               m_cancel_flag;
+
+        // Statistics
+        unsigned                    m_num_mk_enode;
+        unsigned                    m_num_del_enode;
+
+        void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
+            SASSERT(lhs != rhs);
+            m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
+        }
+
+        void push_new_congruence(enode * n1, enode * n2, bool used_commutativity) {
+            SASSERT(n1->m_cg == n2);
+            push_eq(n1, n2, eq_justification::mk_cg(used_commutativity));
+        }
+
+        bool e_internalized(expr const * n) const {
+            return m_app2enode.get(n->get_id(), 0) != 0;
+        }
+
+        void set_app2enode(expr const * n, enode * e) {
+            m_app2enode.setx(n->get_id(), e, 0);
+        }
+
+        enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled, unsigned generation) {
+            TRACE("mk_enode_detail", 
+                  tout << mk_ismt2_pp(n, m_manager) << "\n";
+                  tout <<"suppress_args: " << suppress_args << ", merge_tf: " << merge_tf << ", cgc_enabled: " << cgc_enabled << "\n";);
+            SASSERT(!e_internalized(n));
+            unsigned scope_lvl   = m_context.get_scope_level();
+            unsigned id          = n->get_id();
+            unsigned _generation = 0;
+            if (!m_cached_generation.empty() && m_cached_generation.find(n, _generation)) {
+                generation = _generation;
+            }
+            enode * e            = enode::mk(m_manager, m_region, m_app2enode, n, generation, suppress_args, merge_tf, scope_lvl, cgc_enabled, true);
+            TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
+            if (n->get_num_args() == 0 && m_manager.is_value(n))
+                e->mark_as_interpreted();
+            TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
+            TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);
+            set_app2enode(n, e);
+            m_e_internalized_stack.push_back(n);
+            m_context.push_trail_ptr(&m_mk_enode_trail);
+            m_enodes.push_back(e);
+            if (e->get_num_args() > 0) {
+                if (e->is_true_eq()) {
+                    /* 
+                        bool_var v = enode2bool_var(e);
+                        assign(literal(v), mk_justification(eq_propagation_justification(e->get_arg(0), e->get_arg(1))));
+                        e->m_cg    = e;
+                    */
+                }
+                else {
+                    if (cgc_enabled) {
+                        enode_bool_pair pair = m_cg_table.insert(e);
+                        enode * e_prime      = pair.first;
+                        if (e != e_prime) {
+                            e->m_cg = e_prime;
+                            bool used_commutativity = pair.second;
+                            push_new_congruence(e, e_prime, used_commutativity);
+                        }
+                        else {
+                            e->m_cg = e;
+                        }
+                    }
+                    else {
+                        e->m_cg = e;
+                    }
+                }
+                if (!e->is_eq()) {
+                    unsigned decl_id = n->get_decl()->get_decl_id();
+                    if (decl_id >= m_decl2enodes.size())
+                        m_decl2enodes.resize(decl_id+1);
+                    m_decl2enodes[decl_id].push_back(e);
+                }
+            }
+            SASSERT(e_internalized(n));
+            m_num_mk_enode++;
+            
+            // #ifndef SMTCOMP
+            // if (m_params.m_trace_stream != NULL)
+            //    *m_params.m_trace_stream << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";        
+            // #endif
+
+            return e;
+        }
+
+        void undo_mk_enode() {
+            SASSERT(!m_e_internalized_stack.empty());
+            m_num_del_enode++;
+            expr * n              = m_e_internalized_stack.back();
+            TRACE("undo_mk_enode", tout << "undo_enode: #" << n->get_id() << "\n" << mk_ismt2_pp(n, m_manager) << "\n";);
+            TRACE("mk_var_bug", tout << "undo_mk_enode: " << n->get_id() << "\n";);
+            unsigned n_id         = n->get_id();
+            SASSERT(is_app(n));
+            enode * e             = m_app2enode[n_id];
+            m_app2enode[n_id]     = 0;
+            if (e->is_cgr() && !e->is_true_eq() && e->is_cgc_enabled()) {
+                SASSERT(m_cg_table.contains_ptr(e));
+                m_cg_table.erase(e);
+            }
+            if (e->get_num_args() > 0 && !e->is_eq()) {
+                unsigned decl_id = to_app(n)->get_decl()->get_decl_id();
+                SASSERT(decl_id < m_decl2enodes.size());
+                SASSERT(m_decl2enodes[decl_id].back() == e);
+                m_decl2enodes[decl_id].pop_back();
+            }
+            e->del_eh(m_manager);
+            SASSERT(m_e_internalized_stack.size() == m_enodes.size());
+            m_enodes.pop_back();
+            m_e_internalized_stack.pop_back();
+        }
+
+    };
+
+    euf_manager::euf_manager(context & ctx) {
+    }
+    
+    euf_manager::~euf_manager() {
+    }
+};

src/dead/smt_euf.h

@@ -0,0 +1,55 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_euf.h
+
+Abstract:
+
+    Equality and uninterpreted functions
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-14.
+
+Revision History:
+
+--*/
+#ifndef _SMT_EUF_H_
+#define _SMT_EUF_H_
+
+#include"ast.h"
+#include"smt_enode.h"
+#include"smt_eq_justification.h"
+
+namespace smt {
+    class context;
+
+    class euf_manager {
+        struct imp;
+        imp * m_imp;
+    public:
+        euf_manager(context & ctx);
+        ~euf_manager();
+
+        enode * mk_enode(app * n, bool suppress_args, bool merge_tf, bool cgc_enabled);
+        
+        void add_eq(enode * n1, enode * n2, eq_justification js);
+        bool assume_eq(enode * lhs, enode * rhs);
+        void reset();
+        
+        static bool is_eq(enode const * n1, enode const * n2) { return n1->get_root() == n2->get_root(); }
+        bool is_diseq(enode * n1, enode * n2) const;
+        bool is_ext_diseq(enode * n1, enode * n2, unsigned depth);
+        enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args);
+        bool is_shared(enode * n) const;
+
+        unsigned get_num_enodes_of(func_decl const * decl) const;
+        enode_vector::const_iterator begin_enodes_of(func_decl const * decl) const;
+        enode_vector::const_iterator end_enodes_of(func_decl const * decl) const;
+    };
+};
+
+
+#endif

src/dead/smt_trail.h

@@ -0,0 +1,131 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    smt_trail.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-02-19.
+
+Revision History:
+
+--*/
+#ifndef _SMT_TRAIL_H_
+#define _SMT_TRAIL_H_
+
+namespace smt {
+
+    class context;
+
+    class trail {
+    public:
+        virtual ~trail() {
+        }
+        virtual void undo(context & ctx) = 0;
+    };
+    
+    template<typename T>
+    class value_trail : public trail {
+        T & m_value;
+        T   m_old_value;
+        
+    public:
+        value_trail(T & value):
+            m_value(value),
+            m_old_value(value) {
+        }
+        
+        virtual ~value_trail() {
+        }
+        
+        virtual void undo(context & ctx) {
+            m_value = m_old_value;
+        }
+    };
+
+    template<typename T>
+    class set_ptr_trail : public trail {
+        T * & m_ptr;
+    public:
+        set_ptr_trail(T * & ptr):
+            m_ptr(ptr) {
+            SASSERT(m_ptr == 0);
+        }
+        
+        virtual void undo(context & ctx) {
+            m_ptr = 0;
+        }
+    };
+    
+    template<typename T, bool CallDestructors=true>
+    class vector_value_trail : public trail {
+        vector<T, CallDestructors> & m_vector;
+        unsigned                     m_idx;
+        T                            m_old_value;
+    public:
+        vector_value_trail(vector<T, CallDestructors> & v, unsigned idx):
+            m_vector(v),
+            m_idx(idx),
+            m_old_value(v[idx]) {
+        }
+        
+        virtual ~vector_value_trail() {
+        }
+        
+        virtual void undo(context & ctx) {
+            m_vector[m_idx] = m_old_value;
+        }
+    };
+    
+    template<typename T, bool CallDestructors=true>
+    class push_back_trail : public trail {
+        vector<T, CallDestructors> & m_vector;
+    public:
+        push_back_trail(vector<T, CallDestructors> & v):
+            m_vector(v) {
+        }
+        
+        virtual void undo(context & ctx) {
+            m_vector.pop_back();
+        }
+    };
+    
+    class set_bitvector_trail : public trail {
+        svector<bool> & m_vector;
+        unsigned        m_idx;
+    public:
+        set_bitvector_trail(svector<bool> & v, unsigned idx):
+            m_vector(v),
+            m_idx(idx) {
+            SASSERT(m_vector[m_idx] == false);
+            m_vector[m_idx] = true;
+        }
+        
+        virtual void undo(context & ctx) {
+            m_vector[m_idx] = false;
+        }
+    };
+    
+    template<typename T>
+    class new_obj_trail : public trail {
+        T * m_obj;
+    public:
+        new_obj_trail(T * obj):
+            m_obj(obj) {
+        }
+        
+        virtual void undo(context & ctx) {
+            dealloc(m_obj);
+        }
+    };
+
+};
+
+#endif /* _SMT_TRAIL_H_ */
+

src/dead/st_cmds.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    st_cmds.h
+
+Abstract:
+
+    Commands for testing strategies.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-04-27
+
+Revision History:
+
+--*/
+#ifndef _ST_CMD_H_
+#define _ST_CMD_H_
+
+class cmd_context;
+
+void install_st_cmds(cmd_context & ctx);
+
+#endif

src/dead/test/ackermanize.cpp

@@ -0,0 +1,42 @@
+#include "ackermanize.h"
+#include "smtparser.h"
+#include "ast_pp.h"
+
+void tst_ackermanize()
+{
+    ast_manager manager;
+    
+    smtlib::parser* parser = smtlib::parser::create(manager);
+    ackermanize ack(manager);
+
+    ast_ref<const_decl_ast> fD(manager);
+    ast_ref<const_decl_ast> xD(manager);
+    ast_ref<type_decl_ast> AD(manager);
+    ast_ref<type_ast> A(manager);
+    ast_ref<> a1(manager), a2(manager), a3(manager), a4(manager), 
+        a5(manager), a6(manager), a7(manager);
+    ast_ref<> r(manager);
+
+    AD  = manager.mk_type_decl(symbol("A"));
+    A   = manager.mk_type(AD.get());
+    fD  = manager.mk_const_decl(symbol("f"), A.get(), A.get(), A.get());
+    a1  = manager.mk_const(manager.mk_const_decl(symbol("a1"), A.get()));
+    a2  = manager.mk_const(manager.mk_const_decl(symbol("a2"), A.get()));
+    a3  = manager.mk_const(manager.mk_const_decl(symbol("a3"), A.get()));
+    a4  = manager.mk_const(manager.mk_const_decl(symbol("a4"), A.get()));
+    a5  = manager.mk_const(manager.mk_const_decl(symbol("a5"), A.get()));
+    a6  = manager.mk_const(manager.mk_const_decl(symbol("a6"), A.get()));
+    a7  = manager.mk_const(manager.mk_const_decl(symbol("a7"), A.get()));
+    
+    r = manager.mk_const(manager.get_basic_family_id(),
+                         OP_EQ,
+                         manager.mk_const(fD.get(), a1.get(), a2.get()),
+                         manager.mk_const(fD.get(), a2.get(), a3.get()));             
+
+    TRACE("ackermanize", tout << mk_pp(r.get()) << std::endl;);
+
+    ack.reduce(r);
+
+    TRACE("ackermanize", tout << mk_pp(r.get()) << std::endl;);
+
+}

src/dead/test/core_theory.cpp

@@ -0,0 +1,821 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    core_theory.cpp
+
+Abstract:
+
+    Test core theory
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-20.
+
+Revision History:
+
+--*/
+#include"core_theory.h"
+#include"theory_diff_logic.h"
+
+class core_theory_tester {
+    static void tst1() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        enode * n1 = t.mk_const();
+        SASSERT(n1->check_invariant());
+        enode * n2 = t.mk_const();
+        SASSERT(n2->check_invariant());
+        enode * app1 = t.mk_app_core(1, n1, n2);
+        enode * app2 = t.mk_app_core(1, n2, n2);
+        enode * app3 = t.mk_app_core(1, n1, n2);
+        SASSERT(app1 != app2);
+        SASSERT(app1 == app3);
+
+        literal l1 = t.mk_eq(n1, n2);
+        literal l2 = t.mk_eq(n2, n1);
+        literal l4 = t.mk_eq(n2, app1);
+        SASSERT(l1 == l2);
+        SASSERT(l1 != l4);
+
+        SASSERT(n1->get_root() != n2->get_root());
+
+        t.assert_lit(l1);
+        t.assert_lit(l4);
+        t.propagate();
+
+        SASSERT(n1->get_root() == n2->get_root());
+        TRACE("core_theory", t.display(tout););
+    }
+
+    static void tst2() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        enode * a1 = t.mk_app_core(1, n1, n2);
+
+        literal l1 = t.mk_eq(n1, n2);
+        t.assert_lit(l1);
+        t.propagate();
+
+        t.push_scope();
+        
+        literal l2 = t.mk_eq(n1, n3);
+        t.assign(l2, mk_axiom());
+
+        enode * a2 = t.mk_app_core(1, n1, n1);
+        enode * a3 = t.mk_app_core(1, n1, n3);
+
+        TRACE("core_theory", t.display(tout););
+
+        t.propagate();
+        SASSERT(t.is_equal(a1, a2));
+        SASSERT(!t.is_equal(a1, a3));
+        t.m_sat->mark_as_relevant(l2.var());
+        t.propagate();
+        SASSERT(t.is_equal(a1, a2));
+        SASSERT(t.is_equal(a1, a3));
+
+        t.pop_scope(1);
+
+        t.propagate();
+        SASSERT(to_app(a1)->get_cg() == a1);
+        TRACE("core_theory", t.display(tout););
+    }
+
+    static void tst3() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        enode * a1 = t.mk_app_core(1, n1, n2);
+
+        literal l1 = t.mk_eq(n1, n2);
+        t.assert_lit(l1);
+        t.propagate();
+
+        t.push_scope();
+        
+        literal l2 = t.mk_eq(n1, n3);
+        t.assign(l2, mk_axiom());
+
+        enode * a2 = t.mk_app_core(1, n1, n1);
+        enode * a3 = t.mk_app_core(1, n1, n3);
+
+        TRACE("core_theory", t.display(tout););
+
+        t.propagate();
+        SASSERT(t.is_equal(a1, a2));
+        SASSERT(t.is_equal(a1, a3));
+
+        t.pop_scope(1);
+
+        t.propagate();
+        SASSERT(to_app(a1)->get_cg() == a1);
+        TRACE("core_theory", t.display(tout););
+    }
+
+    static void tst8() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        enode * n6 = t.mk_const();
+        
+        t.push_scope();
+
+        t.assert_lit(~t.mk_eq(n1, n2));
+        t.assert_lit(t.mk_eq(n1, n3));
+        t.assert_lit(t.mk_eq(n2, n4));
+        t.assert_lit(t.mk_eq(n3, n6));
+        t.assert_lit(t.mk_eq(n1, n5));
+        t.propagate();
+        
+        SASSERT(!t.inconsistent());
+
+        t.assert_lit(t.mk_eq(n3, n4));
+        TRACE("core_theory", t.display(tout););
+        t.propagate();
+
+        SASSERT(t.inconsistent());
+
+        t.pop_scope(1);
+    }
+
+    static void tst9() {
+        TRACE("core_theory", tout << "tst9\n";);
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        t.push_scope();
+        enode * n   = t.mk_const();
+        unsigned id = n->get_id();
+        t.pop_scope(1);
+        TRACE("core_theory", tout << "after pop\n";);
+        n = t.mk_const();
+        SASSERT(id == n->get_id());
+        TRACE("core_theory", tout << "end of tst9\n";);
+    }
+
+    static void tst10() {
+        TRACE("core_theory", tout << "tst10\n";);
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        t.push_scope();
+        enode * n   = t.mk_const();
+        unsigned id = n->get_id();
+        t.inc_weak_ref(id);
+        t.pop_scope(1);
+        TRACE("core_theory", tout << "after pop\n";);
+        n = t.mk_const();
+        SASSERT(id + 1 == n->get_id());
+        t.dec_weak_ref(id);
+        n = t.mk_const();
+        SASSERT(id = n->get_id());
+        TRACE("core_theory", tout << "end of tst10\n";);
+    }
+
+    static void tst11() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        t.add_eq(n1, n2, proto_eq_proof::mk_axiom());
+        enode * f1 = t.mk_app_core(1, n1);
+        enode * f2 = t.mk_app_core(1, n2);
+        t.propagate();
+        SASSERT(t.is_equal(f1, f2));
+        t.push_scope();
+        literal l1 = t.mk_lit();
+        literal l2 = t.mk_eq(f1, f2);
+        t.mk_main_clause(l1, l2);
+        SASSERT(t.get_assignment(l2) == l_true);
+        t.pop_scope(1);
+        SASSERT(t.get_assignment(l2) == l_true);
+    }
+
+    static void tst12() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        t.add_diseq(n1, n2, proto_diseq_proof::mk_axiom());
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+        t.add_eq(n1, n3, proto_eq_proof::mk_axiom());
+        t.add_eq(n2, n4, proto_eq_proof::mk_axiom());
+        t.propagate();
+        SASSERT(t.is_diseq(n3, n4));
+        t.push_scope();
+        literal l1 = t.mk_lit();
+        literal l2 = t.mk_eq(n3, n4);
+        t.mk_main_clause(l1, l2);
+        SASSERT(t.get_assignment(l2) == l_false);
+        t.pop_scope(1);
+        SASSERT(t.get_assignment(l2) == l_false);
+    }
+
+    static void tst13() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_app_core(1, n1);
+        enode * n5 = t.mk_app_core(1, n4);
+        enode * n6 = t.mk_app_core(1, n3);
+        enode * n7 = t.mk_app_core(1, n6);
+        
+        SASSERT(!t.is_relevant(n1));
+        SASSERT(!t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+
+        t.add_eq(n6, n1, proto_eq_proof::mk_axiom());
+
+        SASSERT(!t.is_relevant(n1));
+        SASSERT(!t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+
+        t.push_scope();
+
+        t.assert_lit(t.mk_eq(n7,n2));
+        t.propagate();
+        SASSERT(t.is_equal(n7, n2));
+
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(t.is_relevant(n3));
+        SASSERT(t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(t.is_relevant(n6));        
+        SASSERT(t.is_relevant(n7));
+
+        t.pop_scope(1);
+
+        SASSERT(!t.is_relevant(n1));
+        SASSERT(!t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+    }
+
+    static void tst14() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 2;
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_app_core(1, n1);
+        enode * n5 = t.mk_app_core(1, n4);
+        enode * n6 = t.mk_app_core(1, n3);
+        enode * n7 = t.mk_app_core(1, n6);
+
+        t.assert_lit(t.mk_eq(n1,n2));
+        t.propagate();
+
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+
+        t.push_scope();
+        t.assign_eq(n2, n3, proto_eq_proof::mk_axiom());
+        t.propagate();
+
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+
+        t.pop_scope(1);
+        
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+
+        t.push_scope();
+        t.assign_eq(n2, n7, proto_eq_proof::mk_axiom());
+        t.propagate();
+
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(t.is_relevant(n6));        
+        SASSERT(t.is_relevant(n7));
+        
+        t.pop_scope(1);
+
+        SASSERT(t.is_relevant(n1));
+        SASSERT(t.is_relevant(n2));        
+        SASSERT(!t.is_relevant(n3));
+        SASSERT(!t.is_relevant(n4));        
+        SASSERT(!t.is_relevant(n5));
+        SASSERT(!t.is_relevant(n6));        
+        SASSERT(!t.is_relevant(n7));
+    }
+
+    static void tst15() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+  
+        literal l1 = t.mk_lit();
+        literal l2 = t.mk_lit();
+        literal l3 = t.mk_lit();
+        literal l4 = t.mk_lit();
+        
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+        t.push_scope();
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * a1 = t.mk_app_core(1, n1);
+        enode * a2 = t.mk_app_core(1, n2);
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+
+        literal eq1 = t.mk_eq(a1, n3);
+        t.assign(eq1, mk_axiom());
+
+        t.push_scope();
+        literal eq2 = t.mk_eq(a2, n4);
+        t.assign(eq2, mk_axiom());
+
+        TRACE("core_theory", tout << "eq1: " << eq1 << ", eq2: " << eq2 << "\n";);
+
+        t.mk_transient_clause(~eq2, l3);
+        t.mk_transient_clause(~eq2, l4);
+        t.mk_transient_clause(~eq1, l2);
+        literal_vector lits;
+        lits.push_back(~l4); lits.push_back(~l3); lits.push_back(~l2); lits.push_back(~l1);
+        t.mk_transient_clause(lits);
+        SASSERT(t.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            t.m_sat->resolve_conflict();
+        SASSERT(r);
+        SASSERT(t.m_sat->m_scope_lvl == 2);
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] > 0);
+        SASSERT(t.m_sat->m_ref_count[eq2.var()] > 0);
+        t.pop_scope(2);
+        SASSERT(n1->get_ref_count() > 0);
+        SASSERT(n2->get_ref_count() > 0);
+        SASSERT(a1->get_ref_count() > 0);
+        SASSERT(a2->get_ref_count() > 0);
+        t.push_scope();
+        literal eq3 = t.mk_eq(n1, n2);
+        t.assign(eq3, mk_axiom());
+        t.propagate();
+        TRACE("core_theory", t.display(tout););
+        SASSERT(a1->get_root() == a2->get_root());
+#ifdef  Z3DEBUG
+        t.m_sat->del_learned_clauses();
+#endif 
+        t.pop_scope(1);
+    }
+
+    static void tst16(bool use_relevancy) {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = use_relevancy ? 2 : 0;
+
+        literal l0 = t.mk_lit();
+        literal l1 = t.mk_lit();
+        literal l2 = t.mk_lit();
+        literal l3 = t.mk_lit();
+        literal l4 = t.mk_lit();
+
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_app_core(1, n1);
+        
+        t.push_scope();
+        t.assign(l0, mk_axiom());
+        
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+
+        t.push_scope();
+        enode * n5 = t.mk_app_core(1, n2);
+        enode * n6 = t.mk_const();
+        literal eq1 = t.mk_eq(n5, n6);
+        t.assign(eq1, mk_axiom());
+        t.mk_transient_clause(~l1,  l2);
+        t.mk_transient_clause(~eq1, l3);
+        t.mk_transient_clause(~eq1, l4);
+        literal_vector lits;
+        lits.push_back(~l4); lits.push_back(~l3); lits.push_back(~l2); 
+        t.mk_transient_clause(lits);
+        SASSERT(t.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            t.m_sat->resolve_conflict();
+        SASSERT(r);
+        t.propagate();
+        SASSERT(t.m_sat->m_scope_lvl == 2);
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] > 0);
+        SASSERT(t.m_sat->get_assignment(eq1) == l_false);
+        
+        t.pop_scope(1);
+        SASSERT(t.m_sat->m_scope_lvl == 1);
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] > 0);
+        SASSERT(t.m_sat->get_assignment(eq1) == l_undef);
+
+        t.push_scope();
+        SASSERT(n5->get_ref_count() == 1);
+        t.add_eq(n1, n2, proto_eq_proof::mk_axiom());
+        SASSERT(to_app(n4)->get_cg() == n5);
+        if (use_relevancy) {
+            t.mark_as_relevant(n5);
+        }
+        SASSERT(!use_relevancy || n5->get_ref_count() == 3);
+        SASSERT(use_relevancy || n5->get_ref_count() == 2);
+        SASSERT(n5->get_root() != n4->get_root());
+        SASSERT(!use_relevancy || t.is_relevant(n5));
+        t.propagate();
+        SASSERT(n5->get_root() == n4->get_root());
+        SASSERT(!use_relevancy || n5->get_ref_count() == 4);
+        SASSERT(use_relevancy || n5->get_ref_count() == 3);
+#ifdef  Z3DEBUG
+        t.m_sat->del_learned_clauses();
+#endif 
+        SASSERT(!use_relevancy || n5->get_ref_count() == 3);
+        SASSERT(use_relevancy || n5->get_ref_count() == 2);
+
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] == 0);
+
+        t.pop_scope(1);
+    }
+
+    static void tst17() {
+        theory_idl idl;
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+
+        t.add_theory(&idl);
+
+        literal l0 = t.mk_lit();
+        literal l1 = t.mk_lit();
+        literal l2 = t.mk_lit();
+        literal l3 = t.mk_lit();
+        literal l4 = t.mk_lit();
+        enode * n1 = t.mk_const();
+
+        t.push_scope();
+        t.assign(l0, mk_axiom());
+        
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+
+        t.push_scope();
+        enode * n2 = idl.mk_offset(n1, rational(1));
+        enode * n3 = t.mk_const();
+        literal eq1 = t.mk_eq(n2, n3);
+        t.assign(eq1, mk_axiom());
+        t.mk_transient_clause(~l1,  l2);
+        t.mk_transient_clause(~eq1, l3);
+        t.mk_transient_clause(~eq1, l4);
+        literal_vector lits;
+        lits.push_back(~l4); lits.push_back(~l3); lits.push_back(~l2); 
+        t.mk_transient_clause(lits);
+        SASSERT(t.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            t.m_sat->resolve_conflict();
+        SASSERT(r);
+        t.propagate();
+        SASSERT(t.m_sat->m_scope_lvl == 2);
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] > 0);
+        SASSERT(t.m_sat->get_assignment(eq1) == l_false);
+
+        t.pop_scope(1);
+        SASSERT(t.m_sat->m_scope_lvl == 1);
+        SASSERT(t.m_sat->m_ref_count[eq1.var()] > 0);
+        SASSERT(t.m_sat->get_assignment(eq1) == l_undef);
+        SASSERT(n2->get_ref_count() == 1);
+        unsigned n2_id = n2->get_id();
+
+        // n2 is still alive
+#ifdef  Z3DEBUG
+        t.m_sat->del_learned_clauses();
+#endif 
+        // n2 is dead
+        SASSERT(t.m_enodes[n2_id] == 0);
+        // n2_id cannot be reused since its weak_counter > 0
+        // SASSERT(t.m_weak_counters[n2_id] > 0);
+
+        enode * n4 = idl.mk_offset(n1, rational(1)); 
+        SASSERT(n4->get_id() != n2_id);
+        SASSERT(n4->get_id() < static_cast<unsigned>(t.m_next_id));
+   }
+
+    static void tst18() {
+        core_theory t;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        enode * a1 = t.mk_app_core(1, n1, n2);
+
+        literal l1 = t.mk_eq(n1, n3);
+        t.assert_lit(l1);
+        t.propagate();
+
+        enode * args[2] = { n3, n2 };
+
+        SASSERT(t.get_enode_eq_to_app(1, 2, args) != 0);
+        SASSERT(a1->get_root() == t.get_enode_eq_to_app(1, 2, args)->get_root());
+    }
+
+    static void tst19() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        literal l1 = t.mk_eq(n1, n2);
+        literal l2 = t.mk_eq(n2, n3);
+        literal l3 = t.mk_eq(n1, n3);
+        
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        enode * n6 = t.mk_const();
+        enode * n7 = t.mk_const();
+        
+        literal l4 = t.mk_eq(n4, n5);
+        literal l5 = t.mk_eq(n6, n7);
+        literal l6 = t.mk_eq(n5, n7);
+        literal l7 = t.mk_eq(n4, n6);
+        
+        t.mk_main_clause(l3, l7);
+
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+        t.assign(~l2, mk_axiom());
+        t.assign(l4, mk_axiom());
+        t.assign(l5, mk_axiom());
+        t.assign(~l6, mk_axiom());
+        t.propagate();
+        SASSERT(t.inconsistent());
+        t.m_sat->resolve_conflict();
+    }
+
+    static void tst20() {
+        theory_idl idl;
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+
+        t.add_theory(&idl);
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = idl.mk_offset(n1, rational(1));
+        enode * n3 = idl.mk_offset(n2, rational(1));
+        enode * n4 = idl.mk_offset(n1, rational(2));
+        SASSERT(n4 == n3);
+
+        enode * r1 = idl.mk_num(rational(1));
+        enode * r2 = idl.mk_offset(r1, rational(1));
+        enode * r3 = idl.mk_num(rational(2));
+        SASSERT(r2 == r3);
+    }
+
+    static void tst21() {
+        enable_debug("add_eq");
+        enable_debug("core_invariant");
+        theory_idl idl;
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        t.add_theory(&idl);
+        theory_id  idl_id = idl.get_id();
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        literal l1 = t.mk_eq(n1, n2);
+        literal l2 = t.mk_eq(n1, n3);
+        literal l3 = t.mk_eq(n4, n5);
+        literal l4 = t.mk_eq(n4, n3);
+
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+        t.propagate();
+        SASSERT(n2->get_root() == n2);
+        t.push_scope();
+        t.assign(l2, mk_axiom());
+        t.propagate();
+        t.push_scope();
+        t.assign(l3, mk_axiom());
+        t.propagate();
+        SASSERT(n5->get_root() == n5);
+        SASSERT(n4->get_root() == n5);
+        t.push_scope();
+        t.assign(l4, mk_axiom());
+        t.propagate();
+        SASSERT(n2->get_root() == n2);
+        enode * o1 = idl.mk_offset(n4, rational(1));
+        SASSERT(n4->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n2->get_th_var(idl_id) == n4->get_th_var(idl_id));
+        t.pop_scope(1);
+        SASSERT(n4->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n5->get_th_var(idl_id) == n4->get_th_var(idl_id));
+        SASSERT(n2->get_th_var(idl_id) == null_theory_var);
+        t.pop_scope(1);
+        SASSERT(n4->get_th_var(idl.get_id()) != null_theory_var);
+        SASSERT(n5->get_th_var(idl_id) == null_theory_var);
+        SASSERT(n2->get_th_var(idl_id) == null_theory_var);
+    }
+
+    static void tst22() {
+        enable_debug("add_eq");
+        enable_debug("core_invariant");
+        theory_idl idl;
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        t.add_theory(&idl);
+        theory_id  idl_id = idl.get_id();
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        enode * o1 = idl.mk_offset(n2, rational(1));
+        literal l1 = t.mk_eq(n1, n2);
+        literal l2 = t.mk_eq(n1, n3);
+        literal l3 = t.mk_eq(n4, n5);
+        literal l4 = t.mk_eq(n4, n3);
+        
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+        t.propagate();
+        SASSERT(n2->get_root() == n2);
+       
+        t.push_scope();
+        t.assign(l2, mk_axiom());
+        t.propagate();
+
+        t.push_scope();
+        t.assign(l3, mk_axiom());
+        t.propagate();
+        SASSERT(n5->get_root() == n5);
+        SASSERT(n4->get_root() == n5);
+         
+        t.push_scope();
+        t.assign(l4, mk_axiom());
+        t.propagate();
+        SASSERT(n2->get_root() == n2);
+        enode * o2 = idl.mk_offset(n4, rational(1));
+        SASSERT(n4->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n2->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n2->get_th_var(idl_id) != n4->get_th_var(idl_id));
+        
+        t.pop_scope(1);
+        SASSERT(n2->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n4->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n4->get_th_var(idl_id) == n5->get_th_var(idl_id));
+        
+        t.pop_scope(1);
+        SASSERT(n2->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n4->get_th_var(idl_id) != null_theory_var);
+        SASSERT(n5->get_th_var(idl_id) == null_theory_var);
+    }
+
+    static void tst23() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        enable_trace("th_diseq_prop_bug");
+        enable_trace("add_eq");
+
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_true_term();
+        enode * d[2] = {n1, n2};
+        t.assert_distinct_class(2, d);
+        enode * n3 = t.mk_const();
+        enode * n4 = t.mk_const();
+        
+        literal l1 = t.mk_eq(n3, n4);
+        literal l2 = t.mk_eq(n4, n1);
+        literal l3 = t.mk_eq(n3, n2);
+        t.push_scope();
+        t.assign(l1, mk_axiom());
+        t.propagate();
+        SASSERT(n3->get_root() == n4->get_root());
+        t.push_scope();
+        t.assign(l2, mk_axiom());
+        t.propagate();
+        SASSERT(n3->get_root() == n1->get_root());
+        SASSERT(t.is_diseq(n3, n2));
+        SASSERT(t.get_assignment(l3) == l_false);
+        SASSERT(t.m_sat->m_explanation[l3.var()].kind() == EXPL_EXT);
+        literal_vector antecedents;
+        t.get_antecedents(~l3, t.m_sat->m_explanation[l3.var()].obj(), antecedents);
+    }
+
+public:
+    static void run_tests() {
+        tst1();
+        tst2();
+        tst3();
+        tst8();
+        tst9();
+        tst10();
+        tst11();
+        tst12();
+        tst13();
+        tst14();
+        tst15();
+        tst16(false);
+        tst16(true);
+        tst17();
+        tst18();
+        tst19();
+        tst20();
+        tst21();
+        tst22();
+        tst23();
+    }
+};
+
+struct foo {
+    bool_var  m_var;        // boolean variable associated with the equation
+    enode *   m_lhs;
+    enode *   m_rhs;
+};
+
+struct bar {
+    bool m_v1:1;
+    bool m_v2:1;
+    bool m_v3:1;
+    bool m_v4:1;
+    bool m_v5:1;
+    bool m_v6:1;
+    bool m_v7:1;
+    bool m_v8:1;
+};
+
+struct bar2 {
+    bool     m_v1:1;
+    bool     m_v2:1;
+    unsigned m_val:30;
+};
+
+void tst_core_theory() {
+    TRACE("core_theory", tout << "sizeof(equation): " << sizeof(equation) << "\n";);
+    TRACE("core_theory", tout << "sizeof(foo):  " << sizeof(foo) << "\n";);
+    TRACE("core_theory", tout << "sizeof(bar):  " << sizeof(bar) << "\n";);
+    TRACE("core_theory", tout << "sizeof(bar2): " << sizeof(bar2) << "\n";);
+    TRACE("core_theory", tout << "sizeof(theory_var_list): " << sizeof(theory_var_list) << "\n";);
+    TRACE("core_theory", tout << "sizeof(enode): " << sizeof(enode) << "\n";);
+    enable_debug("cg_bug");
+    core_theory_tester::run_tests();
+}
+

src/dead/test/dimacs.cpp

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    tst_dimacs.cpp
+
+Abstract:
+
+    Test dimacs parser
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-02.
+
+Revision History:
+
+--*/
+
+#include <iostream>
+#include <fstream>
+#ifdef _WINDOWS
+#include <windows.h>
+#include <strsafe.h>
+#endif
+#include"trace.h"
+#include"dimacs_parser.h"
+
+class dummy_sat {
+    unsigned m_num_vars;
+public:
+    dummy_sat():m_num_vars(0) {}
+    unsigned get_num_vars() { 
+        return m_num_vars;
+    }
+    void mk_var() {
+        TRACE("dimacs", tout << "making variable: p" << m_num_vars << "\n";);
+        m_num_vars++;
+    }
+    void mk_clause(literal_vector & lits) {
+        TRACE("dimacs", tout << "making clause: " << lits << "\n";);
+    }
+};
+
+static void tst1()
+{
+#ifdef _WINDOWS
+    dummy_sat solver;
+    const char * base = ".";
+    std::string pattern(base);
+    pattern += "\\*.cnf";
+
+    char buffer[MAX_PATH];
+    
+    WIN32_FIND_DATAA data;
+    HANDLE h = FindFirstFileA(pattern.c_str(),&data);
+
+    while (h != INVALID_HANDLE_VALUE) {
+        StringCchPrintfA(buffer, ARRAYSIZE(buffer), "%s\\%s", base, data.cFileName);       
+        
+        TRACE("dimacs", tout << "Parsing: " << buffer << "\n";);
+        
+        std::ifstream s(buffer);
+
+        parse_dimacs(s, solver);
+
+        if (!FindNextFileA(h,&data))
+            break;
+    }
+#endif
+}
+
+void tst_dimacs() {
+    tst1();
+}

src/dead/test/distinct.cpp

@@ -0,0 +1,296 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    distinct.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-11-03.
+
+Revision History:
+
+--*/
+#include"core_theory.h"
+
+class distinct_tester {
+    static void tst1() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        enode * d[3] = {n1, n2, n3};
+        
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        enode * n6 = t.mk_const();
+        
+        t.assert_distinct_class(3, d);
+        TRACE("distinct", t.display(tout););
+        t.propagate();
+
+        t.push();
+        
+        t.assert_lit(t.mk_eq(n1, n2));
+        t.propagate();
+        SASSERT(t.inconsistent());
+        
+        t.pop(1);
+        SASSERT(!t.inconsistent());
+        TRACE("distinct", t.display(tout););
+
+        t.push_scope();
+
+        t.assign(t.mk_eq(n1, n4), mk_axiom());
+        t.assign(t.mk_eq(n2, n5), mk_axiom());
+        t.assign(t.mk_eq(n2, n6), mk_axiom());
+        t.propagate();
+        SASSERT(!t.inconsistent());
+
+        t.assign(t.mk_eq(n4,n5), mk_axiom());
+        t.propagate();
+        TRACE("distinct", t.display(tout););
+        SASSERT(t.inconsistent());
+    }
+    
+    static void tst2() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        t.assert_lit(t.mk_eq(n1,n3));
+        t.propagate();
+
+        enode * d[3] = {n1, n2, n3};
+        
+        t.assert_distinct_class(3, d);
+        SASSERT(t.inconsistent());
+    }
+
+    static void tst3() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        t.assert_lit(t.mk_eq(n1,n3));
+
+        enode * d[3] = {n1, n2, n3};
+        
+        t.assert_distinct_class(3, d);
+        
+        t.propagate();
+        SASSERT(t.inconsistent());
+    }
+
+    static void tst4() {
+#ifdef ENABLE_DISTINCT_CLASSES_SUPPORT
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        t.push();
+   
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        enode * d1[3] = {n1, n2, n3};
+        
+        t.assert_distinct_class(3, d1);
+
+        SASSERT(n1->get_distinct_classes() == 1);
+        SASSERT(n2->get_distinct_classes() == 1);
+        SASSERT(n3->get_distinct_classes() == 1);
+        
+        enode * n4 = t.mk_const();
+        enode * n5 = t.mk_const();
+        enode * n6 = t.mk_const();
+
+        enode * d2[3] = {n4, n5, n6};
+        
+        t.assert_distinct_class(3, d2);
+        
+        SASSERT(n4->get_distinct_classes() == 2);
+        SASSERT(n5->get_distinct_classes() == 2);
+        SASSERT(n6->get_distinct_classes() == 2);
+
+        enode * n7 = t.mk_const();
+        enode * n8 = t.mk_const();
+        enode * n9 = t.mk_const();
+
+        enode * d3[3] = {n7, n8, n9};
+        
+        t.assert_distinct_class(3, d3);
+        
+        SASSERT(n7->get_distinct_classes() == 4);
+        SASSERT(n8->get_distinct_classes() == 4);
+        SASSERT(n9->get_distinct_classes() == 4);
+
+        enode * n10 = t.mk_const();
+        enode * n11 = t.mk_const();
+        enode * n12 = t.mk_const();
+
+        enode * d4[3] = {n10, n11, n12};
+        
+        t.assert_distinct_class(3, d4);
+
+        SASSERT(n10->get_distinct_classes() == 8);
+        SASSERT(n11->get_distinct_classes() == 8);
+        SASSERT(n12->get_distinct_classes() == 8);
+        
+        t.push_scope();
+        
+        t.assign(t.mk_eq(n7, n1), mk_axiom());
+        t.propagate();
+        SASSERT(!t.inconsistent());
+        SASSERT(n1->get_root()->get_distinct_classes() == 5);
+
+        t.push_scope();
+        
+        t.assign(t.mk_eq(n11, n5), mk_axiom());
+        t.propagate();
+        SASSERT(!t.inconsistent());
+        SASSERT(n5->get_root()->get_distinct_classes() == 10);
+
+        t.push_scope();
+        t.assign(t.mk_eq(n7, n3), mk_axiom());
+        t.propagate();
+        SASSERT(t.inconsistent());
+
+        t.pop_scope(1);
+        SASSERT(!t.inconsistent());
+
+        t.push_scope();
+
+        t.assign(t.mk_eq(n11, n1), mk_axiom());
+        t.propagate();
+        SASSERT(!t.inconsistent());
+        SASSERT(n1->get_root()->get_distinct_classes() == 15);
+
+        t.pop_scope(1);
+        
+        SASSERT(!t.inconsistent());
+        SASSERT(n1->get_root()->get_distinct_classes()  == 5);
+        SASSERT(n11->get_root()->get_distinct_classes() == 10);
+        SASSERT(n5->get_root()->get_distinct_classes() == 10);
+
+        t.pop_scope(1);
+        SASSERT(n1->get_root()->get_distinct_classes()  == 5);
+        SASSERT(n7->get_root()->get_distinct_classes()  == 5);
+        SASSERT(n11->get_root()->get_distinct_classes() == 8);
+        SASSERT(n5->get_root()->get_distinct_classes()  == 2);
+        
+        t.pop_scope(1);
+        SASSERT(n1->get_root()->get_distinct_classes()  == 1);
+        SASSERT(n7->get_root()->get_distinct_classes()  == 4);
+        SASSERT(n11->get_root()->get_distinct_classes() == 8);
+        SASSERT(n5->get_root()->get_distinct_classes()  == 2);
+        
+        SASSERT(t.m_num_distinct_classes == 4);
+
+        t.pop(1);
+
+        SASSERT(t.m_num_distinct_classes == 0);
+#endif
+    }
+
+    static void tst5() {
+#ifdef ENABLE_DISTINCT_CLASSES_SUPPORT
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        t.push();
+
+        enode * n1;
+        enode * n2;
+        enode * n3;
+
+        for (unsigned i = 0; i < 40; i++) {
+            n1 = t.mk_const();
+            n2 = t.mk_const();
+            n3 = t.mk_const();
+            
+            enode * d1[3] = {n1, n2, n3};
+            
+            t.assert_distinct_class(3, d1);
+        }
+
+        SASSERT(t.m_num_distinct_classes == 32);
+        SASSERT(n1->get_root()->get_distinct_classes() == 0);
+
+        t.push_scope();
+        t.assign(t.mk_eq(n1, n3), mk_axiom());
+        t.propagate();
+        
+        SASSERT(t.inconsistent());
+
+        t.pop_scope(1);
+        SASSERT(!t.inconsistent());
+
+        t.pop(1);
+        SASSERT(t.m_num_distinct_classes == 0);
+
+        n1 = t.mk_const();
+        n2 = t.mk_const();
+        n3 = t.mk_const();
+
+        enode * d1[3] = {n1, n2, n3};
+        
+        t.assert_distinct_class(3, d1);
+        SASSERT(n1->get_root()->get_distinct_classes() == 1);
+#endif
+    }
+
+    static void tst6() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+
+        t.push_scope();
+        
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+
+        enode * d1[3] = {n1, n2, n3};
+        
+        t.assert_distinct_class(3, d1);
+        
+        SASSERT(t.m_num_distinct_classes == 0);
+        SASSERT(n1->get_root()->get_distinct_classes() == 0);
+
+        t.assign(t.mk_eq(n1, n3), mk_axiom());
+        t.propagate();
+        
+        SASSERT(t.inconsistent());
+    }
+
+public:
+    
+    static void run_tests() {
+        tst1();
+        tst2();
+        tst3();
+        tst4();
+        tst5();
+        tst6();
+    }
+};
+
+
+void tst_distinct() {
+    enable_trace("core_theory_conflict");
+    distinct_tester::run_tests();
+}
+

src/dead/test/fingerprint.cpp

@@ -0,0 +1,101 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    fingerprint.cpp
+
+Abstract:
+
+    Test fingerprint support
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-29.
+
+Revision History:
+
+--*/
+#include"core_theory.h"
+
+bool add_fingerprint(core_theory & t, void * data, enode * n1) {
+    enode * c[1];
+    c[0] = n1;
+    return t.add_fingerprint(data, 1, c);
+}
+
+bool add_fingerprint(core_theory & t, void * data, enode * n1, enode * n2) {
+    enode * c[2];
+    c[0] = n1;
+    c[1] = n2;
+    return t.add_fingerprint(data, 2, c);
+}
+
+bool add_fingerprint(core_theory & t, void * data, enode * n1, enode * n2, enode * n3, enode * n4, enode * n5, enode * n6, enode * n7, enode * n8, enode * n9) {
+    enode * c[9];
+    c[0] = n1;
+    c[1] = n2;
+    c[2] = n3;
+    c[3] = n4;
+    c[4] = n5;
+    c[5] = n6;
+    c[6] = n7;
+    c[7] = n8;
+    c[8] = n9;
+    return t.add_fingerprint(data, 9, c);
+}
+
+class fingerprint_tester {
+
+    static void tst1() {
+        core_theory t;
+        enode * n1 = t.mk_const();
+        enode * n2 = t.mk_const();
+        enode * n3 = t.mk_const();
+        void * d1 = reinterpret_cast<void *>(1);
+        
+        SASSERT(add_fingerprint(t, 0, n1));
+        SASSERT(!add_fingerprint(t, 0, n1));
+        SASSERT(add_fingerprint(t, 0, n2));
+
+        SASSERT(add_fingerprint(t, d1, n1));
+        SASSERT(!add_fingerprint(t, d1, n1));
+        SASSERT(add_fingerprint(t, d1, n2));
+        SASSERT(add_fingerprint(t, d1, n1, n2));
+        SASSERT(add_fingerprint(t, d1, n2, n1));
+        SASSERT(!add_fingerprint(t, d1, n1, n2));
+        SASSERT(!add_fingerprint(t, d1, n2, n1));
+        
+        t.push_scope();
+        
+        SASSERT(add_fingerprint(t, 0, n3));
+        SASSERT(add_fingerprint(t, d1, n3));
+        SASSERT(add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n2)); 
+        SASSERT(!add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n2)); 
+        SASSERT(add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n1)); 
+        SASSERT(!add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n1)); 
+        
+        t.pop_scope(1);
+        
+        SASSERT(!add_fingerprint(t, 0, n1));
+        SASSERT(!add_fingerprint(t, 0, n2));
+        SASSERT(!add_fingerprint(t, d1, n1, n2));
+        SASSERT(!add_fingerprint(t, d1, n2, n1));
+        SASSERT(add_fingerprint(t, 0, n3));
+        SASSERT(add_fingerprint(t, d1, n3));
+        SASSERT(add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n2)); 
+        SASSERT(!add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n2)); 
+        SASSERT(add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n1)); 
+        SASSERT(!add_fingerprint(t, d1, n1, n1, n1, n1, n1, n1, n2, n1, n1)); 
+    }
+
+public:
+    
+    static void run_tests() {
+        tst1();
+    }
+};
+
+void tst_fingerprint() {
+    fingerprint_tester::run_tests();
+}

src/dead/test/gate.cpp

@@ -0,0 +1,472 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    gate.cpp
+
+Abstract:
+
+    Test SAT gates
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-11-02.
+
+Revision History:
+
+--*/
+#include"sat_def.h"
+
+class gate_extension : public no_extension {
+public:
+    bool relevancy_enabled() {
+        return true;
+    }
+
+    bool gates_enabled() {
+        return true;
+    }
+};
+
+
+class gate_no_rel_extension : public no_extension {
+public:
+    bool relevancy_enabled() {
+        return false;
+    }
+
+    bool gates_enabled() {
+        return true;
+    }
+};
+
+class sat_gate_tester {
+
+    static void tst1() {
+        sat_solver<gate_no_rel_extension> solver; 
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        
+        SASSERT(solver.mk_or(l1, l2, l3) == solver.mk_or(l3, l1, l2));
+        
+        SASSERT(solver.mk_or(l1, l1, l3) == solver.mk_or(l3, l1));
+    
+        SASSERT(solver.mk_or(l1, l1, l1) == l1);
+    
+        SASSERT(solver.mk_or(l1, false_literal, l1) == l1);
+        
+        SASSERT(solver.mk_or(l1, true_literal, l1) == true_literal);
+
+        solver.assert_lit(l1);
+
+        SASSERT(solver.mk_or(l1, l2, l3) == true_literal);
+
+        literal l4 = solver.mk_or(l2, l3);
+    
+        SASSERT(l4 != true_literal && l4 != false_literal);
+    
+        solver.push();
+
+        solver.assert_lit(l2);
+    
+        solver.propagate();
+    
+        SASSERT(solver.get_assignment(l4) == l_true);
+
+        solver.pop(1);
+
+        SASSERT(solver.get_assignment(l4) == l_undef);
+
+        solver.push();
+    
+        solver.assert_lit(~l2);
+    
+        solver.assert_lit(~l3);
+
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l4) == l_false);
+
+        solver.pop(1);
+
+        SASSERT(solver.get_assignment(l4) == l_undef);
+
+        SASSERT(l4 == ~solver.mk_and(~l2, ~l3));
+    }
+
+    static void tst1a() {
+        sat_solver<gate_extension> solver; 
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        
+        SASSERT(solver.mk_or(l1, l2, l3) == solver.mk_or(l3, l1, l2));
+        
+        SASSERT(solver.mk_or(l1, l1, l3) == solver.mk_or(l3, l1));
+    
+        SASSERT(solver.mk_or(l1, l1, l1) == l1);
+    
+        SASSERT(solver.mk_or(l1, false_literal, l1) == l1);
+        
+        SASSERT(solver.mk_or(l1, true_literal, l1) == true_literal);
+
+        solver.assert_lit(l1);
+
+        SASSERT(solver.mk_or(l1, l2, l3) != true_literal);
+
+        literal l4 = solver.mk_or(l2, l3);
+    
+        SASSERT(l4 != true_literal && l4 != false_literal);
+    
+        solver.push();
+
+        solver.assert_lit(l2);
+    
+        solver.propagate();
+    
+        SASSERT(solver.get_assignment(l4) == l_true);
+
+        solver.pop(1);
+
+        SASSERT(solver.get_assignment(l4) == l_undef);
+
+        solver.push();
+    
+        solver.assert_lit(~l2);
+    
+        solver.assert_lit(~l3);
+
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l4) == l_false);
+
+        solver.pop(1);
+
+        SASSERT(solver.get_assignment(l4) == l_undef);
+
+        SASSERT(l4 == ~solver.mk_and(~l2, ~l3));
+    }
+
+    static void tst2() {
+        sat_solver<gate_extension> solver; 
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+
+        SASSERT(solver.mk_iff(l1, l2) == solver.mk_iff(l2, l1));
+
+        SASSERT(solver.mk_iff(l1, true_literal) == l1);
+
+        SASSERT(solver.mk_iff(l1, false_literal) == ~l1);
+
+        SASSERT(solver.mk_iff(true_literal, l2) == l2);
+
+        SASSERT(solver.mk_iff(false_literal, l2) == ~l2);
+
+        SASSERT(solver.mk_iff(l1, l1) == true_literal);
+
+        SASSERT(solver.mk_iff(l1, ~l1) == false_literal);
+    }
+
+    static void tst3() {
+        sat_solver<gate_extension> solver; 
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+
+        solver.push();
+
+        literal l3 = solver.mk_or(l1, l2);
+        SASSERT(solver.m_ref_count[l3.var()] == 1);
+
+        solver.pop(1);
+    }
+
+    static void tst4() {
+        sat_solver<gate_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+
+        literal l3 = solver.mk_or(l1, l2);
+        
+        solver.reset();
+        
+        l1 = solver.mk_var();
+
+    }
+
+    static void tst5() {
+        sat_solver<gate_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+
+        solver.push_scope();
+
+        solver.assign(l1, mk_axiom());
+
+        solver.propagate();
+        
+        solver.push_scope();
+
+        literal l4 = solver.mk_or(l1, l2);
+
+        solver.mk_main_clause(l4, l3);
+
+        SASSERT(solver.get_assignment(l4) == l_true);
+        
+        solver.pop_scope(1);
+
+        SASSERT(solver.get_assignment(l4) == l_true);
+    }
+
+    static void tst6() {
+        sat_solver<gate_no_rel_extension> solver;
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        literal l4 = solver.mk_var();
+
+        SASSERT(solver.mk_ite(l1, l2, l3) == solver.mk_ite(~l1, l3, l2));
+
+        SASSERT(solver.mk_ite(l1, l2, l2) == l2);
+
+        solver.assert_lit(l1);
+
+        solver.push_scope();
+
+        SASSERT(solver.mk_ite(l1, l2, l3) == l2);
+
+        SASSERT(solver.mk_ite(~l1, l2, l3) == l3);
+    }
+
+    static void tst6a() {
+        sat_solver<gate_extension> solver;
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        literal l4 = solver.mk_var();
+
+        SASSERT(solver.mk_ite(l1, l2, l3) == solver.mk_ite(~l1, l3, l2));
+
+        SASSERT(solver.mk_ite(l1, l2, l2) == l2);
+
+        solver.assert_lit(l1);
+
+        solver.push_scope();
+
+        SASSERT(solver.mk_ite(l1, l2, l3) != l2);
+
+        SASSERT(solver.mk_ite(~l1, l2, l3) != l3);
+    }
+
+    static void tst7() {
+        sat_solver<gate_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_uniq(l1);
+        SASSERT(l1 != l2);
+
+        solver.push();
+
+        solver.assert_lit(l1);
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.get_assignment(l2) == l_true);
+        
+        solver.pop(1);
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l1) == l_undef);
+        SASSERT(solver.get_assignment(l2) == l_undef);
+
+        solver.assert_lit(~l1);
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l1) == l_false);
+        SASSERT(solver.get_assignment(l2) == l_false);
+    }
+
+    static void tst8() {
+        sat_solver<gate_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_uniq(l1);
+        SASSERT(l1 != l2);
+
+        solver.push_scope();
+
+        solver.assert_lit(l1);
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.get_assignment(l2) == l_true);
+        
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.get_assignment(l2) == l_true);
+    }
+
+    static void tst9() {
+        sat_solver<gate_extension> s;
+        
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        literal l3 = s.mk_var();
+        
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.push_scope();
+        literal l4 = s.mk_var();
+        literal l5 = s.mk_var();
+        literal l6 = s.mk_or(l4, l5);
+        s.assign(l6, mk_axiom());
+        s.mk_transient_clause(~l6, l3);
+        s.mk_transient_clause(~l6, l2);
+        s.mk_transient_clause(literal_vector(~l3, ~l1, ~l2));
+        SASSERT(s.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.m_scope_lvl == 1);
+        SASSERT(s.m_ref_count[l4.var()] > 0);
+        SASSERT(s.m_ref_count[l5.var()] > 0);
+        SASSERT(s.m_ref_count[l6.var()] > 0);
+        s.pop_scope(1);
+        SASSERT(s.get_assignment(l1) == l_undef);
+        SASSERT(s.get_assignment(l4) == l_undef);
+        SASSERT(s.get_assignment(l5) == l_undef);
+        SASSERT(s.get_assignment(l6) == l_undef);
+        SASSERT(s.m_ref_count[l4.var()] > 0);
+        SASSERT(s.m_ref_count[l5.var()] > 0);
+        SASSERT(s.m_ref_count[l6.var()] > 0);
+        s.push_scope();
+        s.assign(~l4, mk_axiom());
+        s.propagate();
+#ifdef  Z3DEBUG
+        s.del_learned_clauses();
+#endif 
+        s.pop_scope(1);
+    }
+    
+    static void tst10() {
+        sat_solver<gate_extension> s;
+        
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        literal l3 = s.mk_var();
+        
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.push_scope();
+        literal l4 = s.mk_var();
+        literal l5 = s.mk_var();
+        literal l6 = s.mk_iff(l4, l5);
+        literal l7 = s.mk_var();
+        literal l8 = s.mk_or(l6, l7);
+        s.assign(l8, mk_axiom());
+        s.mk_transient_clause(~l8, l3);
+        s.mk_transient_clause(~l8, l2);
+        s.mk_transient_clause(literal_vector(~l3, ~l1, ~l2));
+        SASSERT(s.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.m_scope_lvl == 1);
+        s.pop_scope(1);
+        SASSERT(s.m_ref_count[l4.var()] > 0);
+        SASSERT(s.m_ref_count[l5.var()] > 0);
+        SASSERT(s.m_ref_count[l6.var()] > 0);
+        SASSERT(s.m_ref_count[l7.var()] > 0);
+        SASSERT(s.m_ref_count[l8.var()] > 0);
+        s.push_scope();
+        s.assign(~l1, mk_axiom());
+        s.push_scope();
+        s.assign(l5, mk_axiom());
+        s.mk_transient_clause(~l5, ~l4);
+        s.propagate();
+        SASSERT(s.get_assignment(l6) == l_false);
+        SASSERT(s.get_assignment(l8) == l_undef);
+#ifdef  Z3DEBUG
+        s.del_learned_clauses();
+        SASSERT(s.m_ref_count[l7.var()] == 0);
+        SASSERT(s.m_ref_count[l8.var()] ==  0);
+        SASSERT(s.m_ref_count[l4.var()] > 0);
+        SASSERT(s.m_ref_count[l5.var()] > 0);
+        SASSERT(s.m_ref_count[l6.var()] > 0);
+#endif 
+        s.mk_transient_clause(l6, l3);
+        s.mk_transient_clause(l6, l2);
+        s.mk_transient_clause(literal_vector(~l3, l1, ~l2));
+        SASSERT(s.inconsistent());
+#ifdef  Z3DEBUG
+        r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+    }
+
+    static void tst11() {
+        sat_solver<gate_extension> s;
+
+        literal l0 = s.mk_var();
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        
+        s.push_scope();
+        s.assign(~l1, mk_axiom());
+        s.assign(~l2, mk_axiom());
+        s.push_scope();
+        literal l3 = s.mk_or(l1, l2);
+        SASSERT(s.get_assignment(l3) == l_false);
+        s.mk_main_clause(l0, l1, l3);
+        SASSERT(s.m_ref_count[l3.var()] == 3);
+        s.pop_scope(1);
+        SASSERT(s.m_ref_count[l3.var()] == 2);
+        SASSERT(s.get_assignment(l3) == l_false);
+        s.assert_lit(l1);
+        s.propagate();
+        SASSERT(s.inconsistent());
+    }
+  
+public:
+    static void run_tests() {
+        enable_trace("del_gate");
+        enable_trace("sat_solver");
+        enable_trace("gate");
+        enable_trace("del_learned_clauses");
+        tst1();
+        tst1a();
+        tst2();
+        tst3();
+        tst4();
+        tst5();
+        tst6();
+        tst6a();
+        tst7();
+        tst8();
+        tst9();
+        tst10();
+        tst11();
+    }
+};
+
+void tst_gate() {
+    sat_gate_tester::run_tests();
+}

src/dead/test/interval_arithmetic.cpp

@@ -0,0 +1,243 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    interval_arithmetic.cpp
+
+Abstract:
+
+    Test interval arithmetic
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2006-12-05.
+
+Revision History:
+
+--*/
+#include<iostream>
+#include"interval_arithmetic.h"
+#include"trace.h"
+
+
+template<class number, class epsilon>
+void tst_ext_number() {
+    typedef ext_number<number, epsilon> num;
+    num zero;
+    num one(1);
+    num eps(num::epsilon());
+    num m_eps(num::epsilon().neg());
+    num two(number(2));
+    num half(number(1,2));
+    num inf = num::infinity();
+    num eps1 = num::epsilon();
+    num three(number(3));
+    num three_e = num::plus(three, num::epsilon());
+    SASSERT(zero.get_sign() == num::ZERO);
+    SASSERT(one.get_sign() == num::POSITIVE);
+    SASSERT(m_eps.get_sign() == num::NEGATIVE);
+    SASSERT(inf.get_sign() == num::POSITIVE);
+    SASSERT(zero.is_zero());
+    SASSERT(!one.is_zero());
+    SASSERT(!inf.is_zero());
+    SASSERT(inf.is_infinite());
+    SASSERT(!one.is_infinite());
+    SASSERT(one.is_pos());
+    SASSERT(m_eps.is_neg());
+    SASSERT(one != zero);
+    SASSERT(inf != one);
+    SASSERT(inf != zero);
+    SASSERT(zero == zero);
+    SASSERT(zero < one);
+    SASSERT(eps < two);
+    SASSERT(zero < eps);
+    SASSERT(zero < inf);
+    SASSERT(zero == min(zero, eps));
+    SASSERT(zero == min(zero, inf));
+    SASSERT(eps == max(zero, eps));
+    SASSERT(inf == max(zero, inf));
+    SASSERT(min(zero,eps) == min(eps,zero));
+    SASSERT(num::plus(zero, eps) == eps);
+    SASSERT(num::plus(zero, one) == one);
+    SASSERT(num::plus(zero, inf) == inf);
+    SASSERT(num::plus(inf, inf) == inf);
+    SASSERT(inf.neg() < inf);
+    SASSERT(inf.neg() < zero);
+    SASSERT(num::minus(zero, one) == one.neg());
+    SASSERT(num::minus(zero, eps) == eps.neg());
+    SASSERT(num::minus(zero, inf) == inf.neg());
+    SASSERT(num::minus(zero, inf.neg()) == inf);
+    SASSERT(num::minus(inf, inf.neg()) == inf);
+
+    // sup_mult, inf_mult
+    SASSERT(sup_mult(zero, one) == zero);
+    SASSERT(sup_mult(one, one) == one);
+    SASSERT(sup_mult(one, one.neg()) == one.neg());
+    SASSERT(inf_mult(zero, one) == zero);
+    SASSERT(inf_mult(one, one) == one);
+    SASSERT(inf_mult(one, one.neg()) == one.neg());
+
+    // sup_div, inf_div 
+    SASSERT(one < sup_div(three_e, three));
+    SASSERT(inf_div(three, three_e) < one);
+    SASSERT(inf_div(three_e, three) < two);
+    SASSERT(inf_div(three.neg(), three_e.neg()) < one);
+    SASSERT(one < sup_div(three_e.neg(), three.neg()));
+    SASSERT(inf_div(three_e.neg(), three.neg()) < two);
+
+    // sup_power, inf_power
+    SASSERT(sup_power(one,3) == one);
+    SASSERT(sup_power(one,3) > zero);
+    SASSERT(sup_power(num::plus(one, num::epsilon()),3) > one);
+
+    SASSERT(sup_power(one,2) == one);
+    SASSERT(sup_power(one,2) > zero);
+    SASSERT(sup_power(num::plus(one, num::epsilon()),2) > one);
+
+    // sup_root, inf_root    
+    SASSERT(sup_root(one,2) >= zero);
+    SASSERT(inf_root(one,2) <= one);
+    SASSERT(sup_root(zero,2) >= zero);
+    SASSERT(inf_root(zero,2) <= zero);
+
+}
+
+template<class number, class epsilon>
+void tst_interval()
+{
+    typedef interval<number, epsilon> interval;
+    typedef ext_number<number, epsilon> ext_num;
+    ext_num m_inf(ext_num::infinity().neg());
+    ext_num m_three(ext_num(3).neg());
+    ext_num m_three_m_e(ext_num::plus(ext_num(3), ext_num::epsilon()).neg());
+    ext_num m_three_p_e(ext_num::plus(ext_num(3), ext_num::epsilon().neg()).neg()); 
+    ext_num m_eps(ext_num::epsilon().neg());
+    ext_num zero(0);
+    ext_num eps(ext_num::epsilon());
+    ext_num three(ext_num(3));
+    ext_num three_m_e(ext_num::minus(ext_num(3), ext_num::epsilon())); 
+    ext_num three_p_e(ext_num::plus(ext_num(3), ext_num::epsilon())); 
+    ext_num inf(ext_num::infinity());
+    ext_num nums[] = { m_inf, m_three_m_e, m_three, m_three_p_e, m_eps, zero, eps, three_m_e, three, three_p_e, inf };
+
+    unsigned n_nums = 11;
+    //
+    // add_lower
+    // add_upper
+    //
+    for (unsigned i = 0; i < n_nums; ++i) {
+        for (unsigned j = i+1; j < n_nums; ++j) {
+
+            for (unsigned k = 0; k < n_nums; ++k) {
+                interval i1(nums[i], nums[j]);
+                bool ok = i1.add_lower(nums[k]);
+                TRACE("interval_arithmetic", tout << "lower: " << ok << " " 
+                      << nums[k] << " " << i1 << std::endl;);
+            }
+
+            for (unsigned k = 0; k < n_nums; ++k) {
+                interval i1(nums[i], nums[j]);
+                bool ok = i1.add_upper(nums[k]);
+                TRACE("interval_arithmetic", tout << "upper: " << ok << " " 
+                      << nums[k] << " " << i1 << std::endl;);
+            }
+        }
+    }
+
+    //
+    // +
+    // *
+    // -
+    // quotient
+    //
+    for (unsigned i = 0; i < n_nums; ++i) {
+        for (unsigned j = i+1; j < n_nums; ++j) {
+            interval i1(nums[i],nums[j]);
+            
+            interval x = i1.power(0);
+            interval y = i1.power(1);
+            interval z = i1.power(2);
+            interval x1 = i1.power(3);
+
+            for (unsigned k = 0; k < n_nums; ++k) {
+                for (unsigned l = k+1; l < n_nums; ++l) {
+                    interval i2(nums[k],nums[l]);
+                    interval i3 = i1 + i2;
+                    interval i4 = i1 - i2;
+                    interval i5 = i1 * i2;
+                    TRACE("interval_arithmetic", tout << i1 << " + " << i2 << " = " << i3 << std::endl;);
+                    TRACE("interval_arithmetic", tout << i1 << " - " << i2 << " = " << i4 << std::endl;);
+                    TRACE("interval_arithmetic", tout << i1 << " * " << i2 << " = " << i5 << std::endl;);
+                    SASSERT(i5 == i2 * i1);
+                    vector<interval, true> intervals;
+                    interval::quotient(i1, i2, intervals);
+                    TRACE("interval_arithmetic", 
+                          tout << i1 << " / " << i2 << " = " ;
+                          for (unsigned idx = 0; idx < intervals.size(); ++idx) {
+                              tout << intervals[idx] << " ";
+                          }
+                          tout << std::endl;
+                          );
+
+                    unsigned changed_bounds;
+                    x = i1;
+                    y = i2;
+                    z = i3;
+                    TRACE("interval_arithmetic", tout << "check: " << i1 << "=" << i2 << "*" << i3 << std::endl;);
+                    if (interval::check_mult(x, y, z, changed_bounds)) {
+                        TRACE("interval_arithmetic", tout << x << "=" << y << "*" << z << std::endl;);
+                        SASSERT (!!(changed_bounds & 0x1) == (x.low() != i1.low()));
+                        SASSERT (!!(changed_bounds & 0x2) == (x.high() != i1.high()));
+                        SASSERT (!!(changed_bounds & 0x4) == (y.low() != i2.low()));
+                        SASSERT (!!(changed_bounds & 0x8) == (y.high() != i2.high()));
+                        SASSERT (!!(changed_bounds & 0x10) == (z.low() != i3.low()));
+                        SASSERT (!!(changed_bounds & 0x20) == (z.high() != i3.high()));                            
+                    }
+                    else {
+                        TRACE("interval_arithmetic", tout << "unsat" << std::endl;);
+                    }
+
+                    x = i1;
+                    y = i2;
+                    if (interval::check_power(x, y, 3, changed_bounds)) {
+                        TRACE("interval_arithmetic", 
+                              tout << "check: " << i1 << "=" << i2 << "^3" << " -> " 
+                              << x << " = " << y << "^3" << std::endl;);
+                    }
+                    else {
+                        TRACE("interval_arithmetic", tout << "unsat: " << i1 << "=" << i2 << "^4" << std::endl;);
+                    }
+
+
+                    x = i1;
+                    y = i2;
+					if (interval::check_power(x, y, 4, changed_bounds)) {
+                        TRACE("interval_arithmetic", 
+                              tout << "check: " << i1 << "=" << i2 << "^4" << " -> " 
+                              << x << " = " << y << "^4" << std::endl;);
+                    }
+                    else {
+                        TRACE("interval_arithmetic", tout << "unsat: " << i1 << "=" << i2 << "^4" << std::endl;);
+                    }
+                }
+            }
+        }
+    }
+
+
+    // check_mult(i1, i2, i3, change_bounds);
+
+    // check_power(i1, i2, power, changed_bounds);
+}
+
+struct eps1 { rational operator()() { return rational(1); } };
+struct eps0 { inf_rational operator()() { return inf_rational(rational(0),true); } };
+
+void tst_interval_arithmetic() {
+    TRACE("interval_arithmetic", tout << "starting interval_arithmetic test...\n";);
+    tst_ext_number<rational, eps1>();
+    tst_ext_number<inf_rational, eps0>();
+    tst_interval<rational, eps1>();
+    tst_interval<inf_rational, eps0>();
+}

src/dead/test/relevancy.cpp

@@ -0,0 +1,653 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    relevancy.cpp
+
+Abstract:
+
+    Test relevancy propagation.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-11-03.
+
+Revision History:
+
+--*/
+#include"sat_def.h"
+
+class relevancy_extension : public no_extension {
+public:
+    bool relevancy_enabled() {
+        return true;
+    }
+
+    bool gates_enabled() {
+        return true;
+    }
+};
+
+class sat_relevancy_tester {
+
+    static void tst1() {
+        sat_solver<relevancy_extension> solver; 
+        
+        literal l1 = solver.mk_var();
+
+        SASSERT(!solver.is_relevant(l1.var()));
+        
+        solver.assert_lit(l1);
+        
+        SASSERT(solver.is_relevant(l1.var()));
+    }
+
+    static void tst2() {
+        sat_solver<relevancy_extension> solver; 
+        
+        literal l1 = solver.mk_var();
+        
+        solver.push_scope();
+        
+        SASSERT(!solver.is_relevant(l1.var()));
+
+        solver.assert_lit(l1);
+
+        SASSERT(solver.is_relevant(l1.var()));
+        
+        solver.pop_scope(1);
+
+        SASSERT(solver.is_relevant(l1.var()));
+    }
+
+    static void tst3() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+
+        literal l4 = solver.mk_ite(l1, l2, l3);
+        solver.propagate();
+        
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        
+        solver.mark_as_relevant(l4.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+
+        solver.push_scope();
+
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+        
+        solver.assign(~l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+    }
+
+    static void tst4() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        literal l4 = solver.mk_ite(l1, l2, l3);
+        solver.propagate();
+
+        solver.push_scope();
+
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        
+        solver.mark_as_relevant(l4.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+
+        solver.assign(~l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        
+        solver.mark_as_relevant(l4.var());
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+    }
+
+    static void tst5() {
+        sat_solver<relevancy_extension> solver;
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+
+        solver.push_scope();
+
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        literal l4 = solver.mk_ite(l1, l2, l3);
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+
+        solver.mark_as_relevant(l4.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+    }
+
+    static void tst6() {
+        sat_solver<relevancy_extension> solver;
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_iff(l1, l2);
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.push_scope();
+
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.push_scope();
+        
+        solver.mark_as_relevant(l2.var());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.pop_scope(1);
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+    }
+
+    static void tst7() {
+        sat_solver<relevancy_extension> solver;
+        
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_or(l1, l2);
+        
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.mark_as_relevant(l3.var());
+        solver.assign(l3, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.pop_scope(1);
+        solver.propagate();
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.mark_as_relevant(l3.var());
+        solver.assign(l3, mk_axiom());
+        solver.propagate();
+        
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.pop_scope(1);
+        solver.propagate();
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        
+        solver.assign(~l3, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.pop_scope(1);
+        solver.propagate();
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.assign(~l3, mk_axiom());
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+    }
+
+    static void tst8() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_or(l1, l2);
+        
+        solver.push_scope();
+
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+
+        solver.pop_scope(1);
+        solver.propagate();
+        
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+    }
+
+    static void tst9() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_or(l1, l2);
+        
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        
+        solver.assign(l1, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1) || solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l1) != solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+    }
+
+    static void tst10() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_or(l1, l2);
+        
+        solver.assign(l1, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        
+        solver.mark_as_relevant(l3.var());
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1) || solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l1) != solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+    }
+
+    static void tst11() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_iff(l1, l2);
+        literal l4 = solver.mk_var();
+        literal l5 = solver.mk_or(l3, l4);
+
+        solver.propagate();
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        SASSERT(!solver.is_relevant(l5));
+
+        solver.assign(l3, mk_axiom());
+        solver.mark_as_relevant(l5.var());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.is_relevant(l2));
+        SASSERT(solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        SASSERT(solver.is_relevant(l5));
+
+        solver.assign(l4, mk_axiom());
+        solver.propagate();
+        SASSERT(!solver.is_relevant(l4));
+
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(!solver.is_relevant(l4));
+        SASSERT(!solver.is_relevant(l5));
+
+        solver.assign(l4, mk_axiom());
+        solver.mark_as_relevant(l5.var());
+        solver.propagate();
+        
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+        SASSERT(solver.is_relevant(l5));
+        
+        solver.assign(l1, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        solver.assign(l3, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        SASSERT(!solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l4));
+        SASSERT(solver.is_relevant(l5));
+    }
+
+    static void tst12(clause_kind k) {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        
+        solver.mk_aux_clause(l1, l2, k);
+
+        solver.push_scope();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+        
+        solver.pop_scope(1);
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+    }
+
+    static void tst13(clause_kind k) {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        
+        solver.mk_aux_clause(l1, l2, k);
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+
+        solver.assign(l1, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+        SASSERT(!solver.is_relevant(l2));
+    }
+
+    static void tst14() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+
+        solver.push_scope();
+        
+        solver.assign(l1, mk_axiom());
+
+        solver.mk_aux_clause(l1, l2, CLS_MAIN);
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1));
+    }
+
+    static void tst15() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+
+        solver.push_scope();
+        
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+
+        SASSERT(!solver.is_relevant(l1));
+
+        solver.push_scope();
+
+        solver.mk_aux_clause(l1, l2, CLS_MAIN);
+        solver.propagate();
+        
+        SASSERT(solver.is_relevant(l1));
+        
+        solver.pop_scope(1);
+        solver.propagate();
+
+        SASSERT(solver.is_relevant(l1));
+    }
+
+    static void tst16() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+
+        solver.push_scope();
+        solver.assert_lit(l1);
+        solver.propagate();
+        SASSERT(solver.is_relevant(l1));
+        SASSERT(solver.get_assignment(l1) == l_true);
+        solver.assert_lit(l1);
+        solver.pop_scope(1);
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.is_relevant(l1));
+    }
+
+    static void tst17() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        solver.assert_nonrelevant_lit(l1);
+        solver.mk_aux_clause(l1, l2, CLS_MAIN);
+        solver.check();
+        SASSERT(solver.get_assignment(l1) == l_true || solver.get_assignment(l2) == l_true);
+        SASSERT(solver.is_relevant(l1) || solver.is_relevant(l2));
+    }
+
+    static void tst18() {
+        sat_solver<relevancy_extension> solver;
+
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        solver.assert_nonrelevant_lit(l1);
+        literal l3 = solver.mk_or(l1, l2);
+        SASSERT(l3 != true_literal);
+        solver.assert_lit(l3);
+        lbool r = solver.check();
+        SASSERT(r == l_true);
+        SASSERT(solver.is_relevant(l3));
+        SASSERT(solver.is_relevant(l1));
+    }
+
+public:
+
+    static void run_tests() {
+        tst1();
+        tst2();
+        tst3();
+        tst4();
+        tst5();
+        tst6();
+        tst7();
+        tst8();
+        tst9();
+        tst10();
+        tst11();
+        tst12(CLS_MAIN);
+        tst12(CLS_TRANSIENT);
+        tst13(CLS_AUXILIARY);
+        tst13(CLS_EXT_LEMMA);
+        tst13(CLS_EXTERNAL);
+        tst14();
+        tst15();
+        tst16();
+        tst17();
+        tst18();
+    }
+
+};
+
+void tst_relevancy() {
+    sat_relevancy_tester::run_tests();
+}

src/dead/test/sat.cpp

@@ -0,0 +1,389 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    tst_sat.cpp
+
+Abstract:
+
+    Test SAT solver
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-05.
+
+Revision History:
+
+--*/
+
+#include"sat_def.h"
+
+class sat_tester {
+
+    static void tst1() {
+        sat_solver<no_extension> solver;
+        solver.push_user_scope();
+        solver.push_scope();
+        literal l1  = solver.mk_var();
+        SASSERT(solver.m_ref_count[l1.var()] == 1);
+        solver.assert_lit(l1);
+        SASSERT(solver.m_ref_count[l1.var()] == 2);
+        SASSERT(solver.m_weak_ref_count[l1.var()] == 1);
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.m_level[l1.var()] == 1);
+        literal l2 = solver.mk_var();
+        SASSERT(solver.m_ref_count[l2.var()] == 1);
+        SASSERT(solver.get_assignment(l2) == l_undef);
+        SASSERT(solver.m_level.size() == 3);
+        SASSERT(solver.m_free_var_indices.size() == 0);
+        solver.pop_scope(1);
+        SASSERT(solver.m_free_var_indices.size() == 2);
+        SASSERT(solver.m_ref_count[l1.var()] == 0);
+    }
+    
+    template<typename Ext>
+    static void tst2() {
+        sat_solver<Ext> solver;
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        literal l4 = solver.mk_var();
+        solver.mk_aux_clause(~l1, ~l2, l3, CLS_MAIN);
+        solver.mk_aux_clause(~l3, ~l4, CLS_MAIN);
+        solver.push_scope();
+        solver.assign(l1, mk_axiom());
+        solver.assign(l2, mk_axiom());
+        SASSERT(solver.get_assignment(l3) == l_undef);
+        SASSERT(solver.get_assignment(l4) == l_undef);
+        solver.propagate();
+        SASSERT(solver.get_assignment(l3) == l_true);
+        SASSERT(solver.get_assignment(l4) == l_false);
+        solver.pop_scope(1);
+        SASSERT(solver.get_assignment(l1) == l_undef);
+        SASSERT(solver.get_assignment(l2) == l_undef);
+        SASSERT(solver.get_assignment(l3) == l_undef);
+        SASSERT(solver.get_assignment(l4) == l_undef);
+    }
+
+    static void tst3() {
+        sat_solver<no_extension> solver;
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        solver.push_scope();
+        SASSERT(solver.m_ref_count[l1.var()] == 1);
+        solver.mk_aux_clause(~l1, l2, CLS_TRANSIENT);
+        SASSERT(solver.m_ref_count[l1.var()] == 2);
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+        SASSERT(solver.get_assignment(l2) == l_true);
+        SASSERT(solver.m_transient_clauses.size() == 1);
+        TRACE("sat_ext", tout << "ref_count: " << solver.m_ref_count[l1.var()] << ", scope_lvl: " << solver.m_scope_lvl << "\n";);
+        SASSERT(solver.m_ref_count[l1.var()] == 3);
+        SASSERT(solver.m_ref_count[l2.var()] == 3);
+        solver.pop_scope(1);
+        solver.assign(l1, mk_axiom());
+        solver.propagate();
+        SASSERT(solver.get_assignment(l2) == l_undef);
+        SASSERT(solver.m_transient_clauses.size() == 0);
+        SASSERT(solver.m_ref_count[l1.var()] == 2);
+        SASSERT(solver.m_ref_count[l2.var()] == 1);
+    }
+
+    static void tst4() {
+        sat_solver<no_extension> solver;
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        literal l4 = solver.mk_var();
+        solver.push_user_scope();
+        solver.mk_aux_clause(~l1, l2, l4, CLS_MAIN);
+        solver.push_user_scope();
+        solver.mk_aux_clause(~l1, ~l2, l3, CLS_MAIN);
+        solver.push_scope();
+        solver.mk_aux_clause(~l3, ~l4, CLS_TRANSIENT);
+        solver.mk_aux_clause(~l1, ~l4, CLS_MAIN);
+        SASSERT(solver.m_ref_count[l1.var()] == 4);
+        SASSERT(solver.m_ref_count[l2.var()] == 3);
+        SASSERT(solver.m_ref_count[l3.var()] == 3);
+        SASSERT(solver.m_ref_count[l4.var()] == 4);
+        SASSERT(solver.m_main_clauses.size() == 3);
+        SASSERT(solver.m_transient_clauses.size() == 1);
+        solver.pop_scope(2);
+        SASSERT(solver.m_ref_count[l1.var()] == 2);
+        SASSERT(solver.m_ref_count[l2.var()] == 2);
+        SASSERT(solver.m_ref_count[l3.var()] == 1);
+        SASSERT(solver.m_ref_count[l4.var()] == 2);
+        SASSERT(solver.m_main_clauses.size() == 1);
+        SASSERT(solver.m_transient_clauses.size() == 0);
+        solver.assign(l1, mk_axiom());
+        SASSERT(solver.get_assignment(l4) == l_undef);
+        solver.pop_scope(1);
+        SASSERT(solver.m_main_clauses.size() == 0);
+        SASSERT(solver.m_ref_count[l1.var()] == 1);
+        SASSERT(solver.m_ref_count[l2.var()] == 1);
+        SASSERT(solver.m_ref_count[l3.var()] == 1);
+        SASSERT(solver.m_ref_count[l4.var()] == 1);
+    }
+
+    template<typename Ext>
+    static void tst5() {
+        sat_solver<Ext> solver;
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        solver.push_scope();
+        solver.assign(l1, mk_axiom());
+        solver.push_scope();
+        solver.mk_aux_clause(~l1, l2, CLS_MAIN);
+        SASSERT(solver.get_assignment(l2) == l_true);
+        solver.pop_scope(1);
+        SASSERT(solver.get_assignment(l2) == l_true);
+        solver.pop_scope(1);
+        SASSERT(solver.get_assignment(l2) == l_undef);
+        SASSERT(solver.m_main_clauses.size() == 1);
+    }
+
+    static void tst6() {
+        sat_solver<no_extension> solver;
+        
+        literal l = solver.mk_var();
+        solver.assert_lit(l);
+        SASSERT(!solver.inconsistent());
+        solver.push_scope();
+        solver.assign(~l, mk_axiom());
+        SASSERT(solver.inconsistent());
+        solver.pop_scope(1);
+        SASSERT(!solver.inconsistent());
+    }
+
+    class no_ref_count : public no_extension {
+    public:
+        static bool ref_counters_enabled() {
+            return false; 
+        }
+    };
+
+    static void tst7() {
+        sat_solver<no_ref_count> solver;
+        literal l1 = solver.mk_var();
+        solver.push_user_scope();
+        literal l2 = solver.mk_var();
+        SASSERT(solver.get_var_vector_size() == 3);
+        solver.pop_scope(1);
+        SASSERT(solver.get_var_vector_size() == 2);
+    }
+
+    static void tst8() {
+        literal l[2];
+        l[0] = true_literal;
+        l[1] = true_literal;
+        clause * cls = clause::mk_clause(2, l, CLS_EXTERNAL);
+        SASSERT(cls->kind() == CLS_EXTERNAL);
+        dealloc(cls);
+    }
+
+    static void tst9() {
+        sat_solver<no_extension> solver;
+
+        solver.push_scope();
+        literal l1 = solver.mk_var();
+        literal l2 = solver.mk_var();
+        literal l3 = solver.mk_var();
+        solver.mk_aux_clause(l1, l2, l3, CLS_MAIN);
+        solver.pop_scope(1);
+        SASSERT(solver.m_ref_count[l1.var()] == 1);
+        SASSERT(solver.get_assignment(l1) == l_undef);
+        solver.assert_lit(~l2);
+        solver.assert_lit(~l3);
+        solver.propagate();
+        SASSERT(solver.get_assignment(l1) == l_true);
+        SASSERT(solver.m_main_clauses.size() == 1);
+        SASSERT(solver.m_ref_count[l1.var()] == 2);
+        solver.simplify_clauses();
+        SASSERT(solver.m_main_clauses.size() == 0);
+        SASSERT(solver.m_ref_count[l1.var()] == 1);
+        SASSERT(solver.m_weak_ref_count[l1.var()] == 1);
+        SASSERT(solver.get_assignment(l1) == l_true);
+    }
+
+    static void tst10() {
+        sat_solver<no_extension> s;
+        
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        literal l3 = s.mk_var();
+        
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.push_scope();
+        literal l4 = s.mk_var();
+        s.assign(l4, mk_axiom());
+        s.mk_aux_clause(~l4, l3, CLS_TRANSIENT);
+        s.mk_aux_clause(~l4, l2, CLS_TRANSIENT);
+        s.mk_aux_clause(~l3, ~l1, ~l2, CLS_TRANSIENT);
+        SASSERT(s.inconsistent());
+#ifdef  Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.m_scope_lvl == 1);
+        SASSERT(s.m_ref_count[l4.var()] > 0);
+        s.pop_scope(1);
+        SASSERT(s.get_assignment(l1) == l_undef);
+        SASSERT(s.get_assignment(l4) == l_undef);
+        s.push_scope();
+        s.assign(l4, mk_axiom());
+#ifdef  Z3DEBUG
+        s.del_learned_clauses();
+#endif 
+        s.pop_scope(1);
+    }
+
+    static void tst11() {
+        // out-of-order conflict bug.
+        sat_solver<no_extension> s;
+
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.assign(l2, mk_axiom());
+        s.push_scope();
+        s.mk_aux_clause(~l1, ~l2, CLS_TRANSIENT);
+        s.propagate();
+        s.resolve_conflict();
+    }
+
+    static void tst12() {
+        // out-of-order conflict bug.
+        sat_solver<no_extension> s;
+
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        literal l3 = s.mk_var();
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.assign(l2, mk_axiom());
+        s.push_scope();
+        s.assign(l3, mk_axiom());
+        s.mk_aux_clause(~l1, ~l2, CLS_TRANSIENT);
+        s.propagate();
+        s.resolve_conflict();
+    }
+
+    static void tst13() {
+        sat_solver<no_extension> s;
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        literal l3 = s.mk_var();
+        s.push_scope();
+        s.assign(l1, mk_axiom());
+        s.push_scope();
+        s.assign(l2, mk_axiom());
+        s.push_scope();
+        s.mk_aux_clause(~l1, l3, CLS_MAIN);
+        s.propagate();
+        SASSERT(!s.inconsistent());
+        SASSERT(s.get_assignment(l3) == l_true);
+        s.mk_aux_clause(~l1, ~l2, CLS_TRANSIENT);
+        s.propagate();
+        SASSERT(s.inconsistent());
+#ifdef Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.get_assignment(l3) == l_true);
+        TRACE("sat", tout << l3 << " : " << s.get_assignment(l3) << " : " << s.m_level[l3.var()] << " : " << s.m_scope_lvl << "\n";);
+    }
+
+    static void tst14() {
+        sat_solver<no_extension> s;
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        s.push_scope();
+        s.assign(~l1, mk_axiom());
+        s.push_scope();
+        s.assign(~l2, mk_axiom());
+        s.assert_lit(l1);
+        SASSERT(s.inconsistent());
+#ifdef Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.get_assignment(l1) == l_true);
+    }
+
+    static void tst15() {
+        sat_solver<no_extension> s;
+        literal l1 = s.mk_var();
+        literal l2 = s.mk_var();
+        s.push_scope();
+        s.assign(~l1, mk_axiom());
+        s.push_scope();
+        s.assign(~l2, mk_axiom());
+        s.assert_lit(l1);
+        SASSERT(s.inconsistent());
+#ifdef Z3DEBUG
+        bool r = 
+#endif
+            s.resolve_conflict();
+        SASSERT(r);
+        SASSERT(s.get_assignment(l1) == l_true);
+    }
+
+    static void tst16() {
+        sat_solver<no_extension> s;
+        s.push_scope();
+        literal l1 = s.mk_var();
+        bool_var v1 = l1.var();
+        s.inc_weak_ref(v1);
+        s.pop_scope(1);
+        SASSERT(s.get_ref_count(v1) == 0);
+        literal l2 = s.mk_var();
+        SASSERT(l2.var() != v1);
+        s.dec_weak_ref(v1);
+        literal l3 = s.mk_var();
+        SASSERT(l3.var() == v1);
+    }
+
+public:    
+    static void run_tests() {
+        enable_trace("sat_ext");
+        enable_trace("backtrack");
+        enable_trace("mk_clause");
+        enable_debug("mk_clause");
+        enable_trace("propagate");
+        enable_trace("simplify");
+        enable_trace("del_learned_clauses");
+        enable_debug("sat_invariant");
+        TRACE("sat_ext", tout << "running SAT solver tests...\n";);
+        tst1();
+        tst2<no_extension>();
+        tst2<no_ref_count>();
+        tst3();
+        tst4();
+        tst5<no_extension>();
+        tst5<no_ref_count>();
+        tst6();
+        tst7();
+        tst8();
+        tst9();
+        tst10();
+        tst11();
+        tst12();
+        tst13();
+        tst14();
+        tst15();
+        tst16();
+    }
+};
+
+void tst_sat() {
+    TRACE("sat", tout << "sizeof(clause): " << sizeof(clause) << "\n";);
+    sat_tester::run_tests();
+}
+
+

src/dead/test/simplex_polynomial.cpp

@@ -0,0 +1,45 @@
+#include "simplex_polynomial.h"
+
+void tst_simplex_polynomial()
+{
+    polynomial p1, p2, p3, p4;
+    simplex_variable v1(1), v2(2), v3(3), v4(4), v5(5);
+    monomial m1(v1), m2(v2), m3(v3), m4(v4);
+
+    m1 = monomial(v1);
+    m1 *= monomial(v2);
+    m1 *= monomial(v1);
+
+    m1.display(std::cout) << std::endl;
+    m1.normalize();
+    m1.display(std::cout) << std::endl;
+    
+    m2 = m1;
+    SASSERT(m1 == m2);
+
+    p1 = polynomial(rational(1,2));
+    SASSERT(p1.is_const());
+
+    p1 += polynomial(v1);
+    SASSERT(!p1.is_const());
+
+    p1 += polynomial(v2);
+    p1 *= polynomial(v2);
+    p1 -= polynomial(v3);
+    p1 += polynomial(rational(2,3));
+
+    p1.normalize();
+    p1.display(std::cout) << std::endl;
+    SASSERT(p1[0].size() == 0); // first element is a constant.
+
+
+    p1 = polynomial(v1);
+    p2 = polynomial(v2);
+    p3 = polynomial(v3);
+    p3 += p2;
+    p3 *= p1;
+
+    p3.display(std::cout) << std::endl; // multiplication distributes.
+    SASSERT(p3.size() == 2);
+
+}

src/dead/test/template_models.cpp

@@ -0,0 +1,101 @@
+#include "ast_fm.h"
+#include "smtparser.h"
+#include "ast_pp.h"
+
+static void
+simplify_formula(
+    ast_manager&      ast_manager,
+    smtlib::symtable* table,
+    smtlib::parser*   parser,
+    ast*              formula
+    )
+{
+//     front_end_params params;
+//     std::cout << std::make_pair(&ast_manager, formula) << std::endl;
+
+//     const_decl_ast *le_decl = 0, *add_decl = 0, *mul_decl = 0; 
+//     const_decl_ast *lt_decl = 0, *gt_decl = 0, *f_decl = 0;
+//     type_decl_ast*  int_decl = 0;
+//     type_ast* int_type = 0;
+
+//     table->find1("<=", le_decl);
+//     table->find1("+", add_decl);
+//     table->find1("*", mul_decl);
+//     table->find1("f", f_decl);
+//     table->find1("<", lt_decl);
+//     table->find1(">", gt_decl);
+//     table->find("Int", int_decl);
+//     int_type = ast_manager.mk_type(int_decl);
+    
+
+//     ast_simplifier simplifier(ast_manager, params);
+
+// #if 0
+//     iast_arith_simplifier* arith = 
+//         simplifier.add_arithmetic(
+// 			null_theory_id, // TBD
+//             add_decl,
+//             mul_decl,
+//             le_decl,
+//             false
+//             );
+
+//     arith->register_lt(lt_decl);
+//     arith->register_gt(gt_decl);
+// #endif
+//     ast_fm fm(ast_manager, simplifier, le_decl, add_decl, mul_decl);
+
+//     ast_function_replace replace(ast_manager);
+
+//     ast_ref<> templ(ast_manager);
+//     templ = ast_manager.mk_const(add_decl, 
+// 		ast_manager.mk_var(0,int_type), 
+// 		ast_manager.mk_numeral(rational(2), int_type));
+
+//     ast_ref<> result(ast_manager);
+
+//     //
+//     // Replace f by \lambda x . x + 2 in formula.
+//     //
+    
+//     replace(formula, f_decl, 1, templ.get(), result);
+
+//     std::cout << "substituted:" 
+//               << std::make_pair(&ast_manager, result.get()) << std::endl;
+    
+//     //
+//     // Eliminate quantified variables from the formula.
+//     //
+//     fm.eliminate(result.get(), result);
+
+//     std::cout << "projected:" 
+//               << std::make_pair(&ast_manager, result.get()) << std::endl;
+
+}
+
+void tst_template_models()
+{
+    const char* spec = 
+        "(benchmark template_models :logic QF_LIA \n"
+        ":extrafuns ((f Int Int) (b Int) (c Int))\n"
+        ":formula (forall (x Int) (and (< (f x) (f (+ x 1))) (> (f b) b) (> (f c) b))))";
+    
+    ast_manager ast_manager;
+    smtlib::parser* parser = smtlib::parser::create(ast_manager);
+
+    parser->initialize_smtlib();
+
+    parser->parse_string(spec);
+
+    smtlib::benchmark* b = parser->get_benchmark();
+    
+    smtlib::symtable* table = b->get_symtable();
+    vector<smtlib::formula,false> formulas;
+    b->get_formulas(formulas);
+    for (unsigned j = 0; j < formulas.size(); ++j) {
+        simplify_formula(ast_manager, table, 
+                         parser, formulas[j].m_formula);
+    }
+    
+    dealloc(parser);
+}

src/dead/test/th_propagation.cpp

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    th_propagation.cpp
+
+Abstract:
+
+    Test theory propagation.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-11-07.
+
+Revision History:
+
+--*/
+#include"core_theory.h"
+
+class th_propagation_tester {
+    static void tst1() {
+        core_theory t;
+        t.m_params.m_relevancy_lvl = 0;
+        
+        enode * n1  = t.mk_const();
+        enode * n2  = t.mk_const();
+        enode * n3  = t.mk_const();
+        
+        literal eq1 = t.mk_eq(n1,n2);
+        literal eq2 = t.mk_eq(n2,n3);
+        literal eq3 = t.mk_eq(n1,n3);
+
+        literal l1   = t.mk_lit();
+        literal l2   = t.mk_lit();
+        t.mk_main_clause(l1, l2, ~eq3);
+        t.mk_main_clause(~l2, ~eq3);
+        t.mk_main_clause(~l1, ~eq2);
+
+        t.push_scope();
+        t.assign(eq1, mk_axiom());
+        t.propagate();
+
+        t.push_scope();
+        t.assign(eq2, mk_axiom());
+        t.propagate();
+        SASSERT(t.get_assignment(eq3) == l_true);
+        SASSERT(t.inconsistent());
+        bool r = t.m_sat->resolve_conflict();
+        SASSERT(r);
+    }
+
+public:
+    static void run_tests() {
+        enable_trace("th_prop");
+        enable_trace("scope");
+        enable_trace("conflict");
+        tst1();
+    }
+};
+
+void tst_th_propagation() {
+    th_propagation_tester::run_tests();
+}
+

src/dead/test/trail.cpp

@@ -0,0 +1,42 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    trail.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2007-02-26.
+
+Revision History:
+
+--*/
+#include"core_theory.h"
+
+void tst_trail() {
+    core_theory t;
+    bvalue<int> v(10);
+    t.push();
+    v.set(t, 20);
+    v.set(t, 30);
+    SASSERT(v.get() == 30);
+    t.pop(1);
+    SASSERT(v.get() == 10);
+    t.push();
+    t.push();
+    v.set(t, 100);
+    SASSERT(v.get() == 100);
+    t.pop(2);
+    SASSERT(v.get() == 10);
+    t.push();
+    t.push();
+    v.set(t, 40);
+    SASSERT(v.get() == 40);
+    t.pop(1);
+    SASSERT(v.get() == 10);
+}

src/dead/test/watch_list.cpp

@@ -0,0 +1,89 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    tst_watch_list.cpp
+
+Abstract:
+
+    Test watch list data structure.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-02.
+
+Revision History:
+
+--*/
+#include"vector.h"
+#include"sat_types.h"
+
+static void tst1() {
+    watch_list wl;
+    for(unsigned i = 0; i < 10; i++)
+	wl.insert_clause(reinterpret_cast<clause*>(static_cast<size_t>(i+1)));
+}
+
+static void tst2() {
+    ptr_vector<clause> clause_list;
+    vector<literal>   lit_list;
+    watch_list wl;
+    unsigned n = rand()%1000;
+    for (unsigned i = 0; i < n; i++) {
+	unsigned op = rand()%7;
+	if (op <= 1) {
+	    clause * c = reinterpret_cast<clause*>(static_cast<size_t>(rand()));
+	    wl.insert_clause(c);
+	    clause_list.push_back(c);
+	}
+	else if (op <= 3) {
+	    literal l = to_literal(rand());
+	    wl.insert_literal(l);
+	    lit_list.push_back(l);
+	}
+	else if (op <= 4) {
+	    if (!clause_list.empty()) {
+		int idx = rand() % (clause_list.size());
+		clause * c = clause_list[idx];
+		wl.remove_clause(c);
+		ptr_vector<clause>::iterator it = std::find(clause_list.begin(), clause_list.end(), c);
+		SASSERT(it);
+		clause_list.erase(it);
+	    }
+	}
+	else if (op <= 5) {
+	    ptr_vector<clause>::iterator it = clause_list.begin();
+	    ptr_vector<clause>::iterator end = clause_list.end();
+	    watch_list::clause_iterator it2 = wl.begin_clause();
+	    watch_list::clause_iterator end2 = wl.end_clause();
+	    for (; it != end; ++it, ++it2) {
+		SASSERT(it2 != end2);
+		SASSERT(*it == *it2);
+	    }
+	}
+	else if (op <= 6) {
+	    vector<literal>::iterator begin = lit_list.begin();
+	    vector<literal>::iterator it    = lit_list.end();
+	    watch_list::literal_iterator it2 = wl.begin_literals();
+	    watch_list::literal_iterator end2 = wl.end_literals();
+	    while (it != begin) {
+		--it;
+		SASSERT(it2 != end2);
+		SASSERT(*it == *it2);
+		++it2;
+	    }
+	}
+    }
+}
+
+static void tst3() {
+    for (unsigned i = 0; i < 1000; i++)
+	tst2();
+}
+
+void tst_watch_list() {
+    tst1();
+    tst3();
+}
+

src/dead/value_compiler_extension.h

@@ -0,0 +1,46 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    value_compiler_extension.h
+
+Abstract:
+
+    Compiler extension for creating values (i.e., "interpreted" constants that
+    are different any other constant).
+
+Author:
+
+    Leonardo de Moura (leonardo) 2006-10-31.
+
+Revision History:
+
+--*/
+#ifndef _VALUE_COMPILER_EXTENSION_H_
+#define _VALUE_COMPILER_EXTENSION_H_
+
+#include"ast_compiler.h"
+
+class value_compiler_extension : public ast_compiler_plugin {
+    context & m_context;
+public:
+    value_compiler_extension(ast_manager & m, context & ctx):
+        ast_compiler_plugin(m.get_family_id(symbol("interpreted_value"))),
+        m_context(ctx) {
+        ctx.register_plugin(this);
+    }
+
+    virtual ~value_compiler_extension() {
+    }
+
+    virtual bool compile_term(ast_compiler & c, const_ast * a, enode * & r) {
+        SASSERT(a->get_decl()->get_family_id() == m_fid);
+        const_decl_ast * d = a->get_decl();
+        r = m_context.mk_interpreted_const(d);
+        return true;
+    }
+};
+
+#endif /* _VALUE_COMPILER_EXTENSION_H_ */
+