mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Resurrected the dack* options.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-03-04 19:14:57 +00:00
parent 6630994a3d
commit 55ca6ce44b
4 changed files with 23 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/params/dyn_ack_params.cpp
View file

@ -17,16 +17,14 @@ Revision History:
--*/ --*/
#include"dyn_ack_params.h" #include"dyn_ack_params.h"
#include"smt_params_helper.hpp"
#if 0 void dyn_ack_params::updt_params(params_ref const & _p) {
void dyn_ack_params::register_params(ini_params & p) { smt_params_helper p(_p);
p.register_int_param("dack", 0, 2, reinterpret_cast<int&>(m_dack), m_dack = static_cast<dyn_ack_strategy>(p.dack());
"0 - disable dynamic ackermannization, 1 - expand Leibniz's axiom if a congruence is the root of a conflict, 2 - expand Leibniz's axiom if a congruence is used during conflict resolution."); m_dack_eq = p.dack_eq();
p.register_bool_param("dack_eq", m_dack_eq, "enable dynamic ackermannization for transtivity of equalities"); m_dack_factor = p.dack_factor();
p.register_unsigned_param("dack_threshold", m_dack_threshold, "number of times the congruence rule must be used before Leibniz's axiom is expanded"); m_dack_threshold = p.dack_threshold();
p.register_double_param("dack_factor", m_dack_factor, "number of instance per conflict"); m_dack_gc = p.dack_gc();
p.register_unsigned_param("dack_gc", m_dack_gc, "Dynamic ackermannization garbage collection frequency (per conflict)."); m_dack_gc_inv_decay = p.dack_gc_inv_decay();
p.register_double_param("dack_gc_inv_decay", m_dack_gc_inv_decay); }
}
#endif

6
src/smt/params/dyn_ack_params.h
View file

@ -19,6 +19,8 @@ Revision History:
#ifndef _DYN_ACK_PARAMS_H_ #ifndef _DYN_ACK_PARAMS_H_
#define _DYN_ACK_PARAMS_H_ #define _DYN_ACK_PARAMS_H_
#include"params.h"
enum dyn_ack_strategy { enum dyn_ack_strategy {
DACK_DISABLED, DACK_DISABLED,
DACK_ROOT, // congruence is the root of the conflict DACK_ROOT, // congruence is the root of the conflict
@ -34,15 +36,17 @@ struct dyn_ack_params {
double m_dack_gc_inv_decay; double m_dack_gc_inv_decay;
public: public:
dyn_ack_params(): dyn_ack_params(params_ref const & p = params_ref()) :
m_dack(DACK_ROOT), m_dack(DACK_ROOT),
m_dack_eq(false), m_dack_eq(false),
m_dack_factor(0.1), m_dack_factor(0.1),
m_dack_threshold(10), m_dack_threshold(10),
m_dack_gc(2000), m_dack_gc(2000),
m_dack_gc_inv_decay(0.8) { m_dack_gc_inv_decay(0.8) {
updt_params(p);
} }
void updt_params(params_ref const & _p);
}; };

1
src/smt/params/smt_params.cpp
View file

@ -46,6 +46,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
void smt_params::updt_params(params_ref const & p) { void smt_params::updt_params(params_ref const & p) {
preprocessor_params::updt_params(p); preprocessor_params::updt_params(p);
dyn_ack_params::updt_params(p);
qi_params::updt_params(p); qi_params::updt_params(p);
theory_arith_params::updt_params(p); theory_arith_params::updt_params(p);
theory_bv_params::updt_params(p); theory_bv_params::updt_params(p);

8
src/smt/params/smt_params_helper.pyg
View file

@ -45,5 +45,11 @@ def_module_params(module_name='smt',
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
('array.weak', BOOL, False, 'weak array theory'), ('array.weak', BOOL, False, 'weak array theory'),
('array.extensional', BOOL, True, 'extensional array theory') ('array.extensional', BOOL, True, 'extensional array theory'),
('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
('dack.eq', BOOL, False, 'enable dynamic ackermannization for transtivity of equalities'),
('dack.factor', DOUBLE, 0.1, 'number of instance per conflict'),
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded')
)) ))