Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

scripts/mk_util.py

@@ -1785,7 +1785,7 @@ def update_version():
         raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
     if not ONLY_MAKEFILES:
         mk_version_dot_h(major, minor, build, revision)
-        update_all_assembly_infos(major, minor, build, revision)
+        mk_all_assembly_infos(major, minor, build, revision)
         mk_def_files()
         
 # Update files with the version number
@@ -1800,49 +1800,32 @@ def mk_version_dot_h(major, minor, build, revision):
     if VERBOSE:
         print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
 
-# Update version number in AssemblyInfo.cs files
+# Generate AssemblyInfo.cs files with the right version numbers by using AssemblyInfo files as a template
-def update_all_assembly_infos(major, minor, build, revision):
+def mk_all_assembly_infos(major, minor, build, revision):
     for c in get_components():
         if c.has_assembly_info():
-            assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo.cs')
+            assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo')
             if os.path.exists(assembly):
                 # It is a CS file
-                update_assembly_info_version(assembly,
+                mk_assembly_info_version(assembly, major, minor, build, revision)
-                                             major, minor, build, revision, False)
             else:
-                assembly = os.path.join(c.src_dir, c.assembly_info_dir, 'AssemblyInfo.cs')
+                raise MKException("Failed to find assembly info file 'AssemblyInfo' at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
-                if os.path.exists(assembly):
-                    # It is a cpp file
-                    update_assembly_info_version(assembly,
-                                                 major, minor, build, revision, True)
-                else:
-                    raise MKException("Failed to find assembly info file at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
                     
                 
-# Update version number in the given AssemblyInfo.cs files
+# Generate version number in the given 'AssemblyInfo.cs' file using 'AssemblyInfo' as a template.
-def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is_cpp=False):
+def mk_assembly_info_version(assemblyinfo, major, minor, build, revision):
-    if is_cpp:
+    ver_pat   = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
-        ver_pat   = re.compile('[assembly:AssemblyVersionAttribute\("[\.\d]*"\) *')
+    fver_pat  = re.compile('[assembly: AssemblyFileVersion\("[\.\d]*"\) *')
-        fver_pat  = re.compile('[assembly:AssemblyFileVersionAttribute\("[\.\d]*"\) *')
-    else:
-        ver_pat   = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
-        fver_pat  = re.compile('[assembly: AssemblyFileVersion\("[\.\d]*"\) *')
     fin  = open(assemblyinfo, 'r')
-    tmp  = '%s.new' % assemblyinfo
+    tmp  = '%s.cs' % assemblyinfo
     fout = open(tmp, 'w')
     num_updates = 0
     for line in fin:
         if ver_pat.match(line):
-            if is_cpp:
+            fout.write('[assembly: AssemblyVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
-                fout.write('[assembly:AssemblyVersionAttribute("%s.%s.%s.%s")];\n' % (major, minor, build, revision))
-            else:
-                fout.write('[assembly: AssemblyVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
             num_updates = num_updates + 1
         elif fver_pat.match(line):
-            if is_cpp:
+            fout.write('[assembly: AssemblyFileVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
-                fout.write('[assembly:AssemblyFileVersionAttribute("%s.%s.%s.%s")];\n' % (major, minor, build, revision))
-            else:
-                fout.write('[assembly: AssemblyFileVersion("%s.%s.%s.%s")]\n' % (major, minor, build, revision))
             num_updates = num_updates + 1
         else:
             fout.write(line)
@@ -1851,7 +1834,6 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is
     assert num_updates == 2, "unexpected number of version number updates"
     fin.close()
     fout.close()
-    shutil.move(tmp, assemblyinfo)
     if VERBOSE:
         print("Updated '%s'" % assemblyinfo)
 

src/api/api_datalog.cpp

@@ -48,8 +48,11 @@ namespace api {
         if (!m.has_plugin(name)) {
             m.register_plugin(name, alloc(datalog::dl_decl_plugin));
         }        
-        datalog::relation_manager& r = m_context.get_rel_context().get_rmanager();
+        datalog::rel_context* rel = m_context.get_rel_context();
-        r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
+        if (rel) {
+            datalog::relation_manager& r = rel->get_rmanager();
+            r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
+        }
     }        
     
     void fixedpoint_context::reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) {

src/api/java/Status.java

@@ -12,7 +12,7 @@ package com.microsoft.z3;
 public enum Status
 {
     // / Used to signify an unsatisfiable status.
-    UNSATISFIABLE(1),
+    UNSATISFIABLE(-1),
 
     // / Used to signify an unknown status.
     UNKNOWN(0),

src/api/z3_api.h

@@ -778,11 +778,11 @@ typedef enum
         }
         or
         \nicebox{
-             (=> (and ln+1 ln+2 .. ln+m) l0)
+             (=> (and l1 l2 .. ln) l0)
         }
         or in the most general (ground) form:
         \nicebox{
-             (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
+             (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))
         }
         In other words we use the following (Prolog style) convention for Horn 
         implications:
@@ -798,7 +798,7 @@ typedef enum
         general non-ground form is:
 
         \nicebox{
-             (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1)))
+             (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))
         }
 
         The hyper-resolution rule takes a sequence of parameters.

src/ast/rewriter/expr_safe_replace.cpp

@@ -106,3 +106,10 @@ void expr_safe_replace::reset() {
     m_dst.reset();
     m_subst.reset();
 }
+
+void expr_safe_replace::apply_substitution(expr* s, expr* def, expr_ref& t) {
+    reset();
+    insert(s, def);
+    (*this)(t, t);
+    reset();
+}

src/ast/rewriter/expr_safe_replace.h

@@ -39,6 +39,8 @@ public:
 
     void operator()(expr* src, expr_ref& e);
 
+    void apply_substitution(expr* s, expr* def, expr_ref& t);
+
     void reset();
 };
 

src/muz_qe/clp_context.cpp

@@ -205,6 +205,7 @@ namespace datalog {
     };
     
     clp::clp(context& ctx):
+        engine_base(ctx.get_manager(), "clp"),
         m_imp(alloc(imp, ctx)) {        
     }
     clp::~clp() {

src/muz_qe/clp_context.h

@@ -22,23 +22,24 @@ Revision History:
 #include "ast.h"
 #include "lbool.h"
 #include "statistics.h"
+#include "dl_util.h"
 
 namespace datalog {
     class context;
 
-    class clp {
+    class clp : public datalog::engine_base {
         class imp;
         imp* m_imp;
     public:
         clp(context& ctx);
         ~clp();
-        lbool query(expr* query);
+        virtual lbool query(expr* query);
-        void cancel();
+        virtual void cancel();
-        void cleanup();
+        virtual void cleanup();
-        void reset_statistics();
+        virtual void reset_statistics();
-        void collect_statistics(statistics& st) const;
+        virtual void collect_statistics(statistics& st) const;
-        void display_certificate(std::ostream& out) const;        
+        virtual void display_certificate(std::ostream& out) const;        
-        expr_ref get_answer();
+        virtual expr_ref get_answer();
     };
 };
 

src/muz_qe/dl_bmc_engine.cpp

@@ -1416,6 +1416,7 @@ namespace datalog {
     };
     
     bmc::bmc(context& ctx): 
+        engine_base(ctx.get_manager(), "bmc"),
         m_ctx(ctx), 
         m(ctx.get_manager()), 
         m_solver(m, m_fparams),

src/muz_qe/dl_bmc_engine.h

@@ -30,7 +30,7 @@ Revision History:
 namespace datalog {
     class context;
 
-    class bmc {
+    class bmc : public engine_base {
         context&         m_ctx;
         ast_manager&     m;
         smt_params       m_fparams;

src/muz_qe/dl_boogie_proof.cpp

@@ -0,0 +1,297 @@
+/**
+
+Example from Boogie:
+
+(derivation
+(step s!4 (main_loop_LoopHead true true)
+ rule!3  (subst
+    (= assertsPassed@@1 true)
+    (= assertsPassed@2@@0 true)
+    (= main_loop_LoopHead_assertsPassed true)
+  )
+  (labels @950 +895 +668 +670 +893 +899  )
+  (ref  true  ))
+(step s!3 (main true false)
+ rule!1  (subst
+    (= assertsPassed true)
+    (= assertsPassed@0 true)
+    (= assertsPassed@2 false)
+    (= main_assertsPassed false)
+  )
+  (labels @839 +763 +547 +546 +761 +544 +545 +si_fcall_805 +681 +768  )
+  (ref  s!4  ))
+(step s!2 (main_SeqInstr true false)
+ rule!2  (subst
+    (= assertsPassed@@0 true)
+    (= assertsPassed@0@@0 false)
+    (= main_SeqInstr_assertsPassed false)
+  )
+  (labels @890 +851 +572 +si_fcall_883 +853  )
+  (ref  s!3  ))
+(step s!1 (@Fail!0)
+ rule!4  (subst
+    (= assertsPassed@@2 true)
+    (= main_SeqInstr_assertsPassed@@0 false)
+  )
+  (labels  )
+  (ref  s!2  ))
+)
+(model
+"tickleBool -> {
+  true -> true
+  false -> true
+  else -> true
+}
+")
+*/
+
+#include "dl_boogie_proof.h"
+#include "model_pp.h"
+#include "proof_utils.h"
+#include "ast_pp.h"
+#include "dl_util.h"
+
+namespace datalog {
+    
+    /**
+       \brief push hyper-resolution steps upwards such that every use of
+       hyper-resolution uses a premise that is not derived from hyper-resolution.
+              
+       perform the following rewrite:
+       
+       hr(hr(p1,p2,p3,..),p4,p5) => hr(p1,hr(p2,p4),p3,..,p5)
+      
+    */
+
+    void mk_input_resolution(proof_ref& pr) {
+        ast_manager& m = pr.get_manager();
+        proof_ref pr1(m);
+        proof_ref_vector premises1(m), premises2(m), premises(m);
+        expr_ref conclusion1(m), conclusion2(m), conclusion(m);
+        svector<std::pair<unsigned, unsigned> > positions1, positions2, positions;
+        vector<expr_ref_vector> substs1, substs2, substs;
+        
+        if (m.is_hyper_resolve(pr, premises1, conclusion1, positions1, substs1) &&
+            m.is_hyper_resolve(premises1[0].get(), premises, conclusion2, positions, substs2)) {
+            for (unsigned i = 1; i < premises1.size(); ++i) {
+                pr1 = premises1[i].get();
+                mk_input_resolution(pr1);
+                premises1[i] = pr1;
+            }
+            for (unsigned i = 0; i < premises.size(); ++i) {
+                pr1 = premises[i].get();
+                mk_input_resolution(pr1);
+                premises[i] = pr1;
+            }
+            unsigned sz = premises.size();
+            for (unsigned i = 1; i < sz; ++i) {
+                proof* premise = premises[i].get();
+                expr_ref_vector literals(m);
+                expr* l1, *l2;
+                if (!m.is_implies(premise, l1, l2)) {
+                    continue;
+                }
+                datalog::flatten_and(l1, literals);
+                positions2.reset();
+                premises2.reset();
+                premises2.push_back(premise);       
+                substs2.reset();
+                for (unsigned j = 0; j < literals.size(); ++j) {
+                    expr* lit = literals[j].get();
+                    for (unsigned k = 1; k < premises1.size(); ++k) {
+                        if (m.get_fact(premises1[k].get()) == lit) {
+                            premises2.push_back(premises1[k].get());
+                            positions2.push_back(std::make_pair(j+1,0));
+                            substs2.push_back(expr_ref_vector(m));
+                            break;
+                        }
+                    }
+                }
+                premises[i] = m.mk_hyper_resolve(premises2.size(), premises2.c_ptr(), l2, positions2, substs2);
+            }        
+            conclusion = conclusion1;
+            pr = m.mk_hyper_resolve(premises.size(), premises.c_ptr(), conclusion, positions, substs);
+        }
+    }
+    
+    void boogie_proof::set_proof(proof* p) {
+        std::cout << "set proof\n";
+        m_proof = p;
+        proof_utils::push_instantiations_up(m_proof);
+        mk_input_resolution(m_proof);
+        std::cout << "proof set\n";
+    }
+        
+    void boogie_proof::set_model(model* m) {
+        m_model = m;
+    }
+    
+    void boogie_proof::pp(std::ostream& out) {
+        if (m_proof) {
+            pp_proof(out);
+        }
+        if (m_model) {
+            model_pp(out, *m_model);
+        }
+    }
+
+    void boogie_proof::pp_proof(std::ostream& out) {
+        vector<step> steps;
+        ptr_vector<proof> rules;
+        rules.push_back(m_proof);
+        steps.push_back(step());
+        obj_map<proof, unsigned> index;
+        index.insert(m_proof, 0);
+		
+        for (unsigned j = 0; j < rules.size(); ++j) {
+            proof* p = rules[j];
+            proof_ref_vector premises(m);
+            expr_ref conclusion(m);
+            svector<std::pair<unsigned, unsigned> >  positions;
+            vector<expr_ref_vector> substs;
+
+            expr* tmp;
+            steps[j].m_fact = m.get_fact(p);
+            m.is_implies(steps[j].m_fact, tmp, steps[j].m_fact);
+            get_subst(p, steps[j].m_subst);
+            get_labels(p, steps[j].m_labels);
+
+            if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {
+                for (unsigned i = 1; i < premises.size(); ++i) {
+                    proof* premise = premises[i].get();
+                    unsigned position = 0;
+                    if (!index.find(premise, position)) {
+                        position = rules.size();
+                        rules.push_back(premise);
+                        steps.push_back(step());
+                        index.insert(premise, position);
+                    }   
+                    steps[j].m_refs.push_back(position);
+                }
+                get_rule_name(premises[0].get(), steps[j].m_rule_name);
+            }
+        }
+        for (unsigned j = steps.size(); j > 0; ) {
+            --j;
+            step &s = steps[j];
+
+            // TBD
+            s.m_labels;
+
+            // set references, compensate for reverse ordering.
+            for (unsigned i = 0; i < s.m_refs.size(); ++i) {
+                s.m_refs[i] = rules.size()-1-s.m_refs[i];
+            }
+        }
+        steps.reverse();
+        pp_steps(out, steps);
+    }
+
+    /**
+       \brief extract the instantiation by searching for the first occurrence of a hyper-resolution
+       rule that produces an instance.
+     */
+    void boogie_proof::get_subst(proof* p, subst& s) {
+        ptr_vector<proof> todo;
+        todo.push_back(p);
+        ast_mark visited;
+        std::cout << "get_subst\n" << mk_pp(p, m) << "\n";
+        while (!todo.empty()) {
+            proof* p = todo.back();
+            todo.pop_back();
+            if (visited.is_marked(p)) {
+                continue;
+            }
+            visited.mark(p, true);
+            proof_ref_vector premises(m);
+            expr_ref conclusion(m);
+            svector<std::pair<unsigned, unsigned> >  positions;
+            vector<expr_ref_vector> substs;
+            if (m.is_hyper_resolve(p, premises, conclusion, positions, substs)) {               
+                expr_ref_vector const& sub = substs[0];
+                if (!sub.empty()) {
+                    quantifier* q = to_quantifier(m.get_fact(premises[0].get()));
+                    unsigned sz = sub.size();
+                    SASSERT(sz == q->get_num_decls());
+                    for (unsigned i = 0; i < sz; ++i) {
+                        s.push_back(std::make_pair(q->get_decl_name(sz-1-i), sub[i]));
+                    }
+                    return;
+                }
+            }
+            unsigned sz = m.get_num_parents(p);
+            for (unsigned i = 0; i < sz; ++i) {
+                todo.push_back(m.get_parent(p, i));
+            }
+        }
+    }
+
+    void boogie_proof::get_rule_name(proof* p, symbol& n) {
+
+    }
+
+    void boogie_proof::get_labels(proof* p, labels& lbls) {
+        
+    }
+
+    void boogie_proof::pp_steps(std::ostream& out, vector<step>& steps) {
+        out << "(derivation\n";
+        for (unsigned i = 0; i < steps.size(); ++i) {
+            pp_step(out, i, steps[i]);
+        }
+        out << ")\n";
+
+    }
+
+    // step       :: "(" "step" step-name fact rule-name subst labels premises ")"
+    void boogie_proof::pp_step(std::ostream& out, unsigned id, step& s) {
+        out << "(step\n";
+        out << " s!" << id << " "; 
+        pp_fact(out, s.m_fact);
+        out << " " << s.m_rule_name << "\n";
+        pp_subst(out << " ", s.m_subst);
+        pp_labels(out << " ", s.m_labels);
+        pp_premises(out << " ", s.m_refs);
+        out << ")\n";
+    }
+
+    // fact       :: "(" predicate theory-term* ")"
+    void boogie_proof::pp_fact(std::ostream& out, expr* fact) {
+        out << mk_pp(fact, m) << "\n";
+    }
+
+    // subst      :: "(" "subst" assignment* ")"
+    void boogie_proof::pp_subst(std::ostream& out, subst& s) {
+        out << "(subst";
+        for (unsigned i = 0; i < s.size(); ++i) {
+            pp_assignment(out, s[i].first, s[i].second);
+        }
+        out << ")\n";
+    }
+
+    // assignment :: "(" "=" variable theory-term ")"
+    void boogie_proof::pp_assignment(std::ostream& out, symbol const& v, expr* t) {
+        out << "\n  (= " << v << " " << mk_pp(t, m) << ")";
+    }
+
+
+    // labels     :: "(" "labels" label* ")"
+    void boogie_proof::pp_labels(std::ostream& out, labels& lbls) {
+        out << "(labels";
+        for (unsigned i = 0; i < lbls.size(); ++i) {
+            out << " " << lbls[i];
+        }
+        out << ")\n";
+    }
+
+    // premises "(" "ref" step-name* ")"
+    void boogie_proof::pp_premises(std::ostream& out, refs& refs) {
+        out << "(ref";
+        for (unsigned i = 0; i < refs.size(); ++i) {
+            out << " s!" << refs[i];
+        }
+        out << ")\n";
+    }
+
+
+}

src/muz_qe/dl_boogie_proof.h

@@ -0,0 +1,87 @@
+/**
+
+output     :: derivation model
+
+derivation :: "(" "derivation" step* ")"
+
+step       :: "(" "step" step-name fact rule-name subst labels premises ")"
+
+step-name  :: identifier
+
+rule-name  :: identifier
+
+fact       :: "(" predicate theory-term* ")"
+
+subst      :: "(" "subst" assignment* ")"
+
+assignment :: "(" "=" variable theory-term ")"
+
+labels     :: "(" "labels" label* ")"
+
+premises   :: "(" "ref" step-name* ")"
+
+model      :: "(" "model" smtlib2-model ")"
+
+In each step the "fact" is derivable by hyper-resolution from the named 
+premises and the named rule, under the given substitution for the 
+universally quantified variables in the rule. The premises of each 
+step must have occurred previously in the step sequence. The last fact 
+is a nullary placeholder predicate representing satisfaction of the query 
+(its name is arbitrary).
+
+The labels list consists of all the positively labeled sub-formulas whose 
+truth is used in the proof, and all the negatively labeled formulas whose 
+negation is used. A theory-term is a ground term using only interpreted 
+constants of the background theories.
+
+The smtlib2-model gives an interpretation of the uninterpreted constants 
+in the background theory under which the derivation is valid. Currently 
+it is a quoted string in the old z3 model format, for compatibility with 
+Boogie, however, this should be changed to the new model format (using 
+define-fun) when Boogie supports this.
+
+*/
+
+#include "ast.h"
+#include "model.h"
+
+namespace datalog {
+    class boogie_proof {
+        typedef vector<std::pair<symbol,expr*> > subst;
+        typedef svector<symbol> labels;
+        typedef unsigned_vector  refs;
+        struct step {
+            symbol m_rule_name;
+            expr*  m_fact;
+            subst  m_subst;
+            labels m_labels;
+            refs   m_refs;
+        };
+
+        ast_manager& m;
+        proof_ref    m_proof;
+        model_ref    m_model;
+
+        void pp_proof(std::ostream& out);
+        void pp_steps(std::ostream& out, vector<step>& steps);
+        void pp_step(std::ostream& out, unsigned i, step& s);
+        void pp_fact(std::ostream& out, expr* fact);
+        void pp_subst(std::ostream& out, subst& s);
+        void pp_assignment(std::ostream& out, symbol const& v, expr* t);
+        void pp_labels(std::ostream& out, labels& lbls);
+        void pp_premises(std::ostream& out, refs& refs);
+
+        void get_subst(proof* p, subst& sub);
+        void get_rule_name(proof* p, symbol&);
+        void get_labels(proof* p, labels&);
+
+    public:
+        boogie_proof(ast_manager& m): m(m), m_proof(m), m_model(0) {}
+        
+        void set_proof(proof* p);
+        
+        void set_model(model* m);
+
+        void pp(std::ostream& out);
+    };
+}

src/muz_qe/dl_cmds.cpp

@@ -328,9 +328,7 @@ private:
     void print_certificate(cmd_context& ctx) {
         if (m_dl_ctx->get_params().print_certificate()) {
             datalog::context& dlctx = m_dl_ctx->dlctx();
-            if (!dlctx.display_certificate(ctx.regular_stream())) {
+            dlctx.display_certificate(ctx.regular_stream());
-                throw cmd_exception("certificates are not supported for the selected engine");
-            }
             ctx.regular_stream() << "\n";
         }
     }

src/muz_qe/dl_compiler.cpp

@@ -42,7 +42,7 @@ namespace datalog {
             return;
         }
         relation_signature sig;
-        m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
+        m_context.get_rel_context()->get_rmanager().from_predicate(pred, sig);
         reg_idx reg = get_fresh_register(sig);
         e->get_data().m_value=reg;
 
@@ -606,7 +606,7 @@ namespace datalog {
                 }
                 SASSERT(is_app(e));
                 relation_sort arg_sort;
-                m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
+                m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
                 reg_idx new_reg;
                 bool new_dealloc;
                 make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
@@ -1252,7 +1252,7 @@ namespace datalog {
         func_decl_set::iterator fdit = preds.begin();
         func_decl_set::iterator fdend = preds.end();
         for(; fdit!=fdend; ++fdit) {
-            if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
+            if(!m_context.get_rel_context()->get_rmanager().is_saturated(*fdit)) {
                 return false;
             }
         }
@@ -1337,7 +1337,7 @@ namespace datalog {
 
         acc.set_observer(0);
 
-        TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
+        TRACE("dl", execution_code.display(*m_context.get_rel_context(), tout););
     }
 
 

src/muz_qe/dl_context.cpp

@@ -45,6 +45,7 @@ Revision History:
 #include"dl_mk_bit_blast.h"
 #include"dl_mk_array_blast.h"
 #include"dl_mk_karr_invariants.h"
+#include"dl_mk_magic_symbolic.h"
 #include"dl_mk_quantifier_abstraction.h"
 #include"dl_mk_quantifier_instantiation.h"
 #include"datatype_decl_plugin.h"
@@ -238,11 +239,13 @@ namespace datalog {
         m_rule_fmls(m),
         m_background(m),
         m_mc(0),
+        m_rel(0),
+        m_engine(0),
         m_closed(false),
         m_saturation_was_run(false),
         m_last_status(OK),
         m_last_answer(m),
-        m_engine(LAST_ENGINE),
+        m_engine_type(LAST_ENGINE),
         m_cancel(false) {
     }
 
@@ -260,8 +263,7 @@ namespace datalog {
         m_preds.reset();
         m_preds_by_name.reset();
         reset_dealloc_values(m_sorts);
-        m_pdr = 0;
+        m_engine = 0;
-        m_bmc = 0;
         m_rel = 0;
     }
 
@@ -432,8 +434,7 @@ namespace datalog {
 
     void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
             symbol const * relation_names) {
-        if (relation_name_cnt > 0) {
+        if (m_rel && relation_name_cnt > 0) {
-            ensure_rel();
             m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
         }
     }
@@ -445,7 +446,7 @@ namespace datalog {
 
         register_predicate(new_pred, true);
 
-        if (m_rel.get()) {
+        if (m_rel) {
             m_rel->inherit_predicate_kind(new_pred, orig_pred);
         }
         return new_pred;
@@ -542,64 +543,18 @@ namespace datalog {
     }
 
     unsigned context::get_num_levels(func_decl* pred) {
-        switch(get_engine()) {
+        ensure_engine();
-        case DATALOG_ENGINE:
+        return m_engine->get_num_levels(pred);
-            throw default_exception("get_num_levels is not supported for datalog engine");
-        case PDR_ENGINE:
-        case QPDR_ENGINE:
-            ensure_pdr();
-            return m_pdr->get_num_levels(pred);
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            throw default_exception("get_num_levels is not supported for bmc");
-        case TAB_ENGINE:
-            throw default_exception("get_num_levels is not supported for tab");
-        case CLP_ENGINE:
-            throw default_exception("get_num_levels is not supported for clp");
-        default:
-            throw default_exception("unknown engine");
-        } 
     }
 
     expr_ref context::get_cover_delta(int level, func_decl* pred) {
-        switch(get_engine()) {
+        ensure_engine();
-        case DATALOG_ENGINE:
+        return m_engine->get_cover_delta(level, pred);
-            throw default_exception("operation is not supported for datalog engine");
-        case PDR_ENGINE:
-        case QPDR_ENGINE:
-            ensure_pdr();
-            return m_pdr->get_cover_delta(level, pred);
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            throw default_exception("operation is not supported for BMC engine");
-        case TAB_ENGINE:
-            throw default_exception("operation is not supported for TAB engine");
-        case CLP_ENGINE:
-            throw default_exception("operation is not supported for CLP engine");
-        default:
-            throw default_exception("unknown engine");
-        } 
     }
 
     void context::add_cover(int level, func_decl* pred, expr* property) {
-        switch(get_engine()) {
+        ensure_engine();
-        case DATALOG_ENGINE:
+        m_engine->add_cover(level, pred, property);
-            throw default_exception("operation is not supported for datalog engine");
-        case PDR_ENGINE:
-        case QPDR_ENGINE:
-            ensure_pdr();
-            m_pdr->add_cover(level, pred, property);
-            break;
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            throw default_exception("operation is not supported for BMC engine");
-        case TAB_ENGINE:
-            throw default_exception("operation is not supported for TAB engine");
-        case CLP_ENGINE:
-            throw default_exception("operation is not supported for CLP engine");
-        default:
-            throw default_exception("unknown engine");
-        } 
     }
 
     void context::check_uninterpreted_free(rule_ref& r) {
@@ -743,7 +698,7 @@ namespace datalog {
 
     void context::add_fact(func_decl * pred, const relation_fact & fact) {
         if (get_engine() == DATALOG_ENGINE) {
-            ensure_rel();
+            ensure_engine();
             m_rel->add_fact(pred, fact);
         }
         else {
@@ -769,7 +724,7 @@ namespace datalog {
 
     void context::add_table_fact(func_decl * pred, const table_fact & fact) {
         if (get_engine() == DATALOG_ENGINE) {
-            ensure_rel();
+            ensure_engine();
             m_rel->add_fact(pred, fact);
         }
         else {
@@ -907,6 +862,9 @@ namespace datalog {
         m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
         m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
         m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));
+        if (get_params().magic()) {
+            m_transf.register_plugin(alloc(datalog::mk_magic_symbolic, *this, 36020));
+        }
         transform_rules(m_transf);
     }
 
@@ -917,7 +875,7 @@ namespace datalog {
 
     void context::updt_params(params_ref const& p) {
         m_params_ref.copy(p);
-        if (m_pdr.get()) m_pdr->updt_params();        
+        if (m_engine.get()) m_engine->updt_params();
     }
 
     expr_ref context::get_background_assertion() {
@@ -940,45 +898,39 @@ namespace datalog {
         m_cancel = true;
         m_last_status = CANCELED;
         m_transf.cancel();
-        if (m_pdr.get()) m_pdr->cancel();
+        if (m_engine) m_engine->cancel();
-        if (m_bmc.get()) m_bmc->cancel();
-        if (m_tab.get()) m_tab->cancel();
-        if (m_rel.get()) m_rel->set_cancel(true);
     }
 
     void context::cleanup() {
         m_cancel = false;
         m_last_status = OK;
-        if (m_pdr.get()) m_pdr->cleanup();
+        if (m_engine) m_engine->cleanup();
-        if (m_bmc.get()) m_bmc->cleanup();
-        if (m_tab.get()) m_tab->cleanup();
-        if (m_rel.get()) m_rel->set_cancel(false);
     }
 
     class context::engine_type_proc {
         ast_manager&  m;
         arith_util    a;
         datatype_util dt;
-        DL_ENGINE     m_engine;
+        DL_ENGINE     m_engine_type;
 
     public:
-        engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}
+        engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine_type(DATALOG_ENGINE) {}
 
-        DL_ENGINE get_engine() const { return m_engine; }
+        DL_ENGINE get_engine() const { return m_engine_type; }
 
         void operator()(expr* e) {
             if (is_quantifier(e)) {
-                m_engine = QPDR_ENGINE;
+                m_engine_type = QPDR_ENGINE;
             }
-            else if (m_engine != QPDR_ENGINE) {
+            else if (m_engine_type != QPDR_ENGINE) {
                 if (a.is_int_real(e)) {
-                    m_engine = PDR_ENGINE;
+                    m_engine_type = PDR_ENGINE;
                 }
                 else if (is_var(e) && m.is_bool(e)) {
-                    m_engine = PDR_ENGINE;
+                    m_engine_type = PDR_ENGINE;
                 }
                 else if (dt.is_datatype(m.get_sort(e))) {
-                    m_engine = PDR_ENGINE;
+                    m_engine_type = PDR_ENGINE;
                 }
             }
         }
@@ -988,46 +940,46 @@ namespace datalog {
         symbol e = m_params.engine();
         
         if (e == symbol("datalog")) {
-            m_engine = DATALOG_ENGINE;
+            m_engine_type = DATALOG_ENGINE;
         }
         else if (e == symbol("pdr")) {
-            m_engine = PDR_ENGINE;
+            m_engine_type = PDR_ENGINE;
         }
         else if (e == symbol("qpdr")) {
-            m_engine = QPDR_ENGINE;
+            m_engine_type = QPDR_ENGINE;
         }
         else if (e == symbol("bmc")) {
-            m_engine = BMC_ENGINE;
+            m_engine_type = BMC_ENGINE;
         }
         else if (e == symbol("qbmc")) {
-            m_engine = QBMC_ENGINE;
+            m_engine_type = QBMC_ENGINE;
         }
         else if (e == symbol("tab")) {
-            m_engine = TAB_ENGINE;
+            m_engine_type = TAB_ENGINE;
         }
         else if (e == symbol("clp")) {
-            m_engine = CLP_ENGINE;
+            m_engine_type = CLP_ENGINE;
         }
 
-        if (m_engine == LAST_ENGINE) {
+        if (m_engine_type == LAST_ENGINE) {
             expr_fast_mark1 mark;
             engine_type_proc proc(m);
-            m_engine = DATALOG_ENGINE;            
+            m_engine_type = DATALOG_ENGINE;            
-            for (unsigned i = 0; m_engine == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
+            for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
                 rule * r = m_rule_set.get_rule(i);
                 quick_for_each_expr(proc, mark, r->get_head());
                 for (unsigned j = 0; j < r->get_tail_size(); ++j) {
                     quick_for_each_expr(proc, mark, r->get_tail(j));
                 }
-                m_engine = proc.get_engine();
+                m_engine_type = proc.get_engine();
             }
-            for (unsigned i = m_rule_fmls_head; m_engine == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) {
+            for (unsigned i = m_rule_fmls_head; m_engine_type == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) {
                 expr* fml = m_rule_fmls[i].get();
                 while (is_quantifier(fml)) {
                     fml = to_quantifier(fml)->get_expr();
                 }
                 quick_for_each_expr(proc, mark, fml);
-                m_engine = proc.get_engine();
+                m_engine_type = proc.get_engine();
             }
         }
     }
@@ -1038,170 +990,78 @@ namespace datalog {
         m_last_answer = 0;
         switch (get_engine()) {
         case DATALOG_ENGINE:
-            flush_add_rules();
-            return rel_query(query);
         case PDR_ENGINE:
         case QPDR_ENGINE:
-            flush_add_rules();
-            return pdr_query(query);
         case BMC_ENGINE:
         case QBMC_ENGINE:
-            flush_add_rules();
-            return bmc_query(query);
         case TAB_ENGINE:
-            flush_add_rules();
-            return tab_query(query);
         case CLP_ENGINE:
             flush_add_rules();
-            return clp_query(query);
+            break;
         default:
             UNREACHABLE();
-            return rel_query(query);
         }
+        ensure_engine();
+        return m_engine->query(query);
     }
 
     model_ref context::get_model() {
-        switch(get_engine()) {
+        ensure_engine();
-        case PDR_ENGINE:
+        return m_engine->get_model();
-        case QPDR_ENGINE:
-            ensure_pdr();
-            return m_pdr->get_model();
-        default:
-            return model_ref(alloc(model, m));
-        }        
     }
 
     proof_ref context::get_proof() {
-        switch(get_engine()) {
+        ensure_engine();
-        case PDR_ENGINE:
+        return m_engine->get_proof();
-        case QPDR_ENGINE:
-            ensure_pdr();
-            return m_pdr->get_proof();
-        default:
-            return proof_ref(m.mk_asserted(m.mk_true()), m);
-        }                
     }
 
-    void context::ensure_pdr() {
+    void context::ensure_engine() {
-        if (!m_pdr.get()) {
+        if (!m_engine.get()) {
-            m_pdr = alloc(pdr::dl_interface, *this);
+            switch (get_engine()) {
+            case PDR_ENGINE:
+            case QPDR_ENGINE:
+                m_engine = alloc(pdr::dl_interface, *this);
+                break;
+            case DATALOG_ENGINE:
+                m_rel = alloc(rel_context, *this);
+                m_engine = m_rel;
+                break;
+            case BMC_ENGINE:
+            case QBMC_ENGINE:
+                m_engine = alloc(bmc, *this);
+                break;
+            case TAB_ENGINE:
+                m_engine = alloc(tab, *this);
+                break;
+            case CLP_ENGINE:
+                m_engine = alloc(clp, *this);
+                break;
+            }
         }
     }
 
-    lbool context::pdr_query(expr* query) {
+    lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {        
-        ensure_pdr();
+        ensure_engine();
-        return m_pdr->query(query);
+        if (m_rel) {
-    }
+            return m_rel->query(num_rels, rels);
-
+        }
-    void context::ensure_bmc() {
+        else {
-        if (!m_bmc.get()) {
+            return l_undef;
-            m_bmc = alloc(bmc, *this);
         }
     }
-
+        
-    lbool context::bmc_query(expr* query) {
-        ensure_bmc();
-        return m_bmc->query(query);
-    }
-
-    void context::ensure_tab() {
-        if (!m_tab.get()) {
-            m_tab = alloc(tab, *this);
-        }
-    }
-
-    void context::ensure_clp() {
-        if (!m_clp.get()) {
-            m_clp = alloc(clp, *this);
-        }
-    }
-
-    lbool context::tab_query(expr* query) {
-        ensure_tab();
-        return m_tab->query(query);
-    }
-
-    lbool context::clp_query(expr* query) {
-        ensure_clp();
-        return m_clp->query(query);
-    }
-
-    void context::ensure_rel() {
-        if (!m_rel.get()) {
-            m_rel = alloc(rel_context, *this);
-        }
-    }
-
-    lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
-        ensure_rel();
-        return m_rel->query(num_rels, rels);
-    }
-    
-    lbool context::rel_query(expr* query) {
-        ensure_rel();
-        return m_rel->query(query);
-    }
-
-    
     expr* context::get_answer_as_formula() {
         if (m_last_answer) {
             return m_last_answer.get();
         }
-        switch(get_engine()) {
+        ensure_engine();
-        case PDR_ENGINE: 
+        m_last_answer = m_engine->get_answer();
-        case QPDR_ENGINE:
-            ensure_pdr();
-            m_last_answer = m_pdr->get_answer();
-            return m_last_answer.get();
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            ensure_bmc();
-            m_last_answer = m_bmc->get_answer();
-            return m_last_answer.get();
-        case DATALOG_ENGINE:
-            ensure_rel();
-            m_last_answer = m_rel->get_last_answer();
-            return m_last_answer.get();
-        case TAB_ENGINE:
-            ensure_tab();
-            m_last_answer = m_tab->get_answer();
-            return m_last_answer.get();
-        case CLP_ENGINE:
-            ensure_clp();
-            m_last_answer = m_clp->get_answer();
-            return m_last_answer.get();
-        default:
-            UNREACHABLE();
-        }
-        m_last_answer = m.mk_false();
         return m_last_answer.get();
     }
 
-    bool context::display_certificate(std::ostream& out) {
+    void context::display_certificate(std::ostream& out) {
-        switch(get_engine()) {
+        ensure_engine();
-        case DATALOG_ENGINE:            
+        m_engine->display_certificate(out);
-            return false;
-        case PDR_ENGINE: 
-        case QPDR_ENGINE: 
-            ensure_pdr();
-            m_pdr->display_certificate(out);
-            return true;
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            ensure_bmc();
-            m_bmc->display_certificate(out);
-            return true;
-        case TAB_ENGINE:
-            ensure_tab();
-            m_tab->display_certificate(out);
-            return true;
-        case CLP_ENGINE:
-            ensure_clp();
-            m_clp->display_certificate(out);
-            return true;
-        default: 
-            return false;
-        }        
     }
 
     void context::display_profile(std::ostream& out) const {
@@ -1219,26 +1079,14 @@ namespace datalog {
     }
 
     void context::reset_statistics() {
-        if (m_pdr) {
+        if (m_engine) {
-            m_pdr->reset_statistics();
+            m_engine->reset_statistics();
-        }
-        if (m_bmc) {
-            m_bmc->reset_statistics();
-        }
-        if (m_tab) {
-            m_tab->reset_statistics();
         }
     }
 
     void context::collect_statistics(statistics& st) const {
-        if (m_pdr) {
+        if (m_engine) {
-            m_pdr->collect_statistics(st);
+            m_engine->collect_statistics(st);
-        }
-        if (m_bmc) {
-            m_bmc->collect_statistics(st);
-        }
-        if (m_tab) {
-            m_tab->collect_statistics(st);
         }
     }
 
@@ -1246,8 +1094,7 @@ namespace datalog {
     execution_result context::get_status() { return m_last_status; }
 
     bool context::result_contains_fact(relation_fact const& f) {
-        ensure_rel();
+        return m_rel && m_rel->result_contains_fact(f);
-        return m_rel->result_contains_fact(f);
     }
     
     // NB: algebraic data-types declarations will not be printed.

src/muz_qe/dl_context.h

@@ -121,17 +121,14 @@ namespace datalog {
         model_converter_ref m_mc;
         proof_converter_ref m_pc;
 
-        scoped_ptr<pdr::dl_interface>   m_pdr;
+        rel_context*                    m_rel;
-        scoped_ptr<bmc>                 m_bmc;
+        scoped_ptr<engine_base>         m_engine;
-        scoped_ptr<rel_context>         m_rel;
-        scoped_ptr<tab>                 m_tab;
-        scoped_ptr<clp>                 m_clp;
 
         bool               m_closed;
         bool               m_saturation_was_run;
         execution_result   m_last_status;
         expr_ref           m_last_answer;
-        DL_ENGINE          m_engine;
+        DL_ENGINE          m_engine_type;
         volatile bool      m_cancel;
 
 
@@ -161,7 +158,7 @@ namespace datalog {
         rule_manager & get_rule_manager() { return m_rule_manager; }
         smt_params & get_fparams() const { return m_fparams; }
         fixedpoint_params const&  get_params() const { return m_params; }
-        DL_ENGINE get_engine() { configure_engine(); return m_engine; }
+        DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
         th_rewriter& get_rewriter() { return m_rewriter; }
         var_subst & get_var_subst() { return m_var_subst; }
         dl_decl_util & get_decl_util()  { return m_decl_util; }
@@ -454,14 +451,14 @@ namespace datalog {
         /**
            \brief Display a certificate for reachability and/or unreachability.
         */
-        bool display_certificate(std::ostream& out);
+        void display_certificate(std::ostream& out);
 
         /**
            \brief query result if it contains fact.
          */
         bool result_contains_fact(relation_fact const& f);
 
-        rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
+        rel_context* get_rel_context() { ensure_engine(); return m_rel; }
 
     private:
 
@@ -473,25 +470,7 @@ namespace datalog {
 
         void flush_add_rules();
 
-        void ensure_pdr();
+        void ensure_engine();
-
-        void ensure_bmc();
-
-        void ensure_tab();
-
-        void ensure_clp();
-
-        void ensure_rel();
-
-        lbool rel_query(expr* query);
-
-        lbool pdr_query(expr* query);
-
-        lbool bmc_query(expr* query);
-
-        lbool tab_query(expr* query);
-
-        lbool clp_query(expr* query);
 
         void check_quantifier_free(rule_ref& r);        
         void check_uninterpreted_free(rule_ref& r);

src/muz_qe/dl_instruction.cpp

@@ -59,7 +59,7 @@ namespace datalog {
     }
 
     rel_context& execution_context::get_rel_context() { 
-        return m_context.get_rel_context(); 
+        return *m_context.get_rel_context(); 
     }
 
     struct compare_size_proc {

src/muz_qe/dl_mk_backwards.cpp

@@ -48,7 +48,7 @@ namespace datalog {
             neg.reset();
             rule & r = *source.get_rule(i);
             unsigned utsz = r.get_uninterpreted_tail_size();
-            unsigned tsz = r.get_tail_size();
+            unsigned tsz  = r.get_tail_size();
             if (!source.is_output_predicate(r.get_decl())) {
                 tail.push_back(r.get_head());
                 neg.push_back(false);

src/muz_qe/dl_mk_explanations.cpp

@@ -604,7 +604,7 @@ namespace datalog {
         m_e_sort = m_decl_util.mk_rule_sort();
         m_pinned.push_back(m_e_sort);
 
-        relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
+        relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
         symbol er_symbol = explanation_relation_plugin::get_name(m_relation_level);
         m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol));
         if (!m_er_plugin) {
@@ -637,7 +637,7 @@ namespace datalog {
     void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) {
         SASSERT(m_relation_level);
 
-        relation_manager & rmgr = m_context.get_rel_context().get_rmanager();
+        relation_manager & rmgr = m_context.get_rel_context()->get_rmanager();
         unsigned sz = e_decl->get_arity();
         relation_signature sig;
         rmgr.from_predicate(e_decl, sig);
@@ -871,7 +871,7 @@ namespace datalog {
             return 0;
         }
         rule_set * res = alloc(rule_set, m_context);
-        transform_facts(m_context.get_rel_context().get_rmanager(), source, *res);
+        transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res);
         transform_rules(source, *res);
         return res;
     }

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -49,7 +49,8 @@ namespace datalog {
         rm(ctx.get_rule_manager()),
         m_inner_ctx(m, ctx.get_fparams()),
         a(m),
-        m_pinned(m) {
+        m_pinned(m),
+        m_cancel(false) {
             params_ref params;
             params.set_sym("default_relation", symbol("karr_relation"));
             params.set_sym("engine", symbol("datalog"));
@@ -189,6 +190,7 @@ namespace datalog {
     };
 
     void mk_karr_invariants::cancel() {
+        m_cancel = true;
         m_inner_ctx.cancel();
     }
     
@@ -211,6 +213,10 @@ namespace datalog {
 
         get_invariants(*src_loop);
 
+        if (m_cancel) {
+            return 0;
+        }
+
         // figure out whether to update same rules as used for saturation.
         scoped_ptr<rule_set> rev_source = bwd(*src_loop);
         get_invariants(*rev_source);        
@@ -225,7 +231,7 @@ namespace datalog {
 
     void mk_karr_invariants::get_invariants(rule_set const& src) {
         m_inner_ctx.reset();
-        rel_context& rctx = m_inner_ctx.get_rel_context();
+        rel_context& rctx = *m_inner_ctx.get_rel_context();
         ptr_vector<func_decl> heads;
         func_decl_set const& predicates = m_ctx.get_predicates();
         for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) {

src/muz_qe/dl_mk_karr_invariants.h

@@ -57,6 +57,7 @@ namespace datalog {
         arith_util      a;
         obj_map<func_decl, expr*>      m_fun2inv;
         ast_ref_vector m_pinned;
+        volatile bool  m_cancel;
 
         void get_invariants(rule_set const& src);
 

src/muz_qe/dl_mk_magic_sets.cpp

@@ -362,7 +362,7 @@ namespace datalog {
                 rule * r = *it;
                 transform_rule(task.m_adornment, r, *result);
             }
-            if (!m_context.get_rel_context().get_relation(task.m_pred).empty()) {
+            if (!m_context.get_rel_context()->get_relation(task.m_pred).empty()) {
                 //we need a rule to copy facts that are already in a relation into the adorned
                 //relation (since out intentional predicates can have facts, not only rules)
                 create_transfer_rule(task, *result);

src/muz_qe/dl_mk_magic_symbolic.cpp

@@ -0,0 +1,133 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_magic_symbolic.cpp
+
+Abstract:
+
+    Create Horn clauses for magic symbolic flow.
+
+    Q(x)  :- A(y), B(z), phi1(x,y,z).
+    Q(x)  :- C(y), phi2(x,y).
+    A(x)  :- C(y), phi3(x,y).
+    A(x)  :- A(y), phi3(x,y).
+    B(x)  :- C(y), A(z), phi4(x,y,z).
+    C(x)  :- phi5(x).
+
+    Transformed clauses:
+
+    Q_ans(x)   :- Q_query(x), A_ans(y), B_ans(z), phi1(x,y,z).
+    Q_ans(x)   :- Q_query(x), C_ans(y), phi2(x,y).
+    Q_query(x) :- true.
+    
+    A_ans(x)   :- A_query(x), C_ans(y), phi2(x,y)
+    A_ans(x)   :- A_query(x), A_ans(y), phi3(x,y).
+    A_query(y) :- Q_query(x), phi1(x,y,z).
+    A_query(y) :- A_query(x), phi3(x,y).
+    A_query(z) :- B_query(x), C_ans(y), phi4(x,y,z).
+
+    B_ans(x)   :- B_query(x), C_ans(y), A_ans(z), phi4(x,y,z).
+    B_query(z) :- Q_query(x), A_ans(y), phi1(x,y,z).
+
+    C_ans(x)   :- C_query(x), phi5(x).
+    C_query(y) :- Q_query(x), phi2(x,y).
+    C_query(y) :- Q_query(x), phi3(x,y).
+    C_query(y) :- B_query(x), phi4(x,y,z).
+
+General scheme:
+    A(x) :- P1(x_1), ..., Pn(x_n), phi(x,x1,..,x_n).
+
+    P(x) :- Prefix(x,y,z), A(z) ... 
+    
+    A_ans(x) :- A_query(x), P_i_ans(x_i), phi(x,..).
+    A_query(z) :- P_query(x), Prefix_ans(x,y,z).
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-06-19
+
+Revision History:
+
+--*/
+
+#include"dl_mk_magic_symbolic.h"
+#include"dl_context.h"
+
+namespace datalog {
+
+
+    mk_magic_symbolic::mk_magic_symbolic(context & ctx, unsigned priority):
+        plugin(priority),
+        m(ctx.get_manager()),
+        m_ctx(ctx) {        
+    }
+
+    mk_magic_symbolic::~mk_magic_symbolic() { }
+        
+    rule_set * mk_magic_symbolic::operator()(rule_set const & source) {
+        if (!m_ctx.get_params().magic()) {
+            return 0;
+        }
+        context& ctx = source.get_context();
+        rule_manager& rm = source.get_rule_manager();
+        rule_set * result = alloc(rule_set, ctx);
+        unsigned sz = source.get_num_rules();
+        rule_ref new_rule(rm);
+        app_ref_vector tail(m);
+        app_ref head(m);
+        svector<bool> neg;
+        for (unsigned i = 0; i < sz; ++i) {            
+            rule & r = *source.get_rule(i);
+            unsigned utsz = r.get_uninterpreted_tail_size();
+            unsigned tsz  = r.get_tail_size();
+            tail.reset();
+            neg.reset();
+            for (unsigned j = utsz; j < tsz; ++j) {
+                tail.push_back(r.get_tail(j));
+                neg.push_back(false);
+            }
+            tail.push_back(mk_query(r.get_head()));
+            neg.push_back(false);
+            for (unsigned j = 0; j < utsz; ++j) {
+                tail.push_back(mk_ans(r.get_tail(j)));
+                neg.push_back(false);
+            }
+            new_rule = rm.mk(mk_ans(r.get_head()), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true);
+            if (source.is_output_predicate(r.get_decl())) {
+                result->set_output_predicate(new_rule->get_decl());
+            }
+
+            result->add_rule(new_rule);                
+            for (unsigned j = 0; j < utsz; ++j) {
+                new_rule = rm.mk(mk_query(r.get_tail(j)), tail.size()-utsz+j, tail.c_ptr(), neg.c_ptr(), r.name(), true);
+                result->add_rule(new_rule);
+            }            
+            
+        }
+        TRACE("dl", result->display(tout););
+        return result;
+    }
+
+    app_ref mk_magic_symbolic::mk_query(app* q) {
+        string_buffer<64> name;
+        func_decl* f = q->get_decl();
+        name << f->get_name() << "!query";
+        func_decl_ref g(m);
+        g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range());
+        m_ctx.register_predicate(g, false);
+        return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m);
+    }
+
+    app_ref mk_magic_symbolic::mk_ans(app* q) {
+        string_buffer<64> name;
+        func_decl* f = q->get_decl();
+        func_decl_ref g(m);
+        name << f->get_name() << "!ans";
+        g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range());
+        m_ctx.register_predicate(g, false);
+        return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m);        
+    }
+
+};

src/muz_qe/dl_mk_magic_symbolic.h

@@ -0,0 +1,40 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_mk_magic_symbolic.h
+
+Abstract:
+
+    Create Horn clauses for magic symbolic transformation.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-06-19
+
+Revision History:
+
+--*/
+#ifndef _DL_MK_MAGIC_SYMBOLIC_H_
+#define _DL_MK_MAGIC_SYMBOLIC_H_
+
+#include"dl_rule_transformer.h"
+
+namespace datalog {
+
+    class mk_magic_symbolic : public rule_transformer::plugin {
+        ast_manager& m;
+        context&     m_ctx;
+        app_ref      mk_ans(app* q);
+        app_ref      mk_query(app* q);
+    public:
+        mk_magic_symbolic(context & ctx, unsigned priority = 33037);
+        ~mk_magic_symbolic();        
+        rule_set * operator()(rule_set const & source);
+    };
+
+};
+
+#endif /* _DL_MK_MAGIC_SYMBOLIC_H_ */
+

src/muz_qe/dl_mk_partial_equiv.cpp

@@ -97,7 +97,7 @@ namespace datalog {
             return 0;
         }
 
-        relation_manager & rm = m_context.get_rel_context().get_rmanager();
+        relation_manager & rm = m_context.get_rel_context()->get_rmanager();
         rule_set::decl2rules::iterator it  = source.begin_grouped_rules();
         rule_set::decl2rules::iterator end = source.end_grouped_rules();
 

src/muz_qe/dl_mk_rule_inliner.cpp

@@ -206,7 +206,10 @@ namespace datalog {
 
     void mk_rule_inliner::count_pred_occurrences(rule_set const & orig)
     {
-        m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
+        rel_context* rel = m_context.get_rel_context();
+        if (rel) {
+            rel->get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
+        }
 
         rule_set::iterator rend = orig.end();
         for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {

src/muz_qe/dl_mk_similarity_compressor.cpp

@@ -368,7 +368,7 @@ namespace datalog {
             collect_orphan_consts(*it, const_infos, val_fact);
             m_context.add_fact(aux_pred, val_fact);
         }
-        m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred);
+        m_context.get_rel_context()->get_rmanager().mark_saturated(aux_pred);
 
         app * new_head = r->get_head();
         ptr_vector<app> new_tail;

src/muz_qe/dl_mk_simple_joins.cpp

@@ -570,11 +570,15 @@ namespace datalog {
         cost estimate_size(app * t) const {
             func_decl * pred = t->get_decl();
             unsigned n=pred->get_arity();
-            relation_manager& rm = m_context.get_rel_context().get_rmanager();
+            rel_context* rel = m_context.get_rel_context();
+            if (!rel) {
+                return cost(1);
+            }
+            relation_manager& rm = rel->get_rmanager();
             if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
                 || rm.is_saturated(pred)) {
                 SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
-                unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows();
+                unsigned rel_size_int = rel->get_relation(pred).get_size_estimate_rows();
                 if(rel_size_int!=0) {
                     cost rel_size = static_cast<cost>(rel_size_int);
                     cost curr_size = rel_size;

src/muz_qe/dl_mk_subsumption_checker.cpp

@@ -249,7 +249,11 @@ namespace datalog {
     }
 
     void mk_subsumption_checker::scan_for_relations_total_due_to_facts(rule_set const& source) {
-        relation_manager& rm = m_context.get_rel_context().get_rmanager();
+        rel_context* rel = m_context.get_rel_context();
+        if (!rel) {
+            return;
+        }
+        relation_manager& rm = rel->get_rmanager();
 
         decl_set const& candidate_preds = m_context.get_predicates();
 

src/muz_qe/dl_mk_unbound_compressor.cpp

@@ -334,8 +334,10 @@ namespace datalog {
         // TODO mc
         m_modified = false;
 
-        m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
+        rel_context* rel = m_context.get_rel_context();
-
+        if (rel) {
+            rel->get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
+        }
         unsigned init_rule_cnt = source.get_num_rules();
         SASSERT(m_rules.empty());
         for (unsigned i=0; i<init_rule_cnt; i++) {

src/muz_qe/dl_relation_manager.cpp

@@ -614,6 +614,60 @@ namespace datalog {
         return t.get_plugin().mk_project_fn(t, col_cnt, removed_cols);
     }
 
+    class relation_manager::default_relation_filter_interpreted_and_project_fn : public relation_transformer_fn {
+        scoped_ptr<relation_mutator_fn>     m_filter;
+        scoped_ptr<relation_transformer_fn> m_project;
+        unsigned_vector                     m_removed_cols;
+    public:
+        /**
+            This constructor should be used only if we know that the projection operation
+            exists for the result of the join.
+        */
+        default_relation_filter_interpreted_and_project_fn(
+            relation_mutator_fn* filter,
+            unsigned removed_col_cnt,
+            const unsigned * removed_cols)
+            : m_filter(filter), 
+              m_project(0), 
+              m_removed_cols(removed_col_cnt, removed_cols) {}
+
+        virtual relation_base * operator()(const relation_base & t) {
+            scoped_rel<relation_base> t1 = t.clone();
+            (*m_filter)(*t1);
+            if( !m_project) {
+                relation_manager & rmgr = t1->get_plugin().get_manager();
+                m_project = rmgr.mk_project_fn(*t1, m_removed_cols.size(), m_removed_cols.c_ptr());
+                if (!m_project) {
+                    throw default_exception("projection does not exist");
+                }
+            }
+            return (*m_project)(*t1);
+        }
+    };
+
+    relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(
+        const relation_base & t, app * condition,
+        unsigned removed_col_cnt, const unsigned * removed_cols) {
+
+        relation_transformer_fn* res = 
+            t.get_plugin().mk_filter_interpreted_and_project_fn(
+                t, 
+                condition,
+                removed_col_cnt,
+                removed_cols);
+
+        if (!res) {
+            relation_mutator_fn* filter_fn = mk_filter_interpreted_fn(t, condition);
+            if (filter_fn) {
+                res = alloc(default_relation_filter_interpreted_and_project_fn, 
+                            filter_fn,
+                            removed_col_cnt,
+                            removed_cols);
+            }
+        }
+        return res;
+    }
+
 
     class relation_manager::default_relation_join_project_fn : public relation_join_fn {
         scoped_ptr<relation_join_fn> m_join;
@@ -720,14 +774,6 @@ namespace datalog {
         return t.get_plugin().mk_filter_interpreted_fn(t, condition);
     }
 
-    relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t,
-                                                                                 app * condition,
-                                                                                 unsigned removed_col_cnt,
-                                                                                 const unsigned * removed_cols) {
-        return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols);
-    }
-
-
     class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn {
         scoped_ptr<relation_mutator_fn> m_filter;
         scoped_ptr<relation_transformer_fn> m_project;

src/muz_qe/dl_relation_manager.h

@@ -42,6 +42,7 @@ namespace datalog {
         class default_relation_join_project_fn;
         class default_relation_select_equal_and_project_fn;
         class default_relation_intersection_filter_fn;
+        class default_relation_filter_interpreted_and_project_fn;
 
         class auxiliary_table_transformer_fn;
         class auxiliary_table_filter_fn;

src/muz_qe/dl_util.h

@@ -28,6 +28,8 @@ Revision History:
 #include"substitution.h"
 #include"fixedpoint_params.hpp"
 #include"ast_counter.h"
+#include"statistics.h"
+#include"lbool.h"
 
 namespace datalog {
 
@@ -58,6 +60,42 @@ namespace datalog {
         LAST_ENGINE
     };
 
+    class engine_base {
+        ast_manager& m;
+        std::string m_name;
+    public:
+        engine_base(ast_manager& m, char const* name): m(m), m_name(name) {}
+        virtual ~engine_base() {}
+
+        virtual expr_ref get_answer() = 0;
+        virtual lbool query(expr* q) = 0;
+
+        virtual void reset_statistics() {}
+        virtual void display_profile(std::ostream& out) const {}
+        virtual void collect_statistics(statistics& st) const {}
+        virtual unsigned get_num_levels(func_decl* pred) {
+            throw default_exception(std::string("get_num_levels is not supported for ") + m_name);
+        }
+        virtual expr_ref get_cover_delta(int level, func_decl* pred) {
+            throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
+        virtual void add_cover(int level, func_decl* pred, expr* property) {
+            throw default_exception(std::string("operation is not supported for ") + m_name);
+        }
+        virtual void display_certificate(std::ostream& out) const {
+            throw default_exception(std::string("certificates are not supported for ") + m_name);
+        }
+        virtual model_ref get_model() {
+            return model_ref(alloc(model, m));
+        }
+        virtual proof_ref get_proof() {
+            return proof_ref(m.mk_asserted(m.mk_true()), m);
+        }
+        virtual void updt_params() {}
+        virtual void cancel() {}
+        virtual void cleanup() {}
+    };
+
     struct std_string_hash_proc { 
         unsigned operator()(const std::string & s) const 
         { return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17); } 

src/muz_qe/fixedpoint_params.pyg

@@ -10,6 +10,7 @@ def_module_params('fixedpoint',
                           ('bit_blast', BOOL, False, '(PDR) bit-blast bit-vectors'),
                           ('explanations_on_relation_level', BOOL, False, '(DATALOG) if true, explanations are generated as history of each relation, rather than per fact (generate_explanations must be set to true for this option to have any effect)'),
                           ('magic_sets_for_queries', BOOL, False, "(DATALOG) magic set transformation will be used for queries"),
+                          ('magic', BOOL, False, "perform symbolic magic set transformation"),
                           ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"),
                           ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"),
                           ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"),
@@ -60,6 +61,7 @@ def_module_params('fixedpoint',
                                      "by putting in half of the table columns, if it would have been empty otherwise"),
                           ('print_answer', BOOL, False, 'print answer instance(s) to query'),
                           ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
+                          ('print_boogie_certificate', BOOL, False, 'print certificate for reachability or non-reachability using a format understood by Boogie'),
                           ('print_statistics',  BOOL, False, 'print statistics'),
 			  ('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'),
 	                  ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),

src/muz_qe/pdr_context.cpp

@@ -44,6 +44,7 @@ Notes:
 #include "proof_checker.h"
 #include "smt_value_sort.h"
 #include "proof_utils.h"
+#include "dl_boogie_proof.h"
 
 namespace pdr {
 
@@ -1063,7 +1064,7 @@ namespace pdr {
         ast_manager& m = pt.get_manager();
         datalog::context& dctx = ctx.get_context();
         datalog::rule_manager& rm = dctx.get_rule_manager();
-        datalog::rule_unifier unifier(dctx);
+        datalog::rule_unifier unif(dctx);
         datalog::dl_decl_util util(m);
         datalog::rule_ref r0(rm), r1(rm);
         obj_map<expr, proof*> cache;
@@ -1072,7 +1073,7 @@ namespace pdr {
         proof_ref_vector trail(m);
         datalog::rule_ref_vector rules_trail(rm);
         proof* pr = 0;
-        unifier.set_normalize(false);
+        unif.set_normalize(true);
         todo.push_back(m_root);
         update_models();
         while (!todo.empty()) {
@@ -1134,14 +1135,14 @@ namespace pdr {
                 substs.push_back(binding); // TODO base substitution.
                 for (unsigned i = 1; i < rls.size(); ++i) {
                     datalog::rule& src = *rls[i];
-                    bool unified = unifier.unify_rules(*reduced_rule, 0, src);
+                    bool unified = unif.unify_rules(*reduced_rule, 0, src);
                     if (!unified) {
                         IF_VERBOSE(0,
                                    verbose_stream() << "Could not unify rules: ";
                                    reduced_rule->display(dctx, verbose_stream());
                                    src.display(dctx, verbose_stream()););
                     }
-                    expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true);
+                    expr_ref_vector sub1 = unif.get_rule_subst(*reduced_rule, true);
                     TRACE("pdr",
                           for (unsigned k = 0; k < sub1.size(); ++k) {
                               tout << mk_pp(sub1[k].get(), m) << " ";
@@ -1160,8 +1161,8 @@ namespace pdr {
                     }
 
                     positions.push_back(std::make_pair(i,0));
-                    substs.push_back(unifier.get_rule_subst(src, false));
+                    substs.push_back(unif.get_rule_subst(src, false));
-                    VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
+                    VERIFY(unif.apply(*reduced_rule.get(), 0, src, r3));
                     reduced_rule = r3;
                 }
 
@@ -1620,6 +1621,12 @@ namespace pdr {
             IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););  
             m_last_result = l_true;
             validate();
+
+            IF_VERBOSE(1, 
+                       if (m_params.print_boogie_certificate()) {
+                           display_certificate(verbose_stream());
+                       });
+
             return l_true;
         }
         catch (inductive_exception) {
@@ -2129,7 +2136,15 @@ namespace pdr {
             break;
         }
         case l_true: {
-            strm << mk_pp(mk_sat_answer(), m);
+            if (m_params.print_boogie_certificate()) {
+                datalog::boogie_proof bp(m);
+                bp.set_proof(get_proof());
+                bp.set_model(0);
+                bp.pp(strm);
+            }
+            else {
+                strm << mk_pp(mk_sat_answer(), m);
+            }
             break;
         }
         case l_undef: {

src/muz_qe/pdr_dl_interface.cpp

@@ -37,6 +37,7 @@ Revision History:
 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),

src/muz_qe/pdr_dl_interface.h

@@ -23,6 +23,7 @@ Revision History:
 #include "lbool.h"
 #include "dl_rule.h"
 #include "dl_rule_set.h"
+#include "dl_util.h"
 #include "statistics.h"
 
 namespace datalog {
@@ -33,7 +34,7 @@ namespace pdr {
 
     class context;
 
-    class dl_interface {
+    class dl_interface : public datalog::engine_base {
         datalog::context& m_ctx;
         datalog::rule_set m_pdr_rules;
         datalog::rule_set m_old_rules;
@@ -47,31 +48,31 @@ namespace pdr {
         dl_interface(datalog::context& ctx); 
         ~dl_interface();
         
-        lbool query(expr* query);
+        virtual lbool query(expr* query);
 
-        void cancel();
+        virtual void cancel();
 
-        void cleanup();
+        virtual void cleanup();
 
-        void display_certificate(std::ostream& out) const;
+        virtual void display_certificate(std::ostream& out) const;
 
-        void collect_statistics(statistics& st) const;
+        virtual void collect_statistics(statistics& st) const;
 
-        void reset_statistics();
+        virtual void reset_statistics();
 
-        expr_ref get_answer();
+        virtual expr_ref get_answer();
 
-        unsigned get_num_levels(func_decl* pred);
+        virtual unsigned get_num_levels(func_decl* pred);
 
-        expr_ref get_cover_delta(int level, func_decl* pred);
+        virtual expr_ref get_cover_delta(int level, func_decl* pred);
        
-        void add_cover(int level, func_decl* pred, expr* property);
+        virtual void add_cover(int level, func_decl* pred, expr* property);
                
-        void updt_params();
+        virtual void updt_params();
 
-        model_ref get_model();
+        virtual model_ref get_model();
 
-        proof_ref get_proof();
+        virtual proof_ref get_proof();
         
     };
 }

src/muz_qe/pdr_generalizers.cpp

@@ -156,40 +156,19 @@ namespace pdr {
         m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
         m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real()));
     }
-    
+
     void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
+        method2(n, core, uses_level);
+    }
+
+    // use the entire region as starting point for generalization.
+    void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector& core, bool& uses_level) {    
         manager& pm = n.pt().get_pdr_manager();
         expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);
         if (core.empty()) {
             return;
         }        
-        if (!m_left.contains(n.pt().head())) {
+        add_variables(n, eqs);
-            expr_ref left(m), right(m);
-            m_left.insert(n.pt().head(), 0);
-            unsigned sz = n.pt().sig_size();        
-            for (unsigned i = 0; i < sz; ++i) {
-                func_decl* fn0 = n.pt().sig(i);
-                sort* srt = fn0->get_range();
-                if (a.is_int_real(srt)) {
-                    func_decl* fn1 = pm.o2n(fn0, 0);
-                    left  = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
-                    right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
-                    m_left.insert(fn1, left);
-                    m_right.insert(fn1, right);
-                    m_trail.push_back(left);
-                    m_trail.push_back(right);
-                }
-            }
-        }
-        unsigned sz = n.pt().sig_size();        
-        for (unsigned i = 0; i < sz; ++i) {
-            expr* left, *right;
-            func_decl* fn0 = n.pt().sig(i);
-            func_decl* fn1 = pm.o2n(fn0, 0);
-            if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
-                eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right)));
-            }
-        }
         if (!mk_convex(core, 0, conv1)) {
             IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";);
             return;
@@ -230,6 +209,100 @@ namespace pdr {
         }
     }
 
+    // take as starting point two points from different regions.
+    void core_convex_hull_generalizer::method2(model_node& n, expr_ref_vector& core, bool& uses_level) { 
+        expr_ref_vector conv1(m), conv2(m), core1(m), core2(m);
+        if (core.empty()) {
+            return;
+        }
+        manager& pm = n.pt().get_pdr_manager();
+        smt::kernel ctx(m, m_ctx.get_fparams(), m_ctx.get_params().p);
+        expr_ref goal(pm.mk_and(core));
+        ctx.assert_expr(goal);
+        lbool r = ctx.check();
+        if (r != l_true) {
+            IF_VERBOSE(0, verbose_stream() << "unexpected result from satisfiability check\n";);
+            return;
+        }
+        add_variables(n, conv1);
+        model_ref mdl;
+        ctx.get_model(mdl);
+
+        unsigned sz = n.pt().sig_size();        
+        for (unsigned i = 0; i < sz; ++i) {
+            expr_ref_vector constr(m);
+            expr* left, *right;
+            func_decl* fn0 = n.pt().sig(i);
+            func_decl* fn1 = pm.o2n(fn0, 0);
+            if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
+                expr_ref val(m);
+                mdl->eval(fn1, val);
+                if (val) {
+                    conv1.push_back(m.mk_eq(left, val));
+                    constr.push_back(m.mk_eq(right, val));
+                }
+            }
+            expr_ref new_model = pm.mk_and(constr);
+            m_trail.push_back(new_model);
+            m_trail.push_back(goal);
+            m_models.insert(goal, new_model);
+        }
+        conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
+        conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
+        conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
+
+        obj_map<expr, expr*>::iterator it = m_models.begin(), end = m_models.end();
+        for (; it != end; ++it) {
+            if (it->m_key == goal) {
+                continue;
+            }
+            conv1.push_back(it->m_value);
+            expr_ref state = pm.mk_and(conv1);
+            TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
+            model_node nd(0, state, n.pt(), n.level());
+            if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
+                IF_VERBOSE(0,
+                           verbose_stream() << mk_pp(state, m) << "\n";
+                           verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";);
+                core.reset();
+                core.append(conv2);
+                return;
+            }
+            conv1.pop_back();
+        }         
+    }
+
+    void core_convex_hull_generalizer::add_variables(model_node& n, expr_ref_vector& eqs) {
+        manager& pm = n.pt().get_pdr_manager();
+        if (!m_left.contains(n.pt().head())) {
+            expr_ref left(m), right(m);
+            m_left.insert(n.pt().head(), 0);
+            unsigned sz = n.pt().sig_size();        
+            for (unsigned i = 0; i < sz; ++i) {
+                func_decl* fn0 = n.pt().sig(i);
+                sort* srt = fn0->get_range();
+                if (a.is_int_real(srt)) {
+                    func_decl* fn1 = pm.o2n(fn0, 0);
+                    left  = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
+                    right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt);
+                    m_left.insert(fn1, left);
+                    m_right.insert(fn1, right);
+                    m_trail.push_back(left);
+                    m_trail.push_back(right);
+                }
+            }
+        }
+        unsigned sz = n.pt().sig_size();        
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* left, *right;
+            func_decl* fn0 = n.pt().sig(i);
+            func_decl* fn1 = pm.o2n(fn0, 0);
+            if (m_left.find(fn1, left) && m_right.find(fn1, right)) {
+                eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right)));
+            }
+        }
+    }
+
     bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) {
         conv.reset();
         for (unsigned i = 0; i < core.size(); ++i) {

src/muz_qe/pdr_generalizers.h

@@ -80,10 +80,14 @@ namespace pdr {
         expr_ref_vector m_trail;
         obj_map<func_decl, expr*> m_left;
         obj_map<func_decl, expr*> m_right;
+        obj_map<expr, expr*> m_models;
         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& core, bool& uses_level);
+        void method2(model_node& n, expr_ref_vector& core, bool& uses_level);
+        void add_variables(model_node& n, expr_ref_vector& eqs);
     public:
         core_convex_hull_generalizer(context& ctx);
         virtual ~core_convex_hull_generalizer() {}

src/muz_qe/proof_utils.cpp

@@ -608,3 +608,5 @@ void proof_utils::push_instantiations_up(proof_ref& pr) {
     push_instantiations_up_cl push(pr.get_manager());
     push(pr);
 }
+
+

src/muz_qe/proof_utils.h

@@ -42,6 +42,7 @@ public:
     */
     static void push_instantiations_up(proof_ref& pr);
 
+
 };
 
 #endif

src/muz_qe/qe_arith_plugin.cpp

@@ -20,7 +20,7 @@ Revision History:
 
 #include "qe.h"
 #include "ast_pp.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "bool_rewriter.h"
 #include "bv_decl_plugin.h"
 #include "arith_decl_plugin.h"
@@ -93,7 +93,7 @@ namespace qe {
         expr_ref     m_one_r;
         expr_ref     m_tmp;
     public: 
-        scoped_ptr<expr_replacer>  m_replace;
+        expr_safe_replace          m_replace;
         
         bool_rewriter              m_bool_rewriter;
         arith_rewriter             m_arith_rewriter;
@@ -111,7 +111,7 @@ namespace qe {
             m_zero_r(m_arith.mk_numeral(numeral(0), false), m),
             m_one_r(m_arith.mk_numeral(numeral(1), false), m),
             m_tmp(m), 
-            m_replace(mk_default_expr_replacer(m)),
+            m_replace(m),
             m_bool_rewriter(m),
             m_arith_rewriter(m) {
         }
@@ -827,7 +827,7 @@ namespace qe {
             while (index <= up) {
                 expr* n = mk_numeral(index);
                 result = body;
-                m_replace->apply_substitution(x, n, result);
+                m_replace.apply_substitution(x, n, result);
                 ors.push_back(result);
                 ++index;
             }
@@ -857,7 +857,7 @@ namespace qe {
             mk_flat_and(e1, body, result);
             app_ref z(m);
             mk_bounded_var(up, z_bv, z);
-            m_replace->apply_substitution(x, z, result);
+            m_replace.apply_substitution(x, z, result);
         }        
 
 
@@ -966,7 +966,7 @@ namespace qe {
                   << mk_pp(e, m) << "\n";
                   );
             expr_ref result(fml, m);
-            m_replace->apply_substitution(x, e, result);
+            m_replace.apply_substitution(x, e, result);
             simplify(result);
             TRACE("qe", 
                   tout << "singular solved:\n" 
@@ -1044,7 +1044,7 @@ namespace qe {
                   tout << " = 0\n";
                   );
             expr_ref result(fml, m);
-            m_replace->apply_substitution(x, p1, result);
+            m_replace.apply_substitution(x, p1, result);
             simplify(result);            
             m_ctx.elim_var(index-1, result, p1);
             TRACE("qe", tout << "Reduced: " << mk_pp(result, m) << "\n";);
@@ -2080,7 +2080,7 @@ public:
                 app* atm = atoms[i];        
                 t1 = m_util.mk_add(m_util.mk_mul(coeffs[i], z), terms[i]);
                 m_util.mk_divides(divisors[i], t1, new_atom);
-                m_util.m_replace->apply_substitution(atm, new_atom.get(), result);
+                m_util.m_replace.apply_substitution(atm, new_atom.get(), result);
                 
                 m_ctx.add_constraint(false, mk_not(atm), new_atom);
                 m_ctx.add_constraint(false, mk_not(new_atom), atm);
@@ -2121,7 +2121,7 @@ public:
                 m_util.simplify(mod_term2);
                 m_ctx.add_constraint(false, m.mk_eq(mod_term2, m_util.mk_zero(mod_term2)));
 
-                m_util.m_replace->apply_substitution(atm, z1, result);  
+                m_util.m_replace.apply_substitution(atm, z1, result);  
 
                 //
                 // conjoin (coeff*z + rest - z1) mod k == 0 to result
@@ -2153,7 +2153,7 @@ public:
             for (unsigned i = 0; i < sz; ++i) {
                 app* e = bounds.atoms(is_strict, is_lower)[i];
                 m_ctx.add_constraint(true, mk_not(e));
-                m_util.m_replace->apply_substitution(e, m.mk_false(), result);
+                m_util.m_replace.apply_substitution(e, m.mk_false(), result);
             }            
         }
 
@@ -2162,7 +2162,7 @@ public:
             for (unsigned i = 0; i < sz; ++i) {
                 app* e = bounds.atoms(is_strict, !is_lower)[i];
                 m_ctx.add_constraint(true, e);
-                m_util.m_replace->apply_substitution(e, m.mk_true(), result); 
+                m_util.m_replace.apply_substitution(e, m.mk_true(), result); 
             }
         }
 
@@ -2276,7 +2276,7 @@ public:
                     else {
                         m_ctx.add_constraint(true, e);
                     }
-                    m_util.m_replace->apply_substitution(atm, m.mk_true(), result);
+                    m_util.m_replace.apply_substitution(atm, m.mk_true(), result);
                     continue;
                 }
            
@@ -2293,7 +2293,7 @@ public:
                     (same_strict && i < index);
 
                 mk_bound(result_is_strict, is_lower, a, t, b, s, tmp);
-                m_util.m_replace->apply_substitution(e, tmp.get(), result);
+                m_util.m_replace.apply_substitution(e, tmp.get(), result);
 
                 TRACE("qe", 
                       tout << (result_is_strict?"strict result":"non-strict result") << "\n";
@@ -2330,7 +2330,7 @@ public:
                 s = x_t.mk_term(b, s);
                 b = x_t.mk_coeff(b);
                 m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp);
-                m_util.m_replace->apply_substitution(e, tmp.get(), result);
+                m_util.m_replace.apply_substitution(e, tmp.get(), result);
                 
                 m_ctx.add_constraint(true, mk_not(e), tmp);
 
@@ -2398,7 +2398,7 @@ public:
         weights_t                    m_weights;
         th_rewriter                  m_rewriter;        
         nlarith::util                m_util;
-        scoped_ptr<expr_replacer>    m_replacer;
+        expr_safe_replace            m_replace;
         expr_ref_vector              m_trail;
         factor_rewriter_star         m_factor_rw;
         bool                         m_produce_models;
@@ -2407,7 +2407,7 @@ public:
             qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
             m_rewriter(m),
             m_util(m),
-            m_replacer(mk_default_expr_replacer(m)),
+            m_replace(m),
             m_trail(m),
             m_factor_rw(m),
             m_produce_models(produce_models) {
@@ -2480,12 +2480,11 @@ public:
             SASSERT(vl.is_unsigned());
             SASSERT(vl.get_unsigned() < brs->size());
             unsigned j = vl.get_unsigned();
-            expr_substitution sub(m);
+            m_replace.reset();            
             for (unsigned i = 0; i < brs->preds().size(); ++i) {
-                sub.insert(to_app(brs->preds(i)), brs->subst(j)[i]);
+                m_replace.insert(brs->preds(i), brs->subst(j)[i]);
             }
-            m_replacer->set_substitution(&sub);
+            m_replace(fml);
-            (*m_replacer)(fml);
             expr_ref tmp(m.mk_and(brs->constraints(j), fml), m);
             m_factor_rw(tmp, fml);
             if (def) {

src/muz_qe/qe_array_plugin.cpp

@@ -1,7 +1,7 @@
 
 #include "qe.h"
 #include "array_decl_plugin.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "ast_pp.h"
 #include "arith_decl_plugin.h"
 
@@ -11,13 +11,13 @@ namespace qe {
 
     class array_plugin : public qe_solver_plugin {
 
-        scoped_ptr<expr_replacer> m_replace;
+        expr_safe_replace m_replace;
 
     public:
 
         array_plugin(i_solver_context& ctx, ast_manager& m) : 
             qe_solver_plugin(m, m.mk_family_id("array"), ctx),
-            m_replace(mk_default_expr_replacer(m))
+            m_replace(m)
         {
         }
 
@@ -123,7 +123,7 @@ namespace qe {
             if (m_ctx.is_var(a, idx) && 
                 !m_ctx.contains(idx)(rhs)) {
                 expr_ref result(fml, m);
-                m_replace->apply_substitution(a, rhs, result);
+                m_replace.apply_substitution(a, rhs, result);
                 m_ctx.elim_var(idx, result, rhs);
                 return true;
             }                 
@@ -175,7 +175,7 @@ namespace qe {
                       tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
                       );
                 expr_ref result(fml, m);
-                m_replace->apply_substitution(A, store_B_i_t, result);
+                m_replace.apply_substitution(A, store_B_i_t, result);
                 m_ctx.add_var(B);
                 m_ctx.elim_var(idx, result, store_B_i_t);
                 return true;
@@ -248,7 +248,7 @@ namespace qe {
                       tout << "eq: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";
                       );
                 expr_ref result(fml, m);
-                m_replace->apply_substitution(A, store_t, result);
+                m_replace.apply_substitution(A, store_t, result);
                 m_ctx.elim_var(idx, result, store_t);
                 return true;
             }        

src/muz_qe/qe_bool_plugin.cpp

@@ -25,18 +25,18 @@ Notes:
 --*/
 
 #include "qe.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "ast_pp.h"
 #include "model_evaluator.h"
 
 
 namespace qe {
     class bool_plugin : public qe_solver_plugin {
-        scoped_ptr<expr_replacer> m_replace;
+        expr_safe_replace m_replace;
     public:
         bool_plugin(i_solver_context& ctx, ast_manager& m):
             qe_solver_plugin(m, m.get_basic_family_id(), ctx),
-            m_replace(mk_default_expr_replacer(m))
+            m_replace(m)
         {}
         
         virtual void assign(contains_app& x, expr* fml, rational const& vl) {
@@ -51,7 +51,7 @@ namespace qe {
         virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
             SASSERT(vl.is_one() || vl.is_zero());
             expr* tf = (vl.is_one())?m.mk_true():m.mk_false();
-            m_replace->apply_substitution(x.x(), tf, 0, fml);
+            m_replace.apply_substitution(x.x(), tf, fml);
             if (def) {
                 *def = tf;
             }
@@ -103,12 +103,12 @@ namespace qe {
                 app* a = to_app(e);
                 expr* e1;
                 if (m_ctx.is_var(a, idx)) {
-                    m_replace->apply_substitution(a, m.mk_true(), 0, fml);
+                    m_replace.apply_substitution(a, m.mk_true(), fml);
                     m_ctx.elim_var(idx, fml, m.mk_true());
                     return true;
                 }
                 else if (m.is_not(e, e1) && m_ctx.is_var(e1, idx)) {
-                    m_replace->apply_substitution(to_app(e1), m.mk_false(), 0, fml);         
+                    m_replace.apply_substitution(to_app(e1), m.mk_false(), fml);         
                     m_ctx.elim_var(idx, fml, m.mk_false());
                     return true;           
                 }
@@ -148,7 +148,7 @@ namespace qe {
                 }
                 // only occurrences of 'x' must be in positive atoms
                 def = m.mk_true();
-                m_replace->apply_substitution(x, def, 0, fml);
+                m_replace.apply_substitution(x, def, fml);
                 return true;
             }
             else if (!p && n) {
@@ -161,7 +161,7 @@ namespace qe {
                     if (x != *it && contains_x(*it)) return false;
                 }
                 def = m.mk_false();
-                m_replace->apply_substitution(x, def, 0, fml);
+                m_replace.apply_substitution(x, def, fml);
                 return true;            
             }
             else if (contains_x(fml)) {

src/muz_qe/qe_bv_plugin.cpp

@@ -21,19 +21,19 @@ Notes:
 --*/
 
 #include "qe.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "bv_decl_plugin.h"
 #include "model_evaluator.h"
 
 namespace qe {
 
     class bv_plugin : public qe_solver_plugin {
-        scoped_ptr<expr_replacer> m_replace;
+        expr_safe_replace m_replace;
-        bv_util      m_bv;
+        bv_util           m_bv;
     public:
         bv_plugin(i_solver_context& ctx, ast_manager& m): 
             qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
-            m_replace(mk_default_expr_replacer(m)),
+            m_replace(m),
             m_bv(m)
         {}
 
@@ -48,7 +48,7 @@ namespace qe {
 
         virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
             app_ref c(m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x())), m);
-            m_replace->apply_substitution(x.x(), c, 0, fml);
+            m_replace.apply_substitution(x.x(), c, fml);
             if (def) {
                 *def = m_bv.mk_numeral(vl, m_bv.get_bv_size(x.x()));
             }

src/muz_qe/qe_datatype_plugin.cpp

@@ -95,7 +95,7 @@
 
 #include "qe.h"
 #include "datatype_decl_plugin.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "obj_pair_hashtable.h"
 #include "for_each_expr.h"
 #include "ast_pp.h"
@@ -415,7 +415,7 @@ namespace qe {
         typedef obj_pair_map<app, func_decl, subst_clos*> subst_map;
 
         datatype_util              m_datatype_util;
-        scoped_ptr<expr_replacer>  m_replace;
+        expr_safe_replace          m_replace;
         eqs_cache                  m_eqs_cache;
         subst_map                  m_subst_cache;
         ast_ref_vector             m_trail;
@@ -424,7 +424,7 @@ namespace qe {
         datatype_plugin(i_solver_context& ctx, ast_manager& m) : 
             qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
             m_datatype_util(m),
-            m_replace(mk_default_expr_replacer(m)),
+            m_replace(m),
             m_trail(m)
         {
         }
@@ -518,7 +518,7 @@ namespace qe {
             subst_clos* sub = 0;
             
             if (m_subst_cache.find(x.x(), c, sub)) {
-                m_replace->apply_substitution(x.x(), sub->first, 0, fml);
+                m_replace.apply_substitution(x.x(), sub->first, fml);
                 add_def(sub->first, def);
                 for (unsigned i = 0; i < sub->second.size(); ++i) {
                     m_ctx.add_var(sub->second[i]);
@@ -541,7 +541,7 @@ namespace qe {
             m_trail.push_back(t);
 
             add_def(t, def);
-            m_replace->apply_substitution(x.x(), t, 0, fml);
+            m_replace.apply_substitution(x.x(), t, fml);
             sub->first = t;
             m_subst_cache.insert(x.x(), c, sub);
         }
@@ -673,7 +673,7 @@ namespace qe {
                 fml = m.mk_and(is_c, fml);
                 app_ref fresh_x(m.mk_fresh_const("x", s), m);
                 m_ctx.add_var(fresh_x);
-                m_replace->apply_substitution(x, fresh_x, 0, fml);
+                m_replace.apply_substitution(x, fresh_x, fml);
                 add_def(fresh_x, def);
                 TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
                 return;
@@ -697,33 +697,33 @@ namespace qe {
             for (unsigned i = 0; i < eqs.num_recognizers(); ++i) {
                 app* rec = eqs.recognizer(i);
                 if (rec->get_decl() == r) {
-                    m_replace->apply_substitution(rec, m.mk_true(), fml);
+                    m_replace.apply_substitution(rec, m.mk_true(), fml);
                 }
                 else {
-                    m_replace->apply_substitution(rec, m.mk_false(), fml);
+                    m_replace.apply_substitution(rec, m.mk_false(), fml);
                 }
             }
 
             for (unsigned i = 0; i < eqs.num_unsat(); ++i) {
-                m_replace->apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml);
+                m_replace.apply_substitution(eqs.unsat_atom(i), m.mk_false(), fml);
             }
 
             if (idx < eqs.num_eqs()) {
                 expr* t = eqs.eq(idx);
                 expr* c = eqs.eq_cond(idx);
                 add_def(t, def);
-                m_replace->apply_substitution(x, t, fml);
+                m_replace.apply_substitution(x, t, fml);
                 if (!m.is_true(c)) {
                     fml = m.mk_and(c, fml);
                 }
             }
             else {                
                 for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
-                    m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
+                    m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
                 }
 
                 for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
-                    m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
+                    m_replace.apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
                 }
                 if (def) {
                     sort* s = m.get_sort(x);

src/muz_qe/qe_dl_plugin.cpp

@@ -1,6 +1,6 @@
 
 #include "qe.h"
-#include "expr_replacer.h"
+#include "expr_safe_replace.h"
 #include "dl_decl_plugin.h"
 #include "obj_pair_hashtable.h"
 #include "ast_pp.h"
@@ -35,7 +35,7 @@ namespace qe {
 
     class dl_plugin : public qe_solver_plugin {
         typedef obj_pair_map<app,  expr, eq_atoms*> eqs_cache;
-        scoped_ptr<expr_replacer> m_replace;
+        expr_safe_replace         m_replace;
         datalog::dl_decl_util     m_util;
         expr_ref_vector           m_trail;
         eqs_cache                 m_eqs_cache;
@@ -44,7 +44,7 @@ namespace qe {
     public:
         dl_plugin(i_solver_context& ctx, ast_manager& m) : 
             qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
-            m_replace(mk_default_expr_replacer(m)),
+            m_replace(m),
             m_util(m),
             m_trail(m)
         {
@@ -140,7 +140,7 @@ namespace qe {
 
         void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) {
             expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m);
-            m_replace->apply_substitution(x.x(), vl, fml);
+            m_replace.apply_substitution(x.x(), vl, fml);
         }
 
         // assumes that all disequalities can be satisfied.
@@ -148,15 +148,15 @@ namespace qe {
             SASSERT(w <= eqs.num_eqs());
             if (w < eqs.num_eqs()) {
                 expr* e = eqs.eq(w);
-                m_replace->apply_substitution(x.x(), e, fml);
+                m_replace.apply_substitution(x.x(), e, fml);
             }
             else {               
                 for (unsigned i = 0; i < eqs.num_eqs(); ++i) {
-                    m_replace->apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
+                    m_replace.apply_substitution(eqs.eq_atom(i), m.mk_false(), fml);
                 }
 
                 for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
-                    m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
+                    m_replace.apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
                 }
             }
         }

src/muz_qe/rel_context.cpp

@@ -75,7 +75,8 @@ namespace datalog {
     };
 
     rel_context::rel_context(context& ctx)
-        : m_context(ctx), 
+        : engine_base(ctx.get_manager(), "datalog"), 
+          m_context(ctx), 
           m(ctx.get_manager()),
           m_rmanager(ctx),
           m_answer(m), 

src/muz_qe/rel_context.h

@@ -30,7 +30,7 @@ namespace datalog {
     class context;
     typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
 
-    class rel_context {
+    class rel_context : public engine_base {
         context&           m_context;
         ast_manager&       m;
         relation_manager   m_rmanager;
@@ -59,11 +59,11 @@ namespace datalog {
         context&     get_context() const { return m_context; }
         relation_base & get_relation(func_decl * pred); 
         relation_base * try_get_relation(func_decl * pred) const; 
-        expr_ref get_last_answer() { return m_answer; }
+        virtual expr_ref get_answer() { return m_answer; }
 
         bool output_profile() const;
 
-        lbool query(expr* q);
+        virtual lbool query(expr* q);
         lbool query(unsigned num_rels, func_decl * const* rels);
 
         void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
@@ -73,6 +73,9 @@ namespace datalog {
 
         void set_cancel(bool f);
 
+        virtual void cancel() { set_cancel(true); }
+        virtual void cleanup() { set_cancel(false);}
+
         /**
            \brief Restrict the set of used predicates to \c res.
 

src/muz_qe/tab_context.cpp

@@ -1657,6 +1657,7 @@ namespace datalog {
     };
 
     tab::tab(context& ctx):
+        datalog::engine_base(ctx.get_manager(),"tabulation"),
         m_imp(alloc(imp, ctx)) {        
     }
     tab::~tab() {

src/muz_qe/tab_context.h

@@ -22,23 +22,24 @@ Revision History:
 #include "ast.h"
 #include "lbool.h"
 #include "statistics.h"
+#include "dl_util.h"
 
 namespace datalog {
     class context;
 
-    class tab {
+    class tab : public engine_base {
         class imp;
         imp* m_imp;
     public:
         tab(context& ctx);
         ~tab();
-        lbool query(expr* query);
+        virtual lbool query(expr* query);
-        void cancel();
+        virtual void cancel();
-        void cleanup();
+        virtual void cleanup();
-        void reset_statistics();
+        virtual void reset_statistics();
-        void collect_statistics(statistics& st) const;
+        virtual void collect_statistics(statistics& st) const;
-        void display_certificate(std::ostream& out) const;        
+        virtual void display_certificate(std::ostream& out) const;        
-        expr_ref get_answer();
+        virtual expr_ref get_answer();
     };
 };
 

src/shell/datalog_frontend.cpp

@@ -75,7 +75,7 @@ static void display_statistics(
 
         out << "--------------\n";
         out << "instructions  \n";
-        code.display(ctx.get_rel_context(), out);
+        code.display(*ctx.get_rel_context(), out);
 
         out << "--------------\n";
         out << "big relations \n";
@@ -83,7 +83,7 @@ static void display_statistics(
     }
     out << "--------------\n";
     out << "relation sizes\n";
-    ctx.get_rel_context().get_rmanager().display_relation_sizes(out);
+    ctx.get_rel_context()->get_rmanager().display_relation_sizes(out);
 
     if (verbose) {
         out << "--------------\n";
@@ -125,7 +125,7 @@ unsigned read_datalog(char const * file) {
     params.set_sym("engine", symbol("datalog"));
 
     datalog::context ctx(m, s_params, params);
-    datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
+    datalog::relation_manager & rmgr = ctx.get_rel_context()->get_rmanager();
     datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable"));
     SASSERT(&inner_plg);
     rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
@@ -187,7 +187,7 @@ unsigned read_datalog(char const * file) {
             
             datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
             
-            TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout););
+            TRACE("dl_compiler", rules_code.display(*ctx.get_rel_context(), tout););
             
             rules_code.make_annotations(ex_ctx);
             
@@ -227,10 +227,10 @@ unsigned read_datalog(char const * file) {
         
 
         TRACE("dl_compiler", ctx.display(tout);
-              rules_code.display(ctx.get_rel_context(), tout););
+              rules_code.display(*ctx.get_rel_context(), tout););
         
         if (ctx.get_params().output_tuples()) {
-            ctx.get_rel_context().display_output_facts(ctx.get_rules(), std::cout);
+            ctx.get_rel_context()->display_output_facts(ctx.get_rules(), std::cout);
         }
 
         display_statistics(

src/smt/theory_array_base.cpp

@@ -688,7 +688,7 @@ namespace smt {
             }
         }
     }
-
+    
     void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, svector<enode_pair> & todo) {
         SASSERT(r->get_root() == r);
         SASSERT(is_select(sel));
@@ -880,7 +880,7 @@ namespace smt {
             }
             else {
                 theory_var r    = mg_find(v);
-                void * else_val = m_else_values[r];
+                void * else_val = m_else_values[r];                
                 // DISABLED. It seems wrong, since different nodes can share the same
                 // else_val according to the mg class.
                 // SASSERT(else_val == 0 || get_context().is_relevant(UNTAG(app*, else_val)));

src/tactic/fpa/fpa2bv_converter.cpp

@@ -1113,7 +1113,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     mk_nzero(f, nzero); 
     mk_pzero(f, pzero);
     mk_minus_inf(f, ninf);
-    mk_plus_inf(f, pinf);        
+    mk_plus_inf(f, pinf);
 
     expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
     expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
@@ -1134,6 +1134,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     mk_is_neg(z, z_is_neg);
     mk_is_inf(z, z_is_inf);
 
+    expr_ref rm_is_to_neg(m);
+    mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
+
     dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan);
     dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero);
     dbg_decouple("fpa2bv_fma_x_is_pos", x_is_pos);
@@ -1187,31 +1190,28 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     m_simp.mk_or(x_is_zero, inf_cond, inf_or);
     mk_ite(inf_or, nan, neg_x_sgn_inf, v5);
 
-    // z is +-INF -> Z.
+    // z is +-INF -> z.
     mk_is_inf(z, c6);
     v6 = z;
 
-    // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign
+    // (x is 0) || (y is 0) -> z
     m_simp.mk_or(x_is_zero, y_is_zero, c7);
-    expr_ref sign_xor(m);
+    expr_ref ite_c(m);
-    m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor);
+    m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c);
-    mk_ite(sign_xor, nzero, pzero, v7);    
+    mk_ite(ite_c, pzero, z, v7);
     
         
     // else comes the fused multiplication.
     unsigned ebits = m_util.get_ebits(f->get_range());
     unsigned sbits = m_util.get_sbits(f->get_range());
-    SASSERT(ebits <= sbits);
+    SASSERT(ebits <= sbits);    
-
-    expr_ref rm_is_to_neg(m);
-    mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
 
     expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
     expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
     expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m);
     unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
     unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
-    unpack(z, c_sgn, c_sig, c_exp, c_lz, true);
+    unpack(z, c_sgn, c_sig, c_exp, c_lz, true);    
 
     expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m);
     a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
@@ -1220,12 +1220,22 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
 
     expr_ref a_sig_ext(m), b_sig_ext(m);
     a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig);
-    b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig);
+    b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig);    
 
     expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m);
     a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
     b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
-    c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp);
+    c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp);    
+
+    dbg_decouple("fpa2bv_fma_a_sig", a_sig_ext);
+    dbg_decouple("fpa2bv_fma_b_sig", b_sig_ext);
+    dbg_decouple("fpa2bv_fma_c_sig", c_sig);
+    dbg_decouple("fpa2bv_fma_a_exp", a_exp_ext);
+    dbg_decouple("fpa2bv_fma_b_exp", b_exp_ext);
+    dbg_decouple("fpa2bv_fma_c_exp", c_exp_ext);
+    dbg_decouple("fpa2bv_fma_a_lz", a_lz_ext);
+    dbg_decouple("fpa2bv_fma_b_lz", b_lz_ext);
+    dbg_decouple("fpa2bv_fma_c_lz", c_lz_ext);
 
     expr_ref mul_sgn(m), mul_sig(m), mul_exp(m);
     expr * signs[2] = { a_sgn, b_sgn };
@@ -1247,6 +1257,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     
     // Extend c
     c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1)));
+    c_exp_ext = m_bv_util.mk_bv_sub(c_exp_ext, c_lz_ext);
 
     SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits);
     SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits);
@@ -1254,6 +1265,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     expr_ref swap_cond(m);
     swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext);
     SASSERT(is_well_sorted(m, swap_cond));
+    dbg_decouple("fpa2bv_fma_swap_cond", swap_cond);
 
     expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m);
     m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn);
@@ -1261,7 +1273,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2
     m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn);
     m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits
-    m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2
+    m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2        
 
     SASSERT(is_well_sorted(m, e_sgn));
     SASSERT(is_well_sorted(m, e_sig));
@@ -1270,6 +1282,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     SASSERT(is_well_sorted(m, f_sig));
     SASSERT(is_well_sorted(m, f_exp));
 
+    SASSERT(m_bv_util.get_bv_size(e_sig) == 2 * sbits);
+    SASSERT(m_bv_util.get_bv_size(f_sig) == 2 * sbits);
+    SASSERT(m_bv_util.get_bv_size(e_exp) == ebits + 2);
+    SASSERT(m_bv_util.get_bv_size(f_exp) == ebits + 2);
+
     expr_ref res_sgn(m), res_sig(m), res_exp(m);
     
     expr_ref exp_delta(m);
@@ -1278,50 +1295,50 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
 
     // cap the delta    
     expr_ref cap(m), cap_le_delta(m);
-    cap = m_bv_util.mk_numeral(sbits+3, ebits+2);
+    cap = m_bv_util.mk_numeral(2*sbits, ebits+2);
-    cap_le_delta = m_bv_util.mk_ule(exp_delta, cap);
+    cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
     m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
     SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2);
+    SASSERT(is_well_sorted(m, exp_delta));
     dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta);
     
-    // Alignment shift with sticky bit computation.    
+    // Alignment shift with sticky bit computation.
-    expr_ref big_f_sig(m);
-    big_f_sig = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits+4));    
-    SASSERT(is_well_sorted(m, big_f_sig));
-
     expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m);
-    shifted_big = m_bv_util.mk_bv_lshr(big_f_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+4))-(ebits+2)), exp_delta));
+    shifted_big = m_bv_util.mk_bv_lshr(
-    shifted_f_sig = m_bv_util.mk_extract((2*(sbits+4)-1), (sbits+4), shifted_big);
+                    m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), 
-    SASSERT(is_well_sorted(m, shifted_f_sig));
+                    m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
-
+    shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big);
-    sticky_raw = m_bv_util.mk_extract(sbits+3, 0, shifted_big);    
+    sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); 
-    expr_ref sticky(m), sticky_eq(m), nil_sbit4(m), one_sbit4(m); 
+    SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits);
-    nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
+    SASSERT(is_well_sorted(m, shifted_f_sig));    
-    one_sbit4 = m_bv_util.mk_numeral(1, sbits+4);
+       
-    m_simp.mk_eq(sticky_raw, nil_sbit4, sticky_eq);
+    expr_ref sticky(m); 
-    m_simp.mk_ite(sticky_eq, nil_sbit4, one_sbit4, sticky);
+    sticky = m_bv_util.mk_zero_extend(2*sbits-1, m.mk_app(m_bv_util.get_fid(), OP_BREDOR, sticky_raw.get()));
     SASSERT(is_well_sorted(m, sticky));
+    dbg_decouple("fpa2bv_fma_f_sig_sticky_raw", sticky_raw);
+    dbg_decouple("fpa2bv_fma_f_sig_sticky", sticky);
     
     expr * or_args[2] = { shifted_f_sig, sticky };
     shifted_f_sig = m_bv_util.mk_bv_or(2, or_args);
     SASSERT(is_well_sorted(m, shifted_f_sig));
 
-    expr_ref eq_sgn(m);
+    // Significant addition.
-    m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
+    // Two extra bits for catching the overflow.
-    
-    // two extra bits for catching the overflow.
     e_sig = m_bv_util.mk_zero_extend(2, e_sig);
     shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig);
 
-    SASSERT(m_bv_util.get_bv_size(e_sig) == sbits+6);
+    expr_ref eq_sgn(m);
-    SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == sbits+6);
+    m_simp.mk_eq(e_sgn, f_sgn, eq_sgn);
+
+    SASSERT(m_bv_util.get_bv_size(e_sig) == 2*sbits + 2);
+    SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2*sbits + 2);
 
     dbg_decouple("fpa2bv_fma_add_e_sig", e_sig);
     dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig);
 
     expr_ref sum(m);
     m_simp.mk_ite(eq_sgn, 
-                  m_bv_util.mk_bv_add(e_sig, shifted_f_sig), // ADD LZ
+                  m_bv_util.mk_bv_add(e_sig, shifted_f_sig),
                   m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),                  
                   sum);
 
@@ -1330,14 +1347,22 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     dbg_decouple("fpa2bv_fma_add_sum", sum);
 
     expr_ref sign_bv(m), n_sum(m);
-    sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum);        
+    sign_bv = m_bv_util.mk_extract(2*sbits+1, 2*sbits+1, sum);        
     n_sum = m_bv_util.mk_bv_neg(sum);
 
+    expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
+    one_1 = m_bv_util.mk_numeral(1, 1);
+    m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
+    m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
     dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv);    
     dbg_decouple("fpa2bv_fma_add_n_sum", n_sum);         
-    
+    dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
-    family_id bvfid = m_bv_util.get_fid();
 
+    res_exp = e_exp;
+    
+    // Result could overflow into 4.xxx ...
+
+    family_id bvfid = m_bv_util.get_fid();
     expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
     expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m);
     not_e_sgn = m_bv_util.mk_bv_not(e_sgn);
@@ -1348,21 +1373,18 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
     res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
     expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };   
     res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
+    
+    sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs);
+    sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get()));
+    dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky);
 
-    expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
+    expr * res_or_args[2] = {  m_bv_util.mk_extract(2*sbits-1, sbits-4, sig_abs), sticky };
-    one_1 = m_bv_util.mk_numeral(1, 1);
+    res_sig = m_bv_util.mk_bv_or(2, res_or_args);
-    m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
+    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
-    m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
-
-    dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs);
-
-    res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs);
-    res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext);
     
     expr_ref is_zero_sig(m), nil_sbits4(m);
     nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
     m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
-
     SASSERT(is_well_sorted(m, is_zero_sig));
 
     dbg_decouple("fpa2bv_fma_is_zero_sig", is_zero_sig);
@@ -1390,7 +1412,151 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
 }
 
 void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    NOT_IMPLEMENTED_YET();
+    SASSERT(num == 2);
+    
+    expr_ref rm(m), x(m);
+    rm = args[0];
+    x = args[1];    
+
+    expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
+    mk_nan(f, nan);
+    mk_nzero(f, nzero); 
+    mk_pzero(f, pzero);
+    mk_minus_inf(f, ninf);
+    mk_plus_inf(f, pinf);
+
+    expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);    
+    mk_is_nan(x, x_is_nan);
+    mk_is_zero(x, x_is_zero);
+    mk_is_pos(x, x_is_pos);
+    mk_is_inf(x, x_is_inf);
+    
+    expr_ref zero1(m), one1(m);
+    zero1 = m_bv_util.mk_numeral(0, 1);
+    one1 = m_bv_util.mk_numeral(1, 1);
+    
+    expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m);
+    expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m);
+
+    // (x is NaN) -> NaN
+    c1 = x_is_nan;
+    v1 = x;
+    
+    // (x is +oo) -> +oo
+    mk_is_pinf(x, c2);
+    v2 = x;
+                
+    // (x is +-0) -> +-0
+    mk_is_zero(x, c3);
+    v3 = x;
+    
+    // (x < 0) -> NaN
+    mk_is_neg(x, c4);
+    v4 = nan;
+
+    // else comes the actual square root.
+    unsigned ebits = m_util.get_ebits(f->get_range());
+    unsigned sbits = m_util.get_sbits(f->get_range());
+    SASSERT(ebits <= sbits);
+
+    expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
+    unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
+
+    dbg_decouple("fpa2bv_sqrt_sig", a_sig);
+    dbg_decouple("fpa2bv_sqrt_exp", a_exp);
+
+    SASSERT(m_bv_util.get_bv_size(a_sig) == sbits);
+    SASSERT(m_bv_util.get_bv_size(a_exp) == ebits);
+
+    expr_ref res_sgn(m), res_sig(m), res_exp(m);
+
+    res_sgn = zero1;
+
+    expr_ref real_exp(m);
+    real_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(1, a_exp), m_bv_util.mk_zero_extend(1, a_lz));
+    res_exp = m_bv_util.mk_sign_extend(2, m_bv_util.mk_extract(ebits, 1, real_exp));
+
+    expr_ref e_is_odd(m);
+    e_is_odd = m.mk_eq(m_bv_util.mk_extract(0, 0, real_exp), one1);
+
+    dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd);
+    dbg_decouple("fpa2bv_sqrt_real_exp", real_exp);
+
+    expr_ref sig_prime(m);    
+    m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1),
+                            m_bv_util.mk_concat(zero1, a_sig), 
+                            sig_prime);
+    SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1);        
+    dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime);
+
+    // This is algorithm 10.2 in the Handbook of Floating-Point Arithmetic
+    expr_ref Q(m), R(m), S(m), T(m);
+
+    const mpz & p2 = fu().fm().m_powers2(sbits+3);
+    Q = m_bv_util.mk_numeral(p2, sbits+5);
+    R = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(sig_prime, m_bv_util.mk_numeral(0, 4)), Q);
+    S = Q;
+
+    for (unsigned i = 0; i < sbits + 3; i++) {
+        dbg_decouple("fpa2bv_sqrt_Q", Q);
+        dbg_decouple("fpa2bv_sqrt_R", R);
+
+        S = m_bv_util.mk_concat(zero1, m_bv_util.mk_extract(sbits+4, 1, S));
+        
+        expr_ref twoQ_plus_S(m);
+        twoQ_plus_S = m_bv_util.mk_bv_add(m_bv_util.mk_concat(Q, zero1), m_bv_util.mk_concat(zero1, S));
+        T = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(R, zero1), twoQ_plus_S);
+
+        dbg_decouple("fpa2bv_sqrt_T", T);
+
+        SASSERT(m_bv_util.get_bv_size(Q) == sbits + 5);
+        SASSERT(m_bv_util.get_bv_size(R) == sbits + 5);
+        SASSERT(m_bv_util.get_bv_size(S) == sbits + 5);
+        SASSERT(m_bv_util.get_bv_size(T) == sbits + 6);
+
+        expr_ref t_lt_0(m);
+        m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0);        
+        
+        expr * or_args[2] = { Q, S };
+
+        m_simp.mk_ite(t_lt_0, Q,
+                              m_bv_util.mk_bv_or(2, or_args),
+                              Q);
+        m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), 
+                              m_bv_util.mk_extract(sbits+4, 0, T), 
+                              R);
+    }
+
+    expr_ref is_exact(m);
+    m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact);
+    dbg_decouple("fpa2bv_sqrt_is_exact", is_exact);    
+
+    expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m);
+    last = m_bv_util.mk_extract(0, 0, Q);
+    rest = m_bv_util.mk_extract(sbits+3, 1, Q);
+    dbg_decouple("fpa2bv_sqrt_last", last);
+    dbg_decouple("fpa2bv_sqrt_rest", rest);
+    rest_ext = m_bv_util.mk_zero_extend(1, rest);
+    expr_ref sticky(m);
+    m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last),
+                            m_bv_util.mk_numeral(1, sbits+4),
+                            sticky);
+    expr * or_args[2] = { rest_ext, sticky };
+    res_sig = m_bv_util.mk_bv_or(2, or_args);
+
+    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
+
+    expr_ref rounded(m);
+    round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);    
+    v5 = rounded;
+
+    // And finally, we tie them together.
+    mk_ite(c4, v4, v5, result);
+    mk_ite(c3, v3, result, result);
+    mk_ite(c2, v2, result, result);
+    mk_ite(c1, v1, result, result);
+
+    SASSERT(is_well_sorted(m, result));
 }
 
 void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -2105,14 +2271,16 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
     zero_e = m_bv_util.mk_numeral(0, ebits);
 
     if (normalize) {
+        expr_ref is_sig_zero(m), zero_s(m);
+        zero_s = m_bv_util.mk_numeral(0, sbits);
+        m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero);
+
         expr_ref lz_d(m);
-        mk_leading_zeros(denormal_sig, ebits, lz_d);
+        mk_leading_zeros(denormal_sig, ebits, lz_d);        
-        m_simp.mk_ite(is_normal, zero_e, lz_d, lz);
+        m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz);
         dbg_decouple("fpa2bv_unpack_lz", lz);
 
-        expr_ref is_sig_zero(m), shift(m), zero_s(m);
+        expr_ref shift(m);        
-        zero_s = m_bv_util.mk_numeral(0, sbits);
-        m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero);                
         m_simp.mk_ite(is_sig_zero, zero_e, lz, shift);
         dbg_decouple("fpa2bv_unpack_shift", shift);
         SASSERT(is_well_sorted(m, is_sig_zero));