mirror of
https://github.com/Z3Prover/z3
synced 2025-08-02 09:20:22 +00:00
added module descriptions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
1871bef6e1
commit
fa53b1eb92
17 changed files with 159 additions and 33 deletions
26
src/ast/simplifier/arith_simplifier_params.cpp
Normal file
26
src/ast/simplifier/arith_simplifier_params.cpp
Normal file
|
@ -0,0 +1,26 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
arith_simplifier_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"arith_simplifier_params.h"
|
||||
#include"arith_simplifier_params_helper.hpp"
|
||||
|
||||
void arith_simplifier_params::updt_params(params_ref const & _p) {
|
||||
arith_simplifier_params_helper p(_p);
|
||||
m_arith_expand_eqs = p.arith_expand_eqs();
|
||||
m_arith_process_all_eqs = p.arith_process_all_eqs();
|
||||
}
|
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#ifndef _ARITH_SIMPLIFIER_PARAMS_H_
|
||||
#define _ARITH_SIMPLIFIER_PARAMS_H_
|
||||
|
||||
#include"arith_simplifier_params_helper.hpp"
|
||||
#include"params.h"
|
||||
|
||||
struct arith_simplifier_params {
|
||||
bool m_arith_expand_eqs;
|
||||
|
@ -29,11 +29,7 @@ struct arith_simplifier_params {
|
|||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & _p) {
|
||||
arith_simplifier_params_helper p(_p);
|
||||
m_arith_expand_eqs = p.arith_expand_eqs();
|
||||
m_arith_process_all_eqs = p.arith_process_all_eqs();
|
||||
}
|
||||
void updt_params(params_ref const & _p);
|
||||
};
|
||||
|
||||
#endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */
|
||||
|
|
|
@ -1,5 +1,6 @@
|
|||
def_module_params(class_name='arith_simplifier_params_helper',
|
||||
module_name="old_simplify", # Parameters will be in the old_simplify module
|
||||
description="old simplification (stack) still used in the smt module",
|
||||
export=True,
|
||||
params=(
|
||||
('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'),
|
||||
|
|
26
src/ast/simplifier/array_simplifier_params.cpp
Normal file
26
src/ast/simplifier/array_simplifier_params.cpp
Normal file
|
@ -0,0 +1,26 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
array_simplifier_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
This file was created during code reorg.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"array_simplifier_params.h"
|
||||
#include"array_simplifier_params_helper.hpp"
|
||||
|
||||
void array_simplifier_params::updt_params(params_ref const & _p) {
|
||||
array_simplifier_params_helper p(_p);
|
||||
m_array_canonize_simplify = p.array_canonize();
|
||||
m_array_simplify = p.array_simplify();
|
||||
}
|
|
@ -1,5 +1,5 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#ifndef _ARRAY_SIMPLIFIER_PARAMS_H_
|
||||
#define _ARRAY_SIMPLIFIER_PARAMS_H_
|
||||
|
||||
#include"array_simplifier_params_helper.hpp"
|
||||
#include"params.h"
|
||||
|
||||
struct array_simplifier_params {
|
||||
bool m_array_canonize_simplify;
|
||||
|
@ -29,11 +29,7 @@ struct array_simplifier_params {
|
|||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & _p) {
|
||||
array_simplifier_params_helper p(_p);
|
||||
m_array_canonize_simplify = p.array_canonize();
|
||||
m_array_simplify = p.array_simplify();
|
||||
}
|
||||
void updt_params(params_ref const & _p);
|
||||
};
|
||||
|
||||
#endif /* _ARITH_SIMPLIFIER_PARAMS_H_ */
|
||||
|
|
26
src/ast/simplifier/bv_simplifier_params.cpp
Normal file
26
src/ast/simplifier/bv_simplifier_params.cpp
Normal file
|
@ -0,0 +1,26 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
bv_simplifier_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-12-02.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"bv_simplifier_params.h"
|
||||
#include"bv_simplifier_params_helper.hpp"
|
||||
|
||||
void bv_simplifier_params::updt_params(params_ref const & _p) {
|
||||
bv_simplifier_params_helper p(_p);
|
||||
m_hi_div0 = p.bv_hi_div0();
|
||||
m_bv2int_distribute = p.bv_bv2int_distribute();
|
||||
}
|
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#ifndef _BV_SIMPLIFIER_PARAMS_H_
|
||||
#define _BV_SIMPLIFIER_PARAMS_H_
|
||||
|
||||
#include"bv_simplifier_params_helper.hpp"
|
||||
#include"params.h"
|
||||
|
||||
struct bv_simplifier_params {
|
||||
bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted.
|
||||
|
@ -29,11 +29,7 @@ struct bv_simplifier_params {
|
|||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & _p) {
|
||||
bv_simplifier_params_helper p(_p);
|
||||
m_hi_div0 = p.bv_hi_div0();
|
||||
m_bv2int_distribute = p.bv_bv2int_distribute();
|
||||
}
|
||||
void updt_params(params_ref const & _p);
|
||||
};
|
||||
|
||||
#endif /* _BV_SIMPLIFIER_PARAMS_H_ */
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue