3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Editing some comments and also enabling to export the ackermannized formula as a gole.

This commit is contained in:
mikolas 2016-01-26 11:53:47 +00:00
parent d97e2b432c
commit d32c9449b2
4 changed files with 36 additions and 10 deletions

View file

@ -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)

View file

@ -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;

View file

@ -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
//

View file

@ -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