数据成员

Solver solver；

成员函数

init();

solve();

数据成员

Internal * internal;  // Hidden internal solver.
External * external; // Hidden API to internal solver mapping.

成员函数

solve ()

call_external_solve_and_check_results (.)

数据成员

Internal * internal;

成员函数

solve (.)

调用

init();

solver->solve();

solve()内部调用

call_external_solve_and_check_results (.)内部调用

external->solve (.)

solve(.)内部调用

internal->solve (.);

可以

调用

类内

其它

成员

 1 if (verbose () || proof_specified) solver->section ("proof tracing");
 2   if (proof_specified) {
 3     if (!proof_path) {
 4       const bool force_binary = (isatty (1) && get ("binary"));
 5       if (force_binary) set ("--no-binary");
 6       solver->message ("writing %s proof trace to %s'<stdout>'%s",
 7         (get ("binary") ? "binary" : "non-binary"),
 8         tout.green_code (), tout.normal_code ());
 9       if (force_binary)
10         solver->message (
11           "connected to terminal thus non-binary proof forced");
12       solver->trace_proof (stdout, "<stdout>");
13     } else if (!solver->trace_proof (proof_path))
14       APPERR ("can not open and write DRAT proof to '%s'", proof_path);
15     else
16       solver->message (
17         "writing %s proof trace to %s'%s'%s",
18         (get ("binary") ? "binary" : "non-binary"),
19         tout.green_code (), proof_path, tout.normal_code ());
20   } else solver->verbose (1, "will not generate nor write DRAT proof");

1 if (proof_specified) {
2     solver->section ("closing proof");
3     solver->flush_proof_trace ();
4     solver->close_proof_trace ();
5   }

 1 // Enables clausal proof tracing in DRAT format and returns 'true' if
 2   // successfully opened for writing.  Writing proofs has to be enabled
 3   // before calling 'solve', 'add' and 'dimacs', that is in state
 4   // 'CONFIGURING'.  Otherwise only partial proofs would be written.
 5   //
 6   //   require (CONFIGURING)
 7   //   ensure (CONFIGURING)
 8   //
 9   bool trace_proof (FILE * file, const char * name); // Write DRAT proof.
10   bool trace_proof (const char * path);              // Open & write proof.
11 
12   // Flush proof trace file.
13   //
14   //   require (VALID)
15   //   ensure (VALID)
16   //
17   void flush_proof_trace ();
18 
19   // Close proof trace early.
20   //
21   //   require (VALID)
22   //   ensure (VALID)
23   //
24   void close_proof_trace ();

 1 bool Solver::trace_proof (FILE * external_file, const char * name) {
 2   LOG_API_CALL_BEGIN ("trace_proof", name);
 3   REQUIRE_VALID_STATE ();
 4   REQUIRE (state () == CONFIGURING,
 5     "can only start proof tracing to '%s' right after initialization",
 6     name);
 7   REQUIRE (!internal->tracer, "already tracing proof");
 8   File * internal_file = File::write (internal, external_file, name);
 9   assert (internal_file);
10   internal->trace (internal_file);
11   LOG_API_CALL_RETURNS ("trace_proof", name, true);
12   return true;
13 }
14 
15 bool Solver::trace_proof (const char * path) {
16   LOG_API_CALL_BEGIN ("trace_proof", path);
17   REQUIRE_VALID_STATE ();
18   REQUIRE (state () == CONFIGURING,
19     "can only start proof tracing to '%s' right after initialization",
20     path);
21   REQUIRE (!internal->tracer, "already tracing proof");
22   File * internal_file = File::write (internal, path);
23   bool res = (internal_file != 0);
24   internal->trace (internal_file);
25   LOG_API_CALL_RETURNS ("trace_proof", path, res);
26   return res;
27 }
28 
29 void Solver::flush_proof_trace () {
30   LOG_API_CALL_BEGIN ("flush_proof_trace");
31   REQUIRE_VALID_STATE ();
32   REQUIRE (internal->tracer, "proof is not traced");
33   REQUIRE (!internal->tracer->closed (), "proof trace already closed");
34   internal->flush_trace ();
35   LOG_API_CALL_END ("flush_proof_trace");
36 }
37 
38 void Solver::close_proof_trace () {
39   LOG_API_CALL_BEGIN ("close_proof_trace");
40   REQUIRE_VALID_STATE ();
41   REQUIRE (internal->tracer, "proof is not traced");
42   REQUIRE (!internal->tracer->closed (), "proof trace already closed");
43   internal->close_trace ();
44   LOG_API_CALL_END ("close_proof_trace");
45 }

1   // Enable and disable proof logging and checking.
2   //
3   void new_proof_on_demand ();
4   void close_trace ();          // Stop proof tracing.
5   void flush_trace ();          // Flush proof trace file.
6   void trace (File *);          // Start write proof file.
7   void check ();                // Enable online proof checking.

 1 // Enable proof logging and checking by allocating a 'Proof' object.
 2 
 3 void Internal::new_proof_on_demand () {
 4   if (!proof) {
 5     proof = new Proof (this);
 6     LOG ("connecting proof to internal solver");
 7   }
 8 }
 9 
10 // Enable proof tracing.
11 
12 void Internal::trace (File * file) {
13   assert (!tracer);
14   new_proof_on_demand ();
15   tracer = new Tracer (this, file, opts.binary);
16   LOG ("PROOF connecting proof tracer");
17   proof->connect (tracer);
18 }
19 
20 // Enable proof checking.
21 
22 void Internal::check () {
23   assert (!checker);
24   new_proof_on_demand ();
25   checker = new Checker (this);
26   LOG ("PROOF connecting proof checker");
27   proof->connect (checker);
28 }
29 
30 // We want to close a proof trace and stop checking as soon we are done.
31 
32 void Internal::close_trace () {
33   assert (tracer);
34   tracer->close ();
35 }
36 
37 // We can flush a proof trace file before actually closing it.
38 
39 void Internal::flush_trace () {
40   assert (tracer);
41   tracer->flush ();
42 }