mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6616b6a366
commit
8a568d438f
|
@ -114,7 +114,7 @@ namespace recfun {
|
|||
void compute_cases(util& u, replace& subst, is_immediate_pred &,
|
||||
unsigned n_vars, var *const * vars, expr* rhs);
|
||||
void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
|
||||
bool contains_ite(util& u, expr* e); // expression contains a test?
|
||||
bool contains_ite(util& u, expr* e); // expression contains a test over a def?
|
||||
bool contains_def(util& u, expr* e); // expression contains a def
|
||||
public:
|
||||
symbol const & get_name() const { return m_name; }
|
||||
|
|
Loading…
Reference in a new issue