ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
propsearch.c File Reference
#include "propsearch.h"
#include "fastassign.h"
#include "print.h"
#include "trail.h"
#include "proplit.h"
Include dependency graph for propsearch.c:

Go to the source code of this file.

Macros

#define PROPAGATE_LITERAL   search_propagate_literal
 
#define PROPAGATION_TYPE   "search"
 

Functions

clausekissat_search_propagate (kissat *solver)
 

Macro Definition Documentation

◆ PROPAGATE_LITERAL

#define PROPAGATE_LITERAL   search_propagate_literal

Definition at line 8 of file propsearch.c.

◆ PROPAGATION_TYPE

#define PROPAGATION_TYPE   "search"

Definition at line 9 of file propsearch.c.

Function Documentation

◆ kissat_search_propagate()

clause * kissat_search_propagate ( kissat * solver)

Definition at line 46 of file propsearch.c.

46 {
47 KISSAT_assert (!solver->probing);
48 KISSAT_assert (solver->watching);
49 KISSAT_assert (!solver->inconsistent);
50
51 START (propagate);
52
53 solver->ticks = 0;
54 const unsigned *saved_propagate = solver->propagate;
55 clause *conflict = search_propagate (solver);
56 update_search_propagation_statistics (solver, saved_propagate);
57 kissat_update_conflicts_and_trail (solver, conflict, true);
58 if (conflict && solver->randec) {
59 if (!--solver->randec)
60 kissat_very_verbose (solver, "last random decision conflict");
61 else if (solver->randec == 1)
63 "one more random decision conflict to go");
64 else
66 "%s more random decision conflicts to go",
67 FORMAT_COUNT (solver->randec));
68 }
69
70 STOP (propagate);
71
72 return conflict;
73}
#define FORMAT_COUNT(WORD)
Definition format.h:33
#define KISSAT_assert(ignore)
Definition global.h:13
#define solver
Definition kitten.c:211
#define kissat_very_verbose(...)
Definition print.h:52
#define STOP(P)
Definition profile.hpp:158
#define START(P)
Definition profile.hpp:150
Here is the caller graph for this function: