ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
proof.h File Reference
#include <stdbool.h>
#include <stdlib.h>
#include "global.h"
Include dependency graph for proof.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define ADD_BINARY_TO_PROOF(...)
 
#define ADD_TERNARY_TO_PROOF(...)
 
#define ADD_CLAUSE_TO_PROOF(...)
 
#define ADD_LITS_TO_PROOF(...)
 
#define ADD_EMPTY_TO_PROOF(...)
 
#define ADD_STACK_TO_PROOF(...)
 
#define ADD_UNIT_TO_PROOF(...)
 
#define SHRINK_CLAUSE_IN_PROOF(...)
 
#define DELETE_BINARY_FROM_PROOF(...)
 
#define DELETE_TERNARY_FROM_PROOF(...)
 
#define DELETE_CLAUSE_FROM_PROOF(...)
 
#define DELETE_LITS_FROM_PROOF(...)
 
#define DELETE_STACK_FROM_PROOF(...)
 

Macro Definition Documentation

◆ ADD_BINARY_TO_PROOF

#define ADD_BINARY_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 123 of file proof.h.

123#define ADD_BINARY_TO_PROOF(...) \
124 do { \
125 } while (0)

◆ ADD_CLAUSE_TO_PROOF

#define ADD_CLAUSE_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 129 of file proof.h.

129#define ADD_CLAUSE_TO_PROOF(...) \
130 do { \
131 } while (0)

◆ ADD_EMPTY_TO_PROOF

#define ADD_EMPTY_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 135 of file proof.h.

135#define ADD_EMPTY_TO_PROOF(...) \
136 do { \
137 } while (0)

◆ ADD_LITS_TO_PROOF

#define ADD_LITS_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 132 of file proof.h.

132#define ADD_LITS_TO_PROOF(...) \
133 do { \
134 } while (0)

◆ ADD_STACK_TO_PROOF

#define ADD_STACK_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 138 of file proof.h.

138#define ADD_STACK_TO_PROOF(...) \
139 do { \
140 } while (0)

◆ ADD_TERNARY_TO_PROOF

#define ADD_TERNARY_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 126 of file proof.h.

126#define ADD_TERNARY_TO_PROOF(...) \
127 do { \
128 } while (0)

◆ ADD_UNIT_TO_PROOF

#define ADD_UNIT_TO_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 141 of file proof.h.

141#define ADD_UNIT_TO_PROOF(...) \
142 do { \
143 } while (0)

◆ DELETE_BINARY_FROM_PROOF

#define DELETE_BINARY_FROM_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 149 of file proof.h.

149#define DELETE_BINARY_FROM_PROOF(...) \
150 do { \
151 } while (0)

◆ DELETE_CLAUSE_FROM_PROOF

#define DELETE_CLAUSE_FROM_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 155 of file proof.h.

155#define DELETE_CLAUSE_FROM_PROOF(...) \
156 do { \
157 } while (0)

◆ DELETE_LITS_FROM_PROOF

#define DELETE_LITS_FROM_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 158 of file proof.h.

158#define DELETE_LITS_FROM_PROOF(...) \
159 do { \
160 } while (0)

◆ DELETE_STACK_FROM_PROOF

#define DELETE_STACK_FROM_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 161 of file proof.h.

161#define DELETE_STACK_FROM_PROOF(...) \
162 do { \
163 } while (0)

◆ DELETE_TERNARY_FROM_PROOF

#define DELETE_TERNARY_FROM_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 152 of file proof.h.

152#define DELETE_TERNARY_FROM_PROOF(...) \
153 do { \
154 } while (0)

◆ SHRINK_CLAUSE_IN_PROOF

#define SHRINK_CLAUSE_IN_PROOF ( ...)
Value:
do { \
} while (0)

Definition at line 145 of file proof.h.

145#define SHRINK_CLAUSE_IN_PROOF(...) \
146 do { \
147 } while (0)