cadical基本数据结构01

标签：01 const int void VALID ensure 数据结构 cadical require

以下代码基于cadical-rel-1.5.3版本，来源于：

	Solver 在cadical.hpp文件中声明求解器类型。其中成员函数比较有趣的是： int val (int lit); //Line 25, 返回文字的正负性；assert(val(liter)),断言文字liter为非零，即是有效文字； bool failed (int lit); // Determine whether the valid non-zero literal is in the core. void copy (Solver & other) const; // Line
	1 class Solver { 2 3 public: 4 5 // ====== BEGIN IPASIR =================================================== 6 7 // This section implements the corresponding IPASIR functionality. 8 9 Solver (); 10 ~Solver (); 11 12 static const char * signature (); // name of this library 13 14 // Core functionality as in the IPASIR incremental SAT solver interface. 15 // (recall 'READY = CONFIGURING \| UNKNOWN \| SATISFIED \| UNSATISFIED'). 16 // Further note that 'lit' is required to be different from 'INT_MIN' and 17 // different from '0' except for 'add'. 18 19 // Add valid literal to clause or zero to terminate clause. 20 // 21 // require (VALID) // recall 'VALID = READY \| ADDING' 22 // if (lit) ensure (ADDING) // and thus VALID but not READY 23 // if (!lit) ensure (UNKNOWN) // and thus READY 24 // 25 void add (int lit); 26 27 // Assume valid non zero literal for next call to 'solve'. These 28 // assumptions are reset after the call to 'solve' as well as after 29 // returning from 'simplify' and 'lookahead. 30 // 31 // require (READY) 32 // ensure (UNKNOWN) 33 // 34 void assume (int lit); 35 36 // Try to solve the current formula. Returns 37 // 38 // 0 = UNSOLVED (limit reached or interrupted through 'terminate') 39 // 10 = SATISFIABLE 40 // 20 = UNSATISFIABLE 41 // 42 // require (READY) 43 // ensure (UNKNOWN \| SATISFIED \| UNSATISFIED) 44 // 45 // Note, that while in this call the solver actually transitions to state 46 // 'SOLVING', which however is only visible from a different context, 47 // i.e., from a different thread or from a signal handler. Only right 48 // before returning from this call it goes into a 'READY' state. 49 // 50 int solve (); 51 52 // Get value (-lit=false, lit=true) of valid non-zero literal. 53 // 54 // require (SATISFIED) 55 // ensure (SATISFIED) 56 // 57 int val (int lit); 58 59 // Determine whether the valid non-zero literal is in the core. 60 // Returns 'true' if the literal is in the core and 'false' otherwise. 61 // Note that the core does not have to be minimal. 62 // 63 // require (UNSATISFIED) 64 // ensure (UNSATISFIED) 65 // 66 bool failed (int lit); 67 68 // Add call-back which is checked regularly for termination. There can 69 // only be one terminator connected. If a second (non-zero) one is added 70 // the first one is implicitly disconnected. 71 // 72 // require (VALID) 73 // ensure (VALID) 74 // 75 void connect_terminator (Terminator * terminator); 76 void disconnect_terminator (); 77 78 // Add call-back which allows to export learned clauses. 79 // 80 // require (VALID) 81 // ensure (VALID) 82 // 83 void connect_learner (Learner * learner); 84 void disconnect_learner (); 85 86 // ====== END IPASIR ===================================================== 87 88 //------------------------------------------------------------------------ 89 // Adds a literal to the constraint clause. Same functionality as 'add' but 90 // the clause only exists for the next call to solve (same lifetime as 91 // assumptions). Only one constraint may exists at a time. A new constraint 92 // replaces the old. 93 // The main application of this functonality is the model checking algorithm 94 // IC3. See our FMCAD'21 paper [FroleyksBiere-FMCAD'19] for more details. 95 // 96 // Add valid literal to the constraint clause or zero to terminate it. 97 // 98 // require (VALID) // recall 'VALID = READY \| ADDING' 99 // if (lit) ensure (ADDING) // and thus VALID but not READY 100 // if (!lit) && !adding_clause ensure (UNKNOWN) // and thus READY 101 // 102 void constrain (int lit); 103 104 // Determine whether the constraint was used to proof the unsatisfiability. 105 // Note that the formula might still be unsatisfiable without the constraint. 106 // 107 // require (UNSATISFIED) 108 // ensure (UNSATISFIED) 109 // 110 bool constraint_failed (); 111 112 //------------------------------------------------------------------------ 113 // This function determines a good splitting literal. The result can be 114 // zero if the formula is proven to be satisfiable or unsatisfiable. This 115 // can then be checked by 'state ()'. If the formula is empty and 116 // the function is not able to determine satisfiability also zero is 117 // returned but the state remains unknown. 118 // 119 // require (READY) 120 // ensure (UNKNOWN\|SATISFIED\|UNSATISFIED) 121 // 122 int lookahead(void); 123 124 struct CubesWithStatus { 125 int status; 126 std::vector<std::vector<int>> cubes; 127 }; 128 129 CubesWithStatus generate_cubes(int, int min_depth = 0); 130 131 void reset_assumptions (); 132 void reset_constraint (); 133 134 // Return the current state of the solver as defined above. 135 // 136 const State & state () const { return _state; } 137 138 // Similar to 'state ()' but using the staddard competition exit codes of 139 // '10' for 'SATISFIABLE', '20' for 'UNSATISFIABLE' and '0' otherwise. 140 // 141 int status () const { 142 if (_state == SATISFIED) return 10; 143 else if (_state == UNSATISFIED) return 20; 144 else return 0; 145 } 146 147 /----------------------------------------------------------------------/ 148 149 static const char * version (); // return version string 150 151 /----------------------------------------------------------------------/ 152 // Copy 'this' into a fresh 'other'. The copy procedure is not a deep 153 // clone, but only copies irredundant clauses and units. It also makes 154 // sure that witness reconstruction works with the copy as with the 155 // original formula such that both solvers have the same models. 156 // Assumptions are not copied. Options however are copied as well as 157 // flags which remember the current state of variables in preprocessing. 158 // 159 // require (READY) // for 'this' 160 // ensure (READY) // for 'this' 161 // 162 // other.require (CONFIGURING) 163 // other.ensure (CONFIGURING \| UNKNOWN) 164 // 165 void copy (Solver & other) const; 复制过程不是深度克隆，而是只复制非冗余子句和单元。它还确保见证重建可以像处理原始公式一样处理副本，以便两个求解器具有相同的模型。 Assumptions不会被复制。然而，选项和标记被复制，这些标记在预处理中记住了变量的当前状态。 166 167 /----------------------------------------------------------------------/ 168 // Variables are usually added and initialized implicitly whenever a 169 // literal is used as an argument except for the functions 'val', 'fixed', 170 // 'failed' and 'frozen'. However, the library internally keeps a maximum 171 // variable index, which can be queried. 172 // 173 // require (VALID \| SOLVING) 174 // ensure (VALID \| SOLVING) 175 // 176 int vars (); 除了'val'， 'fixed'， 'failed'和'frozen'函数外，变量通常会被隐式地添加和初始化。但是，库内部保留了一个最大变量索引，可以进行查询。 177 178 // Increase the maximum variable index explicitly. This function makes 179 // sure that at least 'min_max_var' variables are initialized. Since it 180 // might need to reallocate tables, it destroys a satisfying assignment 181 // and has the same state transition and conditions as 'assume' etc. 182 // 183 // require (READY) 184 // ensure (UNKNOWN) 185 // 186 void reserve (int min_max_var); 187 188 #ifndef NTRACING 189 //------------------------------------------------------------------------ 190 // This function can be used to write API calls to a file. The same 191 // format is used which 'mobical' can read, execute and also shrink 192 // through delta debugging. 193 // 194 // Tracing API calls can also be achieved by using the environment 195 // variable 'CADICAL_API_TRACE'. That alternative is useful if you do not 196 // want to change the source code using the solver, e.g., if you only have 197 // a binary with the solver linked in. However, that method only allows 198 // to trace one solver instance, while with the following function API 199 // tracing can be enabled for different solver instances individually. 200 // 201 // The solver will flush the file after every trace API call but does not 202 // close it during deletion. It remains owned by the user of the library. 203 // 204 // require (VALID) 205 // ensure (VALID) 206 // 207 void trace_api_calls (FILE * file); 208 #endif 209 210 //------------------------------------------------------------------------ 211 // Option handling. 212 213 // Determine whether 'name' is a valid option name. 214 // 215 static bool is_valid_option (const char * name); 216 217 // Determine whether 'name' enables a specific preprocessing technique. 218 // 219 static bool is_preprocessing_option (const char * name); 220 221 // Determine whether 'arg' is a valid long option of the form '--<name>', 222 // '--<name>=<val>' or '--no-<name>' similar to 'set_long_option' below. 223 // Legal values are 'true', 'false', or '[-]<mantissa>[e<exponent>]'. 224 225 static bool is_valid_long_option (const char * arg); 226 227 // Get the current value of the option 'name'. If 'name' is invalid then 228 // zero is returned. Here '--...' arguments as invalid options. 229 // 230 int get (const char * name); 231 232 // Set the default verbose message prefix (default "c "). 233 // 234 void prefix (const char * verbose_message_prefix); 235 236 // Explicit version of setting an option. If the option '<name>' exists 237 // and '<val>' can be parsed then 'true' is returned. If the option value 238 // is out of range the actual value is computed as the closest (minimum or 239 // maximum) value possible, but still 'true' is returned. 240 // 241 // require (CONFIGURING) 242 // ensure (CONFIGURING) 243 // 244 // Thus options can only bet set right after initialization. 245 // 246 bool set (const char * name, int val); 247 248 // This function accepts options in command line syntax: 249 // 250 // '--<name>=<val>', '--<name>', or '--no-<name>' 251 // 252 // It actually calls the previous 'set' function after parsing 'arg'. The 253 // same values are expected as for 'is_valid_long_option' above and as 254 // with 'set' any value outside of the range of legal values for a 255 // particular option are set to either the minimum or maximum depending on 256 // which side of the valid interval they lie. 257 // 258 // require (CONFIGURING) 259 // ensure (CONFIGURING) 260 // 261 bool set_long_option (const char * arg); 262 263 // Determine whether 'name' is a valid configuration. 264 // 265 static bool is_valid_configuration (const char ); 266 267 // Overwrite (some) options with the forced values of the configuration. 268 // The result is 'true' iff the 'name' is a valid configuration. 269 // 270 // require (CONFIGURING) 271 // ensure (CONFIGURING) 272 // 273 bool configure (const char ); 274 275 // Increase preprocessing and inprocessing limits by '10^<val>'. Values 276 // below '0' are ignored and values above '9' are reduced to '9'. 277 // 278 // require (READY) 279 // ensure (READY) 280 // 281 void optimize (int val); 282 283 // Specify search limits, where currently 'name' can be "conflicts", 284 // "decisions", "preprocessing", or "localsearch". The first two limits 285 // are unbounded by default. Thus using a negative limit for conflicts or 286 // decisions switches back to the default of unlimited search (for that 287 // particular limit). The preprocessing limit determines the number of 288 // preprocessing rounds, which is zero by default. Similarly, the local 289 // search limit determines the number of local search rounds (also zero by 290 // default). As with 'set', the return value denotes whether the limit 291 // 'name' is valid. These limits are only valid for the next 'solve' or 292 // 'simplify' call and reset to their default after 'solve' returns (as 293 // well as overwritten and reset during calls to 'simplify' and 294 // 'lookahead'). We actually also have an internal "terminate" limit 295 // which however should only be used for testing and debugging. 296 // 297 // require (READY) 298 // ensure (READY) 299 // 300 bool limit (const char * arg, int val); 301 bool is_valid_limit (const char * arg); 指定搜索限制，当前“name”可以是“conflicts”、“decisions”、“pre - processing”或“localsearch”。默认情况下，前两个限制是无限制的。因此，对于冲突或决策使用负限制将切换回默认的无限搜索(对于特定的限制)。预处理限制决定预处理轮数，默认为0。类似地，本地搜索限制决定了本地搜索轮的数量(默认情况下也是零)。与'set'一样，返回值表示是否限制'name'有效。这些限制仅对下一个“solve”或“simplify”调用有效，并在“solve”返回后重置为默认值(以及在调用“simplify”和“lookahead”期间重写和重置)。实际上，我们也有一个内部的“终止”限制，但是只能用于测试和调试。 302 303 // The number of currently active variables and clauses can be queried by 304 // these functions. Variables become active if a clause is added with it. 305 // They become inactive if they are eliminated or fixed at the root level 306 // Clauses become inactive if they are satisfied, subsumed, eliminated. 307 // Redundant clauses are reduced regularly and thus the 'redundant' 308 // function is less useful. 309 // 310 // require (VALID) 311 // ensure (VALID) 312 // 313 int active () const; // Number of active variables. 314 int64_t redundant () const; // Number of active redundant clauses. 315 int64_t irredundant () const; // Number of active irredundant clauses. 316 317 //------------------------------------------------------------------------ 318 // This function executes the given number of preprocessing rounds. It is 319 // similar to 'solve' with 'limits ("preprocessing", rounds)' except that 320 // no CDCL nor local search, nor lucky phases are executed. The result 321 // values are also the same: 0=unknown, 10=satisfiable, 20=unsatisfiable. 322 // As 'solve' it resets current assumptions and limits before returning. 323 // The numbers of rounds should not be negative. If the number of rounds 324 // is zero only clauses are restored (if necessary) and top level unit 325 // propagation is performed, which both take some time. 326 // 327 // require (READY) 328 // ensure (UNKNOWN \| SATISFIED \| UNSATISFIED) 329 // 330 int simplify (int rounds = 3); 331 332 //------------------------------------------------------------------------ 333 // Force termination of 'solve' asynchronously. 334 // 335 // require (SOLVING \| READY) 336 // ensure (UNKNOWN) // actually not immediately (synchronously) 337 // 338 void terminate (); 339 340 //------------------------------------------------------------------------ 341 342 // We have the following common reference counting functions, which avoid 343 // to restore clauses but require substantial user guidance. This was the 344 // only way to use inprocessing in incremental SAT solving in Lingeling 345 // (and before in MiniSAT's 'freeze' / 'thaw') and which did not use 346 // automatic clause restoring. In general this is slower than 347 // restoring clauses and should not be used. 348 // 349 // In essence the user freezes variables which potentially are still 350 // needed in clauses added or assumptions used after the next 'solve' 351 // call. As in Lingeling you can freeze a variable multiple times, but 352 // then have to melt it the same number of times again in order to enable 353 // variable eliminating on it etc. The arguments can be literals 354 // (negative indices) but conceptually variables are frozen. 355 // 356 // In the old way of doing things without restore you should not use a 357 // variable incrementally (in 'add' or 'assume'), which was used before 358 // and potentially could have been eliminated in a previous 'solve' call. 359 // This can lead to spurious satisfying assignment. In order to check 360 // this API contract one can use the 'checkfrozen' option. This has the 361 // drawback that restoring clauses implicitly would fail with a fatal 362 // error message even if in principle the solver could just restore 363 // clauses. Thus this option is disabled by default. 364 // 365 // See our SAT'19 paper [FazekasBiereScholl-SAT'19] for more details. 366 // 367 // require (VALID) 368 // ensure (VALID) 369 // 370 bool frozen (int lit) const; 371 void freeze (int lit); 372 void melt (int lit); // Also needs 'require (frozen (lit))'. 373 374 //------------------------------------------------------------------------ 375 376 // Root level assigned variables can be queried with this function. 377 // It returns '1' if the literal is implied by the formula, '-1' if its 378 // negation is implied, or '0' if this is unclear at this point. 379 // 380 // require (VALID) 381 // ensure (VALID) 382 // 383 int fixed (int lit) const; 384 385 //------------------------------------------------------------------------ 386 // Force the default decision phase of a variable to a certain value. 387 // 388 void phase (int lit); 389 void unphase (int lit); 390 391 //------------------------------------------------------------------------ 392 393 // Enables clausal proof tracing in DRAT format and returns 'true' if 394 // successfully opened for writing. Writing proofs has to be enabled 395 // before calling 'solve', 'add' and 'dimacs', that is in state 396 // 'CONFIGURING'. Otherwise only partial proofs would be written. 397 // 398 // require (CONFIGURING) 399 // ensure (CONFIGURING) 400 // 401 bool trace_proof (FILE * file, const char * name); // Write DRAT proof. 402 bool trace_proof (const char * path); // Open & write proof. 403 404 // Flush proof trace file. 405 // 406 // require (VALID) 407 // ensure (VALID) 408 // 409 void flush_proof_trace (); 410 411 // Close proof trace early. 412 // 413 // require (VALID) 414 // ensure (VALID) 415 // 416 void close_proof_trace (); 417 418 //------------------------------------------------------------------------ 419 420 static void usage (); // print usage information for long options 421 422 static void configurations (); // print configuration usage options 423 424 // require (!DELETING) 425 // ensure (!DELETING) 426 // 427 void statistics (); // print statistics 428 void resources (); // print resource usage (time and memory) 429 430 // require (VALID) 431 // ensure (VALID) 432 // 433 void options (); // print current option and value list 434 435 //------------------------------------------------------------------------ 436 // Traverse irredundant clauses or the extension stack in reverse order. 437 // 438 // The return value is false if traversal is aborted early due to one of 439 // the visitor functions returning false. See description of the 440 // iterators below for more details on how to use these functions. 441 // 442 // require (VALID) 443 // ensure (VALID) 444 // 445 bool traverse_clauses (ClauseIterator &) const; 446 bool traverse_witnesses_backward (WitnessIterator &) const; 447 bool traverse_witnesses_forward (WitnessIterator &) const; 448 449 //------------------------------------------------------------------------ 450 // Files with explicit path argument support compressed input and output 451 // if appropriate helper functions 'gzip' etc. are available. They are 452 // called through opening a pipe to an external command. 453 // 454 // If the 'strict' argument is zero then the number of variables and 455 // clauses specified in the DIMACS headers are ignored, i.e., the header 456 // 'p cnf 0 0' is always legal. If the 'strict' argument is larger '1' 457 // strict formatting of the header is required, i.e., single spaces 458 // everywhere and no trailing white space. 459 // 460 // Returns zero if successful and otherwise an error message. 461 // 462 // require (VALID) 463 // ensure (VALID) 464 // 465 const char * read_dimacs (FILE * file, 466 const char * name, int & vars, int strict = 1); 467 468 const char * read_dimacs (const char * path, int & vars, int strict = 1); 469 470 // The following routines work the same way but parse both DIMACS and 471 // INCCNF files (with 'p inccnf' header and 'a <cube>' lines). If the 472 // parser finds and 'p inccnf' header or cubes then 'incremental' is set 473 // to true and the cubes are stored in the given vector (each cube 474 // terminated by a zero). 475 476 const char read_dimacs (FILE * file, 477 const char * name, int & vars, int strict, 478 bool & incremental, std::vector<int> & cubes); 479 480 const char * read_dimacs (const char * path, int & vars, int strict, 481 bool & incremental, std::vector<int> & cubes); 482 483 //------------------------------------------------------------------------ 484 // Write current irredundant clauses and all derived unit clauses 485 // to a file in DIMACS format. Clauses on the extension stack are 486 // not included, nor any redundant clauses. 487 // 488 // The 'min_max_var' parameter gives a lower bound on the number '<vars>' 489 // of variables used in the DIMACS 'p cnf <vars> ...' header. 490 // 491 // Returns zero if successful and otherwise an error message. 492 // 493 // require (VALID) 494 // ensure (VALID) 495 // 496 const char * write_dimacs (const char * path, int min_max_var = 0); 497 498 // The extension stack for reconstruction a solution can be written too. 499 // 500 const char * write_extension (const char * path); 501 502 // Print build configuration to a file with prefix 'c '. If the file 503 // is '<stdout>' or '<stderr>' then terminal color codes might be used. 504 // 505 static void build (FILE * file, const char * prefix = "c "); 506 507 private: 508 509 //==== start of state ==================================================== 510 511 // The solver is in the state ADDING if either the current clause or the 512 // constraint (or both) is not yet terminated. 513 bool adding_clause; 514 bool adding_constraint; 515 516 State _state; // API states as discussed above. 517 518 /----------------------------------------------------------------------/ 519 520 // The 'Solver' class is a 'facade' object for 'External'. It exposes the 521 // public API of 'External' but hides everything else (except for the some 522 // private functions). It is supposed to make it easier to understand the 523 // API and use the solver through the API. 524 525 // This approach has the benefit of decoupling this header file from all 526 // internal data structures, which is particularly useful if the rest of 527 // the source is not available. For instance if only a CaDiCaL library is 528 // installed in a system, then only this header file has to be installed 529 // too, and still allows to compile and link against the library. 530 531 /----------------------------------------------------------------------/ 532 533 // More precisely the CaDiCaL code is split into three layers: 534 // 535 // Solver: facade object providing the actual API of the solver 536 // External: communication layer between 'Solver' and 'Internal' 537 // Internal: the actual solver code 538 // 539 // The 'External' and 'Internal' layers are declared and implemented in 540 // the corresponding '{external,internal}.{hpp,cpp}' files (as expected), 541 // while the 'Solver' facade class is defined in 'cadical.hpp' (here) but 542 // implemented in 'solver.cpp'. The reason for this naming mismatch is, 543 // that we want to use 'cadical.hpp' for the library header (this header 544 // file) and call the binary of the stand alone SAT also 'cadical', which 545 // is more naturally implemented in 'cadical.cpp'. 546 // 547 // Separating 'External' from 'Internal' also allows us to map external 548 // literals to internal literals, which is useful with many fixed or 549 // eliminated variables (during 'compact' the internal variable range is 550 // reduced and external variables are remapped). Such an approach is also 551 // necessary, if we want to use extended resolution in the future (such as 552 // bounded variable addition). 553 // 554 Internal * internal; // Hidden internal solver. 555 External * external; // Hidden API to internal solver mapping. 556 557 #ifndef NTRACING 558 // The API calls to the solver can be traced by setting the environment 559 // variable 'CADICAL_API_TRACE' to point to the path of a file to which 560 // API calls are written. The same format is used which 'mobical' can 561 // read, execute and also shrink through delta debugging. 562 // 563 // The environment variable is read in the constructor and the trace is 564 // opened for writing and then closed again in the destructor. 565 // 566 // Alternatively one case use 'trace_api_calls'. Both 567 // 568 bool close_trace_api_file; // Close file if owned by solver it. 569 FILE * trace_api_file; // Also acts as flag that we are tracing. 570 571 static bool tracing_api_through_environment; 572 573 //===== end of state ==================================================== 574 575 void trace_api_call (const char ) const; 576 void trace_api_call (const char , int) const; 577 void trace_api_call (const char , const char , int) const; 578 #endif 579 580 void transition_to_unknown_state (); 581 582 //------------------------------------------------------------------------ 583 // Used in the stand alone solver application 'App' and the model based 584 // tester 'Mobical'. So only these two classes need direct access to the 585 // otherwise more application specific functions listed here together with 586 // the internal DIMACS parser. 587 588 friend class App; 589 friend class Mobical; 590 friend class Parser; 591 592 // Read solution in competition format for debugging and testing. 593 // 594 // require (VALID) 595 // ensure (VALID) 596 // 597 const char * read_solution (const char * path); 598 599 // Cross-compilation with 'MinGW' needs some work-around for 'printf' 600 // style printing of 64-bit numbers including warning messages. The 601 // followings lines are copies of similar code in 'inttypes.hpp' but we 602 // want to keep the 'cadical.hpp' header file stand-alone. 603 604 # ifndef PRINTF_FORMAT 605 # ifdef __MINGW32__ 606 # define __USE_MINGW_ANSI_STDIO 1 607 # define PRINTF_FORMAT __MINGW_PRINTF_FORMAT 608 # else 609 # define PRINTF_FORMAT printf 610 # endif 611 # endif 612 613 // This gives warning messages for wrong 'printf' style format string usage. 614 // Apparently (on 'gcc 9' at least) the first argument is 'this' here. 615 // 616 // TODO: support for other compilers (beside 'gcc' and 'clang'). 617 618 # define CADICAL_ATTRIBUTE_FORMAT(FORMAT_POSITION,VARIADIC_ARGUMENT_POSITION) \ 619 __attribute__ ((format (PRINTF_FORMAT, FORMAT_POSITION, VARIADIC_ARGUMENT_POSITION))) 620 621 // Messages in a common style. 622 // 623 // require (VALID \| DELETING) 624 // ensure (VALID \| DELETING) 625 // 626 void section (const char ); // print section header 627 void message (const char , ...) // ordinary message 628 CADICAL_ATTRIBUTE_FORMAT (2, 3); 629 630 void message (); // empty line - only prefix 631 void error (const char , ...) // produce error message 632 CADICAL_ATTRIBUTE_FORMAT (2, 3); 633 634 // Explicit verbose level ('section' and 'message' use '0'). 635 // 636 // require (VALID \| DELETING) 637 // ensure (VALID \| DELETING) 638 // 639 void verbose (int level, const char , ...) 640 CADICAL_ATTRIBUTE_FORMAT (3, 4); 641 642 // Factoring out common code to both 'read_dimacs' functions above. 643 // 644 // require (VALID) 645 // ensure (VALID) 646 // 647 const char * read_dimacs (File , int &, int strict, 648 bool incremental = 0, 649 std::vector<int> * = 0); 650 651 // Factored out common code for 'solve', 'simplify' and 'lookahead'. 652 // 653 int call_external_solve_and_check_results (bool preprocess_only); 654 655 //------------------------------------------------------------------------ 656 // Print DIMACS file to '<stdout>' for debugging and testing purposes, 657 // including derived units and assumptions. Since it will print in terms 658 // of internal literals it is otherwise not really useful. To write a 659 // DIMACS formula in terms of external variables use 'write_dimacs'. 660 // 661 // require (!INITIALIZING) 662 // ensure (!INITIALIZING) 663 // 664 void dump_cnf (); 665 friend struct DumpCall; // Mobical calls 'dump_cnf' in 'DumpCall::execute' 666 }; 667 668 /========================================================================/ 669 670 // Connected terminators are checked for termination regularly. If the 671 // 'terminate' function of the terminator returns true the solver is 672 // terminated synchronously as soon it calls this function. 673 674 class Terminator { 675 public: 676 virtual ~Terminator () { } 677 virtual bool terminate () = 0; 678 }; 679 680 // Connected learners which can be used to export learned clauses. 681 // The 'learning' can check the size of the learn clause and only if it 682 // returns true then the individual literals of the learned clause are given 683 // to the learn through 'learn' one by one terminated by a zero literal. 684 685 class Learner { 686 public: 687 virtual ~Learner () { } 688 virtual bool learning (int size) = 0; 689 virtual void learn (int lit) = 0; 690 }; 691 692 /------------------------------------------------------------------------/ 693 694 // Allows to traverse all remaining irredundant clauses. Satisfied and 695 // eliminated clauses are not included, nor any derived units unless such 696 // a unit literal is frozen. Falsified literals are skipped. If the solver 697 // is inconsistent only the empty clause is traversed. 698 // 699 // If 'clause' returns false traversal aborts early. 700 701 class ClauseIterator { 702 public: 703 virtual ~ClauseIterator () { } 704 virtual bool clause (const std::vector<int> &) = 0; 705 };

标签：01,const,int,void,VALID,ensure,数据结构,cadical,require
From： https://www.cnblogs.com/yuweng1689/p/17320614.html

相关文章

赞助商

阅读排行