mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

add DT translation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-01-03 01:47:57 -08:00
parent 129e048a1b
commit 2cd4669e21
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_ast.cpp
View file

@ -1076,7 +1076,6 @@ extern "C" {
case OP_BSREM_I:
case OP_BUREM_I:
case OP_BSMOD_I:
return Z3_OP_UNINTERPRETED;
default:
UNREACHABLE();
@ -1085,9 +1084,10 @@ extern "C" {
}
if (mk_c(c)->get_dt_fid() == _d->get_family_id()) {
switch(_d->get_decl_kind()) {
case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR;
case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER;
case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR;
case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR;
case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER;
case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR;
case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;