1 /******************************************************************** 2 * AUTHORS: Michael Katelman, Vijay Ganesh, Trevor Hansen, Andrew V. Jones 3 * 4 * BEGIN DATE: Apr, 2008 5 * 6 Permission is hereby granted, free of charge, to any person obtaining a copy 7 of this software and associated documentation files (the "Software"), to deal 8 in the Software without restriction, including without limitation the rights 9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell 10 copies of the Software, and to permit persons to whom the Software is 11 furnished to do so, subject to the following conditions: 12 13 The above copyright notice and this permission notice shall be included in 14 all copies or substantial portions of the Software. 15 16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, 21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN 22 THE SOFTWARE. 23 ********************************************************************/ 24 25 #ifndef _cvcl__include__c_interface_h_ 26 #define _cvcl__include__c_interface_h_ 27 28 #ifdef __cplusplus 29 #define _CVCL_DEFAULT_ARG(v) = v 30 #else 31 #define _CVCL_DEFAULT_ARG(v) 32 #endif 33 34 #ifdef __cplusplus 35 extern "C" { 36 #endif 37 38 #include <stdbool.h> 39 40 ///////////////////////////////////////////////////////////////////////////// 41 /// STP API INTERNAL MACROS FOR LINKING 42 /// 43 /// These are undefined at the end of this file to prevent them from leaking 44 /// into code that includes it. 45 ///////////////////////////////////////////////////////////////////////////// 46 47 #if defined(_MSC_VER) 48 // NOTE: for now, we need STP_SHARED_LIB for clients of the statically linked 49 // STP library, for which linking fails when DLL_PUBLIC is __declspec(dllimport). 50 #if defined(STP_SHARED_LIB) && defined(STP_EXPORTS) 51 // This is visible when building the STP library as a DLL. 52 #define DLL_PUBLIC __declspec(dllexport) 53 #elif defined(STP_SHARED_LIB) 54 // This is visible for STP clients. 55 #define DLL_PUBLIC __declspec(dllimport) 56 #else 57 #define DLL_PUBLIC 58 #endif 59 60 // Symbols are hidden by default in MSVC. 61 #define DLL_LOCAL 62 63 #elif defined(__GNUC__) || defined(__clang__) 64 #define DLL_PUBLIC __attribute__((visibility("default"))) 65 #define DLL_LOCAL __attribute__((visibility("hidden"))) 66 #else 67 #define DLL_PUBLIC 68 #define DLL_LOCAL 69 #endif 70 71 ///////////////////////////////////////////////////////////////////////////// 72 /// STP API Types 73 /// 74 /// This gives absolutely no pointer typing at compile-time. Most C 75 /// users prefer this over stronger typing. User is the king. A 76 /// stronger typed interface is in the works. 77 ///////////////////////////////////////////////////////////////////////////// 78 79 #ifdef STP_STRONG_TYPING // not used for now! 80 #else 81 typedef void* VC; 82 typedef void* Expr; 83 typedef void* Type; 84 typedef void* WholeCounterExample; 85 #endif 86 87 ///////////////////////////////////////////////////////////////////////////// 88 /// START API 89 ///////////////////////////////////////////////////////////////////////////// 90 91 //! \brief Returns the C string for the git sha of STP 92 //! 93 DLL_PUBLIC const char* get_git_version_sha(void); 94 95 //! \brief Returns the C string for the git tag of STP 96 //! 97 DLL_PUBLIC const char* get_git_version_tag(void); 98 99 //! \brief Returns the C string for the compilation env of STP 100 //! 101 DLL_PUBLIC const char* get_compilation_env(void); 102 103 //! \brief Processes the given flag represented as char for the given validity checker. 104 //! 105 //! The following flags are supported: 106 //! - 'a': Disables optimization. TODO: What kind of optimization is meant here? 107 //! - 'c': Enables construction of counter examples. 108 //! - 'd': Enables construction and checking of counter examples. Superseeds flag 'c'. 109 //! - 'm': Use SMTLib1 parser. Conflicts with using SMTLib2 parser. 110 //! - 'n': Enables printing of the output. TODO: What is meant with output here? 111 //! - 'p': Enables printing of counter examples. 112 //! - 'q': Enables printing of array values in declared order. 113 //! - 'r': Enables accermannisation. 114 //! - 's': Sets the status flag to true. TODO: What consequenses does this have? 115 //! - 't': Enables quick statistics. TODO: What is this? 116 //! - 'v': Enables printing of nodes. 117 //! - 'w': Enables word-level solving. TODO: What is mean with this? 118 //! - 'y': Enables printing binaries. TODO: What is meant with this? 119 //! 120 //! This function panics if given an unsupported or unknown flag. 121 //! 122 DLL_PUBLIC void process_argument(const char ch, VC bm); 123 124 //! \brief Deprecated: use process_argument instead! 125 //! 126 //! Sets flags for the validity checker. 127 //! For more information about this look into the documentation of process_argument. 128 //! 129 //! Parameter num_absrefine has no effect in the current implementation. 130 //! It is left for compatibility with existing code. 131 //! 132 DLL_PUBLIC void vc_setFlags(VC vc, char c, 133 int num_absrefine _CVCL_DEFAULT_ARG(0)); 134 135 //! \brief Deprecated: use process_argument instead! 136 //! 137 //! Sets flags for the validity checker. 138 //! For more information about this look into the documentation of process_argument. 139 //! 140 DLL_PUBLIC void vc_setFlag(VC vc, char c); 141 142 //! Interface-only flags. 143 //! 144 enum ifaceflag_t 145 { 146 //! Tells the validity checker that it is responsible for resource 147 //! deallocation of its allocated expressions. 148 //! 149 //! This is set to true by default. 150 //! 151 //! Affected methods are: 152 //! - vc_arrayType 153 //! - vc_boolType 154 //! - vc_bvType 155 //! - vc_bv32Type 156 //! - vc_vcConstExprFromInt 157 //! 158 //! Changing this flag while STP is running may result in undefined behaviour. 159 //! 160 //! Use this with great care; otherwise memory leaks are very easily possible! 161 //! 162 EXPRDELETE, 163 164 //! Use the minisat SAT solver. 165 //! 166 MS, 167 168 //! Use a simplifying version of the minisat SAT solver. 169 //! 170 SMS, 171 172 //! Use the crypto minisat version 4 or higher (currently version 5) solver. 173 //! 174 CMS4, 175 176 //! Use the SAT solver Riss. 177 //! 178 RISS, 179 180 //! \brief Deprecated: use `MS` instead! 181 //! 182 //! This used to be the array version of the minisat SAT solver. 183 //! 184 //! Currently simply forwards to MS. 185 //! 186 MSP 187 188 }; 189 190 //! \brief Sets the given interface flag for the given validity checker to param_value. 191 //! 192 //! Use this to set the underlying SAT solver used by STP or to change 193 //! the global behaviour for expression ownership semantics via EXPRDELETE. 194 //! 195 DLL_PUBLIC void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, 196 int param_value); 197 198 //! \brief Deprecated: this functionality is no longer needed! 199 //! 200 //! Since recent versions of STP division is always total. 201 DLL_PUBLIC void make_division_total(VC vc); 202 203 //! \brief Creates a new instance of an STP validity checker. 204 //! 205 //! Validity checker is the context for all STP resources like expressions, 206 //! type and counter examples that may be generated while running STP. 207 //! 208 //! It is also the interface for assertions and queries. 209 //! 210 DLL_PUBLIC VC vc_createValidityChecker(void); 211 212 //! \brief Returns the boolean type for the given validity checker. 213 //! 214 DLL_PUBLIC Type vc_boolType(VC vc); 215 216 //! \brief Returns an array type with the given index type and data type 217 //! for the given validity checker. 218 //! 219 //! Note that index type and data type must both be of bitvector (bv) type. 220 //! 221 DLL_PUBLIC Type vc_arrayType(VC vc, Type typeIndex, Type typeData); 222 223 ///////////////////////////////////////////////////////////////////////////// 224 /// EXPR MANUPULATION METHODS 225 ///////////////////////////////////////////////////////////////////////////// 226 227 //! \brief Returns a variable (symbol) expression with the given name and type. 228 //! 229 //! The type cannot be a function type. (TODO: Are function type still a thing in STP?) 230 //! 231 //! The variable name must only consist of alphanumerics and underscore 232 //! characters, otherwise this may behave in undefined ways, e.g. segfault. 233 //! 234 DLL_PUBLIC Expr vc_varExpr(VC vc, const char* name, Type type); 235 236 //! \brief Similar to vc_varExpr but more bare metal. Do not use this unless 237 //! you really know what you are doing! 238 //! 239 //! Note: This should be deprecated in favor of the saner vc_varExpr API 240 //! and as this API leaks implementation details of STP. 241 //! 242 //! The variable name must only consist of alphanumerics and underscore 243 //! characters, otherwise this may behave in undefined ways, e.g. segfault. 244 //! 245 DLL_PUBLIC Expr vc_varExpr1(VC vc, const char* name, int indexwidth, 246 int valuewidth); 247 248 //! \brief Returns the type of the given expression. 249 //! 250 DLL_PUBLIC Type vc_getType(VC vc, Expr e); 251 252 //! \brief Returns the bit-width of the given bitvector. 253 //! 254 DLL_PUBLIC int vc_getBVLength(VC vc, Expr e); 255 256 //! \brief Create an equality expression. The two children must have the same type. 257 //! 258 //! Returns a boolean expression. 259 //! 260 DLL_PUBLIC Expr vc_eqExpr(VC vc, Expr child0, Expr child1); 261 262 ///////////////////////////////////////////////////////////////////////////// 263 /// BOOLEAN EXPRESSIONS 264 /// 265 /// The following functions create boolean expressions. 266 /// The children provided as arguments must be of type boolean. 267 /// 268 /// An exception is the function vc_iteExpr(). 269 /// In the case of vc_iteExpr() the conditional must always be boolean, 270 /// but the thenExpr (resp. elseExpr) can be bit-vector or boolean type. 271 /// However, the thenExpr and elseExpr must be both of the same type. 272 /// 273 ///////////////////////////////////////////////////////////////////////////// 274 275 //! \brief Creates a boolean expression that represents true. 276 //! 277 DLL_PUBLIC Expr vc_trueExpr(VC vc); 278 279 //! \brief Creates a boolean expression that represents false. 280 //! 281 DLL_PUBLIC Expr vc_falseExpr(VC vc); 282 283 //! \brief Creates a boolean not expression that logically negates its child. 284 //! 285 DLL_PUBLIC Expr vc_notExpr(VC vc, Expr child); 286 287 //! \brief Creates a binary and-expression that represents a conjunction 288 //! of the given boolean child expressions. 289 //! 290 DLL_PUBLIC Expr vc_andExpr(VC vc, Expr left, Expr right); 291 292 //! \brief Creates an and-expression with multiple child boolean expressions 293 //! that represents the conjunction of all of its child expressions. 294 //! 295 //! This API is useful since SMTLib2 defines non-binary expressions for logical-and. 296 //! 297 DLL_PUBLIC Expr vc_andExprN(VC vc, Expr* children, int numOfChildNodes); 298 299 //! \brief Creates a binary or-expression that represents a disjunction 300 //! of the given boolean child expressions. 301 //! 302 DLL_PUBLIC Expr vc_orExpr(VC vc, Expr left, Expr right); 303 304 //! \brief Creates an or-expression with multiple child boolean expressions 305 //! that represents the disjunction of all of its child expressions. 306 //! 307 //! This API is useful since SMTLib2 defines non-binary expressions for logical-or. 308 //! 309 DLL_PUBLIC Expr vc_orExprN(VC vc, Expr* children, int numOfChildNodes); 310 311 //! \brief Creates a binary xor-expressions for the given boolean child expressions. 312 //! 313 DLL_PUBLIC Expr vc_xorExpr(VC vc, Expr left, Expr right); 314 315 //! \brief Creates an implies-expression for the given hyp (hypothesis) and 316 //! conc (conclusion) boolean expressions. 317 //! 318 DLL_PUBLIC Expr vc_impliesExpr(VC vc, Expr hyp, Expr conc); 319 320 //! \brief Creates an if-and-only-if-expression for the given boolean expressions. 321 //! 322 DLL_PUBLIC Expr vc_iffExpr(VC vc, Expr left, Expr right); 323 324 //! \brief Creates an if-then-else-expression for the given conditional boolean expression 325 //! and its then and else expressions which must be of the same type. 326 //! 327 //! The output type of this API may be of boolean or bitvector type. 328 //! 329 DLL_PUBLIC Expr vc_iteExpr(VC vc, Expr conditional, Expr thenExpr, 330 Expr elseExpr); 331 332 //! \brief Returns a bitvector expression from the given boolean expression. 333 //! 334 //! Returns a constant bitvector expression that represents one (1) if 335 //! the given boolean expression was false or returns a bitvector expression 336 //! representing zero (0) otherwise. 337 //! 338 //! Panics if the given expression is not of boolean type. 339 //! 340 DLL_PUBLIC Expr vc_boolToBVExpr(VC vc, Expr form); 341 342 //! \brief Creates a parameterized boolean expression with the given boolean 343 //! variable expression and the parameter param. 344 //! 345 DLL_PUBLIC Expr vc_paramBoolExpr(VC vc, Expr var, Expr param); 346 347 ///////////////////////////////////////////////////////////////////////////// 348 /// ARRAY EXPRESSIONS 349 ///////////////////////////////////////////////////////////////////////////// 350 351 //! \brief Returns an array-read-expression representing the reading of 352 //! the given array's entry of the given index. 353 //! 354 //! The array parameter must be of type array and index must be of type bitvector. 355 //! 356 DLL_PUBLIC Expr vc_readExpr(VC vc, Expr array, Expr index); 357 358 //! \brief Returns an array-write-expressions representing the writing of 359 //! the given new value into the given array at the given entry index. 360 //! 361 //! The array parameter must be of type array, and index and newValue of type bitvector. 362 //! 363 DLL_PUBLIC Expr vc_writeExpr(VC vc, Expr array, Expr index, Expr newValue); 364 365 //! \brief Parses the expression stored in the file of the given filepath 366 //! and returns it on success. 367 //! 368 //! TODO: What format is expected? SMTLib2? 369 //! Does the user have to deallocate resources for the returned expression? 370 //! Why exactly is this "pretty cool!"? 371 //! 372 DLL_PUBLIC Expr vc_parseExpr(VC vc, const char* filepath); 373 374 //! \brief Prints the given expression to stdout in the presentation language. 375 //! 376 DLL_PUBLIC void vc_printExpr(VC vc, Expr e); 377 378 //! \brief Prints the given expression to stdout as C code. 379 //! 380 DLL_PUBLIC void vc_printExprCCode(VC vc, Expr e); 381 382 //! \brief Prints the given expression to stdout in the STMLib2 format. 383 //! 384 DLL_PUBLIC char* vc_printSMTLIB(VC vc, Expr e); 385 386 //! \brief Prints the given expression into the file with the given file descriptor 387 //! in the presentation language. 388 //! 389 DLL_PUBLIC void vc_printExprFile(VC vc, Expr e, int fd); 390 391 // //! \brief Prints the state of the given validity checker into 392 // //! buffer allocated by STP stores it into the given 'buf' alongside 393 // //! its length into 'len'. 394 // //! 395 // //! It is the responsibility of the caller to free the buffer. 396 // //! 397 // void vc_printStateToBuffer(VC vc, char **buf, unsigned long *len); 398 399 //! \brief Prints the given expression into a buffer allocated by STP. 400 //! 401 //! The buffer is returned via output parameter 'buf' alongside its length 'len'. 402 //! It is the responsibility of the caller to free the memory afterwards. 403 DLL_PUBLIC void vc_printExprToBuffer(VC vc, Expr e, char** buf, 404 unsigned long* len); 405 406 //! \brief Prints the counter example after an invalid query to stdout. 407 //! 408 //! This method should only be called after a query which returns false. 409 //! 410 DLL_PUBLIC void vc_printCounterExample(VC vc); 411 412 //! \brief Prints variable declarations to stdout. 413 //! 414 DLL_PUBLIC void vc_printVarDecls(VC vc); 415 416 //! \brief Clears the internal list of variables that are maintained 417 //! for printing purposes via 'vc_printVarDecls'. 418 //! 419 //! A user may want to do this after finishing printing the variable 420 //! declarations to prevent memory leaks. 421 //! This is also useful if printing of declarations is never wanted. 422 //! 423 DLL_PUBLIC void vc_clearDecls(VC vc); 424 425 //! \brief Prints assertions to stdout. 426 //! 427 //! The validity checker's flag 'simplify_print' must be set to '1' 428 //! to enable simplifications of the asserted formulas during printing. 429 //! 430 DLL_PUBLIC void vc_printAsserts(VC vc, int simplify_print _CVCL_DEFAULT_ARG(0)); 431 432 //! \brief Prints the state of the query to a buffer allocated by STP 433 //! that is returned via output parameter 'buf' alongside its 434 //! length in 'len'. 435 //! 436 //! It is the callers responsibility to free the buffer's memory. 437 //! 438 //! The validity checker's flag 'simplify_print' must be set to '1' 439 //! to enable simplifications of the query state during printing. 440 //! 441 DLL_PUBLIC void vc_printQueryStateToBuffer(VC vc, Expr e, char** buf, 442 unsigned long* len, 443 int simplify_print); 444 445 //! \brief Prints the found counter example to a buffer allocated by STP 446 //! that is returned via output parameter 'buf' alongside its 447 //! length in 'len'. 448 //! 449 //! It is the callers responsibility to free the buffer's memory. 450 //! 451 //! The validity checker's flag 'simplify_print' must be set to '1' 452 //! to enable simplifications of the counter example during printing. 453 //! 454 DLL_PUBLIC void vc_printCounterExampleToBuffer(VC vc, char** buf, 455 unsigned long* len); 456 457 //! \brief Prints the query to stdout in presentation language. 458 //! 459 DLL_PUBLIC void vc_printQuery(VC vc); 460 461 ///////////////////////////////////////////////////////////////////////////// 462 /// CONTEXT RELATED METHODS 463 ///////////////////////////////////////////////////////////////////////////// 464 465 //! \brief Adds the given expression as assertion to the given validity checker. 466 //! 467 //! The expression must be of type boolean. 468 //! 469 DLL_PUBLIC void vc_assertFormula(VC vc, Expr e); 470 471 //! \brief Simplifies the given expression with respect to the given validity checker. 472 //! 473 DLL_PUBLIC Expr vc_simplify(VC vc, Expr e); 474 475 //! \brief Checks the validity of the given expression 'e' in the given context. 476 //! 477 //! The timeout is represented and expected in milliseconds. 478 //! The given expression 'e' must be of type boolean. 479 //! 480 //! Returns ... 481 //! 0: if 'e' is INVALID 482 //! 1: if 'e' is VALID 483 //! 2: if errors occured 484 //! 3: if the timeout was reached 485 //! 486 //! Note: The given timeout is a soft timeout. Use the flag '-g' for a hard timeout 487 //! that will abort automatically. Soft timeouts are only checked sparingly, 488 //! so the actual timeout may be larger. 489 //! 490 //! Note: The cryptominisat solver does not check the timeout, yet! 491 //! 492 DLL_PUBLIC int vc_query_with_timeout(VC vc, Expr e, int timeout_ms); 493 494 //! \brief Checks the validity of the given expression 'e' in the given context 495 //! with an unlimited timeout. 496 //! 497 //! This simply forwards to 'vc_query_with_timeout'. 498 //! 499 //! Note: Read the documentation of 'vc_query_with_timeout' for more information 500 //! about subtle details. 501 //! 502 DLL_PUBLIC int vc_query(VC vc, Expr e); 503 504 //! \brief Returns the counter example after an invalid query. 505 //! 506 DLL_PUBLIC Expr vc_getCounterExample(VC vc, Expr e); 507 508 //! \brief Returns an array from a counter example after an invalid query. 509 //! 510 //! The buffer for the array is allocated by STP and returned via the 511 //! non-null expected out parameters 'outIndices' for the indices, 'outValues' 512 //! for the values and 'outSize' for the size of the array. 513 //! 514 //! It is the caller's responsibility to free the memory afterwards. 515 //! 516 DLL_PUBLIC void vc_getCounterExampleArray(VC vc, Expr e, Expr** outIndices, 517 Expr** outValues, int* outSize); 518 519 //! \brief Returns the size of the counter example array, 520 //! i.e. the number of variable and array locations 521 //! in the counter example. 522 //! 523 DLL_PUBLIC int vc_counterexample_size(VC vc); 524 525 //! \brief Checkpoints the current context and increases the scope level. 526 //! 527 //! TODO: What effects has this? 528 //! 529 DLL_PUBLIC void vc_push(VC vc); 530 531 //! \brief Restores the current context to its state at the last checkpoint. 532 //! 533 //! TODO: What effects has this? 534 //! 535 DLL_PUBLIC void vc_pop(VC vc); 536 537 //! \brief Returns the associated integer from the given bitvector expression. 538 //! 539 //! Panics if the given bitvector cannot be represented by an 'int'. 540 //! 541 DLL_PUBLIC int getBVInt(Expr e); 542 543 //! \brief Returns the associated unsigned integer from the given bitvector expression. 544 //! 545 //! Panics if the given bitvector cannot be represented by an 'unsigned int'. 546 //! 547 DLL_PUBLIC unsigned int getBVUnsigned(Expr e); 548 549 //! Return an unsigned long long int from a constant bitvector expressions 550 551 //! \brief Returns the associated unsigned long long integer from the given bitvector expression. 552 //! 553 //! Panics if the given bitvector cannot be represented by an 'unsigned long long int'. 554 //! 555 DLL_PUBLIC unsigned long long int getBVUnsignedLongLong(Expr e); 556 557 ///////////////////////////////////////////////////////////////////////////// 558 /// BITVECTOR OPERATIONS 559 ///////////////////////////////////////////////////////////////////////////// 560 561 //! \brief Returns the bitvector type for the given validity checker. 562 //! 563 DLL_PUBLIC Type vc_bvType(VC vc, int no_bits); 564 565 //! \brief Returns the bitvector type with a bit-width of 32 for the 566 //! given validity checker. 567 //! 568 //! This is equal to calling 'vc_bvType(vc, 32)'. 569 //! 570 //! Note: This is a convenience function that simply forwards its input. 571 //! 572 DLL_PUBLIC Type vc_bv32Type(VC vc); 573 574 //Const expressions for string, int, long-long, etc 575 576 //! \brief Parses the given string and returns an associated bitvector expression. 577 //! 578 //! This function expects the input string to be of decimal format. 579 //! 580 DLL_PUBLIC Expr vc_bvConstExprFromDecStr(VC vc, int width, 581 const char* decimalInput); 582 583 //! \brief Parses the given string and returns an associated bitvector expression. 584 //! 585 //! This function expects the input string to be of binary format. 586 //! 587 DLL_PUBLIC Expr vc_bvConstExprFromStr(VC vc, const char* binaryInput); 588 589 //! \brief Returns a bitvector with 'bitWidth' bit-width from the given 590 //! unsigned integer value. 591 //! 592 //! The 'bitWidth' must be large enough to fully store the given value's bit representation. 593 //! 594 DLL_PUBLIC Expr vc_bvConstExprFromInt(VC vc, int bitWidth, unsigned int value); 595 596 //! \brief Returns a bitvector with 'bitWidth' bit-width from the given 597 //! unsigned long long integer value. 598 //! 599 //! The 'bitWidth' must be large enough to fully store the given value's bit representation. 600 //! 601 DLL_PUBLIC Expr vc_bvConstExprFromLL(VC vc, int bitWidth, 602 unsigned long long value); 603 604 //! \brief Returns a bitvector with a bit-width of 32 from the given 605 //! unsigned integer value. 606 //! 607 DLL_PUBLIC Expr vc_bv32ConstExprFromInt(VC vc, unsigned int value); 608 609 ///////////////////////////////////////////////////////////////////////////// 610 /// BITVECTOR ARITHMETIC OPERATIONS 611 ///////////////////////////////////////////////////////////////////////////// 612 613 //! \brief Returns a bitvector expression representing the concatenation of the two 614 //! given bitvector expressions. 615 //! 616 //! This results in a bitvector with the bit-width of the bit-width sum 617 //! of its children. 618 //! 619 //! Example: Given bitvector 'a = 1101' and 'b = 1000' then 'vc_bvConcatExpr(vc, a, b)' 620 //! results in 'c = 11011000'. 621 //! 622 DLL_PUBLIC Expr vc_bvConcatExpr(VC vc, Expr left, Expr right); 623 624 //! \brief Returns a bitvector expression representing the addition of the two 625 //! given bitvector expressions. 626 //! 627 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 628 //! 629 DLL_PUBLIC Expr vc_bvPlusExpr(VC vc, int bitWidth, Expr left, Expr right); 630 631 //! \brief Returns a bitvector expression representing the addition of the N 632 //! given bitvector expressions in the 'children' array. 633 //! 634 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 635 //! 636 DLL_PUBLIC Expr vc_bvPlusExprN(VC vc, int bitWidth, Expr* children, 637 int numOfChildNodes); 638 639 //! \brief Returns a bitvector expression with a bit-width of 32 640 //! representing the addition of the two given bitvector expressions. 641 //! 642 //! The given bitvector expressions must have a bit-width of 32. 643 //! 644 DLL_PUBLIC Expr vc_bv32PlusExpr(VC vc, Expr left, Expr right); 645 646 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 647 //! representing the subtraction '(left - right)' of the two 648 //! given bitvector expressions. 649 //! 650 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 651 //! 652 DLL_PUBLIC Expr vc_bvMinusExpr(VC vc, int bitWidth, Expr left, Expr right); 653 654 //! \brief Returns a bitvector expression with a bit-width of 32 655 //! representing the subtraction '(left - right)' of the given 656 //! bitvector expressions. 657 //! 658 //! The given bitvector expressions must have a bit-width of 32. 659 //! 660 DLL_PUBLIC Expr vc_bv32MinusExpr(VC vc, Expr left, Expr right); 661 662 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 663 //! representing the multiplication '(left * right)' of the two 664 //! given bitvector expressions. 665 //! 666 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 667 //! 668 DLL_PUBLIC Expr vc_bvMultExpr(VC vc, int bitWidth, Expr left, Expr right); 669 670 //! \brief Returns a bitvector expression with a bit-width of 32 671 //! representing the multiplication '(left * right)' of the given 672 //! bitvector expressions. 673 //! 674 //! The given bitvector expressions must have a bit-width of 32. 675 //! 676 DLL_PUBLIC Expr vc_bv32MultExpr(VC vc, Expr left, Expr right); 677 678 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 679 //! representing the division '(dividend / divisor)' of the two 680 //! given bitvector expressions. 681 //! 682 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 683 //! 684 DLL_PUBLIC Expr vc_bvDivExpr(VC vc, int bitWidth, Expr dividend, Expr divisor); 685 686 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 687 //! representing the modulo '(dividend % divisor)' of the two 688 //! given bitvector expressions. 689 //! 690 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 691 //! 692 DLL_PUBLIC Expr vc_bvModExpr(VC vc, int bitWidth, Expr dividend, Expr divisor); 693 694 //! \brief Returns a (signed) bitvector expression with a bit-width of 'bitWidth' 695 //! representing the signed division '(dividend / divisor)' of the two 696 //! given bitvector expressions. 697 //! 698 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 699 //! 700 DLL_PUBLIC Expr vc_sbvDivExpr(VC vc, int bitWidth, Expr dividend, Expr divisor); 701 702 //! \brief Returns a (signed) bitvector expression with a bit-width of 'bitWidth' 703 //! representing the signed modulo '(dividend % divisor)' of the two 704 //! given bitvector expressions. 705 //! 706 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 707 //! 708 DLL_PUBLIC Expr vc_sbvModExpr(VC vc, int bitWidth, Expr dividend, Expr divisor); 709 710 //! \brief Returns a (signed) bitvector expression with a bit-width of 'bitWidth' 711 //! representing the signed remainder of the two 712 //! given bitvector expressions. 713 //! 714 //! The given bitvector expressions must have the same bit-width as 'bitWidth' 715 //! 716 DLL_PUBLIC Expr vc_sbvRemExpr(VC vc, int bitWidth, Expr dividend, Expr divisor); 717 718 ///////////////////////////////////////////////////////////////////////////// 719 /// BITVECTOR COMPARISON OPERATIONS 720 ///////////////////////////////////////////////////////////////////////////// 721 722 //! \brief Returns a boolean expression representing the less-than 723 //! operation '(left < right)' of the given bitvector expressions. 724 //! 725 DLL_PUBLIC Expr vc_bvLtExpr(VC vc, Expr left, Expr right); 726 727 //! \brief Returns a boolean expression representing the less-equals 728 //! operation '(left <= right)' of the given bitvector expressions. 729 //! 730 DLL_PUBLIC Expr vc_bvLeExpr(VC vc, Expr left, Expr right); 731 732 //! \brief Returns a boolean expression representing the greater-than 733 //! operation '(left > right)' of the given bitvector expressions. 734 //! 735 DLL_PUBLIC Expr vc_bvGtExpr(VC vc, Expr left, Expr right); 736 737 //! \brief Returns a boolean expression representing the greater-equals 738 //! operation '(left >= right)' of the given bitvector expressions. 739 //! 740 DLL_PUBLIC Expr vc_bvGeExpr(VC vc, Expr left, Expr right); 741 742 //! \brief Returns a boolean expression representing the signed less-than 743 //! operation '(left < right)' of the given signed bitvector expressions. 744 //! 745 DLL_PUBLIC Expr vc_sbvLtExpr(VC vc, Expr left, Expr right); 746 747 //! \brief Returns a boolean expression representing the signed less-equals 748 //! operation '(left <= right)' of the given signed bitvector expressions. 749 //! 750 DLL_PUBLIC Expr vc_sbvLeExpr(VC vc, Expr left, Expr right); 751 752 //! \brief Returns a boolean expression representing the signed greater-than 753 //! operation '(left > right)' of the given signed bitvector expressions. 754 //! 755 DLL_PUBLIC Expr vc_sbvGtExpr(VC vc, Expr left, Expr right); 756 757 //! \brief Returns a boolean expression representing the signed greater-equals 758 //! operation '(left >= right)' of the given signed bitvector expressions. 759 //! 760 DLL_PUBLIC Expr vc_sbvGeExpr(VC vc, Expr left, Expr right); 761 762 ///////////////////////////////////////////////////////////////////////////// 763 /// BITVECTOR BITWISE OPERATIONS 764 ///////////////////////////////////////////////////////////////////////////// 765 766 //! \brief Returns a bitvector expression representing the arithmetic 767 //! negation '(-a)' (unary minus) of the given child bitvector expression. 768 //! 769 DLL_PUBLIC Expr vc_bvUMinusExpr(VC vc, Expr child); 770 771 //! \brief Returns a bitvector expression representing the bitwise-and 772 //! operation '(a & b)' for the given bitvector expressions. 773 //! 774 //! The given bitvector expressions must have the same bit-width. 775 //! 776 DLL_PUBLIC Expr vc_bvAndExpr(VC vc, Expr left, Expr right); 777 778 //! \brief Returns a bitvector expression representing the bitwise-or 779 //! operation '(a | b)' for the given bitvector expressions. 780 //! 781 //! The given bitvector expressions must have the same bit-width. 782 //! 783 DLL_PUBLIC Expr vc_bvOrExpr(VC vc, Expr left, Expr right); 784 785 //! \brief Returns a bitvector expression representing the bitwise-xor 786 //! operation '(a ^ b)' for the given bitvector expressions. 787 //! 788 //! The given bitvector expressions must have the same bit-width. 789 //! 790 DLL_PUBLIC Expr vc_bvXorExpr(VC vc, Expr left, Expr right); 791 792 //! \brief Returns a bitvector expression representing the bitwise-not 793 //! operation '~a' for the given bitvector expressions. 794 //! 795 //! The given bitvector expressions must have the same bit-width. 796 //! 797 DLL_PUBLIC Expr vc_bvNotExpr(VC vc, Expr child); 798 799 ///////////////////////////////////////////////////////////////////////////// 800 /// BITVECTOR SHIFT OPERATIONS 801 ///////////////////////////////////////////////////////////////////////////// 802 803 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 804 //! representing the left-shift operation '(left >> right)' of the 805 //! given bitvector expressions. 806 //! 807 //! Note: This is the new API for this kind of operation! 808 //! 809 DLL_PUBLIC Expr vc_bvLeftShiftExprExpr(VC vc, int bitWidth, Expr left, 810 Expr right); 811 812 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 813 //! representing the right-shift operation '(left << right)' of the 814 //! given bitvector expressions. 815 //! 816 //! Note: This is the new API for this kind of operation! 817 //! 818 DLL_PUBLIC Expr vc_bvRightShiftExprExpr(VC vc, int bitWidth, Expr left, 819 Expr right); 820 821 //! \brief Returns a bitvector expression with a bit-width of 'bitWidth' 822 //! representing the signed right-shift operation '(left >> right)' of the 823 //! given bitvector expressions. 824 //! 825 //! Note: This is the new API for this kind of operation! 826 //! 827 DLL_PUBLIC Expr vc_bvSignedRightShiftExprExpr(VC vc, int bitWidth, Expr left, 828 Expr right); 829 830 //! \brief Deprecated: Use the new API instead! 831 //! 832 //! Returns an expression representing the left-shift operation '(child << sh_amt)' 833 //! for the given child bitvector expression. 834 //! 835 //! Note: Use 'vc_bvLeftShiftExprExpr' instead! 836 //! 837 DLL_PUBLIC Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child); 838 839 //! \brief Deprecated: Use the new API instead! 840 //! 841 //! Returns an expression representing the right-shift operation '(child >> sh_amt)' 842 //! for the given child bitvector expression. 843 //! 844 //! Note: Use 'vc_bvRightShiftExprExpr' instead! 845 //! 846 DLL_PUBLIC Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child); 847 848 //! \brief Deprecated: Use the new API instead! 849 //! 850 //! Returns a bitvector expression with a bit-width of 32 851 //! representing the left-shift operation '(child << sh_amt)' 852 //! for the given child bitvector expression. 853 //! 854 //! Note: Use 'vc_bvLeftShiftExprExpr' instead! 855 //! 856 DLL_PUBLIC Expr vc_bv32LeftShiftExpr(VC vc, int sh_amt, Expr child); 857 858 //! \brief Deprecated: Use the new API instead! 859 //! 860 //! Returns a bitvector expression with a bit-width of 32 861 //! representing the right-shift operation '(child >> sh_amt)' 862 //! for the given child bitvector expression. 863 //! 864 //! Note: Use 'vc_bvRightShiftExprExpr' instead! 865 //! 866 DLL_PUBLIC Expr vc_bv32RightShiftExpr(VC vc, int sh_amt, Expr child); 867 868 //! \brief Deprecated: Use the new API instead! 869 //! 870 //! Returns a bitvector expression with a bit-width of 32 871 //! representing the left-shift operation '(child << sh_amt)' 872 //! for the given child bitvector expression. 873 //! 874 //! Note: Use 'vc_bvLeftShiftExprExpr' instead! 875 //! 876 DLL_PUBLIC Expr vc_bvVar32LeftShiftExpr(VC vc, Expr sh_amt, Expr child); 877 878 //! \brief Deprecated: Use the new API instead! 879 //! 880 //! Returns a bitvector expression with a bit-width of 32 881 //! representing the right-shift operation '(child >> sh_amt)' 882 //! for the given child bitvector expression. 883 //! 884 //! Note: Use 'vc_bvRightShiftExprExpr' instead! 885 //! 886 DLL_PUBLIC Expr vc_bvVar32RightShiftExpr(VC vc, Expr sh_amt, Expr child); 887 888 //! \brief Deprecated: Use the new API instead! 889 //! 890 //! Returns a bitvector expression representing the division 891 //! operation of the power of two '(child / 2^rhs)' for the given 892 //! bitvector expressions. 893 //! 894 //! Note: Use 'vc_bvSignedRightShiftExprExpr' instead! 895 //! 896 DLL_PUBLIC Expr vc_bvVar32DivByPowOfTwoExpr(VC vc, Expr child, Expr rhs); 897 898 ///////////////////////////////////////////////////////////////////////////// 899 /// BITVECTOR EXTRACTION & EXTENSION 900 ///////////////////////////////////////////////////////////////////////////// 901 902 //! \brief Returns a bitvector expression representing the extraction 903 //! of the bits within the range of 'low_bit_no' and 'high_bit_no'. 904 //! 905 //! Note: The resulting bitvector expression has a bit-width of 'high_bit_no - low_bit_no'. 906 //! 907 DLL_PUBLIC Expr vc_bvExtract(VC vc, Expr child, int high_bit_no, 908 int low_bit_no); 909 910 //! \brief Superseeded: Use 'vc_bvBoolExtract_Zero' or 'vc_bvBoolExtract_One' instead. 911 //! 912 //! Returns a boolean expression that accepts a bitvector expression 'x' 913 //! and represents the following equation: '(x[bit_no:bit_no] == 0)'. 914 //! 915 //! Note: This is equal to calling 'vc_bvBoolExtract_Zero'. 916 //! 917 DLL_PUBLIC Expr vc_bvBoolExtract(VC vc, Expr x, int bit_no); 918 919 //! \brief Returns a boolean expression that accepts a bitvector expression 'x' 920 //! and represents the following equation: '(x[bit_no:bit_no] == 0)'. 921 //! 922 DLL_PUBLIC Expr vc_bvBoolExtract_Zero(VC vc, Expr x, int bit_no); 923 924 //! \brief Returns a boolean expression that accepts a bitvector expression 'x' 925 //! and represents the following equation: '(x[bit_no:bit_no] == 1)'. 926 //! 927 DLL_PUBLIC Expr vc_bvBoolExtract_One(VC vc, Expr x, int bit_no); 928 929 //! \brief Returns a bitvector expression representing the extension of the given 930 //! to the amount of bits given by 'newWidth'. 931 //! 932 //! Note: This operation retains the signedness of the bitvector is existant. 933 //! 934 DLL_PUBLIC Expr vc_bvSignExtend(VC vc, Expr child, int newWidth); 935 936 ///////////////////////////////////////////////////////////////////////////// 937 /// CONVENIENCE FUNCTIONS FOR ARRAYS 938 ///////////////////////////////////////////////////////////////////////////// 939 940 /*C pointer support: C interface to support C memory arrays in CVCL */ 941 942 //! \brief Convenience function to create a named array expression with 943 //! an index bit-width of 32 and a value bit-width of 8. 944 //! 945 DLL_PUBLIC Expr vc_bvCreateMemoryArray(VC vc, const char* arrayName); 946 947 //! \brief Convenience function to read a bitvector with byte-width 'numOfBytes' of an 948 //! array expression created by 'vc_bvCreateMemoryArray' and return it. 949 //! 950 //! Note: This returns a bitvector expression with a bit-width of 'numOfBytes'. 951 //! 952 DLL_PUBLIC Expr vc_bvReadMemoryArray(VC vc, Expr array, Expr byteIndex, 953 int numOfBytes); 954 955 //! \brief Convenience function to write a bitvector 'element' with byte-width 'numOfBytes' 956 //! into the given array expression at offset 'byteIndex'. 957 //! 958 DLL_PUBLIC Expr vc_bvWriteToMemoryArray(VC vc, Expr array, Expr byteIndex, 959 Expr element, int numOfBytes); 960 961 ///////////////////////////////////////////////////////////////////////////// 962 /// GENERAL EXPRESSION OPERATIONS 963 ///////////////////////////////////////////////////////////////////////////// 964 965 //! \brief Returns a string representation of the given expression. 966 //! 967 //! Note: 968 //! The caller is responsible for deallocating the string afterwards. 969 //! The buffer that stores the string is allocated by STP. 970 //! 971 DLL_PUBLIC char* exprString(Expr e); 972 973 //! \brief Returns a string representation of the given type. 974 //! 975 //! Note: 976 //! The caller is responsible for deallocating the string afterwards. 977 //! The buffer that stores the string is allocated by STP. 978 //! 979 DLL_PUBLIC char* typeString(Type t); 980 981 //! \brief Returns the n-th child of the given expression. 982 //! 983 DLL_PUBLIC Expr getChild(Expr e, int n); 984 985 //! \brief Misleading name! 986 //! 987 //! Returns '1' if the given boolean expression evaluates to 'true', 988 //! returns '0' if the given boolean expression evaluates to 'false', 989 //! or returns '-1' otherwise, i.e. if the given expression was not a 990 //! boolean expression. 991 //! 992 DLL_PUBLIC int vc_isBool(Expr e); 993 994 //! \brief Registers the given error handler function to be called for each 995 //! fatal error that occures while running STP. 996 //! 997 DLL_PUBLIC void 998 vc_registerErrorHandler(void (*error_hdlr)(const char* err_msg)); 999 1000 //! \brief Returns the hash of the given query state. 1001 //! 1002 DLL_PUBLIC int vc_getHashQueryStateToBuffer(VC vc, Expr query); 1003 1004 //! \brief Destroy the given validity checker. 1005 //! 1006 //! Removes all associated expressions with it if 'EXPRDELETE' was set to 'true' 1007 //! via 'vc_setInterfaceFlags' during the process. 1008 //! 1009 DLL_PUBLIC void vc_Destroy(VC vc); 1010 1011 //! \brief Destroy the given expression, freeing its associated memory. 1012 //! 1013 DLL_PUBLIC void vc_DeleteExpr(Expr e); 1014 1015 //! \brief Returns the whole counterexample from the given validity checker. 1016 //! 1017 DLL_PUBLIC WholeCounterExample vc_getWholeCounterExample(VC vc); 1018 1019 //! \brief Returns the value of the given term expression from the given whole counter example. 1020 //! 1021 DLL_PUBLIC Expr vc_getTermFromCounterExample(VC vc, Expr e, 1022 WholeCounterExample c); 1023 1024 //! \brief Destroys the given whole counter example, freeing all of its associated memory. 1025 //! 1026 DLL_PUBLIC void vc_deleteWholeCounterExample(WholeCounterExample cc); 1027 1028 //! Covers all kinds of expressions that exist in STP. 1029 //! 1030 enum exprkind_t 1031 { 1032 UNDEFINED, //!< An undefined expression. 1033 SYMBOL, //!< Named expression (or variable), i.e. created via 'vc_varExpr'. 1034 BVCONST, //!< Bitvector constant expression, i.e. created via 'vc_bvConstExprFromInt'. 1035 BVNOT, //!< Bitvector bitwise-not 1036 BVCONCAT, //!< Bitvector concatenation 1037 BVOR, //!< Bitvector bitwise-or 1038 BVAND, //!< Bitvector bitwise-and 1039 BVXOR, //!< Bitvector bitwise-xor 1040 BVNAND, //!< Bitvector bitwise not-and; OR nand (TODO: does this still exist?) 1041 BVNOR, //!< Bitvector bitwise not-or; OR nor (TODO: does this still exist?) 1042 BVXNOR, //!< Bitvector bitwise not-xor; OR xnor (TODO: does this still exist?) 1043 BVEXTRACT, //!< Bitvector extraction, i.e. via 'vc_bvExtract'. 1044 BVLEFTSHIFT, //!< Bitvector left-shift 1045 BVRIGHTSHIFT, //!< Bitvector right-right 1046 BVSRSHIFT, //!< Bitvector signed right-shift 1047 BVPLUS, //!< Bitvector addition 1048 BVSUB, //!< Bitvector subtraction 1049 BVUMINUS, //!< Bitvector unary minus; OR negate expression 1050 BVMULT, //!< Bitvector multiplication 1051 BVDIV, //!< Bitvector division 1052 BVMOD, //!< Bitvector modulo operation 1053 SBVDIV, //!< Signed bitvector division 1054 SBVREM, //!< Signed bitvector remainder 1055 SBVMOD, //!< Signed bitvector modulo operation 1056 BVSX, //!< Bitvector signed extend 1057 BVZX, //!< Bitvector zero extend 1058 ITE, //!< If-then-else 1059 BOOLEXTRACT, //!< Bitvector boolean extraction 1060 BVLT, //!< Bitvector less-than 1061 BVLE, //!< Bitvector less-equals 1062 BVGT, //!< Bitvector greater-than 1063 BVGE, //!< Bitvector greater-equals 1064 BVSLT, //!< Signed bitvector less-than 1065 BVSLE, //!< Signed bitvector less-equals 1066 BVSGT, //!< Signed bitvector greater-than 1067 BVSGE, //!< Signed bitvector greater-equals 1068 EQ, //!< Equality comparator 1069 FALSE, //!< Constant false boolean expression 1070 TRUE, //!< Constant true boolean expression 1071 NOT, //!< Logical-not boolean expression 1072 AND, //!< Logical-and boolean expression 1073 OR, //!< Logical-or boolean expression 1074 NAND, //!< Logical-not-and boolean expression (TODO: Does this still exist?) 1075 NOR, //!< Logical-not-or boolean expression (TODO: Does this still exist?) 1076 XOR, //!< Logical-xor (either-or) boolean expression 1077 IFF, //!< If-and-only-if boolean expression 1078 IMPLIES, //!< Implication boolean expression 1079 PARAMBOOL, //!< Parameterized boolean expression 1080 READ, //!< Array read expression 1081 WRITE, //!< Array write expression 1082 ARRAY, //!< Array creation expression 1083 BITVECTOR, //!< Bitvector creation expression 1084 BOOLEAN //!< Boolean creation expression 1085 }; 1086 1087 //! \brief Returns the expression-kind of the given expression. 1088 //! 1089 DLL_PUBLIC enum exprkind_t getExprKind(Expr e); 1090 1091 //! \brief Returns the number of child expressions of the given expression. 1092 //! 1093 DLL_PUBLIC int getDegree(Expr e); 1094 1095 //! \brief Returns the bit-width of the given bitvector expression. 1096 //! 1097 DLL_PUBLIC int getBVLength(Expr e); 1098 1099 //! Covers all kinds of types that exist in STP. 1100 //! 1101 enum type_t 1102 { 1103 BOOLEAN_TYPE = 0, 1104 BITVECTOR_TYPE, 1105 ARRAY_TYPE, 1106 UNKNOWN_TYPE 1107 }; 1108 1109 //! \brief Returns the type-kind of the given expression. 1110 //! 1111 DLL_PUBLIC enum type_t getType(Expr e); 1112 1113 // get value bit width 1114 1115 //! \brief Returns the value bit-width of the given expression. 1116 //! 1117 //! This is mainly useful for array expression. 1118 //! 1119 DLL_PUBLIC int getVWidth(Expr e); 1120 1121 //! \brief Returns the index bit-width of the given expression. 1122 //! 1123 //! This is mainly useful for array expression. 1124 //! 1125 DLL_PUBLIC int getIWidth(Expr e); 1126 1127 //! \brief Prints the given counter example to the file that is 1128 //! associated with the given open file descriptor. 1129 //! 1130 DLL_PUBLIC void vc_printCounterExampleFile(VC vc, int fd); 1131 1132 //! \brief Returns the name of the given variable expression. 1133 //! 1134 DLL_PUBLIC const char* exprName(Expr e); 1135 1136 //! \brief Returns the internal node ID of the given expression. 1137 //! 1138 DLL_PUBLIC int getExprID(Expr ex); 1139 1140 //! \brief Parses the given string in CVC or SMTLib1.0 format and extracts 1141 //! query and assertion information into the 'outQuery' and 'outAsserts' 1142 //! buffers respectively. 1143 //! 1144 //! It is the caller's responsibility to free the buffer's memory afterwards. 1145 //! 1146 //! Note: The user can controle the parsed format via 'process_argument'. 1147 //! 1148 //! Returns '1' if parsing was successful. 1149 //! 1150 DLL_PUBLIC int vc_parseMemExpr(VC vc, const char* s, Expr* outQuery, 1151 Expr* outAsserts); 1152 1153 //! \brief Checks if STP was compiled with support for minisat 1154 //! 1155 //! Note: always returns true (future support for minisat being the 1156 //! non-default) 1157 //! 1158 DLL_PUBLIC bool vc_supportsMinisat(VC vc); 1159 1160 //! \brief Sets underlying SAT solver to minisat 1161 //! 1162 DLL_PUBLIC bool vc_useMinisat(VC vc); 1163 1164 //! \brief Checks if underlying SAT solver is minisat 1165 //! 1166 DLL_PUBLIC bool vc_isUsingMinisat(VC vc); 1167 1168 //! \brief Checks if STP was compiled with support for simplifying minisat 1169 //! 1170 //! Note: always returns true (future support for simplifying minisat being 1171 //! the non-default) 1172 //! 1173 DLL_PUBLIC bool vc_supportsSimplifyingMinisat(VC vc); 1174 1175 //! \brief Sets underlying SAT solver to simplifying minisat 1176 //! 1177 DLL_PUBLIC bool vc_useSimplifyingMinisat(VC vc); 1178 1179 //! \brief Checks if underlying SAT solver is simplifying minisat 1180 //! 1181 DLL_PUBLIC bool vc_isUsingSimplifyingMinisat(VC vc); 1182 1183 //! \brief Checks if STP was compiled with support for cryptominisat 1184 //! 1185 DLL_PUBLIC bool vc_supportsCryptominisat(VC vc); 1186 1187 //! \brief Sets underlying SAT solver to cryptominisat 1188 //! 1189 DLL_PUBLIC bool vc_useCryptominisat(VC vc); 1190 1191 //! \brief Checks if underlying SAT solver is cryptominisat 1192 //! 1193 DLL_PUBLIC bool vc_isUsingCryptominisat(VC vc); 1194 1195 //! \brief Checks if STP was compiled with support for riss 1196 //! 1197 DLL_PUBLIC bool vc_supportsRiss(VC vc); 1198 1199 //! \brief Sets underlying SAT solver to riss 1200 //! 1201 DLL_PUBLIC bool vc_useRiss(VC vc); 1202 1203 //! \brief Checks if underlying SAT solver is riss 1204 //! 1205 DLL_PUBLIC bool vc_isUsingRiss(VC vc); 1206 1207 1208 #ifdef __cplusplus 1209 } 1210 #endif 1211 1212 #undef DLL_PUBLIC // Undefine internal macro to prevent it from leaking into the API. 1213 #undef DLL_LOCAL // Undefine internal macro to prevent it from leaking into the API. 1214 1215 #undef _CVCL_DEFAULT_ARG // Undefine macro to not pollute global macro namespace! 1216 1217 #endif // _cvcl__include__c_interface_h_ 1218