ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Public Member Functions | List of all members
CaDiCaL::Proof Class Reference

#include <proof.hpp>

Public Member Functions

 Proof (Internal *)
 
 ~Proof ()
 
void connect (Tracer *t)
 
void disconnect (Tracer *t)
 
void add_original_clause (int64_t, bool, const vector< int > &)
 
void add_assumption_clause (int64_t, const vector< int > &, const vector< int64_t > &)
 
void add_assumption_clause (int64_t, int, const vector< int64_t > &)
 
void add_assumption (int)
 
void add_constraint (const vector< int > &)
 
void reset_assumptions ()
 
void add_external_original_clause (int64_t, bool, const vector< int > &, bool restore=false)
 
void delete_external_original_clause (int64_t, bool, const vector< int > &)
 
void add_derived_empty_clause (int64_t, const vector< int64_t > &)
 
void add_derived_unit_clause (int64_t, int unit, const vector< int64_t > &)
 
void add_derived_clause (Clause *c, const vector< int64_t > &)
 
void add_derived_clause (int64_t, bool, const vector< int > &, const vector< int64_t > &)
 
void delete_clause (int64_t, bool, const vector< int > &)
 
void weaken_minus (int64_t, const vector< int > &)
 
void weaken_plus (int64_t, const vector< int > &)
 
void delete_unit_clause (int64_t id, const int lit)
 
void delete_clause (Clause *)
 
void weaken_minus (Clause *)
 
void weaken_plus (Clause *)
 
void strengthen (int64_t)
 
void finalize_unit (int64_t, int)
 
void finalize_external_unit (int64_t, int)
 
void finalize_clause (int64_t, const vector< int > &c)
 
void finalize_clause (Clause *)
 
void report_status (int, int64_t)
 
void begin_proof (int64_t)
 
void conclude_unsat (ConclusionType, const vector< int64_t > &)
 
void conclude_sat (const vector< int > &model)
 
void conclude_unknown (const vector< int > &trace)
 
void solve_query ()
 
void flush_clause (Clause *)
 
void strengthen_clause (Clause *, int, const vector< int64_t > &)
 
void otfs_strengthen_clause (Clause *, const vector< int > &, const vector< int64_t > &)
 
void flush ()
 

Detailed Description

Definition at line 22 of file proof.hpp.

Constructor & Destructor Documentation

◆ Proof()

CaDiCaL::Proof::Proof ( Internal * s)

Definition at line 202 of file cadical_proof.cpp.

202: internal (s) { LOG ("PROOF new"); }
LOG
#define LOG(...)
Definition cadical_kitten.c:368

◆ ~Proof()

CaDiCaL::Proof::~Proof ( )

Definition at line 204 of file cadical_proof.cpp.

204{ LOG ("PROOF delete"); }

Member Function Documentation

◆ add_assumption()

void CaDiCaL::Proof::add_assumption ( int a)

Definition at line 322 of file cadical_proof.cpp.

322 {
323 // a is already external
324 CADICAL_assert (clause.empty ());
325 CADICAL_assert (proof_chain.empty ());
326 clause.push_back (a);
327 add_assumption ();
328}
CADICAL_assert
#define CADICAL_assert(ignore)
Definition global.h:14

◆ add_assumption_clause() [1/2]

void CaDiCaL::Proof::add_assumption_clause ( int64_t id,
const vector< int > & c,
const vector< int64_t > & chain )

Definition at line 309 of file cadical_proof.cpp.

310 {
311 // literals of c are already external
312 CADICAL_assert (clause.empty ());
313 CADICAL_assert (proof_chain.empty ());
314 for (const auto &lit : c)
315 clause.push_back (lit);
316 for (const auto &cid : chain)
317 proof_chain.push_back (cid);
318 clause_id = id;
319 add_assumption_clause ();
320}
lit
int lit
Definition satVec.h:130

◆ add_assumption_clause() [2/2]

void CaDiCaL::Proof::add_assumption_clause ( int64_t id,
int lit,
const vector< int64_t > & chain )

Definition at line 339 of file cadical_proof.cpp.

340 {
341 CADICAL_assert (clause.empty ());
342 CADICAL_assert (proof_chain.empty ());
343 clause.push_back (lit);
344 for (const auto &cid : chain)
345 proof_chain.push_back (cid);
346 clause_id = id;
347 add_assumption_clause ();
348}

◆ add_constraint()

void CaDiCaL::Proof::add_constraint ( const vector< int > & c)

Definition at line 330 of file cadical_proof.cpp.

330 {
331 // literals of c are already external
332 CADICAL_assert (clause.empty ());
333 CADICAL_assert (proof_chain.empty ());
334 for (const auto &lit : c)
335 clause.push_back (lit);
336 add_constraint ();
337}

◆ add_derived_clause() [1/2]

void CaDiCaL::Proof::add_derived_clause ( Clause * c,
const vector< int64_t > & chain )

Definition at line 283 of file cadical_proof.cpp.

283 {
284 LOG (c, "PROOF adding to proof derived");
285 CADICAL_assert (clause.empty ());
286 CADICAL_assert (proof_chain.empty ());
287 add_literals (c);
288 for (const auto &cid : chain)
289 proof_chain.push_back (cid);
290 clause_id = c->id;
291 redundant = c->redundant;
292 add_derived_clause ();
293}

◆ add_derived_clause() [2/2]

void CaDiCaL::Proof::add_derived_clause ( int64_t id,
bool r,
const vector< int > & c,
const vector< int64_t > & chain )

Definition at line 295 of file cadical_proof.cpp.

296 {
297 LOG (c, "PROOF adding derived clause");
298 CADICAL_assert (clause.empty ());
299 CADICAL_assert (proof_chain.empty ());
300 for (const auto &lit : c)
301 add_literal (lit);
302 for (const auto &cid : chain)
303 proof_chain.push_back (cid);
304 clause_id = id;
305 redundant = r;
306 add_derived_clause ();
307}

◆ add_derived_empty_clause()

void CaDiCaL::Proof::add_derived_empty_clause ( int64_t id,
const vector< int64_t > & chain )

Definition at line 256 of file cadical_proof.cpp.

257 {
258 LOG ("PROOF adding empty clause");
259 CADICAL_assert (clause.empty ());
260 CADICAL_assert (proof_chain.empty ());
261 for (const auto &cid : chain)
262 proof_chain.push_back (cid);
263 clause_id = id;
264 redundant = false;
265 add_derived_clause ();
266}

◆ add_derived_unit_clause()

void CaDiCaL::Proof::add_derived_unit_clause ( int64_t id,
int unit,
const vector< int64_t > & chain )

Definition at line 268 of file cadical_proof.cpp.

269 {
270 LOG ("PROOF adding unit clause %d", internal_unit);
271 CADICAL_assert (proof_chain.empty ());
272 CADICAL_assert (clause.empty ());
273 add_literal (internal_unit);
274 for (const auto &cid : chain)
275 proof_chain.push_back (cid);
276 clause_id = id;
277 redundant = false;
278 add_derived_clause ();
279}

◆ add_external_original_clause()

void CaDiCaL::Proof::add_external_original_clause ( int64_t id,
bool r,
const vector< int > & c,
bool restore = false )

Definition at line 233 of file cadical_proof.cpp.

235 {
236 // literals of c are already external
237 CADICAL_assert (clause.empty ());
238 for (auto const &lit : c)
239 clause.push_back (lit);
240 clause_id = id;
241 redundant = r;
242 add_original_clause (restore);
243}

◆ add_original_clause()

void CaDiCaL::Proof::add_original_clause ( int64_t id,
bool r,
const vector< int > & c )

Definition at line 225 of file cadical_proof.cpp.

225 {
226 LOG (c, "PROOF adding original internal clause");
227 add_literals (c);
228 clause_id = id;
229 redundant = r;
230 add_original_clause ();
231}

◆ begin_proof()

void CaDiCaL::Proof::begin_proof ( int64_t id)

Definition at line 625 of file cadical_proof.cpp.

625 {
626 LOG (clause, "PROOF begin proof");
627 for (auto &tracer : tracers) {
628 tracer->begin_proof (id);
629 }
630}

◆ conclude_sat()

void CaDiCaL::Proof::conclude_sat ( const vector< int > & model)

Definition at line 647 of file cadical_proof.cpp.

647 {
648 LOG (clause, "PROOF conclude sat");
649 for (auto &tracer : tracers) {
650 tracer->conclude_sat (model);
651 }
652}

◆ conclude_unknown()

void CaDiCaL::Proof::conclude_unknown ( const vector< int > & trace)

Definition at line 654 of file cadical_proof.cpp.

654 {
655 LOG (clause, "PROOF conclude unknown");
656 for (auto &tracer : tracers) {
657 tracer->conclude_unknown (trail);
658 }
659}

◆ conclude_unsat()

void CaDiCaL::Proof::conclude_unsat ( ConclusionType con,
const vector< int64_t > & conclusion )

Definition at line 639 of file cadical_proof.cpp.

640 {
641 LOG (clause, "PROOF conclude unsat");
642 for (auto &tracer : tracers) {
643 tracer->conclude_unsat (con, conclusion);
644 }
645}

◆ connect()

void CaDiCaL::Proof::connect ( Tracer * t)
inline

Definition at line 56 of file proof.hpp.

56{ tracers.push_back (t); }

◆ delete_clause() [1/2]

void CaDiCaL::Proof::delete_clause ( Clause * c)

Definition at line 350 of file cadical_proof.cpp.

350 {
351 LOG (c, "PROOF deleting from proof");
352 clause.clear (); // Can be non-empty if an allocation fails during adding.
353 add_literals (c);
354 clause_id = c->id;
355 redundant = c->redundant;
356 delete_clause (); // Increments 'statistics.deleted'.
357}

◆ delete_clause() [2/2]

void CaDiCaL::Proof::delete_clause ( int64_t id,
bool r,
const vector< int > & c )

Definition at line 359 of file cadical_proof.cpp.

359 {
360 LOG (c, "PROOF deleting from proof");
361 CADICAL_assert (clause.empty ());
362 add_literals (c);
363 clause_id = id;
364 redundant = r;
365 delete_clause (); // Increments 'statistics.deleted'.
366}

◆ delete_external_original_clause()

void CaDiCaL::Proof::delete_external_original_clause ( int64_t id,
bool r,
const vector< int > & c )

Definition at line 245 of file cadical_proof.cpp.

246 {
247 // literals of c are already external
248 CADICAL_assert (clause.empty ());
249 for (auto const &lit : c)
250 clause.push_back (lit);
251 clause_id = id;
252 redundant = r;
253 delete_clause ();
254}

◆ delete_unit_clause()

void CaDiCaL::Proof::delete_unit_clause ( int64_t id,
const int lit )

Definition at line 394 of file cadical_proof.cpp.

394 {
395 LOG ("PROOF deleting unit from proof %d", lit);
396 CADICAL_assert (clause.empty ());
397 add_literal (lit);
398 clause_id = id;
399 redundant = false;
400 delete_clause ();
401}

◆ disconnect()

void CaDiCaL::Proof::disconnect ( Tracer * t)

Definition at line 119 of file cadical_proof.cpp.

119 {
120 tracers.erase (std::remove (tracers.begin (), tracers.end (), t),
121 tracers.end ());
122}

◆ finalize_clause() [1/2]

void CaDiCaL::Proof::finalize_clause ( Clause * c)

Definition at line 403 of file cadical_proof.cpp.

403 {
404 LOG (c, "PROOF finalizing clause");
405 CADICAL_assert (clause.empty ());
406 add_literals (c);
407 clause_id = c->id;
408 finalize_clause ();
409}

◆ finalize_clause() [2/2]

void CaDiCaL::Proof::finalize_clause ( int64_t id,
const vector< int > & c )

Definition at line 411 of file cadical_proof.cpp.

411 {
412 LOG (c, "PROOF finalizing clause");
413 CADICAL_assert (clause.empty ());
414 for (const auto &lit : c)
415 add_literal (lit);
416 clause_id = id;
417 finalize_clause ();
418}

◆ finalize_external_unit()

void CaDiCaL::Proof::finalize_external_unit ( int64_t id,
int lit )

Definition at line 428 of file cadical_proof.cpp.

428 {
429 LOG ("PROOF finalizing clause %d", lit);
430 CADICAL_assert (clause.empty ());
431 clause.push_back (lit);
432 clause_id = id;
433 finalize_clause ();
434}

◆ finalize_unit()

void CaDiCaL::Proof::finalize_unit ( int64_t id,
int lit )

Definition at line 420 of file cadical_proof.cpp.

420 {
421 LOG ("PROOF finalizing clause %d", lit);
422 CADICAL_assert (clause.empty ());
423 add_literal (lit);
424 clause_id = id;
425 finalize_clause ();
426}

◆ flush()

void CaDiCaL::Proof::flush ( )

◆ flush_clause()

void CaDiCaL::Proof::flush_clause ( Clause * c)

Definition at line 442 of file cadical_proof.cpp.

442 {
443 LOG (c, "PROOF flushing falsified literals in");
444 CADICAL_assert (clause.empty ());
445 const bool antecedents = (internal->lrat || internal->frat);
446 for (int i = 0; i < c->size; i++) {
447 int internal_lit = c->literals[i];
448 if (internal->fixed (internal_lit) < 0) {
449 if (antecedents) {
450 int64_t id = internal->unit_id (-internal_lit);
451 proof_chain.push_back (id);
452 }
453 continue;
454 }
455 add_literal (internal_lit);
456 }
457 proof_chain.push_back (c->id);
458 redundant = c->redundant;
459 int64_t id = ++internal->clause_id;
460 clause_id = id;
461 add_derived_clause ();
462 delete_clause (c);
463 c->id = id;
464}

◆ otfs_strengthen_clause()

void CaDiCaL::Proof::otfs_strengthen_clause ( Clause * ,
const vector< int > & ,
const vector< int64_t > &  )

Definition at line 492 of file cadical_proof.cpp.

493 {
494 LOG (c, "PROOF otfs strengthen");
495 CADICAL_assert (clause.empty ());
496 for (int i = 0; i < c->size; i++) {
497 int internal_lit = c->literals[i];
498 add_literal (internal_lit);
499 }
500 int64_t id = ++internal->clause_id;
501 clause_id = id;
502 redundant = c->redundant;
503 for (const auto &cid : chain)
504 proof_chain.push_back (cid);
505 add_derived_clause ();
506 delete_clause (c->id, c->redundant, old);
507 c->id = id;
508}

◆ report_status()

void CaDiCaL::Proof::report_status ( int status,
int64_t id )

Definition at line 618 of file cadical_proof.cpp.

618 {
619 LOG ("PROOF reporting status %d", status);
620 for (auto &tracer : tracers) {
621 tracer->report_status (status, id);
622 }
623}

◆ reset_assumptions()

void CaDiCaL::Proof::reset_assumptions ( )

Definition at line 611 of file cadical_proof.cpp.

611 {
612 LOG ("PROOF reset assumptions");
613 for (auto &tracer : tracers) {
614 tracer->reset_assumptions ();
615 }
616}

◆ solve_query()

void CaDiCaL::Proof::solve_query ( )

Definition at line 632 of file cadical_proof.cpp.

632 {
633 LOG (clause, "PROOF solve query");
634 for (auto &tracer : tracers) {
635 tracer->solve_query ();
636 }
637}

◆ strengthen()

void CaDiCaL::Proof::strengthen ( int64_t id)

Definition at line 510 of file cadical_proof.cpp.

510 {
511 clause_id = id;
512 strengthen ();
513}

◆ strengthen_clause()

void CaDiCaL::Proof::strengthen_clause ( Clause * c,
int remove,
const vector< int64_t > & chain )

Definition at line 472 of file cadical_proof.cpp.

473 {
474 LOG (c, "PROOF strengthen by removing %d in", remove);
475 CADICAL_assert (clause.empty ());
476 for (int i = 0; i < c->size; i++) {
477 int internal_lit = c->literals[i];
478 if (internal_lit == remove)
479 continue;
480 add_literal (internal_lit);
481 }
482 int64_t id = ++internal->clause_id;
483 clause_id = id;
484 redundant = c->redundant;
485 for (const auto &cid : chain)
486 proof_chain.push_back (cid);
487 add_derived_clause ();
488 delete_clause (c);
489 c->id = id;
490}

◆ weaken_minus() [1/2]

void CaDiCaL::Proof::weaken_minus ( Clause * c)

Definition at line 368 of file cadical_proof.cpp.

368 {
369 LOG (c, "PROOF weaken minus of");
370 CADICAL_assert (clause.empty ());
371 add_literals (c);
372 clause_id = c->id;
373 weaken_minus ();
374}

◆ weaken_minus() [2/2]

void CaDiCaL::Proof::weaken_minus ( int64_t id,
const vector< int > & c )

Definition at line 376 of file cadical_proof.cpp.

376 {
377 LOG (c, "PROOF deleting from proof");
378 CADICAL_assert (clause.empty ());
379 add_literals (c);
380 clause_id = id;
381 weaken_minus ();
382}

◆ weaken_plus() [1/2]

void CaDiCaL::Proof::weaken_plus ( Clause * c)

Definition at line 384 of file cadical_proof.cpp.

384 {
385 weaken_minus (c);
386 delete_clause (c); // Increments 'statistics.deleted'.
387}

◆ weaken_plus() [2/2]

void CaDiCaL::Proof::weaken_plus ( int64_t id,
const vector< int > & c )

Definition at line 389 of file cadical_proof.cpp.

389 {
390 weaken_minus (id, c);
391 delete_clause (id, false, c); // Increments 'statistics.deleted'.
392}
The documentation for this class was generated from the following files: