From 3dc2028925e6936b07682e342b8a644b7551fb20 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Mar 2016 09:20:57 -0700
Subject: [PATCH] adding min/max

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 CMakeLists.txt  |  4 +--
 src/qe/qsat.cpp | 82 +++++++++++++++++++++++++++++++++++++++++--------
 src/qe/qsat.h   | 11 +++++++
 3 files changed, 83 insertions(+), 14 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index d33f352e1..c169be14d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -294,10 +294,10 @@ if (ENABLE_TRACING)
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE")
 endif()
 # Should we always enable tracing when doing a debug build?
-#list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
 
 ################################################################################
-# Postion indepdent code
+# Postion independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index b080b71a2..0a5c40dbd 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -499,15 +499,7 @@ namespace qe {
             }
         }
     }
-    
-    class qsat : public tactic {
-        
-        struct stats {
-            unsigned m_num_rounds;        
-            stats() { reset(); }
-            void reset() { memset(this, 0, sizeof(*this)); }
-        };
-        
+
         class kernel {
             ast_manager& m;
             smt_params   m_smtp;
@@ -542,6 +534,15 @@ namespace qe {
                       );
             }
         };
+    
+    class qsat : public tactic {
+        
+        struct stats {
+            unsigned m_num_rounds;        
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+        
         
         ast_manager&               m;
         params_ref                 m_params;
@@ -1155,10 +1156,67 @@ namespace qe {
         
         tactic * translate(ast_manager & m) {
             return alloc(qsat, m, m_params, m_qelim, m_force_elim);
-        }
-        
-        
+        }               
     };
+
+   
+
+
+    struct min_max_opt::imp {
+        ast_manager&    m;
+        expr_ref_vector m_fmls;
+        pred_abs        m_pred_abs;
+        qe::mbp         m_mbp;
+        kernel          m_kernel;
+
+        imp(ast_manager& m): 
+            m(m), 
+            m_fmls(m), 
+            m_pred_abs(m), 
+            m_mbp(m),
+            m_kernel(m) {}
+
+        void add(expr* e) {
+            m_fmls.push_back(e);
+        }
+
+        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+            // Assume this is the only call to check.
+            expr_ref_vector defs(m);
+            expr_ref fml = mk_and(m_fmls);
+            m_pred_abs.abstract_atoms(fml, defs);
+            fml = m_pred_abs.mk_abstract(fml);
+            m_kernel.assert_expr(mk_and(defs));
+            m_kernel.assert_expr(fml);
+            // TBD
+            
+            return l_undef;
+        }
+    };
+
+    min_max_opt::min_max_opt(ast_manager& m) {
+        m_imp = alloc(imp, m);
+    }
+
+    min_max_opt::~min_max_opt() {
+        dealloc(m_imp);
+    }
+
+    void min_max_opt::add(expr* e) {
+        m_imp->add(e);
+    }
+
+    void min_max_opt::add(expr_ref_vector const& fmls) {
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            add(fmls[i]);
+        }
+    }
+
+    lbool min_max_opt::check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t) {
+        return m_imp->check(is_max, vars, t);
+    }
+
+
     
 };
 
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
index ee9f9e6ad..91b370294 100644
--- a/src/qe/qsat.h
+++ b/src/qe/qsat.h
@@ -113,6 +113,17 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
+    class min_max_opt {
+        struct imp;
+        imp* m_imp;
+    public:
+        min_max_opt(ast_manager& m);
+        ~min_max_opt();
+        void add(expr* e);
+        void add(expr_ref_vector const& fmls);
+        lbool check(svector<bool> const& is_max, func_decl_ref_vector const& vars, app* t);
+    };
+
 
 }