ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Typedefs | Functions
ccadical.h File Reference
#include "global.h"
#include <stdint.h>
#include <stdio.h>
Include dependency graph for ccadical.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define ccadical_reset   ccadical_release
 
#define ccadical_sat   ccadical_solve
 
#define ccadical_deref   ccadical_val
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct CCaDiCaL CCaDiCaL
 

Functions

const char * ccadical_signature (void)
 
CCaDiCaL * ccadical_init (void)
 
void ccadical_release (CCaDiCaL *)
 
void ccadical_add (CCaDiCaL *, int lit)
 
void ccadical_assume (CCaDiCaL *, int lit)
 
int ccadical_solve (CCaDiCaL *)
 
int ccadical_val (CCaDiCaL *, int lit)
 
int ccadical_failed (CCaDiCaL *, int lit)
 
void ccadical_set_terminate (CCaDiCaL *, void *state, int(*terminate)(void *state))
 
void ccadical_set_learn (CCaDiCaL *, void *state, int max_length, void(*learn)(void *state, int *clause))
 
void ccadical_constrain (CCaDiCaL *, int lit)
 
int ccadical_constraint_failed (CCaDiCaL *)
 
void ccadical_set_option (CCaDiCaL *, const char *name, int val)
 
void ccadical_limit (CCaDiCaL *, const char *name, int limit)
 
int ccadical_get_option (CCaDiCaL *, const char *name)
 
void ccadical_print_statistics (CCaDiCaL *)
 
int64_t ccadical_active (CCaDiCaL *)
 
int64_t ccadical_irredundant (CCaDiCaL *)
 
int ccadical_fixed (CCaDiCaL *, int lit)
 
int ccadical_trace_proof (CCaDiCaL *, FILE *, const char *)
 
void ccadical_close_proof (CCaDiCaL *)
 
void ccadical_conclude (CCaDiCaL *)
 
void ccadical_terminate (CCaDiCaL *)
 
void ccadical_freeze (CCaDiCaL *, int lit)
 
int ccadical_frozen (CCaDiCaL *, int lit)
 
void ccadical_melt (CCaDiCaL *, int lit)
 
int ccadical_simplify (CCaDiCaL *)
 
int ccadical_vars (CCaDiCaL *)
 
int ccadical_reserve_difference (CCaDiCaL *, int number_of_vars)
 
void ccadical_reserve (CCaDiCaL *, int min_max_var)
 
int ccadical_is_inconsistent (CCaDiCaL *)
 

Macro Definition Documentation

◆ ccadical_deref

#define ccadical_deref   ccadical_val

Definition at line 68 of file ccadical.h.

◆ ccadical_reset

#define ccadical_reset   ccadical_release

Definition at line 66 of file ccadical.h.

◆ ccadical_sat

#define ccadical_sat   ccadical_solve

Definition at line 67 of file ccadical.h.

Typedef Documentation

◆ CCaDiCaL

typedef typedefABC_NAMESPACE_HEADER_START struct CCaDiCaL CCaDiCaL

Definition at line 15 of file ccadical.h.

Function Documentation

◆ ccadical_active()

int64_t ccadical_active ( CCaDiCaL * wrapper)

Definition at line 136 of file cadical_ccadical.cpp.

136 {
137 return ((Wrapper *) wrapper)->solver->active ();
138}

◆ ccadical_add()

void ccadical_add ( CCaDiCaL * wrapper,
int lit )

Definition at line 104 of file cadical_ccadical.cpp.

104 {
105 ((Wrapper *) wrapper)->solver->add (lit);
106}
lit
int lit
Definition satVec.h:130
Here is the caller graph for this function:

◆ ccadical_assume()

void ccadical_assume ( CCaDiCaL * wrapper,
int lit )

Definition at line 108 of file cadical_ccadical.cpp.

108 {
109 ((Wrapper *) wrapper)->solver->assume (lit);
110}
Here is the caller graph for this function:

◆ ccadical_close_proof()

void ccadical_close_proof ( CCaDiCaL * ptr)

Definition at line 187 of file cadical_ccadical.cpp.

187 {
188 ((Wrapper *) ptr)->solver->close_proof_trace ();
189}

◆ ccadical_conclude()

void ccadical_conclude ( CCaDiCaL * ptr)

Definition at line 191 of file cadical_ccadical.cpp.

191 {
192 ((Wrapper *) ptr)->solver->conclude ();
193}

◆ ccadical_constrain()

void ccadical_constrain ( CCaDiCaL * wrapper,
int lit )

Definition at line 84 of file cadical_ccadical.cpp.

84 {
85 ((Wrapper *) wrapper)->solver->constrain (lit);
86}

◆ ccadical_constraint_failed()

int ccadical_constraint_failed ( CCaDiCaL * wrapper)

Definition at line 88 of file cadical_ccadical.cpp.

88 {
89 return ((Wrapper *) wrapper)->solver->constraint_failed ();
90}

◆ ccadical_failed()

int ccadical_failed ( CCaDiCaL * wrapper,
int lit )

Definition at line 124 of file cadical_ccadical.cpp.

124 {
125 return ((Wrapper *) wrapper)->solver->failed (lit);
126}
Here is the caller graph for this function:

◆ ccadical_fixed()

int ccadical_fixed ( CCaDiCaL * wrapper,
int lit )

Definition at line 144 of file cadical_ccadical.cpp.

144 {
145 return ((Wrapper *) wrapper)->solver->fixed (lit);
146}

◆ ccadical_freeze()

void ccadical_freeze ( CCaDiCaL * ptr,
int lit )

Definition at line 171 of file cadical_ccadical.cpp.

171 {
172 ((Wrapper *) ptr)->solver->freeze (lit);
173}

◆ ccadical_frozen()

int ccadical_frozen ( CCaDiCaL * ptr,
int lit )

Definition at line 179 of file cadical_ccadical.cpp.

179 {
180 return ((Wrapper *) ptr)->solver->frozen (lit);
181}

◆ ccadical_get_option()

int ccadical_get_option ( CCaDiCaL * wrapper,
const char * name )

Definition at line 100 of file cadical_ccadical.cpp.

100 {
101 return ((Wrapper *) wrapper)->solver->get (name);
102}
name
char * name
Definition main.h:24

◆ ccadical_init()

CCaDiCaL * ccadical_init ( void )

Definition at line 80 of file cadical_ccadical.cpp.

80{ return (CCaDiCaL *) new Wrapper (); }
CCaDiCaL
typedefABC_NAMESPACE_HEADER_START struct CCaDiCaL CCaDiCaL
Definition ccadical.h:15
Here is the caller graph for this function:

◆ ccadical_irredundant()

int64_t ccadical_irredundant ( CCaDiCaL * wrapper)

Definition at line 140 of file cadical_ccadical.cpp.

140 {
141 return ((Wrapper *) wrapper)->solver->irredundant ();
142}

◆ ccadical_is_inconsistent()

int ccadical_is_inconsistent ( CCaDiCaL * ptr)

Definition at line 207 of file cadical_ccadical.cpp.

207 {
208 return ((Wrapper *) ptr)->solver->inconsistent ();
209}
Here is the caller graph for this function:

◆ ccadical_limit()

void ccadical_limit ( CCaDiCaL * wrapper,
const char * name,
int limit )

Definition at line 96 of file cadical_ccadical.cpp.

96 {
97 ((Wrapper *) wrapper)->solver->limit (name, val);
98}
Here is the caller graph for this function:

◆ ccadical_melt()

void ccadical_melt ( CCaDiCaL * ptr,
int lit )

Definition at line 175 of file cadical_ccadical.cpp.

175 {
176 ((Wrapper *) ptr)->solver->melt (lit);
177}

◆ ccadical_print_statistics()

void ccadical_print_statistics ( CCaDiCaL * wrapper)

Definition at line 128 of file cadical_ccadical.cpp.

128 {
129 ((Wrapper *) wrapper)->solver->statistics ();
130}

◆ ccadical_release()

void ccadical_release ( CCaDiCaL * wrapper)

Definition at line 82 of file cadical_ccadical.cpp.

82{ delete (Wrapper *) wrapper; }
Here is the caller graph for this function:

◆ ccadical_reserve()

void ccadical_reserve ( CCaDiCaL * ptr,
int min_max_var )

Definition at line 203 of file cadical_ccadical.cpp.

203 {
204 ((Wrapper *) ptr)->solver->reserve(min_max_var);
205}
Here is the caller graph for this function:

◆ ccadical_reserve_difference()

int ccadical_reserve_difference ( CCaDiCaL * ptr,
int number_of_vars )

Definition at line 199 of file cadical_ccadical.cpp.

199 {
200 return ((Wrapper *) ptr)->solver->reserve_difference (number_of_vars);
201}

◆ ccadical_set_learn()

void ccadical_set_learn ( CCaDiCaL * ptr,
void * state,
int max_length,
void(* learn )(void *state, int *clause) )

Definition at line 159 of file cadical_ccadical.cpp.

160 {
161 Wrapper *wrapper = (Wrapper *) ptr;
162 wrapper->learner.state = state;
163 wrapper->learner.max_length = max_length;
164 wrapper->learner.function = learn;
165 if (learn)
166 wrapper->solver->connect_learner (wrapper);
167 else
168 wrapper->solver->disconnect_learner ();
169}
CaDiCaL::Solver::connect_learner
void connect_learner(Learner *learner)
Definition cadical_solver.cpp:936
CaDiCaL::Wrapper::function
int(* function)(void *)
Definition cadical_ccadical.cpp:17
CaDiCaL::Wrapper::learner
struct CaDiCaL::Wrapper::@141235032232154027043210372131361323260375365300 learner
Here is the call graph for this function:
Here is the caller graph for this function:

◆ ccadical_set_option()

void ccadical_set_option ( CCaDiCaL * wrapper,
const char * name,
int val )

Definition at line 92 of file cadical_ccadical.cpp.

92 {
93 ((Wrapper *) wrapper)->solver->set (name, val);
94}

◆ ccadical_set_terminate()

void ccadical_set_terminate ( CCaDiCaL * ptr,
void * state,
int(* terminate )(void *state) )

Definition at line 148 of file cadical_ccadical.cpp.

149 {
150 Wrapper *wrapper = (Wrapper *) ptr;
151 wrapper->terminator.state = state;
152 wrapper->terminator.function = terminate;
153 if (terminate)
154 wrapper->solver->connect_terminator (wrapper);
155 else
156 wrapper->solver->disconnect_terminator ();
157}
CaDiCaL::Solver::connect_terminator
void connect_terminator(Terminator *terminator)
Definition cadical_solver.cpp:907
CaDiCaL::Wrapper::terminator
struct CaDiCaL::Wrapper::@153037360162222217302235253026335132324125226210 terminator
Here is the call graph for this function:
Here is the caller graph for this function:

◆ ccadical_signature()

const char * ccadical_signature ( void )

Definition at line 78 of file cadical_ccadical.cpp.

78{ return Solver::signature (); }
CaDiCaL::Solver::signature
static const char * signature()
Definition cadical_solver.cpp:1333
Here is the call graph for this function:
Here is the caller graph for this function:

◆ ccadical_simplify()

int ccadical_simplify ( CCaDiCaL * wrapper)

Definition at line 116 of file cadical_ccadical.cpp.

116 {
117 return ((Wrapper *) wrapper)->solver->simplify ();
118}

◆ ccadical_solve()

int ccadical_solve ( CCaDiCaL * wrapper)

Definition at line 112 of file cadical_ccadical.cpp.

112 {
113 return ((Wrapper *) wrapper)->solver->solve ();
114}
Here is the caller graph for this function:

◆ ccadical_terminate()

void ccadical_terminate ( CCaDiCaL * wrapper)

Definition at line 132 of file cadical_ccadical.cpp.

132 {
133 ((Wrapper *) wrapper)->solver->terminate ();
134}

◆ ccadical_trace_proof()

int ccadical_trace_proof ( CCaDiCaL * ptr,
FILE * file,
const char * path )

Definition at line 183 of file cadical_ccadical.cpp.

183 {
184 return ((Wrapper *) ptr)->solver->trace_proof (file, path);
185}
file
Definition file.h:23

◆ ccadical_val()

int ccadical_val ( CCaDiCaL * wrapper,
int lit )

Definition at line 120 of file cadical_ccadical.cpp.

120 {
121 return ((Wrapper *) wrapper)->solver->val (lit);
122}
Here is the caller graph for this function:

◆ ccadical_vars()

int ccadical_vars ( CCaDiCaL * ptr)

Definition at line 195 of file cadical_ccadical.cpp.

195 {
196 return ((Wrapper *) ptr)->solver->vars ();
197}