Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr

src/ackr/ackr_info.h

@@ -20,15 +20,16 @@ Revision History:
 #include"ref.h"
 #include"expr_replacer.h"
 
-//
-// Information about how a formula was extracted into
-// a formula without  uninterpreted function symbols.
-//
-// The intended use is that new terms are added via set_abstr.
-// Once all terms are abstracted, call seal.
-// abstract may only be called when sealed.
-//
-//  The class enables reference counting.
+/** \brief
+   Information about how a formula is being converted into
+   a formula without  uninterpreted function symbols via ackermannization.
+
+ The intended use is that new terms are added via set_abstr.
+ Once all terms are abstracted, call seal.
+ The function abstract may only be called when sealed.
+
+   The class enables reference counting.
+**/
 class ackr_info {
     public:
         ackr_info(ast_manager& m)

src/ackr/lackr.cpp

@@ -60,6 +60,13 @@ lbool lackr::operator() () {
     return rv;
 }
 
+void lackr::mk_ackermann(/*out*/goal_ref& g) {
+    init();
+    eager_enc();
+    for (unsigned i = 0; i < m_abstr.size(); ++i) g->assert_expr(m_abstr.get(i));
+    for (unsigned i = 0; i < m_ackrs.size(); ++i) g->assert_expr(m_ackrs.get(i));
+}
+
 void lackr::init() {
     params_ref simp_p(m_p);
     m_simp.updt_params(simp_p);
@@ -82,6 +89,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
         expr * const arg2 = t2->get_arg(gi);
         if (arg1 == arg2) continue;
         if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) {
+            // quickly abort if there are two distinct numerals
             SASSERT(arg1 != arg2);
             TRACE("lackr", tout << "never eq\n";);
             return false;

src/ackr/lackr.h

@@ -27,6 +27,7 @@
 #include"solver.h"
 #include"util.h"
 #include"tactic_exception.h"
+#include"goal.h"
 
 struct lackr_stats {
     lackr_stats() : m_it(0), m_ackrs_sz(0) {}
@@ -35,6 +36,10 @@ struct lackr_stats {
     unsigned    m_ackrs_sz; // number of congruence constraints
 };
 
+/** \brief
+   A class to encode or directly solve problems with uninterpreted functions via ackermannization.
+   Currently, solving is supported only for QF_UFBV.
+**/
 class lackr {
     public:
         lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas);
@@ -44,8 +49,20 @@ class lackr {
             m_eager = p.eager();
             m_use_sat = p.sat_backend();
         }
+
+        /** \brief
+         * Solve the formula that the class was initialized with.
+         **/
         lbool operator() ();
 
+
+        /** \brief
+        * Converts function occurrences to constants and encodes all congruence ackermann lemmas.
+        * This guarantees a equisatisfiability with the input formula. It has a worst-case quadratic blowup.
+        **/
+        void mk_ackermann(/*out*/goal_ref& g);
+
+
         //
         // getters
         //

src/ackr/lackr_tactic.h

@@ -21,7 +21,7 @@ Revision History:
 tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p);
 
 /*
-ADD_TACTIC("lackr", "lackr.", "mk_lackr_tactic(m, p)")
+ADD_TACTIC("lackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_lackr_tactic(m, p)")
 */
 
 #endif