1 INCLUDE: <sstream> 2 INCLUDE: <theory_arith.h> 3 INCLUDE: <theory_array.h> 4 5 DEFINITION: Java_cvc3_ValidityChecker_jniCreate1 6 jobject 7 return embed_own<ValidityChecker>(env, VCL::create()); 8 9 DEFINITION: Java_cvc3_ValidityChecker_jniCreate2 10 jobject c CLFlags flags 11 return embed_own<ValidityChecker>(env, VCL::create(*flags)); 12 13 14 15 DEFINITION: Java_cvc3_ValidityChecker_jniCreateFlags 16 jobject 17 return embed_copy(env, ValidityChecker::createFlags()); 18 19 DEFINITION: Java_cvc3_ValidityChecker_jniGetFlags 20 jobject c ValidityChecker vc 21 return embed_mut_ref(env, &vc->getFlags()); 22 23 24 25 DEFINITION: Java_cvc3_ValidityChecker_jniBoolType 26 jobject m ValidityChecker vc 27 return embed_copy(env, vc->boolType()); 28 29 DEFINITION: Java_cvc3_ValidityChecker_jniRealType 30 jobject m ValidityChecker vc 31 return embed_copy(env, vc->realType()); 32 33 DEFINITION: Java_cvc3_ValidityChecker_jniIntType 34 jobject m ValidityChecker vc 35 return embed_copy(env, vc->intType()); 36 37 DEFINITION: Java_cvc3_ValidityChecker_jniSubrangeType 38 jobject m ValidityChecker vc c Expr l c Expr r 39 return embed_copy(env, vc->subrangeType(*l, *r)); 40 41 DEFINITION: Java_cvc3_ValidityChecker_jniSubtypeType 42 jobject m ValidityChecker vc c Expr pred c Expr witness 43 return embed_copy(env, vc->subtypeType(*pred, *witness)); 44 45 DEFINITION: Java_cvc3_ValidityChecker_jniTupleType1 46 jobject m ValidityChecker vc c Type type0 c Type type1 47 return embed_copy(env, vc->tupleType(*type0, *type1)); 48 49 DEFINITION: Java_cvc3_ValidityChecker_jniTupleType2 50 jobject m ValidityChecker vc c Type type0 c Type type1 c Type type2 51 return embed_copy(env, vc->tupleType(*type0, *type1, *type2)); 52 53 DEFINITION: Java_cvc3_ValidityChecker_jniTupleType3 54 jobject m ValidityChecker vc cv Type types 55 return embed_copy(env, vc->tupleType(types)); 56 57 DEFINITION: Java_cvc3_ValidityChecker_jniRecordType1 58 jobject m ValidityChecker vc n string field c Type type 59 return embed_copy(env, vc->recordType(field, *type)); 60 61 DEFINITION: Java_cvc3_ValidityChecker_jniRecordType2 62 jobject m ValidityChecker vc n string field0 c Type type0 n string field1 c Type type1 63 return embed_copy(env, vc->recordType(field0, *type0, field1, *type1)); 64 65 DEFINITION: Java_cvc3_ValidityChecker_jniRecordType3 66 jobject m ValidityChecker vc n string field0 c Type type0 n string field1 c Type type1 n string field2 c Type type2 67 return embed_copy(env, vc->recordType(field0, *type0, field1, *type1, field2, *type2)); 68 69 DEFINITION: Java_cvc3_ValidityChecker_jniRecordType4 70 jobject m ValidityChecker vc nv string fields cv Type types 71 return embed_copy(env, vc->recordType(fields, types)); 72 73 DEFINITION: Java_cvc3_ValidityChecker_jniDataType1 74 jobject m ValidityChecker vc n string name n string constructor nv string selectors cv Expr types 75 return embed_copy(env, vc->dataType(name, constructor, selectors, types)); 76 77 DEFINITION: Java_cvc3_ValidityChecker_jniDataType2 78 jobject m ValidityChecker vc n string name nv string constructors nvv string selectors cvv Expr types 79 return embed_copy(env, vc->dataType(name, constructors, selectors, types)); 80 81 DEFINITION: Java_cvc3_ValidityChecker_jniDataType3 82 jobjectArray m ValidityChecker vc nv string names nvv string constructors nvvv string selectors cvvv Expr types 83 vector<Type> result; 84 vc->dataType(names, constructors, selectors, types, result); 85 return toJavaVCopy(env, result); 86 87 DEFINITION: Java_cvc3_ValidityChecker_jniAnyType 88 jobject m ValidityChecker vc 89 return embed_copy(env, Type::anyType(vc->getEM())); 90 91 DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral 92 jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr 93 return embed_copy(env, CVC3::arrayLiteral(*indexVar, *bodyExpr)); 94 95 DEFINITION: Java_cvc3_ValidityChecker_jniArrayType 96 jobject m ValidityChecker vc c Type typeIndex c Type typeData 97 return embed_copy(env, vc->arrayType(*typeIndex, *typeData)); 98 99 DEFINITION: Java_cvc3_ValidityChecker_jniBitvecType 100 jobject m ValidityChecker vc n int n 101 return embed_copy(env, vc->bitvecType(n)); 102 103 DEFINITION: Java_cvc3_ValidityChecker_jniFunType1 104 jobject m ValidityChecker vc c Type typeDom c Type typeRange 105 return embed_copy(env, vc->funType(*typeDom, *typeRange)); 106 107 DEFINITION: Java_cvc3_ValidityChecker_jniFunType2 108 jobject m ValidityChecker vc cv Type typeDom c Type typeRange 109 return embed_copy(env, vc->funType(typeDom, *typeRange)); 110 111 DEFINITION: Java_cvc3_ValidityChecker_jniCreateType1 112 jobject m ValidityChecker vc n string typeName 113 return embed_copy(env, vc->createType(typeName)); 114 115 DEFINITION: Java_cvc3_ValidityChecker_jniCreateType2 116 jobject m ValidityChecker vc n string typeName c Type typeDef 117 return embed_copy(env, vc->createType(typeName, *typeDef)); 118 119 DEFINITION: Java_cvc3_ValidityChecker_jniLookupType 120 jobject m ValidityChecker vc n string typeName 121 return embed_copy(env, vc->lookupType(typeName)); 122 123 124 125 DEFINITION: Java_cvc3_ValidityChecker_jniGetExprManager 126 jobject m ValidityChecker vc 127 return embed_mut_ref(env, vc->getEM()); 128 129 DEFINITION: Java_cvc3_ValidityChecker_jniNullExpr 130 jobject m ValidityChecker vc 131 return embed_copy(env, Expr()); 132 133 DEFINITION: Java_cvc3_ValidityChecker_jniVarExpr1 134 jobject m ValidityChecker vc n string name c Type type 135 return embed_copy(env, vc->varExpr(name, *type)); 136 137 DEFINITION: Java_cvc3_ValidityChecker_jniVarExpr2 138 jobject m ValidityChecker vc n string name c Type type c Expr def 139 return embed_copy(env, vc->varExpr(name, *type, *def)); 140 141 DEFINITION: Java_cvc3_ValidityChecker_jniBoundVarExpr 142 jobject m ValidityChecker vc n string name n string uid c Type type 143 return embed_copy(env, vc->boundVarExpr(name, uid, *type)); 144 145 DEFINITION: Java_cvc3_ValidityChecker_jniLookupVar 146 jobject m ValidityChecker vc n string name 147 Type* type = new Type; 148 jobject result = embed_copy(env, vc->lookupVar(name, type)); 149 delete type; 150 return result; 151 152 DEFINITION: Java_cvc3_ValidityChecker_jniLookupOp 153 jobject m ValidityChecker vc n string name 154 Type* type = new Type; 155 jobject result = embed_copy(env, vc->lookupOp(name, type)); 156 delete type; 157 return result; 158 159 DEFINITION: Java_cvc3_ValidityChecker_jniGetType 160 jobject m ValidityChecker vc c Expr expr 161 return embed_copy(env, vc->getType(*expr)); 162 163 DEFINITION: Java_cvc3_ValidityChecker_jniGetBaseType1 164 jobject m ValidityChecker vc c Expr expr 165 return embed_copy(env, vc->getBaseType(*expr)); 166 167 DEFINITION: Java_cvc3_ValidityChecker_jniGetBaseType2 168 jobject m ValidityChecker vc c Type type 169 return embed_copy(env, vc->getBaseType(*type)); 170 171 DEFINITION: Java_cvc3_ValidityChecker_jniGetTypePred 172 jobject m ValidityChecker vc c Type type c Expr expr 173 return embed_copy(env, vc->getTypePred(*type, *expr)); 174 175 DEFINITION: Java_cvc3_ValidityChecker_jniStringExpr 176 jobject m ValidityChecker vc n string str 177 return embed_copy(env, vc->stringExpr(str)); 178 179 DEFINITION: Java_cvc3_ValidityChecker_jniIdExpr 180 jobject m ValidityChecker vc n string name 181 return embed_copy(env, vc->idExpr(name)); 182 183 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr1 184 jobject m ValidityChecker vc cv Expr kids 185 return embed_copy(env, vc->listExpr(kids)); 186 187 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr2 188 jobject m ValidityChecker vc c Expr expr1 189 return embed_copy(env, vc->listExpr(*expr1)); 190 191 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr3 192 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 193 return embed_copy(env, vc->listExpr(*expr1, *expr2)); 194 195 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr4 196 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 c Expr expr3 197 return embed_copy(env, vc->listExpr(*expr1, *expr2, *expr3)); 198 199 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr5 200 jobject m ValidityChecker vc n string op cv Expr kids 201 return embed_copy(env, vc->listExpr(op, kids)); 202 203 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr6 204 jobject m ValidityChecker vc n string op c Expr expr1 205 return embed_copy(env, vc->listExpr(op, *expr1)); 206 207 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr7 208 jobject m ValidityChecker vc n string op c Expr expr1 c Expr expr2 209 return embed_copy(env, vc->listExpr(op, *expr1, *expr2)); 210 211 DEFINITION: Java_cvc3_ValidityChecker_jniListExpr8 212 jobject m ValidityChecker vc n string op c Expr expr1 c Expr expr2 c Expr expr3 213 return embed_copy(env, vc->listExpr(op, *expr1, *expr2, *expr3)); 214 215 216 DEFINITION: Java_cvc3_ValidityChecker_jniPrintExpr 217 void m ValidityChecker vc c Expr expr 218 vc->printExpr(*expr); 219 220 DEFINITION: Java_cvc3_ValidityChecker_jniParseExpr 221 jobject m ValidityChecker vc c Expr expr 222 return embed_copy(env, vc->parseExpr(*expr)); 223 224 DEFINITION: Java_cvc3_ValidityChecker_jniParseType 225 jobject m ValidityChecker vc c Expr expr 226 return embed_copy(env, vc->parseType(*expr)); 227 228 DEFINITION: Java_cvc3_ValidityChecker_jniImportExpr 229 jobject m ValidityChecker vc c Expr expr 230 return embed_copy(env, vc->importExpr(*expr)); 231 232 DEFINITION: Java_cvc3_ValidityChecker_jniImportType 233 jobject m ValidityChecker vc c Type type 234 return embed_copy(env, vc->importType(*type)); 235 236 DEFINITION: Java_cvc3_ValidityChecker_jniCmdsFromString 237 void m ValidityChecker vc n string s 238 vc->cmdsFromString(s); 239 240 DEFINITION: Java_cvc3_ValidityChecker_jniExprFromString 241 jobject m ValidityChecker vc n string s 242 return embed_copy<Expr>(env, vc->exprFromString(s)); 243 244 DEFINITION: Java_cvc3_ValidityChecker_jniTrueExpr 245 jobject m ValidityChecker vc 246 return embed_copy<Expr>(env, vc->trueExpr()); 247 248 DEFINITION: Java_cvc3_ValidityChecker_jniFalseExpr 249 jobject m ValidityChecker vc 250 return embed_copy<Expr>(env, vc->falseExpr()); 251 252 DEFINITION: Java_cvc3_ValidityChecker_jniNotExpr 253 jobject m ValidityChecker vc c Expr expr 254 return embed_copy(env, vc->notExpr(*expr)); 255 256 DEFINITION: Java_cvc3_ValidityChecker_jniAndExpr1 257 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 258 return embed_copy(env, vc->andExpr(*expr1, *expr2)); 259 260 DEFINITION: Java_cvc3_ValidityChecker_jniAndExpr2 261 jobject m ValidityChecker vc cv Expr children 262 return embed_copy(env, vc->andExpr(children)); 263 264 DEFINITION: Java_cvc3_ValidityChecker_jniOrExpr1 265 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 266 return embed_copy(env, vc->orExpr(*expr1, *expr2)); 267 268 DEFINITION: Java_cvc3_ValidityChecker_jniOrExpr2 269 jobject m ValidityChecker vc cv Expr children 270 return embed_copy(env, vc->orExpr(children)); 271 272 DEFINITION: Java_cvc3_ValidityChecker_jniImpliesExpr 273 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 274 return embed_copy(env, vc->impliesExpr(*expr1, *expr2)); 275 276 DEFINITION: Java_cvc3_ValidityChecker_jniIffExpr 277 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 278 return embed_copy(env, vc->iffExpr(*expr1, *expr2)); 279 280 DEFINITION: Java_cvc3_ValidityChecker_jniEqExpr 281 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 282 return embed_copy(env, vc->eqExpr(*expr1, *expr2)); 283 284 DEFINITION: Java_cvc3_ValidityChecker_jniDistinctExpr 285 jobject m ValidityChecker vc cv Expr children 286 return embed_copy(env, vc->distinctExpr(children)); 287 288 DEFINITION: Java_cvc3_ValidityChecker_jniIteExpr 289 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 c Expr expr3 290 return embed_copy(env, vc->iteExpr(*expr1, *expr2, *expr3)); 291 292 DEFINITION: Java_cvc3_ValidityChecker_jniCreateOp1 293 jobject m ValidityChecker vc n string name c Type type 294 return embed_copy(env, vc->createOp(name, *type)); 295 296 DEFINITION: Java_cvc3_ValidityChecker_jniCreateOp2 297 jobject m ValidityChecker vc n string name c Type type c Expr expr 298 return embed_copy(env, vc->createOp(name, *type, *expr)); 299 300 DEFINITION: Java_cvc3_ValidityChecker_jniEqOp 301 jobject 302 return embed_copy<Op>(env, Op(EQ)); 303 304 DEFINITION: Java_cvc3_ValidityChecker_jniLtOp 305 jobject 306 return embed_copy<Op>(env, Op(LT)); 307 308 DEFINITION: Java_cvc3_ValidityChecker_jniLeOp 309 jobject 310 return embed_copy<Op>(env, Op(LE)); 311 312 DEFINITION: Java_cvc3_ValidityChecker_jniGtOp 313 jobject 314 return embed_copy<Op>(env, Op(GT)); 315 316 DEFINITION: Java_cvc3_ValidityChecker_jniGeOp 317 jobject 318 return embed_copy<Op>(env, Op(GE)); 319 320 DEFINITION: Java_cvc3_ValidityChecker_jniPlusOp 321 jobject 322 return embed_copy<Op>(env, Op(PLUS)); 323 324 DEFINITION: Java_cvc3_ValidityChecker_jniMinusOp 325 jobject 326 return embed_copy<Op>(env, Op(MINUS)); 327 328 DEFINITION: Java_cvc3_ValidityChecker_jniMultOp 329 jobject 330 return embed_copy<Op>(env, Op(MULT)); 331 332 DEFINITION: Java_cvc3_ValidityChecker_jniDivideOp 333 jobject 334 return embed_copy<Op>(env, Op(DIVIDE)); 335 336 337 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr1 338 jobject m ValidityChecker vc c Op op c Expr expr1 339 return embed_copy(env, vc->funExpr(*op, *expr1)); 340 341 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr2 342 jobject m ValidityChecker vc c Op op c Expr expr1 c Expr expr2 343 return embed_copy(env, vc->funExpr(*op, *expr1, *expr2)); 344 345 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr3 346 jobject m ValidityChecker vc c Op op c Expr expr1 c Expr expr2 c Expr expr3 347 return embed_copy(env, vc->funExpr(*op, *expr1, *expr2, *expr3)); 348 349 DEFINITION: Java_cvc3_ValidityChecker_jniFunExpr4 350 jobject m ValidityChecker vc c Op op cv Expr children 351 return embed_copy(env, vc->funExpr(*op, children)); 352 353 DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr1 354 jobject m ValidityChecker vc n int n n int d 355 return embed_copy(env, vc->ratExpr(n, d)); 356 357 DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr2 358 jobject m ValidityChecker vc n string n n string d n int base 359 return embed_copy(env, vc->ratExpr(n, d, base)); 360 361 DEFINITION: Java_cvc3_ValidityChecker_jniRatExpr3 362 jobject m ValidityChecker vc n string n n int base 363 return embed_copy(env, vc->ratExpr(n, base)); 364 365 DEFINITION: Java_cvc3_ValidityChecker_jniUminusExpr 366 jobject m ValidityChecker vc c Expr expr 367 return embed_copy(env, vc->uminusExpr(*expr)); 368 369 DEFINITION: Java_cvc3_ValidityChecker_jniPlusExpr1 370 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 371 return embed_copy(env, vc->plusExpr(*expr1, *expr2)); 372 373 DEFINITION: Java_cvc3_ValidityChecker_jniPlusExpr2 374 jobject m ValidityChecker vc cv Expr kids 375 return embed_copy(env, vc->plusExpr(kids)); 376 377 DEFINITION: Java_cvc3_ValidityChecker_jniMinusExpr 378 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 379 return embed_copy(env, vc->minusExpr(*expr1, *expr2)); 380 381 DEFINITION: Java_cvc3_ValidityChecker_jniMultExpr 382 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 383 return embed_copy(env, vc->multExpr(*expr1, *expr2)); 384 385 DEFINITION: Java_cvc3_ValidityChecker_jniPowExpr 386 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 387 return embed_copy(env, vc->powExpr(*expr1, *expr2)); 388 389 DEFINITION: Java_cvc3_ValidityChecker_jniDivideExpr 390 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 391 return embed_copy(env, vc->divideExpr(*expr1, *expr2)); 392 393 DEFINITION: Java_cvc3_ValidityChecker_jniLtExpr 394 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 395 return embed_copy(env, vc->ltExpr(*expr1, *expr2)); 396 397 DEFINITION: Java_cvc3_ValidityChecker_jniLeExpr 398 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 399 return embed_copy(env, vc->leExpr(*expr1, *expr2)); 400 401 DEFINITION: Java_cvc3_ValidityChecker_jniGtExpr 402 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 403 return embed_copy(env, vc->gtExpr(*expr1, *expr2)); 404 405 DEFINITION: Java_cvc3_ValidityChecker_jniGeExpr 406 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 407 return embed_copy(env, vc->geExpr(*expr1, *expr2)); 408 409 DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr1 410 jobject m ValidityChecker vc n string field c Expr expr 411 return embed_copy(env, vc->recordExpr(field, *expr)); 412 413 DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr2 414 jobject m ValidityChecker vc n string field1 c Expr expr1 n string field2 c Expr expr2 415 return embed_copy(env, vc->recordExpr(field1, *expr1, field2, *expr2)); 416 417 DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr3 418 jobject m ValidityChecker vc n string field1 c Expr expr1 n string field2 c Expr expr2 n string field3 c Expr expr3 419 return embed_copy(env, vc->recordExpr(field1, *expr1, field2, *expr2, field2, *expr2)); 420 421 DEFINITION: Java_cvc3_ValidityChecker_jniRecordExpr4 422 jobject m ValidityChecker vc nv string fields cv Expr exprs 423 return embed_copy(env, vc->recordExpr(fields, exprs)); 424 425 DEFINITION: Java_cvc3_ValidityChecker_jniRecSelectExpr 426 jobject m ValidityChecker vc c Expr record n string field 427 return embed_copy(env, vc->recSelectExpr(*record, field)); 428 429 DEFINITION: Java_cvc3_ValidityChecker_jniRecUpdateExpr 430 jobject m ValidityChecker vc c Expr record n string field c Expr update 431 return embed_copy(env, vc->recUpdateExpr(*record, field, *update)); 432 433 DEFINITION: Java_cvc3_ValidityChecker_jniReadExpr 434 jobject m ValidityChecker vc c Expr array c Expr index 435 return embed_copy(env, vc->readExpr(*array, *index)); 436 437 DEFINITION: Java_cvc3_ValidityChecker_jniWriteExpr 438 jobject m ValidityChecker vc c Expr array c Expr index c Expr value 439 return embed_copy(env, vc->writeExpr(*array, *index, *value)); 440 441 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr1 442 jobject m ValidityChecker vc n string s n int base 443 return embed_copy(env, vc->newBVConstExpr(s, jbase)); 444 445 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr2 446 jobject m ValidityChecker vc nv bool bits 447 return embed_copy(env, vc->newBVConstExpr(bits)); 448 449 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVConstExpr3 450 jobject m ValidityChecker vc c Rational rational n int len 451 return embed_copy(env, vc->newBVConstExpr(*rational, len)); 452 453 DEFINITION: Java_cvc3_ValidityChecker_jniNewConcatExpr1 454 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 455 return embed_copy(env, vc->newConcatExpr(*expr1, *expr2)); 456 457 DEFINITION: Java_cvc3_ValidityChecker_jniNewConcatExpr2 458 jobject m ValidityChecker vc cv Expr kids 459 return embed_copy(env, vc->newConcatExpr(kids)); 460 461 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVExtractExpr 462 jobject m ValidityChecker vc c Expr expr n int hi n int low 463 return embed_copy(env, vc->newBVExtractExpr(*expr, hi, low)); 464 465 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNegExpr 466 jobject m ValidityChecker vc c Expr expr 467 return embed_copy(env, vc->newBVNegExpr(*expr)); 468 469 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVAndExpr1 470 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 471 return embed_copy(env, vc->newBVAndExpr(*expr1, *expr2)); 472 473 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVAndExpr2 474 jobject m ValidityChecker vc cv Expr kids 475 return embed_copy(env, vc->newBVAndExpr(kids)); 476 477 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVOrExpr1 478 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 479 return embed_copy(env, vc->newBVOrExpr(*expr1, *expr2)); 480 481 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVOrExpr2 482 jobject m ValidityChecker vc cv Expr kids 483 return embed_copy(env, vc->newBVOrExpr(kids)); 484 485 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXorExpr1 486 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 487 return embed_copy(env, vc->newBVXorExpr(*expr1, *expr2)); 488 489 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXorExpr2 490 jobject m ValidityChecker vc cv Expr kids 491 return embed_copy(env, vc->newBVXorExpr(kids)); 492 493 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXnorExpr1 494 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 495 return embed_copy(env, vc->newBVXnorExpr(*expr1, *expr2)); 496 497 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVXnorExpr2 498 jobject m ValidityChecker vc cv Expr kids 499 return embed_copy(env, vc->newBVXnorExpr(kids)); 500 501 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNandExpr 502 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 503 return embed_copy(env, vc->newBVNandExpr(*expr1, *expr2)); 504 505 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVNorExpr 506 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 507 return embed_copy(env, vc->newBVNorExpr(*expr1, *expr2)); 508 509 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLTExpr 510 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 511 return embed_copy(env, vc->newBVLTExpr(*expr1, *expr2)); 512 513 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLEExpr 514 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 515 return embed_copy(env, vc->newBVLEExpr(*expr1, *expr2)); 516 517 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSLTExpr 518 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 519 return embed_copy(env, vc->newBVSLTExpr(*expr1, *expr2)); 520 521 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSLEExpr 522 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 523 return embed_copy(env, vc->newBVSLEExpr(*expr1, *expr2)); 524 525 DEFINITION: Java_cvc3_ValidityChecker_jniNewSXExpr 526 jobject m ValidityChecker vc c Expr expr n int len 527 return embed_copy(env, vc->newSXExpr(*expr, len)); 528 529 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVUminusExpr 530 jobject m ValidityChecker vc c Expr expr 531 return embed_copy(env, vc->newBVUminusExpr(*expr)); 532 533 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSubExpr 534 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 535 return embed_copy(env, vc->newBVSubExpr(*expr1, *expr2)); 536 537 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVPlusExpr 538 jobject m ValidityChecker vc n int numbits cv Expr exprs 539 return embed_copy(env, vc->newBVPlusExpr(numbits, exprs)); 540 541 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVMultExpr 542 jobject m ValidityChecker vc n int numbits c Expr expr1 c Expr expr2 543 return embed_copy(env, vc->newBVMultExpr(numbits, *expr1, *expr2)); 544 545 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVUDivExpr 546 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 547 return embed_copy(env, vc->newBVUDivExpr(*expr1, *expr2)); 548 549 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVURemExpr 550 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 551 return embed_copy(env, vc->newBVURemExpr(*expr1, *expr2)); 552 553 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSDivExpr 554 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 555 return embed_copy(env, vc->newBVSDivExpr(*expr1, *expr2)); 556 557 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSRemExpr 558 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 559 return embed_copy(env, vc->newBVSRemExpr(*expr1, *expr2)); 560 561 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSModExpr 562 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 563 return embed_copy(env, vc->newBVSModExpr(*expr1, *expr2)); 564 565 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVSHL 566 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 567 return embed_copy(env, vc->newBVSHL(*expr1, *expr2)); 568 569 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVLSHR 570 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 571 return embed_copy(env, vc->newBVLSHR(*expr1, *expr2)); 572 573 DEFINITION: Java_cvc3_ValidityChecker_jniNewBVASHR 574 jobject m ValidityChecker vc c Expr expr1 c Expr expr2 575 return embed_copy(env, vc->newBVASHR(*expr1, *expr2)); 576 577 DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedLeftShiftExpr 578 jobject m ValidityChecker vc c Expr expr n int r 579 return embed_copy(env, vc->newFixedLeftShiftExpr(*expr, r)); 580 581 DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedConstWidthLeftShiftExpr 582 jobject m ValidityChecker vc c Expr expr n int r 583 return embed_copy(env, vc->newFixedConstWidthLeftShiftExpr(*expr, r)); 584 585 DEFINITION: Java_cvc3_ValidityChecker_jniNewFixedRightShiftExpr 586 jobject m ValidityChecker vc c Expr expr n int r 587 return embed_copy(env, vc->newFixedRightShiftExpr(*expr, r)); 588 589 DEFINITION: Java_cvc3_ValidityChecker_jniComputeBVConst 590 jobject m ValidityChecker vc c Expr expr 591 return embed_copy(env, vc->computeBVConst(*expr)); 592 593 DEFINITION: Java_cvc3_ValidityChecker_jniTupleExpr 594 jobject m ValidityChecker vc cv Expr exprs 595 return embed_copy(env, vc->tupleExpr(exprs)); 596 597 DEFINITION: Java_cvc3_ValidityChecker_jniTupleSelectExpr 598 jobject m ValidityChecker vc c Expr tuple n int index 599 return embed_copy(env, vc->tupleSelectExpr(*tuple, index)); 600 601 DEFINITION: Java_cvc3_ValidityChecker_jniTupleUpdateExpr 602 jobject m ValidityChecker vc c Expr tuple n int index c Expr value 603 return embed_copy(env, vc->tupleUpdateExpr(*tuple, index, *value)); 604 605 DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeConsExpr 606 jobject m ValidityChecker vc n string constructor cv Expr exprs 607 return embed_copy(env, vc->datatypeConsExpr(constructor, exprs)); 608 609 DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeSelExpr 610 jobject m ValidityChecker vc n string selector c Expr expr 611 return embed_copy(env, vc->datatypeSelExpr(selector, *expr)); 612 613 DEFINITION: Java_cvc3_ValidityChecker_jniDatatypeTestExpr 614 jobject m ValidityChecker vc n string constructor c Expr expr 615 return embed_copy(env, vc->datatypeTestExpr(constructor, *expr)); 616 617 DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr1 618 jobject m ValidityChecker vc cv Expr vars c Expr body 619 return embed_copy(env, vc->forallExpr(vars, *body)); 620 621 DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr2 622 jobject m ValidityChecker vc cv Expr vars c Expr body c Expr trigger 623 return embed_copy(env, vc->forallExpr(vars, *body, *trigger)); 624 625 DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr3 626 jobject m ValidityChecker vc cv Expr vars c Expr body cv Expr triggers 627 return embed_copy(env, vc->forallExpr(vars, *body, triggers)); 628 629 DEFINITION: Java_cvc3_ValidityChecker_jniForallExpr4 630 jobject m ValidityChecker vc cv Expr vars c Expr body cvv Expr triggers 631 return embed_copy(env, vc->forallExpr(vars, *body, triggers)); 632 633 DEFINITION: Java_cvc3_ValidityChecker_jniSetTrigger 634 void m ValidityChecker vc c Expr closure c Expr trigger 635 vc->setTrigger(*closure, *trigger); 636 637 DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers 638 void m ValidityChecker vc c Expr closure cv Expr triggers 639 vc->setTriggers(*closure, triggers); 640 641 DEFINITION: Java_cvc3_ValidityChecker_jniSetTriggers2 642 void m ValidityChecker vc c Expr closure cvv Expr triggers 643 vc->setTriggers(*closure, triggers); 644 645 DEFINITION: Java_cvc3_ValidityChecker_jniSetMultiTrigger 646 void m ValidityChecker vc c Expr closure cv Expr multiTrigger 647 vc->setMultiTrigger(*closure, multiTrigger); 648 649 DEFINITION: Java_cvc3_ValidityChecker_jniExistsExpr 650 jobject m ValidityChecker vc cv Expr vars c Expr body 651 return embed_copy(env, vc->existsExpr(vars, *body)); 652 653 DEFINITION: Java_cvc3_ValidityChecker_jniLambdaExpr 654 jobject m ValidityChecker vc cv Expr vars c Expr body 655 return embed_copy(env, vc->lambdaExpr(vars, *body)); 656 657 DEFINITION: Java_cvc3_ValidityChecker_jniTransClosure 658 jobject m ValidityChecker vc c Op p 659 return embed_copy(env, vc->transClosure(*p)); 660 661 DEFINITION: Java_cvc3_ValidityChecker_jniSimulateExpr 662 jobject m ValidityChecker vc c Expr f c Expr s cv Expr inputs c Expr n 663 return embed_copy(env, vc->simulateExpr(*f, *s, inputs, *n)); 664 665 666 DEFINITION: Java_cvc3_ValidityChecker_jniSetResourceLimit 667 void m ValidityChecker vc n int limit 668 vc->setResourceLimit(limit); 669 670 DEFINITION: Java_cvc3_ValidityChecker_jniAssertFormula 671 void m ValidityChecker vc c Expr expr 672 vc->assertFormula(*expr); 673 674 DEFINITION: Java_cvc3_ValidityChecker_jniRegisterAtom 675 void m ValidityChecker vc c Expr expr 676 vc->registerAtom(*expr); 677 678 DEFINITION: Java_cvc3_ValidityChecker_jniGetImpliedLiteral 679 jobject m ValidityChecker vc 680 return embed_copy(env, vc->getImpliedLiteral()); 681 682 DEFINITION: Java_cvc3_ValidityChecker_jniSimplify 683 jobject m ValidityChecker vc c Expr expr 684 return embed_copy(env, vc->simplify(*expr)); 685 686 DEFINITION: Java_cvc3_ValidityChecker_jniQuery 687 jstring m ValidityChecker vc c Expr expr 688 return toJava(env, vc->query(*expr)); 689 690 DEFINITION: Java_cvc3_ValidityChecker_jniCheckUnsat 691 jstring m ValidityChecker vc c Expr expr 692 return toJava(env, vc->checkUnsat(*expr)); 693 694 DEFINITION: Java_cvc3_ValidityChecker_jniCheckContinue 695 jstring m ValidityChecker vc 696 return toJava(env, vc->checkContinue()); 697 698 DEFINITION: Java_cvc3_ValidityChecker_jniRestart 699 jstring m ValidityChecker vc c Expr expr 700 return toJava(env, vc->restart(*expr)); 701 702 DEFINITION: Java_cvc3_ValidityChecker_jniReturnFromCheck 703 void m ValidityChecker vc 704 vc->returnFromCheck(); 705 706 DEFINITION: Java_cvc3_ValidityChecker_jniGetUserAssumptions 707 jobjectArray m ValidityChecker vc 708 vector<Expr> result; 709 vc->getUserAssumptions(result); 710 return toJavaVCopy(env, result); 711 712 DEFINITION: Java_cvc3_ValidityChecker_jniGetInternalAssumptions 713 jobjectArray m ValidityChecker vc 714 vector<Expr> result; 715 vc->getInternalAssumptions(result); 716 return toJavaVCopy(env, result); 717 718 DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptions 719 jobjectArray m ValidityChecker vc 720 vector<Expr> result; 721 vc->getAssumptions(result); 722 return toJavaVCopy(env, result); 723 724 DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptionsUsed 725 jobjectArray m ValidityChecker vc 726 vector<Expr> result; 727 vc->getAssumptionsUsed(result); 728 return toJavaVCopy(env, result); 729 730 DEFINITION: Java_cvc3_ValidityChecker_jniGetCounterExample 731 jobjectArray m ValidityChecker vc n bool inOrder 732 vector<Expr> result; 733 vc->getCounterExample(result, inOrder); 734 return toJavaVCopy(env, result); 735 736 DEFINITION: Java_cvc3_ValidityChecker_jniGetValue 737 jstring m ValidityChecker vc c Expr expr 738 return toJava(env, vc->value(*expr)); 739 740 DEFINITION: Java_cvc3_ValidityChecker_jniGetConcreteModel 741 jobjectArray m ValidityChecker vc 742 ExprMap<Expr> result; 743 vc->getConcreteModel(result); 744 return toJavaHCopy(env, result); 745 746 DEFINITION: Java_cvc3_ValidityChecker_jniInconsistent1 747 jboolean m ValidityChecker vc 748 return vc->inconsistent(); 749 750 DEFINITION: Java_cvc3_ValidityChecker_jniInconsistent2 751 jobjectArray m ValidityChecker vc 752 vector<Expr> result; 753 bool inconsistent = vc->inconsistent(result); 754 assert(inconsistent); 755 return toJavaVCopy(env, result); 756 757 DEFINITION: Java_cvc3_ValidityChecker_jniIncomplete1 758 jboolean m ValidityChecker vc 759 return vc->incomplete(); 760 761 DEFINITION: Java_cvc3_ValidityChecker_jniIncomplete2 762 jobjectArray m ValidityChecker vc 763 vector<std::string> result; 764 bool incomplete = vc->incomplete(result); 765 assert(incomplete); 766 return toJavaVCopy(env, result); 767 768 DEFINITION: Java_cvc3_ValidityChecker_jniGetProof 769 jobject m ValidityChecker vc 770 return embed_copy(env, vc->getProof()); 771 772 DEFINITION: Java_cvc3_ValidityChecker_jniGetTCC 773 jobject m ValidityChecker vc 774 return embed_copy(env, vc->getTCC()); 775 776 DEFINITION: Java_cvc3_ValidityChecker_jniGetAssumptionsTCC 777 jobjectArray m ValidityChecker vc 778 vector<Expr> result; 779 vc->getAssumptionsTCC(result); 780 return toJavaVCopy(env, result); 781 782 DEFINITION: Java_cvc3_ValidityChecker_jniGetProofTCC 783 jobject m ValidityChecker vc 784 return embed_copy(env, vc->getProofTCC()); 785 786 DEFINITION: Java_cvc3_ValidityChecker_jniGetClosure 787 jobject m ValidityChecker vc 788 return embed_copy(env, vc->getClosure()); 789 790 DEFINITION: Java_cvc3_ValidityChecker_jniGetProofClosure 791 jobject m ValidityChecker vc 792 return embed_copy(env, vc->getProofClosure()); 793 794 795 796 797 798 799 DEFINITION: Java_cvc3_ValidityChecker_jniStackLevel 800 jint m ValidityChecker vc 801 return vc->stackLevel(); 802 803 DEFINITION: Java_cvc3_ValidityChecker_jniPush 804 void m ValidityChecker vc 805 vc->push(); 806 807 DEFINITION: Java_cvc3_ValidityChecker_jniPop 808 void m ValidityChecker vc 809 vc->pop(); 810 811 DEFINITION: Java_cvc3_ValidityChecker_jniPopTo 812 void m ValidityChecker vc n int stackLevel 813 vc->popto(stackLevel); 814 815 DEFINITION: Java_cvc3_ValidityChecker_jniScopeLevel 816 jint m ValidityChecker vc 817 return vc->scopeLevel(); 818 819 DEFINITION: Java_cvc3_ValidityChecker_jniPushScope 820 void m ValidityChecker vc 821 vc->pushScope(); 822 823 DEFINITION: Java_cvc3_ValidityChecker_jniPopScope 824 void m ValidityChecker vc 825 vc->popScope(); 826 827 DEFINITION: Java_cvc3_ValidityChecker_jniPopToScope 828 void m ValidityChecker vc n int stackLevel 829 vc->poptoScope(stackLevel); 830 831 DEFINITION: Java_cvc3_ValidityChecker_jniGetCurrentContext 832 jobject m ValidityChecker vc 833 return embed_mut_ref(env, vc->getCurrentContext()); 834 835 836 837 838 839 DEFINITION: Java_cvc3_ValidityChecker_jniLoadFile1 840 void m ValidityChecker vc n string fileName n string lang 841 vc->loadFile(fileName, toCppInputLanguage(env, lang), false); 842 843 844 DEFINITION: Java_cvc3_ValidityChecker_jniGetStatistics 845 jobject m ValidityChecker vc 846 return embed_mut_ref(env, &vc->getStatistics()); 847 848 DEFINITION: Java_cvc3_ValidityChecker_jniPrintStatistics 849 void m ValidityChecker vc 850 vc->printStatistics(); 851 852 853 DEFINITION: Java_cvc3_ValidityChecker_jniSetTimeLimit 854 void m ValidityChecker vc n int n 855 vc->setTimeLimit((unsigned int)n); 856