add bceq experiment

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

src/ast/ast_trail.h

@@ -0,0 +1,76 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    ast_trail.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2008-06-02.
+
+Revision History:
+
+    Extracted AST specific features from trail.h
+    nbjorner 2014-9-28
+
+--*/
+#ifndef _AST_TRAIL_H_
+#define _AST_TRAIL_H_
+
+#include"ast.h"
+#include"trail.h"
+
+
+template<typename S, typename T>
+class ast2ast_trailmap {
+    ref_vector<S, ast_manager> m_domain;
+    ref_vector<T, ast_manager> m_range;
+    obj_map<S, T*>             m_map;
+public:
+    ast2ast_trailmap(ast_manager& m):
+        m_domain(m),
+        m_range(m), 
+        m_map()
+    {}
+
+    bool find(S* s, T*& t) {
+        return m_map.find(s,t);
+    }
+    
+    void insert(S* s, T* t) {
+        SASSERT(!m_map.contains(s));
+        m_domain.push_back(s);
+        m_range.push_back(t);
+        m_map.insert(s,t);
+    }
+    
+    void pop() {
+        SASSERT(!m_domain.empty());
+        m_map.remove(m_domain.back());
+        m_domain.pop_back();
+        m_range.pop_back();
+    }
+};
+
+template<typename Ctx, typename S, typename T>
+class ast2ast_trail : public trail<Ctx> {
+    ast2ast_trailmap<S,T>& m_map;
+public:
+    ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
+        m_map(m) {
+        m.insert(s,t);
+    }
+
+    virtual void undo(Ctx& ctx) {
+        m_map.pop();
+    }    
+};
+
+
+#endif /* _AST_TRAIL_H_ */
+

src/ast/trail.h

@@ -1,404 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    trail.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-02.
-
-Revision History:
-
---*/
-#ifndef _TRAIL_H_
-#define _TRAIL_H_
-
-#include"ast.h"
-#include"obj_hashtable.h"
-#include"region.h"
-
-template<typename Ctx>
-class trail {
-public:
-    virtual ~trail() {
-    }
-    virtual void undo(Ctx & ctx) = 0;
-};
-
-template<typename Ctx, typename T>
-class value_trail : public trail<Ctx> {
-    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(Ctx & ctx) {
-        m_value = m_old_value;
-    }
-};
-
-template<typename Ctx>
-class reset_flag_trail : public trail<Ctx> {
-    bool & m_value;
-public:
-    reset_flag_trail(bool & value):
-        m_value(value) {
-    }
-    
-    virtual ~reset_flag_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_value = false;
-    }
-};
-
-template<typename Ctx, typename T>
-class set_ptr_trail : public trail<Ctx> {
-    T * & m_ptr;
-public:
-    set_ptr_trail(T * & ptr):
-        m_ptr(ptr) {
-        SASSERT(m_ptr == 0);
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_ptr = 0;
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class restore_size_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    unsigned                     m_old_size;
-public:
-    restore_size_trail(vector<T, CallDestructors> & v, unsigned sz):
-        m_vector(v),
-        m_old_size(sz) {
-    }
-    restore_size_trail(vector<T, CallDestructors> & v):
-        m_vector(v),
-        m_old_size(v.size()) {
-    }
-    virtual ~restore_size_trail() {
-    }
-    virtual void undo(Ctx & ctx) {
-        m_vector.shrink(m_old_size);
-    }
-};    
-        
-template<typename Ctx, typename T, bool CallDestructors=true>
-class vector_value_trail : public trail<Ctx> {
-    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(Ctx & ctx) {
-        m_vector[m_idx] = m_old_value;
-    }
-};
-
-
-template<typename Ctx, typename D, typename R>
-class insert_obj_map : public trail<Ctx> {
-    obj_map<D,R>&     m_map;
-    D*                m_obj;
-public:
-    insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
-    virtual ~insert_obj_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); }
-};
-
-template<typename Ctx, typename M, typename D>
-class insert_map : public trail<Ctx> {
-    M&            m_map;
-    D             m_obj;
-public:
-    insert_map(M& t, D o) : m_map(t), m_obj(o) {}
-    virtual ~insert_map() {}
-    virtual void undo(Ctx & ctx) { m_map.remove(m_obj); }
-};
-
-
-
-template<typename Ctx, typename V>
-class push_back_vector : public trail<Ctx> {
-    V & m_vector;
-public:
-    push_back_vector(V & v):
-        m_vector(v) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.pop_back();
-    }
-};
-
-template<typename Ctx, typename T>
-class set_vector_idx_trail : public trail<Ctx> {
-    ptr_vector<T> & m_vector;
-    unsigned                         m_idx;
-public:
-    set_vector_idx_trail(ptr_vector<T> & v, unsigned idx):
-        m_vector(v),
-        m_idx(idx) {
-    }
-    
-    virtual ~set_vector_idx_trail() {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_idx] = 0;
-    }
-};
-    
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    T m_value;
-public:
-    pop_back_trail(vector<T, CallDestructors> & v):
-    m_vector(v),
-    m_value(m_vector.back()) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.push_back(m_value);
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class pop_back2_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-    typedef vector<vector<T, CallDestructors>, true> vector_t;
-    unsigned m_index;
-    T m_value;
-public:
-    pop_back2_trail(vector<T, CallDestructors> & v, unsigned index):
-    m_vector(v),
-    m_index(index),
-    m_value(m_vector[index].back()) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_index].push_back(m_value);
-    }
-};
-
-
-template<typename S, typename T>
-class ast2ast_trailmap {
-    ref_vector<S, ast_manager> m_domain;
-    ref_vector<T, ast_manager> m_range;
-    obj_map<S, T*>             m_map;
-public:
-    ast2ast_trailmap(ast_manager& m):
-        m_domain(m),
-        m_range(m), 
-        m_map()
-    {}
-
-    bool find(S* s, T*& t) {
-        return m_map.find(s,t);
-    }
-    
-    void insert(S* s, T* t) {
-        SASSERT(!m_map.contains(s));
-        m_domain.push_back(s);
-        m_range.push_back(t);
-        m_map.insert(s,t);
-    }
-    
-    void pop() {
-        SASSERT(!m_domain.empty());
-        m_map.remove(m_domain.back());
-        m_domain.pop_back();
-        m_range.pop_back();
-    }
-};
-
-template<typename Ctx, typename S, typename T>
-class ast2ast_trail : public trail<Ctx> {
-    ast2ast_trailmap<S,T>& m_map;
-public:
-    ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) : 
-        m_map(m) {
-        m.insert(s,t);
-    }
-
-    virtual void undo(Ctx& ctx) {
-        m_map.pop();
-    }    
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back_trail : public trail<Ctx> {
-    vector<T, CallDestructors> & m_vector;
-public:
-    push_back_trail(vector<T, CallDestructors> & v):
-        m_vector(v) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector.pop_back();
-    }
-};
-
-template<typename Ctx, typename T, bool CallDestructors=true>
-class push_back2_trail : public trail<Ctx> {
-    typedef vector<vector<T, CallDestructors>, true> vector_t;
-    vector_t & m_vector;
-    unsigned   m_index;
-public:
-    push_back2_trail(vector_t & v, unsigned index) : 
-    m_vector(v),
-    m_index(index) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_vector[m_index].pop_back();
-    }
-};
-
-template<typename Ctx>
-class set_bitvector_trail : public trail<Ctx> {
-    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(Ctx & ctx) {
-        m_vector[m_idx] = false;
-    }
-};
-    
-template<typename Ctx, typename T>
-class new_obj_trail : public trail<Ctx> {
-    T * m_obj;
-public:
-    new_obj_trail(T * obj):
-        m_obj(obj) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        dealloc(m_obj);
-    }
-};
-
-template<typename Ctx, typename M, typename T>
-class obj_ref_trail : public trail<Ctx> {
-    obj_ref<T,M> m_obj;
-public:
-    obj_ref_trail(obj_ref<T,M>& obj):
-        m_obj(obj) {
-    }
-    
-    virtual void undo(Ctx & ctx) {
-        m_obj.reset();
-    }
-};
-
-template<typename Ctx, typename T>
-class insert_obj_trail : public trail<Ctx> {
-    obj_hashtable<T>& m_table;
-    T*                m_obj;
-public:
-    insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
-    virtual ~insert_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.remove(m_obj); }
-};
-
-
-
-template<typename Ctx, typename T>
-class remove_obj_trail : public trail<Ctx> {
-    obj_hashtable<T>& m_table;
-    T*                m_obj;
-public:
-    remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
-    virtual ~remove_obj_trail() {}
-    virtual void undo(Ctx & ctx) { m_table.insert(m_obj); } 
-};
-
-
-template<typename Ctx>
-void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size) {
-    SASSERT(old_size <= s.size());
-    typename ptr_vector<trail<Ctx> >::iterator begin = s.begin() + old_size;
-    typename ptr_vector<trail<Ctx> >::iterator it    = s.end();
-    while (it != begin) {
-        --it;
-        (*it)->undo(ctx);
-    }
-    s.shrink(old_size);
-}
-
-template<typename Ctx>
-class trail_stack {
-    Ctx &                   m_ctx;
-    ptr_vector<trail<Ctx> > m_trail_stack;
-    unsigned_vector         m_scopes;
-    region                  m_region;
-public:
-    trail_stack(Ctx & c):m_ctx(c) {}
-
-    ~trail_stack() {}
-    
-    region & get_region() { return m_region; }
-    
-    void reset() { 
-        pop_scope(m_scopes.size()); 
-        // Undo trail objects stored at lvl 0 (avoid memory leaks if lvl 0 contains new_obj_trail objects).
-        undo_trail_stack(m_ctx, m_trail_stack, 0); 
-    }
-
-    void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
-
-    template<typename TrailObject>
-    void push(TrailObject const & obj) { m_trail_stack.push_back(new (m_region) TrailObject(obj)); }
-
-    unsigned get_num_scopes() const { return m_scopes.size(); }
-
-    void push_scope() { m_region.push_scope(); m_scopes.push_back(m_trail_stack.size()); }
-
-    void pop_scope(unsigned num_scopes) {
-        if (num_scopes == 0) return;
-        unsigned lvl      = m_scopes.size();
-        SASSERT(num_scopes <= lvl);
-        unsigned new_lvl  = lvl - num_scopes;
-        unsigned old_size = m_scopes[new_lvl];
-        undo_trail_stack(m_ctx, m_trail_stack, old_size);
-        m_scopes.shrink(new_lvl);
-        m_region.pop_scope(num_scopes);
-    }
-};
-
-#endif /* _TRAIL_H_ */
-

src/sat/sat_simplifier.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include"sat_simplifier.h"
 #include"sat_simplifier_params.hpp"
 #include"sat_solver.h"
+#include"sat_bceq.h"
 #include"stopwatch.h"
 #include"trace.h"
 
@@ -156,6 +157,14 @@ namespace sat {
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
+#if 0
+        // experiment is disabled.
+        if (!learned) { // && m_equality_inference
+            bceq bc(s);
+            bc();
+        }
+#endif
+
         if (!learned)
             m_num_calls++;
 

src/sat/sat_solver.h

@@ -141,6 +141,7 @@ namespace sat {
         friend class mus;
         friend class sls;
         friend class wsls;
+        friend class bceq;
         friend struct mk_stat;
     public:
         solver(params_ref const & p, extension * ext);

src/smt/theory_array_full.h

@@ -19,8 +19,9 @@ Revision History:
 #ifndef _THEORY_ARRAY_FULL_H_
 #define _THEORY_ARRAY_FULL_H_
 
-#include"theory_array.h"
+#include "theory_array.h"
 #include "simplifier.h"
+#include "ast_trail.h"
 
 namespace smt {
 

src/util/union_find.h

@@ -20,6 +20,7 @@ Revision History:
 #define _UNION_FIND_H_
 
 #include "trail.h"
+#include "trace.h"
 
 class union_find_default_ctx {
 public:
@@ -98,6 +99,7 @@ public:
 
     unsigned get_num_vars() const { return m_find.size(); }
 
+
     unsigned find(unsigned v) const {
         while (true) {
             unsigned new_v = m_find[v];
@@ -109,6 +111,8 @@ public:
 
     unsigned next(unsigned v) const { return m_next[v]; }
 
+    unsigned size(unsigned v) const { return m_size[find(v)]; }
+
     bool is_root(unsigned v) const { return m_find[v] == v; }
 
     void merge(unsigned v1, unsigned v2) {
@@ -131,7 +135,7 @@ public:
     void display(std::ostream & out) const {
         unsigned num = get_num_vars(); 
         for (unsigned v = 0; v < num; v++) {
-            out << "v" << v << " --> v" << m_find[v] << "\n";
+            out << "v" << v << " --> v" << m_find[v] << " (" << size(v) << ")\n";
         }
     }