re-organize muz_qe into separate units

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

src/muz/pdr/pdr_context.h

@@ -0,0 +1,429 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_context.h
+
+Abstract:
+
+    PDR for datalog
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-11-20.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_CONTEXT_H_
+#define _PDR_CONTEXT_H_
+
+#ifdef _CYGWIN
+#undef min
+#undef max
+#endif
+#include <deque>
+#include "pdr_manager.h"
+#include "pdr_prop_solver.h"
+#include "pdr_reachable_cache.h"
+
+
+namespace datalog {
+    class rule_set;
+    class context;
+};
+
+namespace pdr {
+
+    class pred_transformer;
+    class model_node;
+    class context;
+
+    typedef obj_map<datalog::rule const, app_ref_vector*> rule2inst;
+    typedef obj_map<func_decl, pred_transformer*> decl2rel;
+
+
+    // 
+    // Predicate transformer state.
+    // A predicate transformer corresponds to the 
+    // set of rules that have the same head predicates.
+    // 
+    
+    class pred_transformer {
+
+        struct stats {
+            unsigned m_num_propagations;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        typedef obj_map<datalog::rule const, expr*> rule2expr;
+        typedef obj_map<datalog::rule const, ptr_vector<app> > rule2apps;
+
+        manager&                     pm;        // pdr-manager
+        ast_manager&                 m;         // manager
+        context&                     ctx;
+        
+        func_decl_ref                m_head;    // predicate 
+        func_decl_ref_vector         m_sig;     // signature
+        ptr_vector<pred_transformer> m_use;     // places where 'this' is referenced.
+        ptr_vector<datalog::rule>    m_rules;   // rules used to derive transformer
+        prop_solver                  m_solver;  // solver context
+        vector<expr_ref_vector>      m_levels;  // level formulas
+        expr_ref_vector              m_invariants;      // properties that are invariant.
+        obj_map<expr, unsigned>      m_prop2level;      // map property to level where it occurs.
+        obj_map<expr, datalog::rule const*> m_tag2rule; // map tag predicate to rule. 
+        rule2expr                    m_rule2tag;        // map rule to predicate tag.
+        rule2inst                    m_rule2inst;       // map rules to instantiations of indices
+        rule2expr                    m_rule2transition; // map rules to transition 
+        rule2apps                    m_rule2vars;       // map rule to auxiliary variables
+        expr_ref                     m_transition;      // transition relation.
+        expr_ref                     m_initial_state;   // initial state.
+        reachable_cache              m_reachable; 
+        ptr_vector<func_decl>        m_predicates;
+        stats                        m_stats;
+
+        void init_sig();
+        void ensure_level(unsigned level);
+        bool add_property1(expr * lemma, unsigned lvl);  // add property 'p' to state at level lvl.
+        void add_child_property(pred_transformer& child, expr* lemma, unsigned lvl); 
+        void mk_assumptions(func_decl* head, expr* fml, expr_ref_vector& result);
+
+        // Initialization
+        void init_rules(decl2rel const& pts, expr_ref& init, expr_ref& transition);
+        void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init,                                      
+                       ptr_vector<datalog::rule const>& rules, expr_ref_vector& transition);
+        void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
+
+        void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
+
+        // Debugging
+        bool check_filled(app_ref_vector const& v) const;
+        
+        void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r);
+
+    public:
+        pred_transformer(context& ctx, manager& pm, func_decl* head);
+        ~pred_transformer();
+
+        void add_rule(datalog::rule* r) { m_rules.push_back(r); }
+        void add_use(pred_transformer* pt) { if (!m_use.contains(pt)) m_use.insert(pt); }
+        void initialize(decl2rel const& pts);
+
+        func_decl* head() const { return m_head; }
+        ptr_vector<datalog::rule> const& rules() const { return m_rules; }
+        func_decl* sig(unsigned i) { init_sig(); return m_sig[i].get(); } // signature 
+        func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); }
+        unsigned  sig_size() { init_sig(); return m_sig.size(); }
+        expr*  transition() const { return m_transition; }
+        expr*  initial_state() const { return m_initial_state; }
+        expr*  rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }
+        unsigned get_num_levels() { return m_levels.size(); }
+        expr_ref get_cover_delta(func_decl* p_orig, int level);
+        void     add_cover(unsigned level, expr* property);
+
+        std::ostream& display(std::ostream& strm) const;
+
+        void collect_statistics(statistics& st) const;
+        void reset_statistics();
+
+        bool is_reachable(expr* state);
+        void remove_predecessors(expr_ref_vector& literals);
+        void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
+        datalog::rule const& find_rule(model_core const& model) const;
+        expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); }
+        ptr_vector<app>& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); }
+
+        bool propagate_to_next_level(unsigned level);
+        void propagate_to_infinity(unsigned level);
+        void add_property(expr * lemma, unsigned lvl);  // add property 'p' to state at level.
+
+        lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level);
+        bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = 0);
+        bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level);
+
+        expr_ref get_formulas(unsigned level, bool add_axioms);
+
+        void simplify_formulas();
+
+        expr_ref get_propagation_formula(decl2rel const& pts, unsigned level);
+
+        manager& get_pdr_manager() const { return pm; }
+        ast_manager& get_manager() const { return m; }
+
+        void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
+
+        void close(expr* e);
+
+        app_ref_vector& get_inst(datalog::rule const* r) { return *m_rule2inst.find(r);}
+
+        void inherit_properties(pred_transformer& other);
+
+        void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
+
+        prop_solver& get_solver() { return m_solver; }
+        prop_solver const& get_solver() const { return m_solver; }
+
+        void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
+        bool get_use_farkas() const { return get_solver().get_use_farkas(); }
+        class scoped_farkas {
+            bool m_old;
+            pred_transformer& m_p;
+        public:
+            scoped_farkas(pred_transformer& p, bool v): m_old(p.get_use_farkas()), m_p(p) {
+                p.set_use_farkas(v);
+            }
+            ~scoped_farkas() { m_p.set_use_farkas(m_old); }
+        };
+
+    };
+
+
+    // structure for counter-example search.
+    class model_node {
+        model_node*            m_parent;
+        pred_transformer&      m_pt;
+        expr_ref               m_state;
+        model_ref              m_model;
+        ptr_vector<model_node> m_children;
+        unsigned               m_level;       
+        unsigned               m_orig_level;
+        unsigned               m_depth;
+        bool                   m_closed;
+        datalog::rule const*   m_rule;
+    public:
+        model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
+            m_parent(parent), m_pt(pt), m_state(state), m_model(0), 
+                m_level(level), m_orig_level(level), m_depth(0), m_closed(false), m_rule(0) {
+            if (m_parent) {
+                m_parent->m_children.push_back(this);
+                SASSERT(m_parent->m_level == level+1);
+                SASSERT(m_parent->m_level > 0);
+                m_depth = m_parent->m_depth+1;
+            }
+        }
+        void set_model(model_ref& m) { m_model = m; }
+        unsigned level() const { return m_level; }
+        unsigned orig_level() const { return m_orig_level; }
+        unsigned depth() const { return m_depth; }
+        void     increase_level() { ++m_level; }
+        expr*    state() const { return m_state; }
+        ptr_vector<model_node> const& children() { return m_children; }
+        pred_transformer& pt() const { return m_pt; }
+        model_node* parent() const { return m_parent; }
+        model* get_model_ptr() const { return m_model.get(); }
+        model const&  get_model() const { return *m_model; }
+        unsigned index() const;
+
+        bool is_closed() const { return m_closed; }
+        bool is_open() const { return !is_closed(); }
+
+        bool is_1closed() {
+            if (is_closed()) return true;
+            if (m_children.empty()) return false;
+            for (unsigned i = 0; i < m_children.size(); ++i) {
+                if (m_children[i]->is_open()) return false;
+            }
+            return true;
+        }
+
+        void set_closed();     
+        void set_pre_closed() { m_closed = true; }
+        void reset() { m_children.reset(); }
+
+        void set_rule(datalog::rule const* r) { m_rule = r; }
+        datalog::rule* get_rule();
+
+        void mk_instantiate(datalog::rule_ref& r0, datalog::rule_ref& r1, expr_ref_vector& binding);
+
+        std::ostream& display(std::ostream& out, unsigned indent);
+    };
+
+    class model_search {
+        bool               m_bfs;
+        model_node*        m_root;
+        std::deque<model_node*> m_leaves;
+        vector<obj_map<expr, unsigned> > m_cache;
+        
+        obj_map<expr, unsigned>& cache(model_node const& n);
+        void erase_children(model_node& n);
+        void erase_leaf(model_node& n);
+        void remove_node(model_node& n);
+        void enqueue_leaf(model_node& n); // add leaf to priority queue.
+        void update_models();
+    public:
+        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        ~model_search();
+
+        void reset();
+        model_node* next();
+        bool is_repeated(model_node& n) const;
+        void add_leaf(model_node& n); // add fresh node.
+        void set_leaf(model_node& n); // Set node as leaf, remove children.
+
+        void set_root(model_node* n);
+        model_node& get_root() const { return *m_root; }
+        std::ostream& display(std::ostream& out) const; 
+        expr_ref get_trace(context const& ctx);
+        proof_ref get_proof_trace(context const& ctx);
+        void backtrack_level(bool uses_level, model_node& n);
+    };
+
+    struct model_exception { };
+    struct inductive_exception {};
+
+
+    // 'state' is unsatisfiable at 'level' with 'core'. 
+    // Minimize or weaken core.
+    class core_generalizer {
+    protected:
+        context& m_ctx;
+    public:
+        typedef vector<std::pair<expr_ref_vector,bool> > cores;
+        core_generalizer(context& ctx): m_ctx(ctx) {}
+        virtual ~core_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) = 0;
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
+            new_cores.push_back(std::make_pair(core, uses_level));
+            if (!core.empty()) {
+                (*this)(n, new_cores.back().first, new_cores.back().second);
+            }
+        }
+        virtual void collect_statistics(statistics& st) const {}
+        virtual void reset_statistics() {}
+    };
+
+    class context {
+
+        struct stats {
+            unsigned m_num_nodes;
+            unsigned m_max_depth;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+        
+        smt_params&    m_fparams;
+        fixedpoint_params const&    m_params;
+        ast_manager&         m;
+        datalog::context*    m_context;
+        manager              m_pm;  
+        decl2rel             m_rels;         // Map from relation predicate to fp-operator.       
+        func_decl_ref        m_query_pred;
+        pred_transformer*    m_query;
+        mutable model_search m_search;
+        lbool                m_last_result;
+        unsigned             m_inductive_lvl;
+        unsigned             m_expanded_lvl;
+        ptr_vector<core_generalizer>  m_core_generalizers;
+        stats                m_stats;
+        volatile bool        m_cancel;
+        model_converter_ref  m_mc;
+        proof_converter_ref  m_pc;
+        
+        // Functions used by search.
+        void solve_impl();
+        bool check_reachability(unsigned level);        
+        void propagate(unsigned max_prop_lvl);
+        void close_node(model_node& n);
+        void check_pre_closed(model_node& n);
+        void expand_node(model_node& n);
+        lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level);
+        void create_children(model_node& n);
+        expr_ref mk_sat_answer() const;
+        expr_ref mk_unsat_answer() const;
+        
+        // Generate inductive property
+        void get_level_property(unsigned lvl, expr_ref_vector& res, vector<relation_info> & rs) const;
+
+
+        // Initialization
+        class classifier_proc;
+        void init_core_generalizers(datalog::rule_set& rules);
+
+        bool check_invariant(unsigned lvl);
+        bool check_invariant(unsigned lvl, func_decl* fn);
+
+        void checkpoint();
+
+        void init_rules(datalog::rule_set& rules, decl2rel& transformers);
+
+        void simplify_formulas();
+
+        void reset_core_generalizers();
+
+        void validate();
+
+    public:       
+        
+        /**
+           Initial values of predicates are stored in corresponding relations in dctx.
+           
+           We check whether there is some reachable state of the relation checked_relation.
+        */
+        context(
+            smt_params&        fparams,
+            fixedpoint_params const&  params,
+            ast_manager&       m);
+
+        ~context();
+        
+        smt_params&       get_fparams() const { return m_fparams; }
+        fixedpoint_params const& get_params() const { return m_params; }
+        ast_manager&      get_manager() const { return m; }
+        manager&          get_pdr_manager() { return m_pm; }
+        decl2rel const&   get_pred_transformers() const { return m_rels; }
+        pred_transformer& get_pred_transformer(func_decl* p) const { return *m_rels.find(p); }
+        datalog::context& get_context() const { SASSERT(m_context); return *m_context; }
+        expr_ref          get_answer();
+
+        bool              is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; }
+        bool              is_utvpi() const { return m_fparams.m_arith_mode == AS_UTVPI; }
+
+        void collect_statistics(statistics& st) const;
+        void reset_statistics();
+
+        std::ostream& display(std::ostream& strm) const;        
+
+        void display_certificate(std::ostream& strm) const;
+
+        lbool solve();
+
+        void cancel();
+
+        void cleanup();
+
+        void reset();
+
+        void set_query(func_decl* q) { m_query_pred = q; }
+
+        void set_unsat() { m_last_result = l_false; }
+
+        void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
+
+        model_converter_ref get_model_converter() { return m_mc; }
+
+        void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
+
+        void update_rules(datalog::rule_set& rules);
+
+        void set_axioms(expr* axioms) { m_pm.set_background(axioms); }
+
+        unsigned get_num_levels(func_decl* p);
+
+        expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
+
+        void add_cover(int level, func_decl* pred, expr* property);
+
+        model_ref get_model();
+
+        proof_ref get_proof() const;
+
+        model_node& get_root() const { return m_search.get_root(); }
+
+    };
+
+};
+
+#endif

src/muz/pdr/pdr_dl_interface.cpp

@@ -0,0 +1,225 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_dl.cpp
+
+Abstract:
+
+    SMT2 interface for the datalog PDR
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-22.
+
+Revision History:
+
+--*/
+
+#include "dl_context.h"
+#include "dl_mk_coi_filter.h"
+#include "dl_mk_interp_tail_simplifier.h"
+#include "dl_mk_subsumption_checker.h"
+#include "dl_mk_rule_inliner.h"
+#include "dl_rule.h"
+#include "dl_rule_transformer.h"
+#include "smt2parser.h"
+#include "pdr_context.h"
+#include "pdr_dl_interface.h"
+#include "dl_rule_set.h"
+#include "dl_mk_slice.h"
+#include "dl_mk_unfold.h"
+#include "dl_mk_coalesce.h"
+#include "model_smt2_pp.h"
+#include "dl_transforms.h"
+
+using namespace pdr;
+
+dl_interface::dl_interface(datalog::context& ctx) : 
+    engine_base(ctx.get_manager(), "pdr"),
+    m_ctx(ctx), 
+    m_pdr_rules(ctx), 
+    m_old_rules(ctx),
+    m_context(0),
+    m_refs(ctx.get_manager()) {
+    m_context = alloc(pdr::context, ctx.get_fparams(), ctx.get_params(), ctx.get_manager());
+}
+
+
+dl_interface::~dl_interface() {
+    dealloc(m_context);
+}
+
+
+//
+// Check if the new rules are weaker so that we can 
+// re-use existing context.
+// 
+void dl_interface::check_reset() {
+    datalog::rule_set const& new_rules = m_ctx.get_rules();
+    datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules();  
+    bool is_subsumed = !old_rules.empty();
+    for (unsigned i = 0; is_subsumed && i < new_rules.get_num_rules(); ++i) {
+        is_subsumed = false;
+        for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) {
+            if (m_ctx.check_subsumes(*old_rules[j], *new_rules.get_rule(i))) {
+                is_subsumed = true;
+            }
+        }
+        if (!is_subsumed) {
+            TRACE("pdr", new_rules.get_rule(i)->display(m_ctx, tout << "Fresh rule "););
+            m_context->reset();
+        }
+    }
+    m_old_rules.replace_rules(new_rules);
+}
+
+
+lbool dl_interface::query(expr * query) {
+    //we restore the initial state in the datalog context
+    m_ctx.ensure_opened();
+    m_refs.reset();
+    m_pred2slice.reset();
+    ast_manager& m =                      m_ctx.get_manager();
+    datalog::rule_manager& rm = m_ctx.get_rule_manager();
+
+    datalog::rule_set        old_rules(m_ctx.get_rules());
+    func_decl_ref            query_pred(m);
+    rm.mk_query(query, m_ctx.get_rules());
+    expr_ref bg_assertion = m_ctx.get_background_assertion();
+
+    check_reset();
+
+    TRACE("pdr",
+          if (!m.is_true(bg_assertion)) {
+              tout << "axioms:\n";
+              tout << mk_pp(bg_assertion, m) << "\n";
+          }
+          tout << "query: " << mk_pp(query, m) << "\n";
+          tout << "rules:\n";
+          m_ctx.display_rules(tout);
+          );
+
+
+    apply_default_transformation(m_ctx);
+
+    if (m_ctx.get_params().slice()) {
+        datalog::rule_transformer transformer(m_ctx);
+        datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
+        transformer.register_plugin(slice);
+        m_ctx.transform_rules(transformer);
+        
+        // track sliced predicates.
+        obj_map<func_decl, func_decl*> const& preds = slice->get_predicates();
+        obj_map<func_decl, func_decl*>::iterator it  = preds.begin();
+        obj_map<func_decl, func_decl*>::iterator end = preds.end();
+        for (; it != end; ++it) {
+            m_pred2slice.insert(it->m_key, it->m_value);
+            m_refs.push_back(it->m_key);
+            m_refs.push_back(it->m_value);
+        }
+    }
+
+    if (m_ctx.get_params().unfold_rules() > 0) {
+        unsigned num_unfolds = m_ctx.get_params().unfold_rules();
+        datalog::rule_transformer transf1(m_ctx), transf2(m_ctx);        
+        transf1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+        transf2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
+        if (m_ctx.get_params().coalesce_rules()) {
+            m_ctx.transform_rules(transf1);
+        }
+        while (num_unfolds > 0) {
+            m_ctx.transform_rules(transf2);
+            --num_unfolds;
+        }
+    }
+
+    if (m_ctx.get_rules().get_output_predicates().empty()) {
+        m_context->set_unsat();
+        return l_false;
+    }
+
+    query_pred = m_ctx.get_rules().get_output_predicate();
+
+    IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););
+    m_pdr_rules.replace_rules(m_ctx.get_rules());
+    m_pdr_rules.close();
+    m_ctx.record_transformed_rules();
+    m_ctx.reopen();
+    m_ctx.replace_rules(old_rules);
+    
+    datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode.
+
+    m_context->set_proof_converter(m_ctx.get_proof_converter());
+    m_context->set_model_converter(m_ctx.get_model_converter());
+    m_context->set_query(query_pred);
+    m_context->set_axioms(bg_assertion);
+    m_context->update_rules(m_pdr_rules);
+    
+    if (m_pdr_rules.get_rules().empty()) {
+        m_context->set_unsat();
+        IF_VERBOSE(1, model_smt2_pp(verbose_stream(), m, *m_context->get_model(),0););
+        return l_false;
+    }
+        
+    return m_context->solve();
+
+}
+
+expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {
+    func_decl* pred = pred_orig;
+    m_pred2slice.find(pred_orig, pred);
+    SASSERT(pred);
+    return m_context->get_cover_delta(level, pred_orig, pred);
+}
+
+void dl_interface::add_cover(int level, func_decl* pred, expr* property) {
+    if (m_ctx.get_params().slice()) {
+        throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers");
+    }
+    m_context->add_cover(level, pred, property);
+}
+
+unsigned dl_interface::get_num_levels(func_decl* pred) {
+    m_pred2slice.find(pred, pred);
+    SASSERT(pred);
+    return m_context->get_num_levels(pred);
+}
+
+void dl_interface::collect_statistics(statistics& st) const {
+    m_context->collect_statistics(st);
+}
+
+void dl_interface::reset_statistics() {
+    m_context->reset_statistics();
+}
+
+void dl_interface::display_certificate(std::ostream& out) const {
+    m_context->display_certificate(out);
+}
+
+expr_ref dl_interface::get_answer() {
+    return m_context->get_answer();
+}
+
+void dl_interface::cancel() {
+    m_context->cancel();
+}
+
+void dl_interface::cleanup() {
+    m_context->cleanup();
+}
+
+void dl_interface::updt_params() {
+    dealloc(m_context);
+    m_context = alloc(pdr::context, m_ctx.get_fparams(), m_ctx.get_params(), m_ctx.get_manager());
+}
+
+model_ref dl_interface::get_model() {
+    return m_context->get_model();
+}
+
+proof_ref dl_interface::get_proof() {
+    return m_context->get_proof();
+}

src/muz/pdr/pdr_dl_interface.h

@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_dl_interface.h
+
+Abstract:
+
+    SMT2 interface for the datalog PDR
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-22.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_DL_INTERFACE_H_
+#define _PDR_DL_INTERFACE_H_
+
+#include "lbool.h"
+#include "dl_rule.h"
+#include "dl_rule_set.h"
+#include "dl_util.h"
+#include "dl_engine_base.h"
+#include "statistics.h"
+
+namespace datalog {
+    class context;
+}
+
+namespace pdr {
+
+    class context;
+
+    class dl_interface : public datalog::engine_base {
+        datalog::context& m_ctx;
+        datalog::rule_set m_pdr_rules;
+        datalog::rule_set m_old_rules;
+        context*          m_context;
+        obj_map<func_decl, func_decl*> m_pred2slice;
+        ast_ref_vector    m_refs;
+
+        void check_reset();
+
+    public:
+        dl_interface(datalog::context& ctx); 
+        ~dl_interface();
+        
+        virtual lbool query(expr* query);
+
+        virtual void cancel();
+
+        virtual void cleanup();
+
+        virtual void display_certificate(std::ostream& out) const;
+
+        virtual void collect_statistics(statistics& st) const;
+
+        virtual void reset_statistics();
+
+        virtual expr_ref get_answer();
+
+        virtual unsigned get_num_levels(func_decl* pred);
+
+        virtual expr_ref get_cover_delta(int level, func_decl* pred);
+       
+        virtual void add_cover(int level, func_decl* pred, expr* property);
+               
+        virtual void updt_params();
+
+        virtual model_ref get_model();
+
+        virtual proof_ref get_proof();
+        
+    };
+}
+
+
+#endif

src/muz/pdr/pdr_farkas_learner.cpp

@@ -0,0 +1,880 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_farkas_learner.cpp
+
+Abstract:
+
+    Proviced abstract interface and some inplementations of algorithms
+    for strenghtning lemmas
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-11-1.
+
+Revision History:
+
+--*/
+
+#include "ast_smt2_pp.h"
+#include "array_decl_plugin.h"
+#include "bool_rewriter.h"
+#include "dl_decl_plugin.h"
+#include "for_each_expr.h"
+#include "dl_util.h"
+#include "rewriter.h"
+#include "rewriter_def.h"
+#include "pdr_util.h"
+#include "pdr_farkas_learner.h"
+#include "th_rewriter.h"
+#include "ast_ll_pp.h"
+#include "arith_bounds_tactic.h"
+#include "proof_utils.h"
+#include "reg_decl_plugins.h"
+
+#define PROOF_MODE PGM_FINE
+//#define PROOF_MODE PGM_COARSE
+
+namespace pdr {
+
+    class farkas_learner::constr {
+
+        ast_manager&     m;
+        arith_util       a;
+        app_ref_vector   m_ineqs;
+        vector<rational> m_coeffs;
+
+        void mk_coerce(expr*& e1, expr*& e2) {
+            if (a.is_int(e1) && a.is_real(e2)) {
+                e1 = a.mk_to_real(e1);
+            }
+            else if (a.is_int(e2) && a.is_real(e1)) {
+                e2 = a.mk_to_real(e2);
+            }
+        }
+
+        app* mk_add(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_add(e1, e2);
+        }
+
+        app* mk_mul(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_mul(e1, e2);
+        }
+
+        app* mk_le(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_le(e1, e2);
+        }
+
+        app* mk_ge(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_ge(e1, e2);
+        }
+
+        app* mk_gt(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_gt(e1, e2);
+        }
+
+        app* mk_lt(expr* e1, expr* e2) {
+            mk_coerce(e1, e2);
+            return a.mk_lt(e1, e2);
+        }
+
+        void mul(rational const& c, expr* e, expr_ref& res) {
+            expr_ref tmp(m);
+            if (c.is_one()) {
+                tmp = e;
+            }
+            else {
+                tmp = mk_mul(a.mk_numeral(c, c.is_int() && a.is_int(e)), e);
+            }
+            res = mk_add(res, tmp);
+        }
+
+        bool is_int_sort(app* c) {
+            SASSERT(m.is_eq(c) || a.is_le(c) || a.is_lt(c) || a.is_gt(c) || a.is_ge(c));
+            SASSERT(a.is_int(c->get_arg(0)) || a.is_real(c->get_arg(0)));
+            return a.is_int(c->get_arg(0));
+        }
+
+        bool is_int_sort() {
+            SASSERT(!m_ineqs.empty());
+            return is_int_sort(m_ineqs[0].get());
+        }
+
+        void normalize_coeffs() {
+            rational l(1);
+            for (unsigned i = 0; i < m_coeffs.size(); ++i) {
+                l = lcm(l, denominator(m_coeffs[i]));
+            }
+            if (!l.is_one()) {
+                for (unsigned i = 0; i < m_coeffs.size(); ++i) {
+                    m_coeffs[i] *= l;
+                }
+            }
+        }
+
+        app* mk_one() {
+            return a.mk_numeral(rational(1), true);
+        }
+
+        app* fix_sign(bool is_pos, app* c) {
+            expr* x, *y;
+            SASSERT(m.is_eq(c) || a.is_le(c) || a.is_lt(c) || a.is_gt(c) || a.is_ge(c));
+            bool is_int = is_int_sort(c);
+            if (is_int && is_pos && (a.is_lt(c, x, y) || a.is_gt(c, y, x))) {
+                return mk_le(mk_add(x, mk_one()), y);
+            }
+            if (is_int && !is_pos && (a.is_le(c, x, y) || a.is_ge(c, y, x))) {
+                // !(x <= y) <=> x > y <=> x >= y + 1
+                return mk_ge(x, mk_add(y, mk_one()));
+            }
+            if (is_pos) {
+                return c;
+            }
+            if (a.is_le(c, x, y)) return mk_gt(x, y);
+            if (a.is_lt(c, x, y)) return mk_ge(x, y);
+            if (a.is_ge(c, x, y)) return mk_lt(x, y);
+            if (a.is_gt(c, x, y)) return mk_le(x, y);
+            UNREACHABLE();
+            return c;
+        }
+        
+    public:
+        constr(ast_manager& m) : m(m), a(m), m_ineqs(m) {}
+
+        /** add a multiple of constraint c to the current constr */
+        void add(rational const & coef, app * c) {
+            bool is_pos = true;
+            expr* e;
+            while (m.is_not(c, e)) {
+                is_pos = !is_pos;
+                c = to_app(e);
+            }
+
+            if (!coef.is_zero() && !m.is_true(c)) {
+                m_coeffs.push_back(coef);                
+                m_ineqs.push_back(fix_sign(is_pos, c));                
+            }
+        }
+
+        //
+        // Extract the complement of premises multiplied by Farkas coefficients.
+        //
+        void get(expr_ref& res) {
+            if (m_coeffs.empty()) {
+                res = m.mk_false();
+                return;
+            }
+            bool is_int = is_int_sort();
+            if (is_int) {                
+                normalize_coeffs();
+            }
+            TRACE("pdr", 
+                  for (unsigned i = 0; i < m_coeffs.size(); ++i) {
+                      tout << m_coeffs[i] << ": " << mk_pp(m_ineqs[i].get(), m) << "\n";
+                  }
+                  );
+            app_ref zero(a.mk_numeral(rational::zero(), is_int), m);
+            res = zero;
+            bool is_strict = false;
+            bool is_eq     = true;
+            expr* x, *y;
+            for (unsigned i = 0; i < m_coeffs.size(); ++i) {
+                app* c = m_ineqs[i].get();
+                if (m.is_eq(c, x, y)) {
+                    mul(m_coeffs[i],  x, res);
+                    mul(-m_coeffs[i], y, res);
+                }
+                if (a.is_lt(c, x, y) || a.is_gt(c, y, x)) {
+                    mul(m_coeffs[i],  x, res);
+                    mul(-m_coeffs[i], y, res);
+                    is_strict = true;
+                    is_eq = false;
+                }
+                if (a.is_le(c, x, y) || a.is_ge(c, y, x)) {
+                    mul(m_coeffs[i],  x, res);
+                    mul(-m_coeffs[i], y, res);
+                    is_eq = false;
+                }
+            }
+
+            zero = a.mk_numeral(rational::zero(), a.is_int(res));
+            if (is_eq) {
+                res = m.mk_eq(res, zero);
+            }
+            else if (is_strict) {
+                res = mk_lt(res, zero);
+            }
+            else {
+                res = mk_le(res, zero);
+            }            
+            res = m.mk_not(res);
+            th_rewriter rw(m);
+            params_ref params;
+            params.set_bool("gcd_rounding", true);
+            rw.updt_params(params);
+            proof_ref pr(m);
+            expr_ref tmp(m);
+            rw(res, tmp, pr);
+            fix_dl(tmp);
+            res = tmp;
+        }
+
+        // patch: swap addends to make static 
+        // features recognize difference constraint.
+        void fix_dl(expr_ref& r) {
+            expr* e;
+            if (m.is_not(r, e)) {
+                r = e;
+                fix_dl(r);
+                r = m.mk_not(r);
+                return;
+            }
+            expr* e1, *e2, *e3, *e4;
+            if ((m.is_eq(r, e1, e2) || a.is_lt(r, e1, e2) || a.is_gt(r, e1, e2) || 
+                 a.is_le(r, e1, e2) || a.is_ge(r, e1, e2))) {
+                if (a.is_add(e1, e3, e4) && a.is_mul(e3)) {
+                    r = m.mk_app(to_app(r)->get_decl(), a.mk_add(e4,e3), e2);
+                }
+            }
+        }
+    };
+    
+    farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr) 
+        : m_proof_params(get_proof_params(params)), 
+          m_pr(PROOF_MODE),
+          m_combine_farkas_coefficients(true),
+          p2o(m_pr, outer_mgr),
+          o2p(outer_mgr, m_pr)
+    {
+        reg_decl_plugins(m_pr);
+        m_ctx = alloc(smt::kernel, m_pr, m_proof_params);
+    }
+
+    smt_params farkas_learner::get_proof_params(smt_params& orig_params) {
+        smt_params res(orig_params);
+        res.m_arith_bound_prop = BP_NONE;
+        // temp hack to fix the build
+        // res.m_conflict_resolution_strategy = CR_ALL_DECIDED;
+        res.m_arith_auto_config_simplex = true;
+        res.m_arith_propagate_eqs = false;
+        res.m_arith_eager_eq_axioms = false;
+        res.m_arith_eq_bounds = false;
+        return res;
+    }
+
+    class farkas_learner::equality_expander_cfg : public default_rewriter_cfg
+    {
+        ast_manager& m;
+        arith_util   m_ar;
+    public:
+        equality_expander_cfg(ast_manager& m) : m(m), m_ar(m) {}
+
+        bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+            expr * x, *y;
+            if (m.is_eq(s, x, y) && (m_ar.is_int(x) || m_ar.is_real(x))) {
+                t = m.mk_and(m_ar.mk_ge(x, y), m_ar.mk_le(x, y));
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+    };
+
+    class collect_pure_proc {
+        func_decl_set& m_symbs;
+    public:
+        collect_pure_proc(func_decl_set& s):m_symbs(s) {}
+
+        void operator()(app* a) {
+            if (a->get_family_id() == null_family_id) {
+                m_symbs.insert(a->get_decl());
+            }
+        }
+        void operator()(var*) {}
+        void operator()(quantifier*) {}
+    };
+
+
+    bool farkas_learner::get_lemma_guesses(expr * A_ext, expr * B_ext, expr_ref_vector& lemmas)
+    {
+        expr_ref A(o2p(A_ext), m_pr);
+        expr_ref B(o2p(B_ext), m_pr);
+        proof_ref pr(m_pr);
+        expr_ref tmp(m_pr);
+        expr_ref_vector ilemmas(m_pr);
+        equality_expander_cfg ee_rwr_cfg(m_pr);
+        rewriter_tpl<equality_expander_cfg> ee_rwr(m_pr, false, ee_rwr_cfg);
+
+        lemmas.reset();
+
+        ee_rwr(A, A);
+        ee_rwr(B, B);
+
+        expr_set bs;
+        expr_ref_vector blist(m_pr);
+        qe::flatten_and(B, blist);
+        for (unsigned i = 0; i < blist.size(); ++i) {
+            bs.insert(blist[i].get());
+        }
+
+
+        if (!m_ctx) {
+            m_ctx = alloc(smt::kernel, m_pr, m_proof_params);
+        }
+
+        m_ctx->push();
+        m_ctx->assert_expr(A);
+        expr_set::iterator it = bs.begin(), end = bs.end();
+        for (; it != end; ++it) {
+            m_ctx->assert_expr(*it);
+        }
+        lbool res = m_ctx->check();
+        bool is_unsat = res == l_false;
+        if (is_unsat) {
+            pr = m_ctx->get_proof();
+            get_lemmas(m_ctx->get_proof(), bs, ilemmas);
+            for (unsigned i = 0; i < ilemmas.size(); ++i) {
+                lemmas.push_back(p2o(ilemmas[i].get()));
+            }
+        }
+        m_ctx->pop(1);
+
+        IF_VERBOSE(3, {
+                for (unsigned i = 0; i < ilemmas.size(); ++i) {
+                    verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n";
+                }
+            });
+
+        TRACE("farkas_learner",
+              tout << (is_unsat?"unsat":"sat") << "\n";
+              tout << "A: " << mk_pp(A_ext, m_ctx->m()) << "\n";
+              tout << "B: " << mk_pp(B_ext, m_ctx->m()) << "\n";
+              for (unsigned i = 0; i < lemmas.size(); ++i) {
+                  tout << "B': " << mk_pp(ilemmas[i].get(), m_pr) << "\n";
+              });
+        DEBUG_CODE(
+            if (is_unsat) {
+                m_ctx->push();
+                m_ctx->assert_expr(A);
+                for (unsigned i = 0; i < ilemmas.size(); ++i) {
+                    m_ctx->assert_expr(ilemmas[i].get());
+                }
+                lbool res2 = m_ctx->check();
+                SASSERT(l_false == res2);
+                m_ctx->pop(1);
+            }
+            );
+        return is_unsat;
+    }
+
+    //
+    // Perform simple subsumption check of lemmas.
+    //
+    void farkas_learner::simplify_lemmas(expr_ref_vector& lemmas) {
+        ast_manager& m = lemmas.get_manager();
+        goal_ref g(alloc(goal, m, false, false, false));
+        TRACE("farkas_simplify_lemmas",            
+              for (unsigned i = 0; i < lemmas.size(); ++i) {
+                  tout << mk_pp(lemmas[i].get(), m) << "\n";
+              });
+
+        for (unsigned i = 0; i < lemmas.size(); ++i) {
+            g->assert_expr(lemmas[i].get()); 
+        }
+        expr_ref tmp(m);
+        model_converter_ref mc;
+        proof_converter_ref pc;
+        expr_dependency_ref core(m);
+        goal_ref_buffer result;
+        tactic_ref simplifier = mk_arith_bounds_tactic(m);
+        (*simplifier)(g, result, mc, pc, core);
+        lemmas.reset();
+        SASSERT(result.size() == 1);
+        goal* r = result[0];
+        for (unsigned i = 0; i < r->size(); ++i) {
+            lemmas.push_back(r->form(i));
+        }
+        TRACE("farkas_simplify_lemmas", 
+              tout << "simplified:\n";           
+              for (unsigned i = 0; i < lemmas.size(); ++i) {
+                  tout << mk_pp(lemmas[i].get(), m) << "\n";
+              });
+    }
+
+
+    void farkas_learner::combine_constraints(unsigned n, app * const * lits, rational const * coeffs, expr_ref& res)
+    {
+        ast_manager& m = res.get_manager();
+        if (m_combine_farkas_coefficients) {
+            constr res_c(m);
+            for(unsigned i = 0; i < n; ++i) {
+                res_c.add(coeffs[i], lits[i]);
+            }
+            res_c.get(res);
+        }
+        else {
+            bool_rewriter rw(m);
+            rw.mk_or(n, (expr*const*)(lits), res);
+        }
+    }
+
+    class farkas_learner::constant_replacer_cfg : public default_rewriter_cfg
+    {
+        const obj_map<expr, expr *>& m_translation;
+    public:
+        constant_replacer_cfg(const obj_map<expr, expr *>& translation)
+            : m_translation(translation)
+        { }
+
+        bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+            return m_translation.find(s, t);
+        }
+    };
+
+    // every uninterpreted symbol is in symbs
+    class is_pure_expr_proc {
+        func_decl_set const& m_symbs;
+    public:
+        struct non_pure {};
+
+        is_pure_expr_proc(func_decl_set const& s):m_symbs(s) {}
+
+        void operator()(app* a) {
+            if (a->get_family_id() == null_family_id) {
+                if (!m_symbs.contains(a->get_decl())) {
+                    throw non_pure();
+                }
+            }
+        }
+        void operator()(var*) {}
+        void operator()(quantifier*) {}
+    };
+
+    bool farkas_learner::is_pure_expr(func_decl_set const& symbs, expr* e) const {
+        is_pure_expr_proc proc(symbs);
+        try {
+            for_each_expr(proc, e);
+        }
+        catch (is_pure_expr_proc::non_pure) {
+            return false;
+        }
+        return true;
+    };
+
+
+    /**
+       Revised version of Farkas strengthener.
+       1. Mark B-pure nodes as derivations that depend only on B.
+       2. Collect B-influenced nodes
+       3. (optional) Permute B-pure units over resolution steps to narrow dependencies on B.
+       4. Weaken B-pure units for resolution with Farkas Clauses.
+       5. Add B-pure units elsewhere.
+
+       Rules:
+       - hypothesis h |- h
+
+                    H |- false
+       - lemma      ----------
+                     |- not H
+
+                    Th |- L \/ C   H |- not L
+       - th-lemma   -------------------------
+                           H  |- C
+
+         Note: C is false for theory axioms, C is unit literal for propagation.
+
+       - rewrite        |- t = s
+
+                        H |- t = s
+       - monotonicity   ----------------
+                       H |- f(t) = f(s)
+
+                        H |- t = s H' |- s = u
+       - trans          ----------------------
+                            H, H' |- t = u
+
+                        H |- C \/ L  H' |- not L
+       - unit_resolve   ------------------------
+                                H, H' |- C
+
+                        H |- a ~ b   H' |- a
+       - mp             --------------------
+                             H, H' |- b
+
+       - def-axiom       |- C
+       
+       - asserted        |- f
+
+       Mark nodes by:
+          - Hypotheses
+          - Dependency on bs
+          - Dependency on A
+
+       A node is unit derivable from bs if:
+          - It has no hypotheses.
+          - It depends on bs.
+          - It does not depend on A.
+
+       NB: currently unit derivable is not symmetric: A clause can be 
+       unit derivable, but a unit literal with hypotheses is not.
+       This is clearly wrong, because hypotheses are just additional literals
+       in a clausal version.
+
+       NB: the routine is not interpolating, though an interpolating variant would 
+       be preferrable because then we can also use it for model propagation.
+
+       We collect the unit derivable nodes from bs.
+       These are the weakenings of bs, besides the 
+       units under Farkas.
+                    
+    */
+
+#define INSERT(_x_) if (!lemma_set.contains(_x_)) { lemma_set.insert(_x_); lemmas.push_back(_x_); }
+
+    void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas) {
+        ast_manager& m = lemmas.get_manager();
+        bool_rewriter brwr(m);
+        func_decl_set Bsymbs;
+        collect_pure_proc collect_proc(Bsymbs);
+        expr_set::iterator it = bs.begin(), end = bs.end();
+        for (; it != end; ++it) {
+            for_each_expr(collect_proc, *it);
+        }
+
+        proof_ref pr(root, m);
+        proof_utils::reduce_hypotheses(pr);
+        proof_utils::permute_unit_resolution(pr);
+        IF_VERBOSE(3, verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";);
+        
+        ptr_vector<expr_set> hyprefs;
+        obj_map<expr, expr_set*> hypmap;
+        obj_hashtable<expr> lemma_set;
+        ast_mark b_depend, a_depend, visited, b_closed;
+        expr_set* empty_set = alloc(expr_set);
+        hyprefs.push_back(empty_set); 
+        ptr_vector<proof> todo;
+        TRACE("pdr_verbose", tout << mk_pp(pr, m) << "\n";);
+        todo.push_back(pr);
+        while (!todo.empty()) {
+            proof* p = todo.back();
+            SASSERT(m.is_proof(p));
+            if (visited.is_marked(p)) {
+                todo.pop_back();
+                continue;
+            }
+            bool all_visit = true;
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                expr* arg = p->get_arg(i);
+                SASSERT(m.is_proof(arg));
+                if (!visited.is_marked(arg)) {
+                    all_visit = false;
+                    todo.push_back(to_app(arg));
+                }
+            }
+            if (!all_visit) {
+                continue;
+            }
+            visited.mark(p, true);
+            todo.pop_back();
+
+            // retrieve hypotheses and dependencies on A, bs.
+            bool b_dep = false, a_dep = false;
+            expr_set* hyps = empty_set;
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                expr* arg = p->get_arg(i);
+                a_dep = a_dep || a_depend.is_marked(arg);
+                b_dep = b_dep || b_depend.is_marked(arg);
+                expr_set* hyps2 = hypmap.find(arg);
+                if (hyps != hyps2 && !hyps2->empty()) {
+                    if (hyps->empty()) {
+                        hyps = hyps2;
+                    }
+                    else {
+                        expr_set* hyps3 = alloc(expr_set);
+                        datalog::set_union(*hyps3, *hyps);
+                        datalog::set_union(*hyps3, *hyps2);
+                        hyps = hyps3;
+                        hyprefs.push_back(hyps);
+                    }
+                }
+            }
+            hypmap.insert(p, hyps);
+            a_depend.mark(p, a_dep);
+            b_depend.mark(p, b_dep);
+
+#define IS_B_PURE(_p) (b_depend.is_marked(_p) && !a_depend.is_marked(_p) && hypmap.find(_p)->empty())
+
+
+            // Add lemmas that depend on bs, have no hypotheses, don't depend on A.
+            if ((!hyps->empty() || a_depend.is_marked(p)) && 
+                b_depend.is_marked(p) && !is_farkas_lemma(m, p)) {
+                for (unsigned i = 0; i < m.get_num_parents(p); ++i) {                
+                    app* arg = to_app(p->get_arg(i));
+                    if (IS_B_PURE(arg)) {
+                        expr* fact = m.get_fact(arg);
+                        if (is_pure_expr(Bsymbs, fact)) {
+                            TRACE("farkas_learner", 
+                                  tout << "Add: " << mk_pp(m.get_fact(arg), m) << "\n";
+                                  tout << mk_pp(arg, m) << "\n";
+                                  );
+                            INSERT(fact);
+                        }
+                        else {
+                            get_asserted(p, bs, b_closed, lemma_set, lemmas);
+                            b_closed.mark(p, true);
+                        }
+                    }
+                }
+            }
+            
+            switch(p->get_decl_kind()) {
+            case PR_ASSERTED:
+                if (bs.contains(m.get_fact(p))) {
+                    b_depend.mark(p, true);
+                }
+                else {
+                    a_depend.mark(p, true);
+                }
+                break;
+            case PR_HYPOTHESIS: {
+                SASSERT(hyps == empty_set);
+                hyps = alloc(expr_set);
+                hyps->insert(m.get_fact(p));
+                hyprefs.push_back(hyps);
+                hypmap.insert(p, hyps);
+                break;
+            }
+            case PR_DEF_AXIOM: {
+                if (!is_pure_expr(Bsymbs, m.get_fact(p))) {
+                    a_depend.mark(p, true);
+                }
+                break;
+            }
+            case PR_LEMMA: {
+                expr_set* hyps2 = alloc(expr_set);
+                hyprefs.push_back(hyps2);
+                datalog::set_union(*hyps2, *hyps); 
+                hyps = hyps2;
+                expr* fml = m.get_fact(p);
+                hyps->remove(fml);
+                if (m.is_or(fml)) {
+                    for (unsigned i = 0; i < to_app(fml)->get_num_args(); ++i) {
+                        expr* f = to_app(fml)->get_arg(i);
+                        expr_ref hyp(m);
+                        brwr.mk_not(f, hyp);
+                        hyps->remove(hyp);
+                    }
+                }
+                hypmap.insert(p, hyps);
+                break;
+            }
+            case PR_TH_LEMMA: {
+                if (!is_farkas_lemma(m, p)) break;
+               
+                SASSERT(m.has_fact(p));
+                unsigned prem_cnt = m.get_num_parents(p);
+                func_decl * d = p->get_decl();
+                SASSERT(d->get_num_parameters() >= prem_cnt+2);
+                SASSERT(d->get_parameter(0).get_symbol() == "arith");
+                SASSERT(d->get_parameter(1).get_symbol() == "farkas");
+                parameter const* params = d->get_parameters() + 2;
+
+                app_ref_vector lits(m);
+                expr_ref tmp(m);
+                unsigned num_b_pures = 0;
+                rational coef;
+                vector<rational> coeffs;
+
+                TRACE("farkas_learner", 
+                        for (unsigned i = 0; i < prem_cnt; ++i) {
+                            VERIFY(params[i].is_rational(coef));
+                            proof* prem = to_app(p->get_arg(i));
+                            bool b_pure = IS_B_PURE(prem);
+                            tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n";
+                        }
+                        tout << mk_pp(m.get_fact(p), m) << "\n";
+                      );
+
+                // NB. Taking 'abs' of coefficients is a workaround.
+                // The Farkas coefficient extraction in arith_core must be wrong.
+                // The coefficients would be always positive relative to the theory lemma.
+
+                for(unsigned i = 0; i < prem_cnt; ++i) {                    
+                    expr * prem_e = p->get_arg(i);
+                    SASSERT(is_app(prem_e));
+                    proof * prem = to_app(prem_e);
+                   
+                    if(IS_B_PURE(prem)) {
+                        ++num_b_pures;
+                    }
+                    else {
+                        VERIFY(params[i].is_rational(coef));
+                        lits.push_back(to_app(m.get_fact(prem)));
+                        coeffs.push_back(abs(coef));
+                    }
+                }
+                params += prem_cnt;
+                if (prem_cnt + 2 < d->get_num_parameters()) {
+                    unsigned num_args = 1;
+                    expr* fact = m.get_fact(p);
+                    expr* const* args = &fact;
+                    if (m.is_or(fact)) {
+                        app* _or = to_app(fact);
+                        num_args = _or->get_num_args();
+                        args = _or->get_args();                        
+                    }
+                    SASSERT(prem_cnt + 2 + num_args == d->get_num_parameters());
+                    for (unsigned i = 0; i < num_args; ++i) {
+                        expr* prem_e = args[i];
+                        brwr.mk_not(prem_e, tmp);
+                        VERIFY(params[i].is_rational(coef));
+                        SASSERT(is_app(tmp));
+                        lits.push_back(to_app(tmp));
+                        coeffs.push_back(abs(coef));
+                    }
+
+                }
+                SASSERT(coeffs.size() == lits.size());
+                if (num_b_pures > 0) {
+                    expr_ref res(m);
+                    combine_constraints(coeffs.size(), lits.c_ptr(), coeffs.c_ptr(), res);
+                    TRACE("farkas_learner", tout << "Add: " << mk_pp(res, m) << "\n";);
+                    INSERT(res);
+                    b_closed.mark(p, true);
+                }
+            }
+            default:
+                break;
+            }
+        }
+
+        std::for_each(hyprefs.begin(), hyprefs.end(), delete_proc<expr_set>());
+        simplify_lemmas(lemmas);
+    }
+
+    void farkas_learner::get_consequences(proof* root, expr_set const& bs, expr_ref_vector& consequences) {
+        TRACE("farkas_learner", tout << "get consequences\n";);
+        m_combine_farkas_coefficients = false;
+        get_lemmas(root, bs, consequences);
+        m_combine_farkas_coefficients = true;
+    }
+
+    void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas) {
+        ast_manager& m = lemmas.get_manager();
+        ast_mark visited;
+        proof* p0 = p;
+        ptr_vector<proof> todo;        
+        todo.push_back(p);
+                      
+        while (!todo.empty()) {
+            p = todo.back();
+            todo.pop_back();
+            if (visited.is_marked(p) || b_closed.is_marked(p)) {
+                continue;
+            }
+            visited.mark(p, true);
+            for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+                expr* arg = p->get_arg(i);
+                SASSERT(m.is_proof(arg));
+                todo.push_back(to_app(arg));
+            }
+            if (p->get_decl_kind() == PR_ASSERTED &&
+                bs.contains(m.get_fact(p))) {
+                expr* fact = m.get_fact(p);
+                TRACE("farkas_learner", 
+                      tout << mk_ll_pp(p0,m) << "\n";
+                      tout << "Add: " << mk_pp(p,m) << "\n";);
+                INSERT(fact);
+                b_closed.mark(p, true);
+            }
+        }
+    }
+
+
+    bool farkas_learner::is_farkas_lemma(ast_manager& m, expr* e) {
+        app * a;
+        func_decl* d;
+        symbol sym;
+        return 
+            is_app(e) && 
+            (a = to_app(e), d = a->get_decl(), true) &&
+            PR_TH_LEMMA == a->get_decl_kind() &&
+            d->get_num_parameters() >= 2 &&
+            d->get_parameter(0).is_symbol(sym) && sym == "arith" &&
+            d->get_parameter(1).is_symbol(sym) && sym == "farkas" &&
+            d->get_num_parameters() >= m.get_num_parents(to_app(e)) + 2;
+    };
+
+
+    void farkas_learner::test()  {
+        smt_params params;
+        enable_trace("farkas_learner");
+               
+        bool res;
+        ast_manager m;
+        reg_decl_plugins(m);        
+        arith_util a(m);
+        pdr::farkas_learner fl(params, m);
+        expr_ref_vector lemmas(m);
+        
+        sort_ref int_s(a.mk_int(), m);
+        expr_ref x(m.mk_const(symbol("x"), int_s), m);
+        expr_ref y(m.mk_const(symbol("y"), int_s), m);
+        expr_ref z(m.mk_const(symbol("z"), int_s), m);    
+        expr_ref u(m.mk_const(symbol("u"), int_s), m);  
+        expr_ref v(m.mk_const(symbol("v"), int_s), m);
+
+        // A: x > y >= z
+        // B: x < z
+        // Farkas: x <= z
+        expr_ref A(m.mk_and(a.mk_gt(x,y), a.mk_ge(y,z)),m);        
+        expr_ref B(a.mk_gt(z,x),m);        
+        res = fl.get_lemma_guesses(A, B, lemmas);        
+        std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n";
+
+        // A: x > y >= z + 2
+        // B: x = 1, z = 8
+        // Farkas: x <= z + 2
+        expr_ref one(a.mk_numeral(rational(1), true), m);
+        expr_ref two(a.mk_numeral(rational(2), true), m);
+        expr_ref eight(a.mk_numeral(rational(8), true), m);
+        A = m.mk_and(a.mk_gt(x,y),a.mk_ge(y,a.mk_add(z,two)));
+        B = m.mk_and(m.mk_eq(x,one), m.mk_eq(z, eight));
+        res = fl.get_lemma_guesses(A, B, lemmas);        
+        std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n";
+
+        // A: x > y >= z \/ x >= u > z
+        // B: z > x + 1
+        // Farkas: z >= x
+        A = m.mk_or(m.mk_and(a.mk_gt(x,y),a.mk_ge(y,z)),m.mk_and(a.mk_ge(x,u),a.mk_gt(u,z)));
+        B = a.mk_gt(z, a.mk_add(x,one));
+        res = fl.get_lemma_guesses(A, B, lemmas);        
+        std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n";
+
+        // A: (x > y >= z \/ x >= u > z \/ u > v)
+        // B: z > x + 1 & not (u > v)
+        // Farkas: z >= x & not (u > v)
+        A = m.mk_or(m.mk_and(a.mk_gt(x,y),a.mk_ge(y,z)),m.mk_and(a.mk_ge(x,u),a.mk_gt(u,z)), a.mk_gt(u, v));
+        B = m.mk_and(a.mk_gt(z, a.mk_add(x,one)), m.mk_not(a.mk_gt(u, v)));
+        res = fl.get_lemma_guesses(A, B, lemmas);        
+        std::cout << "\nres: " << res << "\nlemmas: " << pp_cube(lemmas, m) << "\n";
+        
+    }
+
+    void farkas_learner::collect_statistics(statistics& st) const {
+        if (m_ctx) {
+            m_ctx->collect_statistics(st);
+        }
+    }
+
+
+};
+

src/muz/pdr/pdr_farkas_learner.h

@@ -0,0 +1,125 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_farkas_learner.h
+
+Abstract:
+
+    SMT2 interface for the datalog PDR
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-11-1.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_FARKAS_LEARNER_H_
+#define _PDR_FARKAS_LEARNER_H_
+
+#include "arith_decl_plugin.h"
+#include "ast_translation.h"
+#include "bv_decl_plugin.h"
+#include "smt_kernel.h"
+#include "bool_rewriter.h"
+#include "pdr_util.h"
+#include "smt_params.h"
+#include "tactic.h"
+
+namespace pdr {
+
+class farkas_learner {
+    class farkas_collector;
+    class constant_replacer_cfg;
+    class equality_expander_cfg;
+    class constr;
+
+    typedef obj_hashtable<expr> expr_set;
+
+    smt_params               m_proof_params;
+    ast_manager              m_pr;
+    scoped_ptr<smt::kernel>  m_ctx;
+
+    // 
+    // true:  produce a combined constraint by applying Farkas coefficients.
+    // false: produce a conjunction of the negated literals from the theory lemmas.
+    //
+    bool                     m_combine_farkas_coefficients; 
+
+
+    static smt_params get_proof_params(smt_params& orig_params);
+
+    //
+    // all ast objects passed to private functions have m_proof_mgs as their ast_manager
+    //
+
+    ast_translation p2o;       /** Translate expression from inner ast_manager to outer one */
+    ast_translation o2p;       /** Translate expression from outer ast_manager to inner one */
+
+
+    /** All ast opbjects here are in the m_proof_mgs */
+    void get_lemma_guesses_internal(proof * p, expr* A, expr * B, expr_ref_vector& lemmas);
+
+    bool farkas2lemma(proof * fstep, expr* A, expr * B, expr_ref& res);
+
+    void combine_constraints(unsigned cnt, app * const * constrs, rational const * coeffs, expr_ref& res);
+
+    bool try_ensure_lemma_in_language(expr_ref& lemma, expr* A, const func_decl_set& lang);
+
+    bool is_farkas_lemma(ast_manager& m, expr* e);
+   
+    void get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas);
+
+    bool is_pure_expr(func_decl_set const& symbs, expr* e) const;
+
+    static void test();
+
+public:
+    farkas_learner(smt_params& params, ast_manager& m);
+
+    /**
+       All ast objects have the ast_manager which was passed as 
+       an argument to the constructor (i.e. m_outer_mgr)
+       
+       B is a conjunction of literals.
+       A && B is unsat, equivalently A => ~B is valid
+       Find a weakened B' such that
+       A && B' is unsat and B' uses vocabulary (and constants) in common with A.
+       return lemmas to weaken B.     
+    */
+
+    bool get_lemma_guesses(expr * A, expr * B, expr_ref_vector& lemmas);
+
+    /**
+        Traverse a proof and retrieve lemmas using the vocabulary from bs.
+    */
+    void get_lemmas(proof* root, expr_set const& bs, expr_ref_vector& lemmas);
+
+    /**
+       Traverse a proof and retrieve consequences of A that are used to establish ~B.
+       The assumption is that:
+
+          A => \/ ~consequences[i]  and  \/ ~consequences[i] => ~B
+
+       e.g., the second implication can be rewritten as:
+
+          B => /\ consequences[i]
+     */
+    void get_consequences(proof* root, expr_set const& bs, expr_ref_vector& consequences);
+
+    /**
+       \brief Simplify lemmas using subsumption.
+     */
+    void simplify_lemmas(expr_ref_vector& lemmas);
+
+    void collect_statistics(statistics& st) const;
+
+};
+
+
+}
+
+#endif

src/muz/pdr/pdr_generalizers.h

@@ -0,0 +1,118 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_generalizers.h
+
+Abstract:
+
+    Generalizer plugins.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-11-22.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_GENERALIZERS_H_
+#define _PDR_GENERALIZERS_H_
+
+#include "pdr_context.h"
+#include "arith_decl_plugin.h"
+
+namespace pdr {
+
+    class core_bool_inductive_generalizer : public core_generalizer {
+        unsigned m_failure_limit;
+    public:
+        core_bool_inductive_generalizer(context& ctx, unsigned failure_limit) : core_generalizer(ctx), m_failure_limit(failure_limit) {}
+        virtual ~core_bool_inductive_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };
+
+    template <typename T>
+    class r_map : public map<rational, T, rational::hash_proc, rational::eq_proc> {
+    };
+
+    class core_arith_inductive_generalizer : public core_generalizer {
+        typedef std::pair<expr*, unsigned> term_loc_t;
+        typedef r_map<vector<term_loc_t> > bounds_t;
+
+        ast_manager&    m;
+        arith_util      a;
+        expr_ref_vector m_refs;
+        bounds_t        m_lb;
+        bounds_t        m_ub;
+
+        struct eq {
+            expr*    m_term;
+            rational m_value;
+            unsigned m_i;
+            unsigned m_j;
+            eq(expr* t, rational const& r, unsigned i, unsigned j): m_term(t), m_value(r), m_i(i), m_j(j) {}
+        };
+        void reset();
+        void insert_bound(bool is_lower, expr* x, rational const& r, unsigned i);
+        void get_eqs(expr_ref_vector const& core, svector<eq>& eqs);
+        bool substitute_alias(rational const&r, expr* x, expr* e, expr_ref& result);
+    public:
+        core_arith_inductive_generalizer(context& ctx);
+        virtual ~core_arith_inductive_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };
+
+    class core_farkas_generalizer : public core_generalizer {
+        farkas_learner m_farkas_learner;
+    public:
+        core_farkas_generalizer(context& ctx, ast_manager& m, smt_params& p);
+        virtual ~core_farkas_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);  
+        virtual void collect_statistics(statistics& st) const;
+    };
+
+    class core_convex_hull_generalizer : public core_generalizer {
+        ast_manager&    m;
+        arith_util      a;
+        expr_ref_vector m_sigma;
+        expr_ref_vector m_trail;
+        vector<obj_map<func_decl, expr*> > m_vars;
+        obj_map<expr, expr*> m_models;
+        bool m_is_closure;
+        expr_ref mk_closure(expr* e);
+        bool mk_closure(expr_ref_vector& conj);
+        bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv);
+        void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv);
+        bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result);
+        bool translate(func_decl* fn, unsigned index, expr_ref& result);
+        void method1(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
+        void method2(model_node& n, expr_ref_vector& core, bool& uses_level);
+        void method3(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
+        void add_variables(model_node& n, unsigned num_vars, expr_ref_vector& fmls);
+    public:
+        core_convex_hull_generalizer(context& ctx, bool is_closure);
+        virtual ~core_convex_hull_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };	
+
+    class core_multi_generalizer : public core_generalizer {
+        core_bool_inductive_generalizer m_gen;
+    public:
+        core_multi_generalizer(context& ctx, unsigned max_failures): core_generalizer(ctx), m_gen(ctx, max_failures) {}
+        virtual ~core_multi_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
+    };
+
+    class core_induction_generalizer : public core_generalizer {
+        class imp;
+    public:
+        core_induction_generalizer(context& ctx): core_generalizer(ctx) {}
+        virtual ~core_induction_generalizer() {}
+        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+    };
+};
+#endif

src/muz/pdr/pdr_manager.cpp

@@ -0,0 +1,328 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_manager.cpp
+
+Abstract:
+
+    A manager class for PDR, taking care of creating of AST 
+    objects and conversions between them.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-8-25.
+
+Revision History:
+
+--*/
+
+#include <sstream>
+#include "pdr_manager.h"
+#include "ast_smt2_pp.h"
+#include "for_each_expr.h"
+#include "has_free_vars.h"
+#include "expr_replacer.h"
+#include "expr_abstract.h"
+#include "model2expr.h"
+#include "model_smt2_pp.h"
+#include "model_converter.h"
+
+namespace pdr {
+
+    class collect_decls_proc {
+        func_decl_set& m_bound_decls;
+        func_decl_set& m_aux_decls;
+    public:
+        collect_decls_proc(func_decl_set& bound_decls, func_decl_set& aux_decls):
+            m_bound_decls(bound_decls),
+            m_aux_decls(aux_decls) {
+        }
+        
+        void operator()(app* a) {
+            if (a->get_family_id() == null_family_id) {
+                func_decl* f = a->get_decl();
+                if (!m_bound_decls.contains(f)) {
+                    m_aux_decls.insert(f);
+                }
+            }
+        }
+        void operator()(var* v) {}
+        void operator()(quantifier* q) {}
+    };
+
+    typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
+
+    expr_ref inductive_property::fixup_clause(expr* fml) const {        
+        expr_ref_vector disjs(m);
+        qe::flatten_or(fml, disjs);
+        expr_ref result(m);
+        bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result);
+        return result;
+    }
+
+    expr_ref inductive_property::fixup_clauses(expr* fml) const {
+        expr_ref_vector conjs(m);
+        expr_ref result(m);
+        qe::flatten_and(fml, conjs);
+        for (unsigned i = 0; i < conjs.size(); ++i) {
+            conjs[i] = fixup_clause(conjs[i].get());
+        }
+        bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result);
+        return result;
+    }
+
+    std::string inductive_property::to_string() const {
+        std::stringstream stm;
+        model_ref md;
+        expr_ref result(m);
+        to_model(md);
+        model_smt2_pp(stm, m, *md.get(), 0); 
+        return stm.str();
+    }
+
+    void inductive_property::to_model(model_ref& md) const {
+        md = alloc(model, m);
+        vector<relation_info> const& rs = m_relation_info;
+        expr_ref_vector conjs(m);
+        for (unsigned i = 0; i < rs.size(); ++i) {
+            relation_info ri(rs[i]);
+            func_decl * pred = ri.m_pred;
+            expr_ref prop = fixup_clauses(ri.m_body);
+            func_decl_ref_vector const& sig = ri.m_vars;
+            expr_ref q(m);
+            expr_ref_vector sig_vars(m);
+            for (unsigned j = 0; j < sig.size(); ++j) {
+                sig_vars.push_back(m.mk_const(sig[sig.size()-j-1]));
+            }
+            expr_abstract(m, 0, sig_vars.size(), sig_vars.c_ptr(), prop, q);
+            if (sig.empty()) {
+                md->register_decl(pred, q);
+            }
+            else {
+                func_interp* fi = alloc(func_interp, m, sig.size());
+                fi->set_else(q);
+                md->register_decl(pred, fi);
+            }
+        }
+        TRACE("pdr", model_smt2_pp(tout, m, *md, 0););
+        apply(const_cast<model_converter_ref&>(m_mc), md, 0);
+    }
+
+    expr_ref inductive_property::to_expr() const {
+        model_ref md;
+        expr_ref result(m);
+        to_model(md);
+        model2expr(md, result);
+        return result;        
+    }
+
+    
+    void inductive_property::display(ptr_vector<datalog::rule> const& rules, std::ostream& out) const {
+        func_decl_set bound_decls, aux_decls;
+        collect_decls_proc collect_decls(bound_decls, aux_decls);
+
+        for (unsigned i = 0; i < m_relation_info.size(); ++i) {
+            bound_decls.insert(m_relation_info[i].m_pred);
+            func_decl_ref_vector const& sig = m_relation_info[i].m_vars;
+            for (unsigned j = 0; j < sig.size(); ++j) {
+                bound_decls.insert(sig[j]);
+            }
+            for_each_expr(collect_decls, m_relation_info[i].m_body);
+        }
+        for (unsigned i = 0; i < rules.size(); ++i) {
+            bound_decls.insert(rules[i]->get_decl());
+        }
+        for (unsigned i = 0; i < rules.size(); ++i) {
+            unsigned u_sz = rules[i]->get_uninterpreted_tail_size();
+            unsigned t_sz = rules[i]->get_tail_size();
+            for (unsigned j = u_sz; j < t_sz; ++j) {
+                for_each_expr(collect_decls, rules[i]->get_tail(j));
+            }
+        }
+        smt2_pp_environment_dbg env(m);
+        func_decl_set::iterator it = aux_decls.begin(), end = aux_decls.end();
+        for (; it != end; ++it) {
+            func_decl* f = *it;
+            ast_smt2_pp(out, f, env);
+            out << "\n";
+        }
+
+        out << to_string() << "\n";
+        for (unsigned i = 0; i < rules.size(); ++i) {
+            out << "(push)\n";
+            out << "(assert (not\n";
+            rules[i]->display_smt2(m, out);
+            out << "))\n";
+            out << "(check-sat)\n";
+            out << "(pop)\n";
+        }
+    }
+
+    vector<std::string> manager::get_state_suffixes() {
+        vector<std::string> res;
+        res.push_back("_n");
+        return res;
+    }
+    
+    manager::manager(smt_params& fparams, fixedpoint_params const& params, ast_manager& manager) :
+        m(manager),
+        m_fparams(fparams),
+        m_params(params),
+        m_brwr(m),
+        m_mux(m, get_state_suffixes()),
+        m_background(m.mk_true(), m),
+        m_contexts(fparams, params, m),
+        m_next_unique_num(0)
+    {        
+    }
+
+
+    void manager::add_new_state(func_decl * s) {
+        SASSERT(s->get_arity()==0); //we currently don't support non-constant states
+        decl_vector vect;
+        SASSERT(o_index(0)==1); //we assume this in the number of retrieved symbols
+        m_mux.create_tuple(s, s->get_arity(), s->get_domain(), s->get_range(), 2, vect);
+        m_o0_preds.push_back(vect[o_index(0)]);
+    }
+    
+    func_decl * manager::get_o_pred(func_decl* s, unsigned idx)
+    {
+        func_decl * res = m_mux.try_get_by_prefix(s, o_index(idx));
+        if(res) { return res; }
+        add_new_state(s);
+        res = m_mux.try_get_by_prefix(s, o_index(idx));
+        SASSERT(res);
+        return res;
+    }
+    
+    func_decl * manager::get_n_pred(func_decl* s)
+    {
+        func_decl * res = m_mux.try_get_by_prefix(s, n_index());
+        if(res) { return res; }
+        add_new_state(s);
+        res = m_mux.try_get_by_prefix(s, n_index());
+        SASSERT(res);
+        return res;
+    }
+    
+    void manager::mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res) {
+        m_brwr.mk_and(mdl.size(), mdl.c_ptr(), res);
+    }
+    
+    void manager::mk_core_into_cube(const expr_ref_vector & core, expr_ref & res) {
+        m_brwr.mk_and(core.size(), core.c_ptr(), res);
+    }
+    
+    void manager::mk_cube_into_lemma(expr * cube, expr_ref & res) {
+        m_brwr.mk_not(cube, res);
+    }
+    
+    void manager::mk_lemma_into_cube(expr * lemma, expr_ref & res) {
+        m_brwr.mk_not(lemma, res);
+    }
+    
+    expr_ref manager::mk_and(unsigned sz, expr* const* exprs) {
+        expr_ref result(m);
+        m_brwr.mk_and(sz, exprs, result);
+        return result;
+    }
+    
+    expr_ref manager::mk_or(unsigned sz, expr* const* exprs) {
+        expr_ref result(m);
+        m_brwr.mk_or(sz, exprs, result);
+        return result;
+    }
+
+    expr_ref manager::mk_not_and(expr_ref_vector const& conjs) {
+        expr_ref result(m), e(m);
+        expr_ref_vector es(conjs);
+        qe::flatten_and(es);
+        for (unsigned i = 0; i < es.size(); ++i) {
+            m_brwr.mk_not(es[i].get(), e);
+            es[i] = e;
+        }
+        m_brwr.mk_or(es.size(), es.c_ptr(), result);
+        return result;
+    }
+    
+    void manager::get_or(expr* e, expr_ref_vector& result) {
+        result.push_back(e);
+        for (unsigned i = 0; i < result.size(); ) {
+            e = result[i].get();
+            if (m.is_or(e)) {
+                result.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+                result[i] = result.back();
+                result.pop_back();
+            }
+            else {
+                ++i;
+            }
+        }
+    }
+    
+    bool manager::try_get_state_and_value_from_atom(expr * atom0, app *& state, app_ref& value)
+    {
+        if(!is_app(atom0)) {
+            return false;
+        }
+        app * atom = to_app(atom0);
+        expr * arg1;
+        expr * arg2;
+        app * candidate_state;
+        app_ref candidate_value(m);
+        if(m.is_not(atom, arg1)) {
+            if(!is_app(arg1)) {
+                return false;
+            }
+            candidate_state = to_app(arg1);
+            candidate_value = m.mk_false();
+        }
+        else if(m.is_eq(atom, arg1, arg2)) {
+            if(!is_app(arg1) || !is_app(arg2)) {
+                return false;
+            }
+            if(!m_mux.is_muxed(to_app(arg1)->get_decl())) {
+                std::swap(arg1, arg2);
+            }
+            candidate_state = to_app(arg1);
+            candidate_value = to_app(arg2);
+        }
+        else {
+            candidate_state = atom;
+            candidate_value = m.mk_true();
+        }
+        if(!m_mux.is_muxed(candidate_state->get_decl())) {
+            return false;
+        }
+        state = candidate_state;
+        value = candidate_value;
+        return true;
+    }
+    
+    bool manager::try_get_state_decl_from_atom(expr * atom, func_decl *& state) {
+        app_ref dummy_value_holder(m);
+        app * s;
+        if(try_get_state_and_value_from_atom(atom, s, dummy_value_holder)) {
+            state = s->get_decl();
+            return true;
+        }
+        else {
+            return false;
+        }
+    }       
+        
+    bool manager::implication_surely_holds(expr * lhs, expr * rhs, expr * bg) {
+        smt::kernel sctx(m, get_fparams());
+        if(bg) {
+            sctx.assert_expr(bg);
+        }
+        sctx.assert_expr(lhs);
+        expr_ref neg_rhs(m.mk_not(rhs),m);
+        sctx.assert_expr(neg_rhs);
+        lbool smt_res = sctx.check();
+        return smt_res==l_false;
+    }
+
+};

src/muz/pdr/pdr_manager.h

@@ -0,0 +1,309 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_manager.h
+
+Abstract:
+
+    A manager class for PDR, taking care of creating of AST 
+    objects and conversions between them.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-8-25.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_MANAGER_H_
+#define _PDR_MANAGER_H_
+
+#include <utility>
+#include <map>
+#include "bool_rewriter.h"
+#include "expr_replacer.h"
+#include "expr_substitution.h"
+#include "map.h"
+#include "ref_vector.h"
+#include "smt_kernel.h"
+#include "pdr_util.h"
+#include "pdr_sym_mux.h"
+#include "pdr_farkas_learner.h"
+#include "pdr_smt_context_manager.h"
+#include "dl_rule.h"
+
+
+namespace smt {
+    class context;
+}
+
+namespace pdr {
+
+    struct relation_info {
+        func_decl_ref         m_pred;
+        func_decl_ref_vector  m_vars;
+        expr_ref              m_body;
+        relation_info(ast_manager& m, func_decl* pred, ptr_vector<func_decl> const& vars, expr* b): 
+            m_pred(pred, m), m_vars(m, vars.size(), vars.c_ptr()), m_body(b, m) {}
+        relation_info(relation_info const& other): m_pred(other.m_pred), m_vars(other.m_vars), m_body(other.m_body) {}
+    };
+
+    class unknown_exception {};
+
+    class inductive_property {
+        ast_manager&             m;
+        model_converter_ref      m_mc;
+        vector<relation_info>    m_relation_info;
+        expr_ref fixup_clauses(expr* property) const;
+        expr_ref fixup_clause(expr* clause) const;
+    public:
+        inductive_property(ast_manager& m, model_converter_ref& mc, vector<relation_info> const& relations):
+            m(m),
+            m_mc(mc),
+            m_relation_info(relations) {}
+
+        std::string to_string() const;
+
+        expr_ref to_expr() const;
+
+        void to_model(model_ref& md) const;
+
+        void display(ptr_vector<datalog::rule> const& rules, std::ostream& out) const;
+    };
+
+    class manager
+    {
+        ast_manager&      m;
+        smt_params& m_fparams;
+        fixedpoint_params const& m_params;
+        
+        mutable bool_rewriter m_brwr;
+        
+        sym_mux               m_mux;
+        expr_ref              m_background;
+        decl_vector           m_o0_preds;
+        pdr::smt_context_manager   m_contexts;
+        
+        /** whenever we need an unique number, we get this one and increase */
+        unsigned m_next_unique_num;
+        
+        
+        static vector<std::string> get_state_suffixes();
+        
+        unsigned n_index() const { return 0; }
+        unsigned o_index(unsigned i) const { return i+1; }
+        
+        void add_new_state(func_decl * s);
+        
+    public:
+        manager(smt_params& fparams, fixedpoint_params const& params, 
+                ast_manager & manager);
+        
+        ast_manager& get_manager() const { return m; }
+        smt_params& get_fparams() const { return m_fparams; }
+        fixedpoint_params const& get_params() const { return m_params; }
+        bool_rewriter& get_brwr() const { return m_brwr; }
+
+        expr_ref mk_and(unsigned sz, expr* const* exprs);
+        expr_ref mk_and(expr_ref_vector const& exprs) {
+            return mk_and(exprs.size(), exprs.c_ptr());
+        }
+        expr_ref mk_and(expr* a, expr* b) {
+            expr* args[2] = { a, b };
+            return mk_and(2, args);
+        }
+        expr_ref mk_or(unsigned sz, expr* const* exprs);
+        expr_ref mk_or(expr_ref_vector const& exprs) {
+            return mk_or(exprs.size(), exprs.c_ptr());
+        }
+
+        expr_ref mk_not_and(expr_ref_vector const& exprs);
+        
+        void get_or(expr* e, expr_ref_vector& result);
+        
+        //"o" predicates stand for the old states and "n" for the new states
+        func_decl * get_o_pred(func_decl * s, unsigned idx);
+        func_decl * get_n_pred(func_decl * s);
+        
+        /**
+           Marks symbol as non-model which means it will not appear in models collected by 
+           get_state_cube_from_model function.
+           This is to take care of auxiliary symbols introduced by the disjunction relations
+           to relativize lemmas coming from disjuncts.
+        */
+        void mark_as_non_model(func_decl * p) {
+            m_mux.mark_as_non_model(p);
+        }
+        
+        
+        func_decl * const * begin_o0_preds() const { return m_o0_preds.begin(); }
+        func_decl * const * end_o0_preds() const { return m_o0_preds.end(); }
+        
+        bool is_state_pred(func_decl * p) const { return m_mux.is_muxed(p); }
+        func_decl * to_o0(func_decl * p) { return m_mux.conv(m_mux.get_primary(p), 0, o_index(0)); }
+        
+        bool is_o(func_decl * p, unsigned idx) const { 
+            return m_mux.has_index(p, o_index(idx)); 
+        }
+        bool is_o(expr* e, unsigned idx) const {
+            return is_app(e) && is_o(to_app(e)->get_decl(), idx);
+        }
+        bool is_o(func_decl * p) const { 
+            unsigned idx;
+            return m_mux.try_get_index(p, idx) && idx!=n_index();
+        }
+        bool is_o(expr* e) const {
+            return is_app(e) && is_o(to_app(e)->get_decl());
+        }
+        bool is_n(func_decl * p) const { 
+            return m_mux.has_index(p, n_index()); 
+        }
+        bool is_n(expr* e) const {
+            return is_app(e) && is_n(to_app(e)->get_decl());
+        }
+        
+        /** true if p should not appead in models propagates into child relations */
+        bool is_non_model_sym(func_decl * p) const 
+        { return m_mux.is_non_model_sym(p); }
+        
+        
+        /** true if f doesn't contain any n predicates */
+        bool is_o_formula(expr * f) const { 
+            return !m_mux.contains(f, n_index()); 
+        }
+
+        /** true if f contains only o state preds of index o_idx */
+        bool is_o_formula(expr * f, unsigned o_idx) const { 
+            return m_mux.is_homogenous_formula(f, o_index(o_idx)); 
+        }
+        /** true if f doesn't contain any o predicates */
+        bool is_n_formula(expr * f) const { 
+            return m_mux.is_homogenous_formula(f, n_index()); 
+        }
+        
+        func_decl * o2n(func_decl * p, unsigned o_idx) const {
+            return m_mux.conv(p, o_index(o_idx), n_index()); 
+        }
+        func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const { 
+            return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx)); 
+        }
+        func_decl * n2o(func_decl * p, unsigned o_idx) const {
+            return m_mux.conv(p, n_index(), o_index(o_idx)); 
+        }
+    
+        void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const
+        { m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous); }
+        
+        void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous=true) const
+        { m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous); }
+        
+        void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const
+        { m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous); }
+        
+        void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous=true) const
+        { m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous); }
+        
+        /**
+           Return true if all state symbols which e contains are of one kind (either "n" or one of "o").
+        */
+        bool is_homogenous_formula(expr * e) const {
+            return m_mux.is_homogenous_formula(e);
+        }
+
+        /**
+            Collect indices used in expression.
+        */
+        void collect_indices(expr* e, unsigned_vector& indices) const {
+            m_mux.collect_indices(e, indices);
+        }
+
+        /**
+            Collect used variables of each index.
+        */
+        void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const {
+            m_mux.collect_variables(e, vars);
+        }
+        
+        /**
+           Return true iff both s1 and s2 are either "n" or "o" of the same index.
+           If one (or both) of them are not state symbol, return false.
+        */
+        bool have_different_state_kinds(func_decl * s1, func_decl * s2) const {
+            unsigned i1, i2;
+            return m_mux.try_get_index(s1, i1) && m_mux.try_get_index(s2, i2) && i1!=i2;
+        }
+        
+        /**
+           Increase indexes of state symbols in formula by dist.
+           The 'N' index becomes 'O' index with number dist-1.
+        */
+        void formula_shift(expr * src, expr_ref & tgt, unsigned dist) const {
+            SASSERT(n_index()==0);
+            SASSERT(o_index(0)==1);
+            m_mux.shift_formula(src, dist, tgt);
+        }
+        
+        void mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res);
+        void mk_core_into_cube(const expr_ref_vector & core, expr_ref & res);
+        void mk_cube_into_lemma(expr * cube, expr_ref & res);
+        void mk_lemma_into_cube(expr * lemma, expr_ref & res);
+        
+        /**
+           Remove from vec all atoms that do not have an "o" state.
+           The order of elements in vec may change.
+           An assumption is that atoms having "o" state of given index
+           do not have "o" states of other indexes or "n" states.
+        */
+        void filter_o_atoms(expr_ref_vector& vec, unsigned o_idx) const 
+        { m_mux.filter_idx(vec, o_index(o_idx)); }
+        void filter_n_atoms(expr_ref_vector& vec) const 
+        { m_mux.filter_idx(vec, n_index()); }
+        
+        /**
+           Partition literals into o_lits and others.
+        */
+        void partition_o_atoms(expr_ref_vector const& lits, 
+                               expr_ref_vector& o_lits,
+                               expr_ref_vector& other,
+                               unsigned o_idx) const {
+            m_mux.partition_o_idx(lits, o_lits, other, o_index(o_idx));
+        }
+        
+        void filter_out_non_model_atoms(expr_ref_vector& vec) const
+        { m_mux.filter_non_model_lits(vec); }
+        
+        bool try_get_state_and_value_from_atom(expr * atom, app *& state, app_ref& value);
+        bool try_get_state_decl_from_atom(expr * atom, func_decl *& state);
+        
+        
+        std::string pp_model(const model_core & mdl) const
+            {  return m_mux.pp_model(mdl); }
+        
+
+        void set_background(expr* b) { m_background = b; }
+        
+        expr* get_background() const { return m_background; }
+        
+        
+        /**
+           Return true if we can show that lhs => rhs. The function can have false negatives
+           (i.e. when smt::context returns unknown), but no false positives.
+           
+           bg is background knowledge and can be null
+        */
+        bool implication_surely_holds(expr * lhs, expr * rhs, expr * bg=0);
+        
+        unsigned get_unique_num() { return m_next_unique_num++; }
+        
+        pdr::smt_context* mk_fresh() {  return m_contexts.mk_fresh();   }
+        
+        void collect_statistics(statistics& st) const { m_contexts.collect_statistics(st); }
+
+        void reset_statistics() { m_contexts.reset_statistics(); }
+    };
+}
+
+#endif

src/muz/pdr/pdr_prop_solver.cpp

@@ -0,0 +1,460 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    prop_solver.cpp
+
+Abstract:
+
+    SMT solver abstraction for PDR.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-8-17.
+
+Revision History:
+
+--*/
+
+#include <sstream>
+#include "model.h"
+#include "pdr_util.h"
+#include "pdr_prop_solver.h"
+#include "ast_smt2_pp.h"
+#include "dl_util.h"
+#include "model_pp.h"
+#include "smt_params.h"
+#include "datatype_decl_plugin.h"
+#include "bv_decl_plugin.h"
+#include "pdr_farkas_learner.h"
+#include "ast_smt2_pp.h"
+#include "expr_replacer.h"
+
+//
+// Auxiliary structure to introduce propositional names for assumptions that are not
+// propositional. It is to work with the smt::context's restriction
+// that assumptions be propositional literals.
+//
+
+namespace pdr {
+
+    class prop_solver::safe_assumptions {
+        prop_solver&        s;
+        ast_manager&        m;
+        expr_ref_vector     m_atoms;
+        expr_ref_vector     m_assumptions;
+        obj_map<app,expr *> m_proxies2expr;
+        obj_map<expr, app*> m_expr2proxies;
+        unsigned            m_num_proxies;
+
+        app * mk_proxy(expr* literal) {
+            app* res;
+            SASSERT(!is_var(literal)); //it doesn't make sense to introduce names to variables
+            if (m_expr2proxies.find(literal, res)) {
+                return res;
+            }
+            SASSERT(s.m_proxies.size() >= m_num_proxies);
+            if (m_num_proxies == s.m_proxies.size()) {
+                std::stringstream name;
+                name << "pdr_proxy_" << s.m_proxies.size();
+                res = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort());
+                s.m_proxies.push_back(res);
+                s.m_aux_symbols.insert(res->get_decl());
+            }
+            else {
+                res = s.m_proxies[m_num_proxies].get();
+            }
+            ++m_num_proxies;
+            m_expr2proxies.insert(literal, res);
+            m_proxies2expr.insert(res, literal);
+            expr_ref implies(m.mk_or(m.mk_not(res), literal), m);
+            s.m_ctx->assert_expr(implies);
+            m_assumptions.push_back(implies);
+            TRACE("pdr_verbose", tout << "name asserted " << mk_pp(implies, m) << "\n";);    
+            return res;
+        }
+
+        void mk_safe(expr_ref_vector& conjs) {
+            qe::flatten_and(conjs);
+            expand_literals(conjs);
+            for (unsigned i = 0; i < conjs.size(); ++i) {
+                expr * lit = conjs[i].get();
+                expr * lit_core = lit;
+                m.is_not(lit, lit_core);
+                SASSERT(!m.is_true(lit));
+                if (!is_uninterp(lit_core) || to_app(lit_core)->get_num_args() != 0) {
+                    conjs[i] = mk_proxy(lit);
+                }
+            }
+            m_assumptions.append(conjs);
+        }
+
+        expr* apply_accessor(
+            ptr_vector<func_decl> const& acc,
+            unsigned j,
+            func_decl* f,
+            expr* c) {
+            if (is_app(c) && to_app(c)->get_decl() == f) {
+                return to_app(c)->get_arg(j);
+            }
+            else {
+                return m.mk_app(acc[j], c);
+            }
+        }
+
+        void expand_literals(expr_ref_vector& conjs) {
+            arith_util arith(m);
+            datatype_util dt(m);
+            bv_util       bv(m);
+            expr* e1, *e2, *c, *val;
+            rational r;
+            unsigned bv_size;
+
+            TRACE("pdr", 
+                  tout << "begin expand\n";
+                  for (unsigned i = 0; i < conjs.size(); ++i) {
+                      tout << mk_pp(conjs[i].get(), m) << "\n";
+                  });
+
+            for (unsigned i = 0; i < conjs.size(); ++i) {
+                expr* e = conjs[i].get();
+                if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
+                    conjs[i] = arith.mk_le(e1,e2);
+                    if (i+1 == conjs.size()) {
+                        conjs.push_back(arith.mk_ge(e1, e2));
+                    }
+                    else {
+                        conjs.push_back(conjs[i+1].get());
+                        conjs[i+1] = arith.mk_ge(e1, e2);
+                    }
+                    ++i;
+                }
+                else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
+                         (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
+                    func_decl* f = to_app(val)->get_decl();
+                    func_decl* r = dt.get_constructor_recognizer(f);
+                    conjs[i] = m.mk_app(r, c);
+                    ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
+                    for (unsigned j = 0; j < acc.size(); ++j) {
+                        conjs.push_back(m.mk_eq(apply_accessor(acc, j, f, c), to_app(val)->get_arg(j)));
+                    }
+                }
+                else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
+                         (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
+                    rational two(2);
+                    for (unsigned j = 0; j < bv_size; ++j) {
+                        parameter p(j);
+                        //expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
+                        expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c));
+                        if ((r % two).is_zero()) {
+                            e = m.mk_not(e);
+                        }
+                        r = div(r, two);
+                        if (j == 0) {
+                            conjs[i] = e;
+                        }
+                        else {
+                            conjs.push_back(e);
+                        }
+                    }
+                }
+            }
+            TRACE("pdr", 
+                  tout << "end expand\n";
+                  for (unsigned i = 0; i < conjs.size(); ++i) {
+                      tout << mk_pp(conjs[i].get(), m) << "\n";
+                  });
+        }
+
+    public:
+        safe_assumptions(prop_solver& s, expr_ref_vector const& assumptions): 
+            s(s), m(s.m), m_atoms(assumptions), m_assumptions(m), m_num_proxies(0) {
+              mk_safe(m_atoms);
+        }
+        
+        ~safe_assumptions() {
+        }    
+        
+        expr_ref_vector const& atoms() const { return m_atoms; }
+        
+        unsigned assumptions_size() const { return m_assumptions.size(); }
+        
+        expr* assumptions(unsigned i) const { return m_assumptions[i]; }
+
+        void undo_proxies(expr_ref_vector& es) {
+            expr_ref e(m);
+            expr* r;
+            for (unsigned i = 0; i < es.size(); ++i) {
+                e = es[i].get();
+                if (is_app(e) && m_proxies2expr.find(to_app(e), r)) {
+                    es[i] = r;
+                }
+            }
+        }
+        
+        void elim_proxies(expr_ref_vector& es) {
+            expr_substitution sub(m, false, m.proofs_enabled());
+            proof_ref pr(m);
+            if (m.proofs_enabled()) {
+                pr = m.mk_asserted(m.mk_true());
+            }
+            obj_map<app,expr*>::iterator it = m_proxies2expr.begin(), end = m_proxies2expr.end();
+            for (; it != end; ++it) {
+                sub.insert(it->m_key, m.mk_true(), pr);
+            }
+            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+            rep->set_substitution(&sub);
+            replace_proxies(*rep, es);
+        }
+    private:
+
+        void replace_proxies(expr_replacer& rep, expr_ref_vector& es) {
+            expr_ref e(m);
+            for (unsigned i = 0; i < es.size(); ++i) {
+                e = es[i].get();
+                rep(e);
+                es[i] = e;
+                if (m.is_true(e)) {
+                    es[i] = es.back();
+                    es.pop_back();
+                    --i;
+                }
+            }        
+        }
+    };
+
+
+    prop_solver::prop_solver(manager& pm, symbol const& name) :
+        m_fparams(pm.get_fparams()),
+        m(pm.get_manager()),
+        m_pm(pm),
+        m_name(name),
+        m_try_minimize_core(pm.get_params().try_minimize_core()),
+        m_ctx(pm.mk_fresh()),
+        m_pos_level_atoms(m),
+        m_neg_level_atoms(m),
+        m_proxies(m),
+        m_core(0),
+        m_model(0),
+        m_consequences(0),
+        m_subset_based_core(false),
+        m_use_farkas(false),
+        m_in_level(false),
+        m_current_level(0)
+    {
+        m_ctx->assert_expr(m_pm.get_background());
+    }
+
+    void prop_solver::add_level() {
+        unsigned idx = level_cnt();
+        std::stringstream name;
+        name << m_name << "#level_" << idx;
+        func_decl * lev_pred = m.mk_fresh_func_decl(name.str().c_str(), 0, 0,m.mk_bool_sort());
+        m_aux_symbols.insert(lev_pred);
+        m_level_preds.push_back(lev_pred);
+
+        app_ref pos_la(m.mk_const(lev_pred), m);
+        app_ref neg_la(m.mk_not(pos_la.get()), m);
+
+        m_pos_level_atoms.push_back(pos_la);
+        m_neg_level_atoms.push_back(neg_la);
+
+        m_level_atoms_set.insert(pos_la.get());
+        m_level_atoms_set.insert(neg_la.get());
+    }
+
+    void prop_solver::ensure_level(unsigned lvl) {
+        while (lvl>=level_cnt()) {
+            add_level();
+        }
+    }
+
+    unsigned prop_solver::level_cnt() const {
+        return m_level_preds.size();
+    }
+
+    void prop_solver::push_level_atoms(unsigned level, expr_ref_vector& tgt) const {
+        unsigned lev_cnt = level_cnt();
+        for (unsigned i=0; i<lev_cnt; i++) {
+            bool active = i>=level;
+            app * lev_atom = active ? m_neg_level_atoms[i] : m_pos_level_atoms[i];
+            tgt.push_back(lev_atom);
+        }
+    }
+
+    void prop_solver::add_formula(expr * form) {
+        SASSERT(!m_in_level);
+        m_ctx->assert_expr(form);
+        IF_VERBOSE(21, verbose_stream() << "$ asserted " << mk_pp(form, m) << "\n";);
+        TRACE("pdr", tout << "add_formula: " << mk_pp(form, m) << "\n";);
+    }
+
+    void prop_solver::add_level_formula(expr * form, unsigned level) {
+        ensure_level(level);
+        app * lev_atom = m_pos_level_atoms[level].get();
+        app_ref lform(m.mk_or(form, lev_atom), m);
+        add_formula(lform.get());
+    }
+
+
+    lbool prop_solver::check_safe_assumptions(
+        safe_assumptions& safe,
+        const expr_ref_vector& atoms)
+    {
+        flet<bool> _model(m_fparams.m_model, m_model != 0);
+        expr_ref_vector expr_atoms(m);
+        expr_atoms.append(atoms.size(), atoms.c_ptr());
+
+        if (m_in_level) {
+            push_level_atoms(m_current_level, expr_atoms);
+        }
+
+        lbool result = m_ctx->check(expr_atoms);
+
+        TRACE("pdr", 
+               tout << mk_pp(m_pm.mk_and(expr_atoms), m) << "\n";
+               tout << result << "\n";);
+
+        if (result == l_true && m_model) {
+            m_ctx->get_model(*m_model);
+            TRACE("pdr_verbose", model_pp(tout, **m_model); );
+        }
+        
+        if (result == l_false) { 
+            unsigned core_size = m_ctx->get_unsat_core_size(); 
+            m_assumes_level = false;
+            for (unsigned i = 0; i < core_size; ++i) {
+                if (m_level_atoms_set.contains(m_ctx->get_unsat_core_expr(i))) {
+                    m_assumes_level = true;
+                    break;
+                }
+            }
+        }
+
+        if (result == l_false  && 
+            m_core && 
+            m.proofs_enabled() && 
+            m_use_farkas    && 
+            !m_subset_based_core) {
+            extract_theory_core(safe);
+        }
+        else if (result == l_false && m_core) {
+            extract_subset_core(safe);    
+            SASSERT(expr_atoms.size() >= m_core->size());
+        }
+        m_core = 0;
+        m_model = 0;
+        m_subset_based_core = false;
+        return result;
+    }
+
+    void prop_solver::extract_subset_core(safe_assumptions& safe) {
+        unsigned core_size = m_ctx->get_unsat_core_size(); 
+        m_core->reset();
+        for (unsigned i = 0; i < core_size; ++i) {
+            expr * core_expr = m_ctx->get_unsat_core_expr(i);
+            SASSERT(is_app(core_expr));
+
+            if (m_level_atoms_set.contains(core_expr)) {
+                continue;
+            }
+            if (m_ctx->is_aux_predicate(core_expr)) {
+                continue;
+            }
+            m_core->push_back(to_app(core_expr));
+        }        
+
+        safe.undo_proxies(*m_core);
+
+        TRACE("pdr", 
+            tout << "core_exprs: ";
+                for (unsigned i = 0; i < core_size; ++i) {
+                tout << mk_pp(m_ctx->get_unsat_core_expr(i), m) << " ";
+            }
+            tout << "\n";
+            tout << "core: " << mk_pp(m_pm.mk_and(*m_core), m) << "\n";              
+        );
+    }
+
+
+    void prop_solver::extract_theory_core(safe_assumptions& safe) {
+        proof_ref pr(m);
+        pr = m_ctx->get_proof();
+        IF_VERBOSE(21, verbose_stream() << mk_ismt2_pp(pr, m) << "\n";);
+        farkas_learner fl(m_fparams, m);
+        expr_ref_vector lemmas(m);
+        obj_hashtable<expr> bs;
+        for (unsigned i = 0; i < safe.assumptions_size(); ++i) {
+            bs.insert(safe.assumptions(i));
+        }
+        fl.get_lemmas(pr, bs, lemmas);
+        safe.elim_proxies(lemmas);
+        fl.simplify_lemmas(lemmas); // redundant?
+
+        bool outside_of_logic = 
+            (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
+             !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) ||
+            (m_fparams.m_arith_mode == AS_UTVPI &&
+             !is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr()));
+
+        if (outside_of_logic) {
+            IF_VERBOSE(2, 
+                       verbose_stream() << "not diff\n";
+                       for (unsigned i = 0; i < lemmas.size(); ++i) {
+                           verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+                       });
+            extract_subset_core(safe);
+        }        
+        else {
+
+            IF_VERBOSE(2, 
+                       verbose_stream() << "Lemmas\n";            
+                       for (unsigned i = 0; i < lemmas.size(); ++i) {
+                           verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+                       });
+
+            m_core->reset();
+            m_core->append(lemmas);
+
+            if (m_consequences) {
+                fl.get_consequences(pr, bs, *m_consequences);
+            }
+        }
+    }
+
+    lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) {
+        return check_assumptions_and_formula(atoms, m.mk_true());
+    }
+
+    lbool prop_solver::check_conjunction_as_assumptions(expr * conj) {
+        expr_ref_vector asmp(m);
+        asmp.push_back(conj);
+        return check_assumptions(asmp);
+    }
+
+    lbool prop_solver::check_assumptions_and_formula(const expr_ref_vector & atoms, expr * form) 
+    {
+        pdr::smt_context::scoped _scoped(*m_ctx);
+        safe_assumptions safe(*this, atoms);
+        m_ctx->assert_expr(form);    
+        CTRACE("pdr", !m.is_true(form), tout << "check with formula: " << mk_pp(form, m) << "\n";);
+        lbool res = check_safe_assumptions(safe, safe.atoms());
+
+        //
+        // we don't have to undo model naming, as from the model 
+        // we extract the values for state variables directly
+        //
+        return res;
+    }
+
+    void prop_solver::collect_statistics(statistics& st) const {
+    }
+
+    void prop_solver::reset_statistics() {
+    }
+
+    
+
+
+}

src/muz/pdr/pdr_prop_solver.h

@@ -0,0 +1,139 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    prop_solver.h
+
+Abstract:
+
+    SAT solver abstraction for PDR.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-8-17.
+
+Revision History:
+
+--*/
+
+#ifndef _PROP_SOLVER_H_
+#define _PROP_SOLVER_H_
+
+#include <map>
+#include <string>
+#include <utility>
+#include "ast.h"
+#include "obj_hashtable.h"
+#include "smt_kernel.h"
+#include "util.h"
+#include "vector.h"
+#include "pdr_manager.h"
+#include "pdr_smt_context_manager.h"
+
+namespace pdr {
+    class prop_solver {
+    
+    private:
+        smt_params&         m_fparams;        
+        ast_manager&        m;
+        manager&            m_pm;
+        symbol              m_name;
+        bool                m_try_minimize_core;
+        scoped_ptr<pdr::smt_context> m_ctx;
+        decl_vector         m_level_preds;      
+        app_ref_vector      m_pos_level_atoms;  // atoms used to identify level
+        app_ref_vector      m_neg_level_atoms;  // 
+        obj_hashtable<expr> m_level_atoms_set;
+        app_ref_vector      m_proxies;          // predicates for assumptions
+        expr_ref_vector*    m_core; 
+        model_ref*          m_model;
+        expr_ref_vector*    m_consequences;
+        bool                m_subset_based_core;
+        bool                m_assumes_level;
+        bool                m_use_farkas;
+        func_decl_set       m_aux_symbols;      
+        bool                m_in_level;         
+        unsigned            m_current_level;    // set when m_in_level
+        
+        /** Add level atoms activating certain level into a vector */
+        void push_level_atoms(unsigned level, expr_ref_vector & tgt) const;
+        
+        void ensure_level(unsigned lvl);
+
+        class safe_assumptions;
+
+        void extract_theory_core(safe_assumptions& assumptions);
+
+        void extract_subset_core(safe_assumptions& assumptions);
+        
+        lbool check_safe_assumptions(
+            safe_assumptions& assumptions,
+            expr_ref_vector const& atoms);
+        
+        
+    public:
+        prop_solver(pdr::manager& pm, symbol const& name);
+        
+        /** return true is s is a symbol introduced by prop_solver */
+        bool is_aux_symbol(func_decl * s) const { 
+            return 
+                m_aux_symbols.contains(s) ||
+                m_ctx->is_aux_predicate(s); 
+        }
+
+        void set_core(expr_ref_vector* core) { m_core = core; }
+        void set_model(model_ref* mdl) { m_model = mdl; }
+        void set_subset_based_core(bool f) { m_subset_based_core = f; }
+        void set_consequences(expr_ref_vector* consequences) { m_consequences = consequences; }
+
+        bool assumes_level() const { return m_assumes_level; }
+        
+        void add_level();
+        unsigned level_cnt() const;
+        
+        class scoped_level {
+            bool& m_lev;
+        public:
+            scoped_level(prop_solver& ps, unsigned lvl):m_lev(ps.m_in_level) { 
+                SASSERT(!m_lev); m_lev = true; ps.m_current_level = lvl; 
+            }
+            ~scoped_level() { m_lev = false; }
+        };
+        
+        void set_use_farkas(bool f) { m_use_farkas = f; }
+        bool get_use_farkas() const { return m_use_farkas; }
+        
+        void add_formula(expr * form);
+        void add_level_formula(expr * form, unsigned level);
+                
+        /**
+         * Return true iff conjunction of atoms is consistent with the current state of 
+         * the solver.
+         *
+         * If the conjunction of atoms is inconsistent with the solver state and core is non-zero,
+         * core will contain an unsatisfiable core of atoms.
+         *
+         * If the conjunction of atoms is consistent with the solver state and o_model is non-zero,
+         * o_model will contain the "o" literals true in the assignment.
+         */
+        lbool check_assumptions(const expr_ref_vector & atoms);
+        
+        lbool check_conjunction_as_assumptions(expr * conj);
+        
+        /**
+         * Like check_assumptions, except it also asserts an extra formula
+         */
+        lbool check_assumptions_and_formula(
+            const expr_ref_vector & atoms, 
+            expr * form);
+        
+        void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
+        
+    };
+}
+
+
+#endif

src/muz/pdr/pdr_reachable_cache.cpp

@@ -0,0 +1,127 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    reachable_cache.cpp
+
+Abstract:
+
+    Object for caching of reachable states.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-14.
+
+Revision History:
+
+--*/
+
+#include "pdr_reachable_cache.h"
+
+namespace pdr {
+
+    reachable_cache::reachable_cache(pdr::manager & pm, fixedpoint_params const& params)
+        : m(pm.get_manager()), 
+          m_pm(pm), 
+          m_ctx(0),
+          m_ref_holder(m), 
+          m_disj_connector(m),
+          m_cache_mode((datalog::PDR_CACHE_MODE)params.cache_mode()) {
+        if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
+            m_ctx = pm.mk_fresh();
+            m_ctx->assert_expr(m_pm.get_background());
+        }
+    }
+    
+    
+    void reachable_cache::add_disjuncted_formula(expr * f) {
+        app_ref new_connector(m.mk_fresh_const("disj_conn", m.mk_bool_sort()), m);
+        app_ref neg_new_connector(m.mk_not(new_connector), m);
+        app_ref extended_form(m);
+        
+        if(m_disj_connector) {
+            extended_form = m.mk_or(m_disj_connector, neg_new_connector, f);
+        }
+        else {
+            extended_form = m.mk_or(neg_new_connector, f);
+        }
+        if (m_ctx) {
+            m_ctx->assert_expr(extended_form);
+        }
+        
+        m_disj_connector = new_connector;
+    }
+    
+    void reachable_cache::add_reachable(expr * cube) {
+        
+        switch (m_cache_mode) {
+        case datalog::NO_CACHE: 
+            break;
+            
+        case datalog::HASH_CACHE: 
+            m_stats.m_inserts++;
+            m_cache.insert(cube);
+            m_ref_holder.push_back(cube);
+            break;
+            
+        case datalog::CONSTRAINT_CACHE: 
+            m_stats.m_inserts++;
+            TRACE("pdr", tout << mk_pp(cube, m) << "\n";);
+            add_disjuncted_formula(cube);
+            break;
+            
+        default:
+            UNREACHABLE();        
+        }
+    }
+
+    bool reachable_cache::is_reachable(expr * cube) {
+        bool found = false;
+        switch (m_cache_mode) {
+        case datalog::NO_CACHE: 
+            return false;
+
+        case datalog::HASH_CACHE: 
+            found = m_cache.contains(cube);
+            break;
+
+        case datalog::CONSTRAINT_CACHE: {        
+            if(!m_disj_connector) {
+                found = false;
+                break;
+            }
+            expr * connector = m_disj_connector.get();
+            expr_ref_vector assms(m);
+            assms.push_back(connector);
+            m_ctx->push();
+            m_ctx->assert_expr(cube);
+            lbool res = m_ctx->check(assms);
+            m_ctx->pop();
+               
+            TRACE("pdr", tout << "is_reachable: " << res << " " << mk_pp(cube, m) << "\n";);
+
+            found = res == l_true;
+            break;
+        }
+
+        default:
+            UNREACHABLE();
+            break;
+        }
+        if (found) m_stats.m_hits++; m_stats.m_miss++;
+        return found;
+    }
+
+    void reachable_cache::collect_statistics(statistics& st) const {
+        st.update("cache inserts", m_stats.m_inserts);
+        st.update("cache miss", m_stats.m_miss);
+        st.update("cache hits", m_stats.m_hits);
+    }
+
+    void reachable_cache::reset_statistics() {
+        m_stats.reset();
+    }
+
+
+}

src/muz/pdr/pdr_reachable_cache.h

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    reachable_cache.h
+
+Abstract:
+
+    Object for caching of reachable states.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-14.
+
+Revision History:
+
+--*/
+
+
+#ifndef _REACHABLE_CACHE_H_
+#define _REACHABLE_CACHE_H_
+#include "ast.h"
+#include "ref_vector.h"
+#include "pdr_manager.h"
+#include "pdr_smt_context_manager.h"
+
+namespace pdr {
+    class reachable_cache {
+        struct stats {
+            unsigned             m_hits;
+            unsigned             m_miss;
+            unsigned             m_inserts;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
+        ast_manager &        m;
+        manager &            m_pm;
+        scoped_ptr<smt_context>    m_ctx;
+        ast_ref_vector       m_ref_holder;
+        app_ref              m_disj_connector;
+        obj_hashtable<expr>  m_cache;
+        stats                m_stats;
+        datalog::PDR_CACHE_MODE m_cache_mode;
+        
+        void add_disjuncted_formula(expr * f);
+        
+    public:
+        reachable_cache(pdr::manager & pm, fixedpoint_params const& params);
+        
+        void add_init(app * f)   { add_disjuncted_formula(f); }
+        
+        /** add cube whose all models are reachable */
+        void add_reachable(expr * cube);
+        
+        /** return true if there is a model of cube which is reachable */
+        bool is_reachable(expr * cube);
+        
+        void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
+    };
+}
+
+#endif

src/muz/pdr/pdr_smt_context_manager.cpp

@@ -0,0 +1,167 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_smt_context_manager.cpp
+
+Abstract:
+
+    Manager of smt contexts
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-11-26.
+
+Revision History:
+
+--*/
+
+#include "pdr_smt_context_manager.h"
+#include "has_free_vars.h"
+#include "ast_pp.h"
+#include "ast_smt_pp.h"
+#include <sstream>
+#include "smt_params.h"
+
+namespace pdr {
+
+    smt_context::smt_context(smt_context_manager& p, ast_manager& m, app* pred):
+        m_pred(pred, m),
+        m_parent(p),
+        m_in_delay_scope(false),
+        m_pushed(false)
+    {}
+
+    bool smt_context::is_aux_predicate(func_decl* p) {
+        return m_parent.is_aux_predicate(p);
+    }
+    
+    smt_context::scoped::scoped(smt_context& ctx): m_ctx(ctx) {
+        SASSERT(!m_ctx.m_in_delay_scope);
+        SASSERT(!m_ctx.m_pushed);
+        m_ctx.m_in_delay_scope = true;
+    }
+
+    smt_context::scoped::~scoped() {
+        SASSERT(m_ctx.m_in_delay_scope);
+        if (m_ctx.m_pushed) {
+            m_ctx.pop(); 
+            m_ctx.m_pushed = false;
+        }
+        m_ctx.m_in_delay_scope = false;        
+    }
+
+
+    _smt_context::_smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred):
+        smt_context(p, ctx.m(), pred),
+        m_context(ctx)
+    {}
+
+    void _smt_context::assert_expr(expr* e) {
+        ast_manager& m = m_context.m();
+        if (m.is_true(e)) {
+            return;
+        }
+        CTRACE("pdr", has_free_vars(e), tout << mk_pp(e, m) << "\n";);
+        SASSERT(!has_free_vars(e));
+        if (m_in_delay_scope && !m_pushed) {
+            m_context.push();
+            m_pushed = true;
+        }
+        expr_ref fml(m);
+        fml = m_pushed?e:m.mk_implies(m_pred, e);
+        m_context.assert_expr(fml);
+    }
+
+    lbool _smt_context::check(expr_ref_vector& assumptions) {
+        ast_manager& m = m_pred.get_manager();
+        if (!m.is_true(m_pred)) {
+            assumptions.push_back(m_pred);
+        }
+        TRACE("pdr_check", 
+              {
+                  ast_smt_pp pp(m);
+                  for (unsigned i = 0; i < m_context.size(); ++i) {
+                      pp.add_assumption(m_context.get_formulas()[i]);
+                  }
+                  for (unsigned i = 0; i < assumptions.size(); ++i) {
+                      pp.add_assumption(assumptions[i].get());
+                  }
+
+                  static unsigned lemma_id = 0;
+                  std::ostringstream strm;
+                  strm << "pdr-lemma-" << lemma_id << ".smt2";
+                  std::ofstream out(strm.str().c_str());
+                  pp.display_smt2(out, m.mk_true());
+                  out.close();
+                  lemma_id++;
+                  tout << "pdr_check: " << strm.str() << "\n";
+              });
+        lbool result = m_context.check(assumptions.size(), assumptions.c_ptr());
+        if (!m.is_true(m_pred)) {
+            assumptions.pop_back();
+        }
+        return result;
+    }
+
+    void _smt_context::get_model(model_ref& model) {
+        m_context.get_model(model);
+    }
+
+    proof* _smt_context::get_proof() {
+        return m_context.get_proof();
+    }
+
+    smt_context_manager::smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m):
+        m_fparams(fp), 
+        m(m), 
+        m_max_num_contexts(p.max_num_contexts()),
+        m_num_contexts(0), 
+        m_predicate_list(m) {
+    }
+    
+    
+    smt_context_manager::~smt_context_manager() {
+        TRACE("pdr",tout << "\n";);
+        std::for_each(m_contexts.begin(), m_contexts.end(), delete_proc<smt::kernel>());
+    }
+
+    smt_context* smt_context_manager::mk_fresh() {        
+        ++m_num_contexts;
+        app_ref pred(m);
+        smt::kernel * ctx = 0;
+        if (m_max_num_contexts == 0) {
+            m_contexts.push_back(alloc(smt::kernel, m, m_fparams));
+            pred = m.mk_true();
+            ctx = m_contexts[m_num_contexts-1];
+        }
+        else {
+            if (m_contexts.size() < m_max_num_contexts) {
+                m_contexts.push_back(alloc(smt::kernel, m, m_fparams));
+            }
+            std::stringstream name;
+            name << "#context" << m_num_contexts;
+            pred = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort());    
+            m_predicate_list.push_back(pred);
+            m_predicate_set.insert(pred->get_decl());
+            ctx = m_contexts[(m_num_contexts-1)%m_max_num_contexts];
+        }        
+        return  alloc(_smt_context, *ctx, *this, pred);   
+    }
+
+    void smt_context_manager::collect_statistics(statistics& st) const {
+        for (unsigned i = 0; i < m_contexts.size(); ++i) {
+            m_contexts[i]->collect_statistics(st);
+        }
+    }
+
+    void smt_context_manager::reset_statistics() {
+        for (unsigned i = 0; i < m_contexts.size(); ++i) {
+            m_contexts[i]->reset_statistics();
+        }
+    }
+
+
+};
+

src/muz/pdr/pdr_smt_context_manager.h

@@ -0,0 +1,110 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_smt_context_manager.h
+
+Abstract:
+
+    Manager of smt contexts
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2011-11-26.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_SMT_CONTEXT_MANAGER_H_
+#define _PDR_SMT_CONTEXT_MANAGER_H_
+
+#include "smt_kernel.h"
+#include "sat_solver.h"
+#include "func_decl_dependencies.h"
+#include "dl_util.h"
+
+namespace pdr {
+    
+    class smt_context_manager;
+
+    class smt_context {
+    protected:
+        app_ref              m_pred;
+        smt_context_manager& m_parent;
+        bool          m_in_delay_scope;
+        bool          m_pushed;
+    public:
+        smt_context(smt_context_manager& p, ast_manager& m, app* pred);
+        virtual ~smt_context() {}
+        virtual void assert_expr(expr* e) = 0;
+        virtual lbool check(expr_ref_vector& assumptions) = 0;
+        virtual void get_model(model_ref& model) = 0;
+        virtual proof* get_proof() = 0;
+        virtual unsigned get_unsat_core_size() = 0;
+        virtual expr* get_unsat_core_expr(unsigned i) = 0;
+        virtual void push() = 0;
+        virtual void pop() = 0;
+        bool is_aux_predicate(func_decl* p);
+        bool is_aux_predicate(expr* p) { return is_app(p) && is_aux_predicate(to_app(p)->get_decl()); }
+        class scoped {
+            smt_context& m_ctx;
+        public:
+            scoped(smt_context& ctx);
+            ~scoped();
+        };
+    };
+
+    class _smt_context : public smt_context {
+        smt::kernel & m_context;
+    public:
+        _smt_context(smt::kernel & ctx, smt_context_manager& p, app* pred); 
+        virtual ~_smt_context() {}
+        virtual void assert_expr(expr* e);
+        virtual lbool check(expr_ref_vector& assumptions);
+        virtual void get_model(model_ref& model);
+        virtual proof* get_proof();
+        virtual void push() { m_context.push(); }
+        virtual void pop() { m_context.pop(1); }
+        virtual unsigned get_unsat_core_size() { return m_context.get_unsat_core_size(); }
+        virtual expr* get_unsat_core_expr(unsigned i) { return m_context.get_unsat_core_expr(i); }
+    };
+
+    // TBD: 
+    class sat_context : public smt_context {
+        sat::solver m_solver;
+    public:
+        sat_context(smt::kernel & ctx, smt_context_manager& p, app* pred); 
+        virtual ~sat_context() {}
+        virtual void assert_expr(expr* e);
+        virtual lbool check(expr_ref_vector& assumptions);
+        virtual void get_model(model_ref& model);
+        virtual proof* get_proof();
+        virtual void pop() { m_solver.pop(1); }
+        virtual void push() { m_solver.push(); }
+        // TBD: add unsat core extraction with sat::solver.
+        virtual unsigned get_unsat_core_size();
+        virtual expr* get_unsat_core_expr(unsigned i);
+    };
+
+    class smt_context_manager {
+        smt_params&        m_fparams;
+        ast_manager&             m;
+        unsigned                 m_max_num_contexts;
+        ptr_vector<smt::kernel>  m_contexts;
+        unsigned                 m_num_contexts;
+        app_ref_vector           m_predicate_list;
+        func_decl_set            m_predicate_set;        
+    public:
+        smt_context_manager(smt_params& fp, fixedpoint_params const& p, ast_manager& m);
+        ~smt_context_manager();
+        smt_context* mk_fresh();                
+        void collect_statistics(statistics& st) const;
+        void reset_statistics();
+        bool is_aux_predicate(func_decl* p) const { return m_predicate_set.contains(p); }
+    };
+
+};
+
+#endif

src/muz/pdr/pdr_sym_mux.cpp

@@ -0,0 +1,600 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sym_mux.cpp
+
+Abstract:
+
+    A symbol multiplexer that helps with having multiple versions of each of a set of symbols.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-8.
+
+Revision History:
+
+--*/
+
+#include <sstream>
+#include "ast_pp.h"
+#include "for_each_expr.h"
+#include "model.h"
+#include "rewriter.h"
+#include "rewriter_def.h"
+#include "pdr_util.h"
+#include "pdr_sym_mux.h"
+
+using namespace pdr;
+
+sym_mux::sym_mux(ast_manager & m, const vector<std::string> & suffixes)
+    : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
+{
+    unsigned suf_sz = m_suffixes.size();
+    for(unsigned i = 0; i < suf_sz; ++i) {
+        symbol suff_sym = symbol(m_suffixes[i].c_str());
+        m_used_suffixes.insert(suff_sym);
+    }
+}
+
+std::string sym_mux::get_suffix(unsigned i) const {
+    while(m_suffixes.size() <= i) {
+        std::string new_suffix;
+        symbol new_syffix_sym;
+        do {
+            std::stringstream stm;
+            stm<<'_'<<m_next_sym_suffix_idx;
+            m_next_sym_suffix_idx++;
+            new_suffix = stm.str();
+            new_syffix_sym = symbol(new_suffix.c_str());
+        } 
+        while (m_used_suffixes.contains(new_syffix_sym));
+        m_used_suffixes.insert(new_syffix_sym);
+        m_suffixes.push_back(new_suffix);
+    }
+    return m_suffixes[i];
+}
+
+void sym_mux::create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, 
+    unsigned tuple_length, decl_vector & tuple)
+{
+    SASSERT(tuple_length>0);
+    while(tuple.size()<tuple_length) {
+        tuple.push_back(0);
+    }
+    SASSERT(tuple.size()==tuple_length);
+    std::string pre = prefix->get_name().str();
+    for(unsigned i=0; i<tuple_length; i++) {
+
+        if (tuple[i] != 0) {
+            SASSERT(tuple[i]->get_arity()==arity);
+            SASSERT(tuple[i]->get_range()==range);
+            //domain should match as well, but we won't bother checking an array equality
+        }
+        else {
+            std::string name = pre+get_suffix(i);
+            tuple[i] = m.mk_func_decl(symbol(name.c_str()), arity, domain, range);
+        }
+        m_ref_holder.push_back(tuple[i]);
+        m_sym2idx.insert(tuple[i], i);
+        m_sym2prim.insert(tuple[i], tuple[0]);
+    }
+
+    m_prim2all.insert(tuple[0], tuple);
+    m_prefix2prim.insert(prefix, tuple[0]);
+    m_prim2prefix.insert(tuple[0], prefix);
+    m_prim_preds.push_back(tuple[0]);
+    m_ref_holder.push_back(prefix);
+}
+
+void sym_mux::ensure_tuple_size(func_decl * prim, unsigned sz) const {
+    SASSERT(m_prim2all.contains(prim));
+    decl_vector& tuple = m_prim2all.find_core(prim)->get_data().m_value;
+    SASSERT(tuple[0]==prim);
+
+    if(sz <= tuple.size()) { return; }
+
+    func_decl * prefix;
+    TRUSTME(m_prim2prefix.find(prim, prefix));
+    std::string prefix_name = prefix->get_name().bare_str();
+    for(unsigned i=tuple.size(); i<sz; ++i) {
+        std::string name = prefix_name+get_suffix(i);
+        func_decl * new_sym = m.mk_func_decl(symbol(name.c_str()), prefix->get_arity(), 
+            prefix->get_domain(), prefix->get_range());
+
+        tuple.push_back(new_sym);
+        m_ref_holder.push_back(new_sym);
+        m_sym2idx.insert(new_sym, i);
+        m_sym2prim.insert(new_sym, prim);
+    }
+}
+
+func_decl * sym_mux::conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const
+{
+    if(src_idx==tgt_idx) { return sym; }
+    func_decl * prim = (src_idx==0) ? sym : get_primary(sym);
+    if(tgt_idx>src_idx) {
+        ensure_tuple_size(prim, tgt_idx+1);
+    }
+    decl_vector & sym_vect = m_prim2all.find_core(prim)->get_data().m_value;
+    SASSERT(sym_vect[src_idx]==sym);
+    return sym_vect[tgt_idx];
+}
+
+
+func_decl * sym_mux::get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, 
+    unsigned arity, sort * const * domain, sort * range)
+{
+    func_decl * prim = try_get_primary_by_prefix(prefix);
+    if(prim) {
+        SASSERT(prim->get_arity()==arity);
+        SASSERT(prim->get_range()==range);
+        //domain should match as well, but we won't bother checking an array equality
+
+        return conv(prim, 0, idx);
+    }
+
+    decl_vector syms;
+    create_tuple(prefix, arity, domain, range, idx+1, syms);
+    return syms[idx];
+}
+
+bool sym_mux::is_muxed_lit(expr * e, unsigned idx) const
+{
+    if(!is_app(e)) { return false; }
+    app * a = to_app(e);
+    if(m.is_not(a) && is_app(a->get_arg(0))) {
+        a = to_app(a->get_arg(0));
+    }
+    return is_muxed(a->get_decl());
+}
+
+
+struct sym_mux::formula_checker
+{
+    formula_checker(const sym_mux & parent, bool all, unsigned idx) : 
+        m_parent(parent), m_all(all), m_idx(idx),
+        m_found_what_needed(false)
+    {
+    }
+
+    void operator()(expr * e)
+    {
+        if(m_found_what_needed || !is_app(e)) { return; }
+
+        func_decl * sym = to_app(e)->get_decl();
+        unsigned sym_idx;
+        if(!m_parent.try_get_index(sym, sym_idx)) { return; }
+        
+        bool have_idx = sym_idx==m_idx;
+
+        if( m_all ? (!have_idx) : have_idx ) {
+            m_found_what_needed = true;
+        }
+
+    }
+
+    bool all_have_idx() const
+    {
+        SASSERT(m_all); //we were looking for the queried property
+        return !m_found_what_needed;
+    }
+
+    bool some_with_idx() const
+    {
+        SASSERT(!m_all); //we were looking for the queried property
+        return m_found_what_needed;
+    }
+
+private:
+    const sym_mux & m_parent;
+    bool m_all;
+    unsigned m_idx;
+
+    /**
+    If we check whether all muxed symbols are of given index, we look for 
+    counter-examples, checking whether form contains a muxed symbol of an index, 
+    we look for symbol of index m_idx.
+    */
+    bool m_found_what_needed;
+};
+
+bool sym_mux::contains(expr * e, unsigned idx) const
+{
+    formula_checker chck(*this, false, idx);
+    for_each_expr(chck, m_visited, e);
+    m_visited.reset();
+    return chck.some_with_idx();
+}
+
+bool sym_mux::is_homogenous_formula(expr * e, unsigned idx) const
+{
+    formula_checker chck(*this, true, idx);
+    for_each_expr(chck, m_visited, e);
+    m_visited.reset();
+    return chck.all_have_idx();
+}
+
+bool sym_mux::is_homogenous(const expr_ref_vector & vect, unsigned idx) const
+{
+    expr * const * begin = vect.c_ptr();
+    expr * const * end = begin + vect.size();
+    for(expr * const * it = begin; it!=end; it++) {
+        if(!is_homogenous_formula(*it, idx)) {
+            return false;
+        }
+    }
+    return true;
+}
+
+class sym_mux::index_collector {
+    sym_mux const& m_parent;
+    svector<bool> m_indices;
+public:
+    index_collector(sym_mux const& s): 
+      m_parent(s) {}
+
+    void operator()(expr * e) {    
+        if (is_app(e)) {
+            func_decl * sym = to_app(e)->get_decl();
+            unsigned idx;
+            if (m_parent.try_get_index(sym, idx)) { 
+                SASSERT(idx > 0);
+                --idx;
+                if (m_indices.size() <= idx) {
+                    m_indices.resize(idx+1, false);
+                }
+                m_indices[idx] = true;
+            }
+        }
+    }
+
+    void extract(unsigned_vector& indices) {
+        for (unsigned i = 0; i < m_indices.size(); ++i) {
+            if (m_indices[i]) {
+                indices.push_back(i);
+            }
+        }
+    }
+};
+
+
+
+void sym_mux::collect_indices(expr* e, unsigned_vector& indices) const {
+    indices.reset();
+    index_collector collector(*this);
+    for_each_expr(collector, m_visited, e);
+    m_visited.reset();
+    collector.extract(indices);
+}
+
+class sym_mux::variable_collector {
+    sym_mux const& m_parent;
+    vector<ptr_vector<app> >& m_vars;
+public:
+    variable_collector(sym_mux const& s, vector<ptr_vector<app> >& vars): 
+      m_parent(s), m_vars(vars) {}
+
+    void operator()(expr * e) {    
+        if (is_app(e)) {
+            func_decl * sym = to_app(e)->get_decl();
+            unsigned idx;
+            if (m_parent.try_get_index(sym, idx)) { 
+                SASSERT(idx > 0);
+                --idx;
+                if (m_vars.size() <= idx) {
+                    m_vars.resize(idx+1, ptr_vector<app>());
+                }
+                m_vars[idx].push_back(to_app(e));
+            }
+        }
+    }
+};
+
+void sym_mux::collect_variables(expr* e, vector<ptr_vector<app> >& vars) const {
+    vars.reset();
+    variable_collector collector(*this, vars);
+    for_each_expr(collector, m_visited, e);
+    m_visited.reset();
+}
+
+class sym_mux::hmg_checker {
+    const sym_mux & m_parent;
+
+    bool m_found_idx;
+    unsigned m_idx;
+    bool m_multiple_indexes;
+
+public:
+    hmg_checker(const sym_mux & parent) : 
+      m_parent(parent), m_found_idx(false), m_multiple_indexes(false)
+    {
+    }
+
+    void operator()(expr * e)
+    {
+        if(m_multiple_indexes || !is_app(e)) { return; }
+
+        func_decl * sym = to_app(e)->get_decl();
+        unsigned sym_idx;
+        if(!m_parent.try_get_index(sym, sym_idx)) { return; }
+        
+        if(!m_found_idx) {
+            m_found_idx = true;
+            m_idx = sym_idx;
+            return;
+        }
+        if(m_idx==sym_idx) { return; }
+        m_multiple_indexes = true;
+    }
+
+    bool has_multiple_indexes() const
+    {
+        return m_multiple_indexes;
+    }
+};
+
+bool sym_mux::is_homogenous_formula(expr * e) const {
+    hmg_checker chck(*this);
+    for_each_expr(chck, m_visited, e);
+    m_visited.reset();
+    return !chck.has_multiple_indexes();
+}
+
+
+struct sym_mux::conv_rewriter_cfg : public default_rewriter_cfg
+{
+private:
+    ast_manager & m;
+    const sym_mux & m_parent;
+    unsigned m_from_idx;
+    unsigned m_to_idx;
+    bool m_homogenous;
+public:
+    conv_rewriter_cfg(const sym_mux & parent, unsigned from_idx, unsigned to_idx, bool homogenous) 
+        : m(parent.get_manager()), 
+        m_parent(parent), 
+        m_from_idx(from_idx), 
+        m_to_idx(to_idx),
+        m_homogenous(homogenous) {}
+
+    bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+        if(!is_app(s)) { return false; }
+        app * a = to_app(s);
+        func_decl * sym = a->get_decl();
+        if(!m_parent.has_index(sym, m_from_idx)) {
+            SASSERT(!m_homogenous || !m_parent.is_muxed(sym));
+            return false;
+        }
+        func_decl * tgt = m_parent.conv(sym, m_from_idx, m_to_idx);
+
+        t = m.mk_app(tgt, a->get_args());
+        return true;
+    }
+};
+
+void sym_mux::conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous) const
+{
+    if(src_idx==tgt_idx) {
+        res = f;
+        return;
+    }
+    conv_rewriter_cfg r_cfg(*this, src_idx, tgt_idx, homogenous);
+    rewriter_tpl<conv_rewriter_cfg> rwr(m, false, r_cfg);
+    rwr(f, res);
+}
+
+struct sym_mux::shifting_rewriter_cfg : public default_rewriter_cfg
+{
+private:
+    ast_manager & m;
+    const sym_mux & m_parent;
+    int m_shift;
+public:
+    shifting_rewriter_cfg(const sym_mux & parent, int shift) 
+        : m(parent.get_manager()), 
+        m_parent(parent), 
+        m_shift(shift) {}
+
+    bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+        if(!is_app(s)) { return false; }
+        app * a = to_app(s);
+        func_decl * sym = a->get_decl();
+
+        unsigned idx;
+        if(!m_parent.try_get_index(sym, idx)) {
+            return false;
+        }
+        SASSERT(static_cast<int>(idx)+m_shift>=0);
+        func_decl * tgt = m_parent.conv(sym, idx, idx+m_shift);
+        t = m.mk_app(tgt, a->get_args());
+        return true;
+    }
+};
+
+void sym_mux::shift_formula(expr * f, int dist, expr_ref & res) const
+{
+    if(dist==0) {
+        res = f;
+        return;
+    }
+    shifting_rewriter_cfg r_cfg(*this, dist);
+    rewriter_tpl<shifting_rewriter_cfg> rwr(m, false, r_cfg);
+    rwr(f, res);
+}
+
+void sym_mux::conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, 
+    expr_ref_vector & res) const
+{
+    res.reset();
+    expr * const * begin = vect.c_ptr();
+    expr * const * end = begin + vect.size();
+    for(expr * const * it = begin; it!=end; it++) {
+        expr_ref converted(m);
+        conv_formula(*it, src_idx, tgt_idx, converted);
+        res.push_back(converted);
+    }
+}
+
+void sym_mux::filter_idx(expr_ref_vector & vect, unsigned idx) const {
+    unsigned i = 0;
+    while (i < vect.size()) {
+        expr* e = vect[i].get();
+        if(contains(e, idx) && is_homogenous_formula(e, idx)) {
+            i++;
+        }
+        else {
+            //we don't allow mixing states inside vector elements
+            SASSERT(!contains(e, idx));
+            vect[i] = vect.back();
+            vect.pop_back();
+        }
+    }
+}
+
+void sym_mux::partition_o_idx(
+    expr_ref_vector const& lits, 
+    expr_ref_vector& o_lits,
+    expr_ref_vector& other, unsigned idx) const {
+
+    for (unsigned i = 0; i < lits.size(); ++i) {
+        if (contains(lits[i], idx) && is_homogenous_formula(lits[i], idx)) {
+            o_lits.push_back(lits[i]);
+        }
+        else {
+            other.push_back(lits[i]);
+        }
+    }
+}
+
+
+
+class sym_mux::nonmodel_sym_checker {
+    const sym_mux & m_parent;
+
+    bool m_found;
+public:
+    nonmodel_sym_checker(const sym_mux & parent) : 
+      m_parent(parent), m_found(false)
+    {
+    }
+
+    void operator()(expr * e)
+    {
+        if(m_found || !is_app(e)) { return; }
+
+        func_decl * sym = to_app(e)->get_decl();
+
+        if(m_parent.is_non_model_sym(sym)) {
+            m_found = true;
+        }
+    }
+
+    bool found() const
+    {
+        return m_found;
+    }
+};
+
+bool sym_mux::has_nonmodel_symbol(expr * e) const {
+    nonmodel_sym_checker chck(*this);
+    for_each_expr(chck, e);
+    return chck.found();
+}
+
+void sym_mux::filter_non_model_lits(expr_ref_vector & vect) const {
+    unsigned i=0;
+    while(i<vect.size()) {
+        if(!has_nonmodel_symbol(vect[i].get())) {
+            i++;
+            continue;
+        }
+        vect[i] = vect.back();
+        vect.pop_back();
+    }
+}
+
+class sym_mux::decl_idx_comparator
+{
+    const sym_mux & m_parent;
+public:
+    decl_idx_comparator(const sym_mux & parent)
+        : m_parent(parent)
+    { }
+
+    bool operator()(func_decl * sym1, func_decl * sym2)
+    {
+        unsigned idx1, idx2;
+        if(!m_parent.try_get_index(sym1, idx1)) { idx1 = UINT_MAX; }
+        if(!m_parent.try_get_index(sym2, idx2)) { idx2 = UINT_MAX; }
+
+        if(idx1!=idx2) { return idx1<idx2; }
+        return lt(sym1->get_name(), sym2->get_name());
+    }
+};
+
+std::string sym_mux::pp_model(const model_core & mdl) const {
+    decl_vector consts;
+    unsigned sz = mdl.get_num_constants();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * d = mdl.get_constant(i);
+        consts.push_back(d);
+    }
+
+    std::sort(consts.begin(), consts.end(), decl_idx_comparator(*this));
+
+    std::stringstream res;
+
+    decl_vector::iterator end = consts.end();
+    for(decl_vector::iterator it = consts.begin(); it!=end; it++) {
+        func_decl * d = *it;
+        std::string name   = d->get_name().str();
+        const char * arrow = " -> "; 
+        res << name << arrow;
+        unsigned indent = static_cast<unsigned>(name.length() + strlen(arrow));
+        res << mk_pp(mdl.get_const_interp(d), m, indent) << "\n";
+
+        if(it+1!=end) {
+            unsigned idx1, idx2;
+            if(!try_get_index(*it, idx1)) { idx1 = UINT_MAX; }
+            if(!try_get_index(*(it+1), idx2)) { idx2 = UINT_MAX; }
+            if(idx1!=idx2) { res << "\n"; }
+        }
+    }
+    return res.str();
+}
+
+
+#if 0
+
+class sym_mux::index_renamer_cfg : public default_rewriter_cfg{
+    const sym_mux & m_parent;
+    unsigned        m_idx;
+
+public:
+    index_renamer_cfg(const sym_mux & p, unsigned idx) : m_parent(p), m_idx(idx) {}
+
+    bool get_subst(expr * s, expr * & t, proof * & t_pr) {
+        if (!is_app(s)) return false;
+        app * a = to_app(s);
+        if (a->get_family_id() != null_family_id) {
+            return false;
+        }
+        func_decl * sym = a->get_decl();
+        unsigned idx;
+        if(!m_parent.try_get_index(sym, idx)) {
+            return false;
+        }        
+        if (m_idx == idx) {
+            return false;
+        }
+        ast_manager& m = m_parent.get_manager();
+        symbol name = symbol((sym->get_name().str() + "!").c_str());
+        func_decl * tgt = m.mk_func_decl(name, sym->get_arity(), sym->get_domain(), sym->get_range());
+        t = m.mk_app(tgt, a->get_num_args(), a->get_args());
+        return true;    
+    }
+};
+
+#endif

src/muz/pdr/pdr_sym_mux.h

@@ -0,0 +1,249 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sym_mux.h
+
+Abstract:
+
+    A symbol multiplexer that helps with having multiple versions of each of a set of symbols.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-9-8.
+
+Revision History:
+
+--*/
+
+#ifndef _SYM_MUX_H_
+#define _SYM_MUX_H_
+
+#include "ast.h"
+#include "map.h"
+#include "vector.h"
+
+class model_core;
+
+namespace pdr {
+class sym_mux
+{
+public:
+    typedef ptr_vector<app> app_vector;
+    typedef ptr_vector<func_decl> decl_vector;
+private:
+    typedef obj_map<func_decl,unsigned> sym2u;
+    typedef obj_map<func_decl, decl_vector> sym2dv;
+    typedef obj_map<func_decl,func_decl *> sym2sym;
+    typedef obj_map<func_decl, func_decl *> sym2pred;
+    typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbols;
+
+    ast_manager &           m;
+    mutable ast_ref_vector  m_ref_holder;
+    mutable expr_mark       m_visited;
+
+    mutable unsigned       m_next_sym_suffix_idx;
+    mutable symbols        m_used_suffixes;
+    /** Here we have default suffixes for each of the variants */
+    mutable vector<std::string> m_suffixes;
+
+
+    /**
+       Primary symbol is the 0-th variant. This member maps from primary symbol
+       to vector of all its variants (including the primary variant).
+    */
+    sym2dv m_prim2all;
+
+    /**
+       For each symbol contains its variant index
+    */
+    mutable sym2u m_sym2idx;
+    /**
+       For each symbol contains its primary variant
+    */
+    mutable sym2sym m_sym2prim;
+
+    /**
+       Maps prefixes passed to the create_tuple to 
+       the primary symbol created from it.
+    */
+    sym2pred m_prefix2prim;
+
+    /**
+       Maps pripary symbols to prefixes that were used to create them.
+    */
+    sym2sym     m_prim2prefix;
+
+    decl_vector m_prim_preds;
+
+    obj_hashtable<func_decl> m_non_model_syms;
+
+    struct formula_checker;
+    struct conv_rewriter_cfg;
+    struct shifting_rewriter_cfg;
+    class decl_idx_comparator;
+    class hmg_checker;
+    class nonmodel_sym_checker;
+    class index_renamer_cfg;
+    class index_collector;
+    class variable_collector;
+
+    std::string get_suffix(unsigned i) const;
+    void ensure_tuple_size(func_decl * prim, unsigned sz) const;
+
+    expr_ref isolate_o_idx(expr* e, unsigned idx) const;
+public:
+    sym_mux(ast_manager & m, const vector<std::string> & suffixes);
+
+    ast_manager & get_manager() const { return m; }
+
+    bool is_muxed(func_decl * sym) const { return m_sym2idx.contains(sym); }
+
+    bool try_get_index(func_decl * sym, unsigned & idx) const {
+        return m_sym2idx.find(sym,idx);
+    }
+
+    bool has_index(func_decl * sym, unsigned idx) const {
+        unsigned actual_idx;
+        return try_get_index(sym, actual_idx) && idx==actual_idx;
+    }
+
+    /** Return primary symbol. sym must be muxed. */
+    func_decl * get_primary(func_decl * sym) const {
+        func_decl * prim;
+        TRUSTME(m_sym2prim.find(sym, prim));
+        return prim;
+    }
+
+    /**
+    Return primary symbol created from prefix, or 0 if the prefix was never used.
+    */
+    func_decl * try_get_primary_by_prefix(func_decl* prefix) const {
+        func_decl * res;
+        if(!m_prefix2prim.find(prefix, res)) {
+            return 0;
+        }
+        return res;
+    }
+
+    /**
+    Return symbol created from prefix, or 0 if the prefix was never used.
+    */
+    func_decl * try_get_by_prefix(func_decl* prefix, unsigned idx) const {
+        func_decl * prim = try_get_primary_by_prefix(prefix);
+        if(!prim) {
+            return 0;
+        }
+        return conv(prim, 0, idx);
+    }
+
+    /**
+    Marks symbol as non-model which means it will not appear in models collected by 
+    get_muxed_cube_from_model function.
+    This is to take care of auxiliary symbols introduced by the disjunction relations
+    to relativize lemmas coming from disjuncts.
+    */
+    void mark_as_non_model(func_decl * sym) {
+        SASSERT(is_muxed(sym));
+        m_non_model_syms.insert(get_primary(sym));
+    }
+
+    func_decl * get_or_create_symbol_by_prefix(func_decl* prefix, unsigned idx, 
+        unsigned arity, sort * const * domain, sort * range);
+
+
+
+    bool is_muxed_lit(expr * e, unsigned idx) const;
+
+    bool is_non_model_sym(func_decl * s) const { 
+        return is_muxed(s) && m_non_model_syms.contains(get_primary(s));
+    }
+
+    /**
+    Create a multiplexed tuple of propositional constants.
+    Symbols may be suplied in the tuple vector,
+    those beyond the size of the array and those with corresponding positions 
+    assigned to zero will be created using prefix.
+    Tuple length must be at least one.
+    */
+    void create_tuple(func_decl* prefix, unsigned arity, sort * const * domain, sort * range, 
+        unsigned tuple_length, decl_vector & tuple);
+
+    /**
+    Return true if the only multiplexed symbols which e contains are of index idx.
+    */
+    bool is_homogenous_formula(expr * e, unsigned idx) const;
+    bool is_homogenous(const expr_ref_vector & vect, unsigned idx) const;
+
+    /**
+    Return true if all multiplexed symbols which e contains are of one index.
+    */
+    bool is_homogenous_formula(expr * e) const;
+
+    /**
+    Return true if expression e contains a muxed symbol of index idx.
+    */
+    bool contains(expr * e, unsigned idx) const;
+
+    /**
+        Collect indices used in expression.
+    */
+    void collect_indices(expr* e, unsigned_vector& indices) const;
+
+    /**
+        Collect used variables of each index.
+    */
+    void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const;
+
+    /**
+    Convert symbol sym which has to be of src_idx variant into variant tgt_idx.
+    */
+    func_decl * conv(func_decl * sym, unsigned src_idx, unsigned tgt_idx) const;
+
+    
+    /**
+    Convert src_idx symbols in formula f variant into tgt_idx.
+    If homogenous is true, formula cannot contain symbols of other variants.
+    */
+    void conv_formula(expr * f, unsigned src_idx, unsigned tgt_idx, expr_ref & res, bool homogenous=true) const;
+    void conv_formula_vector(const expr_ref_vector & vect, unsigned src_idx, unsigned tgt_idx, 
+        expr_ref_vector & res) const;
+
+    /**
+    Shifts the muxed symbols in f by dist. Dist can be negative, but it should never shift 
+    symbol index to a negative value.
+    */
+    void shift_formula(expr * f, int dist, expr_ref & res) const;
+
+    /**
+    Remove from vect literals (atoms or negations of atoms) of symbols
+    that contain multiplexed symbols with indexes other than idx.
+
+    Each of the literals can contain only symbols multiplexed with one index
+    (this trivially holds if the literals are propositional).
+
+    Order of elements in vect may be modified by this function
+    */
+    void filter_idx(expr_ref_vector & vect, unsigned idx) const;
+
+    /**
+        Partition literals into o_literals and others.
+    */
+    void partition_o_idx(expr_ref_vector const& lits, 
+                         expr_ref_vector& o_lits,
+                         expr_ref_vector& other, unsigned idx) const;
+
+    bool has_nonmodel_symbol(expr * e) const;
+    void filter_non_model_lits(expr_ref_vector & vect) const;
+
+    func_decl * const * begin_prim_preds() const { return m_prim_preds.begin(); }
+    func_decl * const * end_prim_preds() const { return m_prim_preds.end(); }
+
+    void get_muxed_cube_from_model(const model_core & model, expr_ref_vector & res) const;
+
+    std::string pp_model(const model_core & mdl) const;
+};
+}
+
+#endif

src/muz/pdr/pdr_util.h

@@ -0,0 +1,169 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    pdr_util.h
+
+Abstract:
+
+    Utility functions for PDR.
+
+Author:
+
+    Krystof Hoder (t-khoder) 2011-8-19.
+
+Revision History:
+
+--*/
+
+#ifndef _PDR_UTIL_H_
+#define _PDR_UTIL_H_
+
+#include "ast.h"
+#include "ast_pp.h"
+#include "obj_hashtable.h"
+#include "ref_vector.h"
+#include "simplifier.h"
+#include "trace.h"
+#include "vector.h"
+#include "arith_decl_plugin.h"
+#include "array_decl_plugin.h"
+#include "bv_decl_plugin.h"
+
+
+class model;
+class model_core;
+
+namespace pdr {
+
+    /**
+     * Return the ceiling of base 2 logarithm of a number, 
+     * or zero if the nmber is zero.
+     */
+    unsigned ceil_log2(unsigned u);
+
+    typedef ptr_vector<app> app_vector;
+    typedef ptr_vector<func_decl> decl_vector;
+    typedef obj_hashtable<func_decl> func_decl_set;
+    
+    std::string pp_cube(const ptr_vector<expr>& model, ast_manager& manager);
+    std::string pp_cube(const expr_ref_vector& model, ast_manager& manager);
+    std::string pp_cube(const ptr_vector<app>& model, ast_manager& manager);
+    std::string pp_cube(const app_ref_vector& model, ast_manager& manager);
+    std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager);
+    std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager);
+    
+    class model_evaluator {
+        ast_manager&           m;
+        arith_util             m_arith;
+        array_util             m_array;
+        obj_map<expr,rational> m_numbers;
+        expr_ref_vector        m_refs;
+        obj_map<expr, expr*>   m_values;
+        model_ref              m_model;
+        
+        //00 -- non-visited
+        //01 -- X
+        //10 -- false
+        //11 -- true
+        expr_mark      m1;
+        expr_mark      m2;
+        expr_mark      m_visited;
+        
+
+        void reset();
+        void setup_model(model_ref& model);
+        void assign_value(expr* e, expr* v);
+        void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
+        void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
+        expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
+        void eval_arith(app* e);
+        void eval_basic(app* e);
+        void eval_eq(app* e, expr* arg1, expr* arg2);
+        void eval_array_eq(app* e, expr* arg1, expr* arg2);
+        void inherit_value(expr* e, expr* v);
+        
+        inline bool is_unknown(expr* x)  { return !m1.is_marked(x) && !m2.is_marked(x); }
+        inline void set_unknown(expr* x)  { m1.mark(x, false); m2.mark(x, false); }
+        inline bool is_x(expr* x)  { return !m1.is_marked(x) && m2.is_marked(x); }
+        inline bool is_false(expr* x)  { return m1.is_marked(x) && !m2.is_marked(x); }
+        inline bool is_true(expr* x)  { return m1.is_marked(x) && m2.is_marked(x); }
+        inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
+        inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+        inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+        inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
+        inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
+        inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
+        inline void set_number(expr* x, rational const& v) { 
+            set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); 
+        }
+        inline expr* get_value(expr* x) { return m_values.find(x); }
+        inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
+        
+        bool check_model(ptr_vector<expr> const & formulas);
+
+        bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case);
+
+        void eval_exprs(expr_ref_vector& es);
+        
+    public:
+        model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {}
+            
+        /**
+           \brief extract equalities from model that suffice to satisfy formula.
+               
+           \pre model satisfies formulas
+        */
+            
+       expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
+            
+       /**
+          \brief extract literals from formulas that satisfy formulas.
+
+          \pre model satisfies formulas
+       */
+       expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
+
+       /** 
+           for_each_expr visitor.
+       */
+       void operator()(expr* e) {} 
+
+       expr_ref eval(model_ref& mdl, expr* e);
+
+       expr_ref eval(model_ref& mdl, func_decl* d);
+    };
+
+    /**
+       \brief replace variables that are used in many disequalities by
+       an equality using the model. 
+       
+       Assumption: the model satisfies the conjunctions.       
+     */
+    void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml);
+
+    
+
+    /**
+       \brief hoist non-boolean if expressions.
+     */
+    void hoist_non_bool_if(expr_ref& fml);
+
+
+    /**
+       \brief normalize coefficients in polynomials so that least coefficient is 1.
+     */
+    void normalize_arithmetic(expr_ref& t);
+
+
+    /**
+       \brief determine if formulas belong to difference logic or UTVPI fragment.
+     */
+    bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
+
+    bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
+
+}
+
+#endif