Commits

Leonardo de Moura committed 67f5ed4

move array_property_expander to dead code bin

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

Comments (0)

Files changed (12)

scripts/mk_make.py

 add_lib('subpaving', ['util'], 'math/subpaving')
 add_lib('ast', ['util', 'polynomial'])
 add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
-# array_property is only used in test exe
-add_lib('array_property', ['ast', 'rewriter'], 'ast/array_property')
 # Simplifier module will be deleted in the future.
 # It has been replaced with rewriter module.
 add_lib('simplifier', ['rewriter'], 'ast/simplifier')
 # TODO: delete SMT 1.0 frontend
 add_lib('api', ['portfolio', 'user_plugin'])
 add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
-add_exe('test', ['api', 'fuzzing', 'array_property'], exe_name='test-z3')
+add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
 
 mk_makefile()

src/ast/array_property/array_property_expander.cpp

-/*++
-Copyright (c) 2010 Microsoft Corporation
-
-Module Name:
-
-    array_property_expander.cpp
-
-Abstract:
-
-    Expand array operations for the array property fragment formulas.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2010-16-12
-
-Revision History:
-
---*/
-
-#include"array_property_expander.h"
-#include"obj_hashtable.h"
-#include"var_subst.h"
-#include"array_decl_plugin.h"
-#include"for_each_expr.h"
-
-array_property_expander::array_property_expander(ast_manager& m):
-    m_manager(m) {
-}
-
-namespace array_property_exp {
-    class proc {
-        ast_manager& m_manager;
-        unsigned&    m_offset;
-        expr_ref_vector m_trail;
-        family_id    m_fid;
-        array_util   m_util;
-        obj_map<expr, expr*> m_mem;
-
-
-        void insert(expr* a, expr* b) {
-            m_trail.push_back(b);
-            m_mem.insert(a, b);
-        }
-
-
-    public:
-        proc(ast_manager& m, unsigned& offset) : 
-            m_manager(m),
-            m_offset(offset),
-            m_trail(m),
-            m_fid(m.get_family_id("array")),
-            m_util(m)
-        {}
-
-        expr* find(expr* e) {
-            expr* result = 0;
-            VERIFY(m_mem.find(e, result));
-            return result;
-        }
-
-        void operator()(var* n) { insert(n, n); }
-
-        void operator()(quantifier* q) {
-            expr* e = find(q->get_expr());
-            quantifier* q2 = m_manager.update_quantifier(q, e);
-            insert(q, q2);
-        }
-
-        void operator()(app* n) {
-            ast_manager& m = m_manager;
-            unsigned num_args = n->get_num_args();
-            ptr_buffer<expr> args;
-            for (unsigned i = 0; i < num_args; ++i) {
-                args.push_back(find(n->get_arg(i)));
-            }
-            if (m_manager.is_eq(n) && m_util.is_array(args[0])) {
-                visit_eq(n);
-                return;
-            }
-            if (m_manager.is_distinct(n) && num_args > 0 && m_util.is_array(args[0])) {
-                ptr_buffer<expr> eqs;
-                for (unsigned i = 0; i < num_args; ++i) {
-                    for (unsigned j = i + 1; j < num_args; ++j) {
-                        eqs.push_back(m.mk_not(m.mk_eq(args[i], args[j])));
-                    }
-                }
-                insert(n, m.mk_and(eqs.size(), eqs.c_ptr()));               
-                return;
-            }
-
-            if (m_util.is_select(n)) {
-                SASSERT(num_args > 0);
-
-                // select(store(A,i,v),j) -> ite(i = j, v, select(A,j))
-                if (m_util.is_store(args[0])) {
-                    app* a = to_app(args[0]);
-                    expr* b = find(a->get_arg(0));
-                    expr* v = find(a->get_arg(a->get_num_args()-1));
-                    ptr_buffer<expr> eqs;
-                    SASSERT(num_args + 1 == a->get_num_args());
-                    for (unsigned i = 1; i < num_args; ++i) {
-                        eqs.push_back(m.mk_eq(args[i], find(a->get_arg(i))));
-                    }
-                    expr* r = m.mk_ite(m.mk_and(eqs.size(), eqs.c_ptr()), v, mk_select(b, num_args-1, args.c_ptr()+1));
-                    insert(n, r);
-                    return;
-                }
-
-                // select(ite(a,b,c),i) -> ite(a, select(b,i), select(c, i))
-                if (m.is_ite(args[0])) {
-                    app* k = to_app(args[0]);
-                    expr* a = k->get_arg(0);
-                    expr* b = mk_select(k->get_arg(1), args.size()-1, args.c_ptr()+1);
-                    expr* c = mk_select(k->get_arg(2), args.size()-1, args.c_ptr()+1);
-                    expr* r = m.mk_ite(a, b, c);
-                    insert(n, r);
-                    return;
-                }
-
-                // select(map_f(A,B),i) -> f(select(A,i), select(B,i))
-                if (m_util.is_map(args[0])) {
-                    app* a = to_app(args[0]);
-                    func_decl* f = a->get_decl(); 
-                    SASSERT(f->get_num_parameters() == 1);
-                    SASSERT(f->get_parameter(0).is_ast());
-                    SASSERT(is_func_decl(f->get_parameter(0).get_ast()));                    
-                    parameter p = f->get_parameter(0);
-                    func_decl* d = to_func_decl(p.get_ast());
-                    ptr_buffer<expr> args2;
-                    for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                        args2.push_back(mk_select(find(a->get_arg(i)), args.size()-1, args.c_ptr()+1));
-                    }
-                    expr* r = m.mk_app(d, args2.size(), args2.c_ptr()); 
-                    insert(n, r);
-                    return;                    
-                }
-
-                // select(const v, i) -> v
-                if (m_util.is_const(args[0])) {
-                    insert(n, to_app(args[0])->get_arg(0));
-                    return;
-                }
-            }       
-            expr* r = m_manager.mk_app(n->get_decl(), args.size(), args.c_ptr());
-            insert(n, r);
-        }
-        
-    private:
-        void visit_eq(app* eq) {
-            ast_manager& m = m_manager;
-            SASSERT(m.is_eq(eq));
-            sort* s = m.get_sort(eq->get_arg(0));
-            SASSERT(is_sort_of(s, m_fid, ARRAY_SORT));
-            // sort* rng = get_array_range(s);
-            unsigned arity = get_array_arity(s);
-            shift_vars sh(m);
-            expr_ref e1(m), e2(m);
-            sh(find(eq->get_arg(0)), arity, e1);
-            sh(find(eq->get_arg(1)), arity, e2);
-            expr_ref_vector args(m);
-            buffer<symbol> names;
-            ptr_buffer<sort>   sorts;
-            args.push_back(e1);
-            for (unsigned i = 0; i < arity; ++i) {
-                args.push_back(m.mk_var(i, get_array_domain(s, i)));
-                sorts.push_back(get_array_domain(s, arity - i - 1));
-                names.push_back(symbol(m_offset++));
-            }
-            e1 = mk_select(args.size(), args.c_ptr());
-            args[0] = e2;
-            e2 = mk_select(args.size(), args.c_ptr());
-            e1 = m.mk_eq(e1, e2);
-            
-            e1 = m.mk_quantifier(true, arity, sorts.c_ptr(), names.c_ptr(), e1, 1);
-            insert(eq, e1);
-        }
-
-        app* mk_select(unsigned n, expr* const* args) {
-            return m_manager.mk_app(m_fid, OP_SELECT, 0, 0, n, args);
-        }
-        
-        app* mk_select(expr* a, unsigned n, expr* const* args) {
-            ptr_buffer<expr> args2;
-            args2.push_back(a);
-            args2.append(n, args);
-            return mk_select(n+1, args2.c_ptr());
-        }
-    };
-};
-
-void array_property_expander::operator()(unsigned num_fmls, expr* const* fmls, expr_ref_vector& result) {
-    ast_manager& m = m_manager;
-    unsigned offset = 0;
-    for (unsigned i = 0; i < num_fmls; ++i) {
-        bool change = false;
-        expr_ref e(m);
-        result.push_back(fmls[i]);
-        do {
-            array_property_exp::proc p(m, offset);
-            e = result[i].get();
-            for_each_expr(p, e);
-            result[i] = p.find(e);
-            change = e != result[i].get();
-        }
-        while (change);        
-    }
-}
-

src/ast/array_property/array_property_expander.h

-/*++
-Copyright (c) 2010 Microsoft Corporation
-
-Module Name:
-
-    array_property_expander.h
-
-Abstract:
-
-    Expand array operations for the array property fragment formulas.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2010-16-12
-
-Revision History:
-
---*/
-#ifndef _ARRAY_PROPERTY_EXPANDER_H_
-#define _ARRAY_PROPERTY_EXPANDER_H_
-
-#include"ast.h"
-
-class array_property_expander {
-    ast_manager& m_manager;
-public:
-    array_property_expander(ast_manager& m);
-    void operator()(unsigned num_fmls, expr* const* fmls, expr_ref_vector& result);    
-};
-
-
-#endif /* _ARRAY_PROPERTY_EXPANDER_H_ */
-

src/ast/array_property/array_property_recognizer.cpp

-/*++
-Copyright (c) 2010 Microsoft Corporation
-
-Module Name:
-
-    array_property_recognizer.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2010-16-12
-
-Revision History:
-
---*/
-
-#include"array_decl_plugin.h"
-#include"array_property_recognizer.h"
-#include"for_each_expr.h"
-
-
-array_property_recognizer::array_property_recognizer(ast_manager& m):
-    m_manager(m) {}
-
-namespace is_array_property_ns {
-    struct bad {};
-    class proc {
-        ast_manager& m_manager;
-        family_id    m_fid;
-        bool         m_has_quantifier;
-
-        void check_array_sort(expr* n) {
-            if (is_sort_of(m_manager.get_sort(n), m_fid, ARRAY_SORT)) {
-                throw bad();
-            }            
-        }
-
-    public:
-        proc(ast_manager& m) : 
-            m_manager(m), 
-            m_fid(m.get_family_id("array")), 
-            m_has_quantifier(false) {}
-
-        bool has_quantifier() const { return m_has_quantifier; }
-
-        void operator()(var* n) {
-            check_array_sort(n);
-        }
-
-        void operator()(quantifier * ) { 
-            m_has_quantifier = true; 
-        }
-
-        void operator()(app* n) {
-            unsigned num_args = n->get_num_args();
-            if (m_manager.is_eq(n) || m_manager.is_distinct(n)) {
-                return;
-            }
-            family_id fid = n->get_family_id();
-            if (fid == m_fid) {                
-                switch(n->get_decl_kind()) {
-                case OP_STORE:
-                    for (unsigned i = 1; i + 1 < num_args; ++i) {
-                        check_array_sort(n->get_arg(i));
-                    }
-                    return;
-                case OP_SELECT:
-                    for (unsigned i = 1; i < num_args; ++i) {
-                        check_array_sort(n->get_arg(i));
-                    }
-                    return;
-                case OP_CONST_ARRAY:
-                case OP_ARRAY_MAP:
-                    return;
-                default:
-                    throw bad();
-                }                
-            }
-            // arrays cannot be arguments of other functions.
-            for (unsigned i = 0; i < num_args; ++i) {
-                check_array_sort(n->get_arg(i));
-            }
-        }
-    };
-};
-
-bool array_property_recognizer::operator()(unsigned num_fmls, expr* const* fmls) {
-    is_array_property_ns::proc p(m_manager);
-    try {
-        for (unsigned i = 0; i < num_fmls; ++i) {
-            for_each_expr(p, fmls[i]);
-        }
-    }
-    catch (is_array_property_ns::bad) {
-        return false;
-    }
-    return p.has_quantifier();
-}
-
-

src/ast/array_property/array_property_recognizer.h

-/*++
-Copyright (c) 2010 Microsoft Corporation
-
-Module Name:
-
-    array_property_recognizer.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2010-16-12
-
-Revision History:
-
---*/
-#ifndef _ARRAY_PROPERTY_RECOGNIZER_H_
-#define _ARRAY_PROPERTY_RECOGNIZER_H_
-
-#include"ast.h"
-
-class array_property_recognizer {
-    ast_manager& m_manager;
-public:
-    array_property_recognizer(ast_manager& m);
-    bool operator()(unsigned num_fmls, expr* const* fmls);    
-};
-
-
-#endif /* _ARRAY_PROPERTY_RECOGNIZER_H_ */
-

src/dead/array_property/array_property_expander.cpp

+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    array_property_expander.cpp
+
+Abstract:
+
+    Expand array operations for the array property fragment formulas.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-16-12
+
+Revision History:
+
+--*/
+
+#include"array_property_expander.h"
+#include"obj_hashtable.h"
+#include"var_subst.h"
+#include"array_decl_plugin.h"
+#include"for_each_expr.h"
+
+array_property_expander::array_property_expander(ast_manager& m):
+    m_manager(m) {
+}
+
+namespace array_property_exp {
+    class proc {
+        ast_manager& m_manager;
+        unsigned&    m_offset;
+        expr_ref_vector m_trail;
+        family_id    m_fid;
+        array_util   m_util;
+        obj_map<expr, expr*> m_mem;
+
+
+        void insert(expr* a, expr* b) {
+            m_trail.push_back(b);
+            m_mem.insert(a, b);
+        }
+
+
+    public:
+        proc(ast_manager& m, unsigned& offset) : 
+            m_manager(m),
+            m_offset(offset),
+            m_trail(m),
+            m_fid(m.get_family_id("array")),
+            m_util(m)
+        {}
+
+        expr* find(expr* e) {
+            expr* result = 0;
+            VERIFY(m_mem.find(e, result));
+            return result;
+        }
+
+        void operator()(var* n) { insert(n, n); }
+
+        void operator()(quantifier* q) {
+            expr* e = find(q->get_expr());
+            quantifier* q2 = m_manager.update_quantifier(q, e);
+            insert(q, q2);
+        }
+
+        void operator()(app* n) {
+            ast_manager& m = m_manager;
+            unsigned num_args = n->get_num_args();
+            ptr_buffer<expr> args;
+            for (unsigned i = 0; i < num_args; ++i) {
+                args.push_back(find(n->get_arg(i)));
+            }
+            if (m_manager.is_eq(n) && m_util.is_array(args[0])) {
+                visit_eq(n);
+                return;
+            }
+            if (m_manager.is_distinct(n) && num_args > 0 && m_util.is_array(args[0])) {
+                ptr_buffer<expr> eqs;
+                for (unsigned i = 0; i < num_args; ++i) {
+                    for (unsigned j = i + 1; j < num_args; ++j) {
+                        eqs.push_back(m.mk_not(m.mk_eq(args[i], args[j])));
+                    }
+                }
+                insert(n, m.mk_and(eqs.size(), eqs.c_ptr()));               
+                return;
+            }
+
+            if (m_util.is_select(n)) {
+                SASSERT(num_args > 0);
+
+                // select(store(A,i,v),j) -> ite(i = j, v, select(A,j))
+                if (m_util.is_store(args[0])) {
+                    app* a = to_app(args[0]);
+                    expr* b = find(a->get_arg(0));
+                    expr* v = find(a->get_arg(a->get_num_args()-1));
+                    ptr_buffer<expr> eqs;
+                    SASSERT(num_args + 1 == a->get_num_args());
+                    for (unsigned i = 1; i < num_args; ++i) {
+                        eqs.push_back(m.mk_eq(args[i], find(a->get_arg(i))));
+                    }
+                    expr* r = m.mk_ite(m.mk_and(eqs.size(), eqs.c_ptr()), v, mk_select(b, num_args-1, args.c_ptr()+1));
+                    insert(n, r);
+                    return;
+                }
+
+                // select(ite(a,b,c),i) -> ite(a, select(b,i), select(c, i))
+                if (m.is_ite(args[0])) {
+                    app* k = to_app(args[0]);
+                    expr* a = k->get_arg(0);
+                    expr* b = mk_select(k->get_arg(1), args.size()-1, args.c_ptr()+1);
+                    expr* c = mk_select(k->get_arg(2), args.size()-1, args.c_ptr()+1);
+                    expr* r = m.mk_ite(a, b, c);
+                    insert(n, r);
+                    return;
+                }
+
+                // select(map_f(A,B),i) -> f(select(A,i), select(B,i))
+                if (m_util.is_map(args[0])) {
+                    app* a = to_app(args[0]);
+                    func_decl* f = a->get_decl(); 
+                    SASSERT(f->get_num_parameters() == 1);
+                    SASSERT(f->get_parameter(0).is_ast());
+                    SASSERT(is_func_decl(f->get_parameter(0).get_ast()));                    
+                    parameter p = f->get_parameter(0);
+                    func_decl* d = to_func_decl(p.get_ast());
+                    ptr_buffer<expr> args2;
+                    for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                        args2.push_back(mk_select(find(a->get_arg(i)), args.size()-1, args.c_ptr()+1));
+                    }
+                    expr* r = m.mk_app(d, args2.size(), args2.c_ptr()); 
+                    insert(n, r);
+                    return;                    
+                }
+
+                // select(const v, i) -> v
+                if (m_util.is_const(args[0])) {
+                    insert(n, to_app(args[0])->get_arg(0));
+                    return;
+                }
+            }       
+            expr* r = m_manager.mk_app(n->get_decl(), args.size(), args.c_ptr());
+            insert(n, r);
+        }
+        
+    private:
+        void visit_eq(app* eq) {
+            ast_manager& m = m_manager;
+            SASSERT(m.is_eq(eq));
+            sort* s = m.get_sort(eq->get_arg(0));
+            SASSERT(is_sort_of(s, m_fid, ARRAY_SORT));
+            // sort* rng = get_array_range(s);
+            unsigned arity = get_array_arity(s);
+            shift_vars sh(m);
+            expr_ref e1(m), e2(m);
+            sh(find(eq->get_arg(0)), arity, e1);
+            sh(find(eq->get_arg(1)), arity, e2);
+            expr_ref_vector args(m);
+            buffer<symbol> names;
+            ptr_buffer<sort>   sorts;
+            args.push_back(e1);
+            for (unsigned i = 0; i < arity; ++i) {
+                args.push_back(m.mk_var(i, get_array_domain(s, i)));
+                sorts.push_back(get_array_domain(s, arity - i - 1));
+                names.push_back(symbol(m_offset++));
+            }
+            e1 = mk_select(args.size(), args.c_ptr());
+            args[0] = e2;
+            e2 = mk_select(args.size(), args.c_ptr());
+            e1 = m.mk_eq(e1, e2);
+            
+            e1 = m.mk_quantifier(true, arity, sorts.c_ptr(), names.c_ptr(), e1, 1);
+            insert(eq, e1);
+        }
+
+        app* mk_select(unsigned n, expr* const* args) {
+            return m_manager.mk_app(m_fid, OP_SELECT, 0, 0, n, args);
+        }
+        
+        app* mk_select(expr* a, unsigned n, expr* const* args) {
+            ptr_buffer<expr> args2;
+            args2.push_back(a);
+            args2.append(n, args);
+            return mk_select(n+1, args2.c_ptr());
+        }
+    };
+};
+
+void array_property_expander::operator()(unsigned num_fmls, expr* const* fmls, expr_ref_vector& result) {
+    ast_manager& m = m_manager;
+    unsigned offset = 0;
+    for (unsigned i = 0; i < num_fmls; ++i) {
+        bool change = false;
+        expr_ref e(m);
+        result.push_back(fmls[i]);
+        do {
+            array_property_exp::proc p(m, offset);
+            e = result[i].get();
+            for_each_expr(p, e);
+            result[i] = p.find(e);
+            change = e != result[i].get();
+        }
+        while (change);        
+    }
+}
+

src/dead/array_property/array_property_expander.h

+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    array_property_expander.h
+
+Abstract:
+
+    Expand array operations for the array property fragment formulas.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-16-12
+
+Revision History:
+
+--*/
+#ifndef _ARRAY_PROPERTY_EXPANDER_H_
+#define _ARRAY_PROPERTY_EXPANDER_H_
+
+#include"ast.h"
+
+class array_property_expander {
+    ast_manager& m_manager;
+public:
+    array_property_expander(ast_manager& m);
+    void operator()(unsigned num_fmls, expr* const* fmls, expr_ref_vector& result);    
+};
+
+
+#endif /* _ARRAY_PROPERTY_EXPANDER_H_ */
+

src/dead/array_property/array_property_recognizer.cpp

+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    array_property_recognizer.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-16-12
+
+Revision History:
+
+--*/
+
+#include"array_decl_plugin.h"
+#include"array_property_recognizer.h"
+#include"for_each_expr.h"
+
+
+array_property_recognizer::array_property_recognizer(ast_manager& m):
+    m_manager(m) {}
+
+namespace is_array_property_ns {
+    struct bad {};
+    class proc {
+        ast_manager& m_manager;
+        family_id    m_fid;
+        bool         m_has_quantifier;
+
+        void check_array_sort(expr* n) {
+            if (is_sort_of(m_manager.get_sort(n), m_fid, ARRAY_SORT)) {
+                throw bad();
+            }            
+        }
+
+    public:
+        proc(ast_manager& m) : 
+            m_manager(m), 
+            m_fid(m.get_family_id("array")), 
+            m_has_quantifier(false) {}
+
+        bool has_quantifier() const { return m_has_quantifier; }
+
+        void operator()(var* n) {
+            check_array_sort(n);
+        }
+
+        void operator()(quantifier * ) { 
+            m_has_quantifier = true; 
+        }
+
+        void operator()(app* n) {
+            unsigned num_args = n->get_num_args();
+            if (m_manager.is_eq(n) || m_manager.is_distinct(n)) {
+                return;
+            }
+            family_id fid = n->get_family_id();
+            if (fid == m_fid) {                
+                switch(n->get_decl_kind()) {
+                case OP_STORE:
+                    for (unsigned i = 1; i + 1 < num_args; ++i) {
+                        check_array_sort(n->get_arg(i));
+                    }
+                    return;
+                case OP_SELECT:
+                    for (unsigned i = 1; i < num_args; ++i) {
+                        check_array_sort(n->get_arg(i));
+                    }
+                    return;
+                case OP_CONST_ARRAY:
+                case OP_ARRAY_MAP:
+                    return;
+                default:
+                    throw bad();
+                }                
+            }
+            // arrays cannot be arguments of other functions.
+            for (unsigned i = 0; i < num_args; ++i) {
+                check_array_sort(n->get_arg(i));
+            }
+        }
+    };
+};
+
+bool array_property_recognizer::operator()(unsigned num_fmls, expr* const* fmls) {
+    is_array_property_ns::proc p(m_manager);
+    try {
+        for (unsigned i = 0; i < num_fmls; ++i) {
+            for_each_expr(p, fmls[i]);
+        }
+    }
+    catch (is_array_property_ns::bad) {
+        return false;
+    }
+    return p.has_quantifier();
+}
+
+

src/dead/array_property/array_property_recognizer.h

+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    array_property_recognizer.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-16-12
+
+Revision History:
+
+--*/
+#ifndef _ARRAY_PROPERTY_RECOGNIZER_H_
+#define _ARRAY_PROPERTY_RECOGNIZER_H_
+
+#include"ast.h"
+
+class array_property_recognizer {
+    ast_manager& m_manager;
+public:
+    array_property_recognizer(ast_manager& m);
+    bool operator()(unsigned num_fmls, expr* const* fmls);    
+};
+
+
+#endif /* _ARRAY_PROPERTY_RECOGNIZER_H_ */
+

src/test/array_property_expander.cpp

-#include "array_property_expander.h"
-#include "array_property_recognizer.h"
-#include "smtparser.h"
-#include "array_decl_plugin.h"
-#include "ast_pp.h"
-#include <sstream>
-
-static void test_array_expand(ast_manager& m, expr* fml) {
-    std::cout << mk_pp(fml, m) << "\n";
-    expr_ref_vector result(m);
-    array_property_expander exp(m);
-    array_property_recognizer rec(m);
-    exp(1, &fml, result);
-    std::cout << mk_pp(result[0].get(), m) << "\n";
-    std::cout << rec(1, &fml) << "\n";
-}
-
-
-static void parse_string(char const* fml) {
-    ast_manager m;
-    m.register_plugin(symbol("array"), alloc(array_decl_plugin)); 
-    scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
-    parser->initialize_smtlib();
-
-    std::ostringstream buffer;
-    buffer << "(benchmark array :status unknown :logic AUFLIA \n"
-           << ":extrafuns ((A (Array Int Int)) (B (Array Int Int)))\n"
-           << ":extrafuns ((C (Array Int (Array Int Int))))\n"
-           << ":extrafuns ((D (Array Int Bool Int)))\n"
-           << ":extrafuns ((i Int) (j Int))\n"
-           << ":extrafuns ((f Int Int))\n"
-           << ":formula " << fml << ")";
-    parser->parse_string(buffer.str().c_str());
-    smtlib::benchmark* b = parser->get_benchmark();
-    smtlib::theory::expr_iterator it  = b->begin_formulas();
-    smtlib::theory::expr_iterator end = b->end_formulas();
-    for (; it != end; ++it) {
-        test_array_expand(m, *it);
-    }
-}
-
-
-void tst_array_property_expander() {
-    parse_string("(= A B)");
-    parse_string("(= A (store B i 4))");
-    parse_string("(= C (store C 0 (store (select C 0) i 1)))");
-    parse_string("(exists (i Int) (= C (store C 0 (store (select C 0) i 1))))");
-    parse_string("(forall (i Int) (b Bool) (= D (store D i b 4)))");
-    parse_string("(= (const[Array] 3) A)");
-    parse_string("(= (map[f] A) B)");
-
-}
-

src/test/dead/array_property_expander.cpp

+#include "array_property_expander.h"
+#include "array_property_recognizer.h"
+#include "smtparser.h"
+#include "array_decl_plugin.h"
+#include "ast_pp.h"
+#include <sstream>
+
+static void test_array_expand(ast_manager& m, expr* fml) {
+    std::cout << mk_pp(fml, m) << "\n";
+    expr_ref_vector result(m);
+    array_property_expander exp(m);
+    array_property_recognizer rec(m);
+    exp(1, &fml, result);
+    std::cout << mk_pp(result[0].get(), m) << "\n";
+    std::cout << rec(1, &fml) << "\n";
+}
+
+
+static void parse_string(char const* fml) {
+    ast_manager m;
+    m.register_plugin(symbol("array"), alloc(array_decl_plugin)); 
+    scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
+    parser->initialize_smtlib();
+
+    std::ostringstream buffer;
+    buffer << "(benchmark array :status unknown :logic AUFLIA \n"
+           << ":extrafuns ((A (Array Int Int)) (B (Array Int Int)))\n"
+           << ":extrafuns ((C (Array Int (Array Int Int))))\n"
+           << ":extrafuns ((D (Array Int Bool Int)))\n"
+           << ":extrafuns ((i Int) (j Int))\n"
+           << ":extrafuns ((f Int Int))\n"
+           << ":formula " << fml << ")";
+    parser->parse_string(buffer.str().c_str());
+    smtlib::benchmark* b = parser->get_benchmark();
+    smtlib::theory::expr_iterator it  = b->begin_formulas();
+    smtlib::theory::expr_iterator end = b->end_formulas();
+    for (; it != end; ++it) {
+        test_array_expand(m, *it);
+    }
+}
+
+
+void tst_array_property_expander() {
+    parse_string("(= A B)");
+    parse_string("(= A (store B i 4))");
+    parse_string("(= C (store C 0 (store (select C 0) i 1)))");
+    parse_string("(exists (i Int) (= C (store C 0 (store (select C 0) i 1))))");
+    parse_string("(forall (i Int) (b Bool) (= D (store D i b 4)))");
+    parse_string("(= (const[Array] 3) A)");
+    parse_string("(= (map[f] A) B)");
+
+}
+

src/test/main.cpp

     TST(dl_product_relation);
     TST(dl_relation);
     TST(imdd);
-    TST(array_property_expander);
     TST(parray);
     TST(stack);
     TST(escaped);