n/a

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

src/qe/qe_mbp.h

@@ -24,28 +24,25 @@ Revision History:
 #include "ast.h"
 #include "params.h"
 
-class qe_mbp {
+namespace qe {
-    class impl;
+    class mbp {
-    impl * m_impl;
+        class impl;
-public:
+        impl * m_impl;
-    qe_mbp(ast_manager& m);
+    public:
+        mbp(ast_manager& m);
         
-    ~qe_mbp();
+        ~mbp();
         
-    /**
+        /**
-       \brief
+           \brief
-       Apply model-based qe on constants provided as vector of variables. 
+           Apply model-based qe on constants provided as vector of variables. 
-       Return the updated formula and updated set of variables that were not eliminated.
+           Return the updated formula and updated set of variables that were not eliminated.
            
-    */
+        */
-    void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
+        void operator()(app_ref_vector& vars, model_ref& mdl, expr_ref& fml);
         
-    /**
+        void set_cancel(bool f);
-        \brief full rewriting based light-weight quantifier elimination round.
+    };
-    */
+}
-    void operator()(expr_ref& fml, proof_ref& pr);
-
-    void set_cancel(bool f);
-};
 
 #endif 

src/qe/qsat.cpp

@@ -0,0 +1,200 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.cpp
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#include "qsat.h"
+#include "smt_kernel.h"
+#include "qe_mbp.h"
+
+namespace qe;
+
+sturct qdef_t {
+    expr_ref        m_pred;
+    expr_ref        m_expr;
+    expr_ref_vector m_vars;
+    bool            m_is_forall;
+    qdef_t(expr_ref& p, expr_ref& e, expr_ref_vector const& vars, bool is_forall):
+        m_pred(p), 
+        m_expr(e),
+        m_vars(vars),
+        m_is_forall(is_forall) {}
+};
+
+typedef vector<qdef_t> qdefs_t;
+
+struct pdef_t {
+    expr_ref  m_pred;
+    expr_ref  m_atom;
+    pdef_t(expr_ref& p, expr_ref& a):
+        m_pred(p), 
+        m_atom(a)
+    {}
+};
+
+class qsat::impl {
+    ast_manager& m;
+    mbp          mbp;
+
+    /**
+       \brief replace quantified sub-formulas by a predicate, introduce definitions for the predicate.
+     */
+    void remove_quantifiers(expr_ref_vector& fmls, qdefs_t& defs) {
+        
+    }
+
+    /** 
+        \brief create propositional abstration of formula by replacing atomic sub-formulas by fresh 
+        propositional variables, and adding definitions for each propositional formula on the side.
+        Assumption is that the formula is quantifier-free.
+    */
+    void mk_abstract(expr_ref_vector& fmls, vector<pdef_t>& pdefs) {
+        expr_ref_vector todo(fmls), trail(m);
+        obj_map<expr,expr*> cache;
+        ptr_vector<expr> args;
+        expr_ref r(m);
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            if (cache.contains(e)) {
+                todo.pop_back();
+                continue;
+            }
+            SASSERT(is_app(e));
+            app* a = to_app(e);
+            if (a->get_family_id() == m.get_basic_family_id()) {
+                unsigned sz = a->get_num_args();
+                args.reset();
+                for (unsigned i = 0; i < sz; ++i) {
+                    expr* f = a->get_arg(i);
+                    if (cache.find(f, f)) {
+                        args.push_back(f);
+                    }
+                    else {
+                        todo.push_back(f);
+                    }
+                }
+                if (args.size() == sz) {
+                    r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+                    cache.insert(e, r);
+                    trail.push_back(r);
+                    todo.pop_back(e);
+                }
+            }
+            else if (is_uninterpreted_const(a)) {
+                cache.insert(e, e);
+            }
+            else {
+                // TBD: nested Booleans.
+                r = m.mk_fresh_const("p",m.mk_bool_sort());
+                trail.push_back(r);
+                cache.insert(e, r);
+                pdefs.push_back(pdef_t(e, r));
+            }
+        }
+        
+        for (unsigned i = 0; i < fmls.size(); ++i) {
+            fmls[i] = cache.find(fmls[i].get());
+        }
+    }
+
+    /** 
+        \brief use dual propagation to minimize model.
+    */
+    void minimize_assignment(app_ref_vector& assignment) {
+        
+    }
+
+public:
+    impl(ast_manager& m):
+        m(m),
+        mbp(m) {}
+
+    void updt_params(params_ref const & p) {
+    }
+    void collect_param_descrs(param_descrs & r) {
+    }
+    void operator()(/* in */  goal_ref const & in, 
+                    /* out */ goal_ref_buffer & result, 
+                    /* out */ model_converter_ref & mc, 
+                    /* out */ proof_converter_ref & pc,
+                    /* out */ expr_dependency_ref & core) {
+
+    }
+
+    void collect_statistics(statistics & st) const {
+
+    }
+    void reset_statistics() {
+    }
+    void cleanup() {
+    }
+    void set_logic(symbol const & l) {
+    }
+    void set_progress_callback(progress_callback * callback) {
+    }
+    tactic * translate(ast_manager & m) {
+        return 0;
+    }
+
+};
+
+qsat::qsat(ast_manager& m) {
+    m_impl = alloc(impl, m);
+}
+
+qsat::~qsat() {
+    dealloc(m_impl);
+}
+
+void qsat::updt_params(params_ref const & p) {
+    m_impl->updt_params(p);
+}
+void qsat::collect_param_descrs(param_descrs & r) {
+    m_impl->collect_param_descrs(r);
+}
+void qsat::operator()(/* in */  goal_ref const & in, 
+                      /* out */ goal_ref_buffer & result, 
+                      /* out */ model_converter_ref & mc, 
+                      /* out */ proof_converter_ref & pc,
+                      /* out */ expr_dependency_ref & core) {
+    (*m_impl)(in, result, mc, pc, core);
+}
+
+void qsat::collect_statistics(statistics & st) const {
+    m_impl->collect_statistics(st);
+}
+void qsat::reset_statistics() {
+    m_impl->reset_statistics();
+}
+void qsat::cleanup() {
+    m_impl->cleanup();
+}
+void qsat::set_logic(symbol const & l) {
+    m_impl->set_logic(l);
+}
+void qsat::set_progress_callback(progress_callback * callback) {
+    m_impl->set_progress_callback(callback);
+}
+tactic * qsat::translate(ast_manager & m) {
+    return m_impl->translate(m);
+}
+
+
+};
+
+#endif 

src/qe/qsat.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    qsat.h
+
+Abstract:
+
+    Quantifier Satisfiability Solver.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+
+--*/
+
+#ifndef __QE_MBP_H__
+#define __QE_MBP_H__
+
+#include "tactic.h"
+
+namespace qe {
+    class qsat : public tactic {
+        class impl;
+        impl * m_impl;
+    public:
+        qsat(ast_manager& m);
+        ~qsat();
+        
+        virtual void updt_params(params_ref const & p);
+        virtual void collect_param_descrs(param_descrs & r);
+        virtual void operator()(/* in */  goal_ref const & in, 
+                                /* out */ goal_ref_buffer & result, 
+                                /* out */ model_converter_ref & mc, 
+                                /* out */ proof_converter_ref & pc,
+                                /* out */ expr_dependency_ref & core);
+        
+        virtual void collect_statistics(statistics & st) const;
+        virtual void reset_statistics();
+        virtual void cleanup() = 0;
+        virtual void set_logic(symbol const & l);
+        virtual void set_progress_callback(progress_callback * callback);
+        virtual tactic * translate(ast_manager & m);
+        
+    };
+};
+
+#endif