mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Move Z3_get_implied_equalities from v3 to v4 ml api as it now needs Z3_solver type

Browse source
This commit is contained in:
Josh Berdine 2012-12-20 12:54:44 +00:00
parent fd5372d7a2
commit a7f89dcdd2
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/z3_api.h
View file

@ -6924,12 +6924,15 @@ END_MLAPI_EXCLUDE
); );
/*@}*/ /*@}*/
#endif
/** /**
@name Deprecated Constraints API @name Deprecated Constraints API
*/ */
/*@{*/ /*@{*/
#ifdef CorML3
/** /**
\brief Set the SMTLIB logic to be used in the given logical context. \brief Set the SMTLIB logic to be used in the given logical context.
It is incorrect to invoke this function after invoking It is incorrect to invoke this function after invoking
@ -7111,7 +7114,9 @@ END_MLAPI_EXCLUDE
__out Z3_model * m, __out Z3_ast* proof, __out Z3_model * m, __out Z3_ast* proof,
__inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[] __inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[]
); );
#endif
#ifdef CorML4
/** /**
\brief Retrieve congruence class representatives for terms. \brief Retrieve congruence class representatives for terms.
@ -7142,7 +7147,9 @@ END_MLAPI_EXCLUDE
__in_ecount(num_terms) Z3_ast const terms[], __in_ecount(num_terms) Z3_ast const terms[],
__out_ecount(num_terms) unsigned class_ids[] __out_ecount(num_terms) unsigned class_ids[]
); );
#endif
#ifdef CorML3
/** /**
\brief Delete a model object. \brief Delete a model object.