| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/ |
| H A D | satoko.h | 35 typedef struct solver_t_ satoko_t; typedef
90 extern satoko_t *satoko_create(void);
91 extern void satoko_destroy(satoko_t *);
92 extern void satoko_reset(satoko_t *);
102 extern int satoko_simplify(satoko_t *);
103 extern int satoko_solve(satoko_t *);
110 extern void satoko_rollback(satoko_t *);
111 extern void satoko_bookmark(satoko_t *);
135 extern int satoko_varnum(satoko_t *);
136 extern int satoko_clausenum(satoko_t *);
[all …]
|
| H A D | solver_api.c | 433 satoko_stats_t * satoko_stats(satoko_t *s) in satoko_stats()
438 satoko_opts_t * satoko_options(satoko_t *s) in satoko_options()
443 void satoko_bookmark(satoko_t *s) in satoko_bookmark()
456 void satoko_unbookmark(satoko_t *s) in satoko_unbookmark()
469 void satoko_reset(satoko_t *s) in satoko_reset()
508 void satoko_rollback(satoko_t *s) in satoko_rollback()
625 int satoko_varnum(satoko_t *s) in satoko_varnum()
630 int satoko_clausenum(satoko_t *s) in satoko_clausenum()
635 int satoko_learntnum(satoko_t *s) in satoko_learntnum()
640 int satoko_conflictnum(satoko_t *s) in satoko_conflictnum()
[all …]
|
| H A D | cnf_reader.c | 108 int satoko_parse_dimacs(char *fname, satoko_t **solver) in satoko_parse_dimacs()
110 satoko_t *p = NULL; in satoko_parse_dimacs()
|
| H A D | solver.h | 219 static inline int solver_has_marks(satoko_t *s) in solver_has_marks()
224 static inline int solver_stop(satoko_t *s) in solver_stop()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaSatoko.c | 99 satoko_t * Gia_ManSatokoFromDimacs( char * pFileName, satoko_opts_t * opts ) in Gia_ManSatokoFromDimacs()
101 satoko_t * pSat = satoko_create(); in Gia_ManSatokoFromDimacs()
152 satoko_t * pSat = Gia_ManSatokoFromDimacs( pFileName, opts ); in Gia_ManSatokoDimacs()
172 satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts ) in Gia_ManSatokoInit()
174 satoko_t * pSat = satoko_create(); in Gia_ManSatokoInit()
188 satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts ) in Gia_ManSatokoCreate()
191 satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); in Gia_ManSatokoCreate()
202 satoko_t * pSat; in Gia_ManSatokoCallOne()
225 satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); in Gia_ManSatokoCall()
|
| H A D | giaSupp.c | 345 satoko_t * pSat; // SAT solver
422 void Gia_Min2AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat ) in Gia_Min2AddClausesMux()
530 void Gia_Min2AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat… in Gia_Min2AddClausesSuper()
605 void Gia_Min2ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * p… in Gia_Min2ObjAddToFrontier()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcMesh.c | 53 static inline int Bmc_MeshVarValue( satoko_t * p, int v ) in Bmc_MeshVarValue()
71 int Bmc_MeshAddOneHotness( satoko_t * pSat, int iFirst, int iLast ) in Bmc_MeshAddOneHotness()
109 satoko_t * pSat = satoko_create(); in Bmc_MeshTest()
|
| H A D | bmcBmc.c | 186 int * Sat2_SolverGetModel( satoko_t * p, int * pVars, int nVars ) in Sat2_SolverGetModel()
211 satoko_t * pSat2 = NULL; in Saig_ManBmcSimple()
|
| H A D | bmcBmc2.c | 53 satoko_t * pSat2; // SAT solver
|
| H A D | bmcBmcS.c | 37 #define bmc_sat_solver satoko_t
|
| H A D | bmcBmc3.c | 65 satoko_t * pSat2; // SAT solver
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/cec/ |
| H A D | cecSat.c | 54 satoko_t * pSat; // SAT solver
119 void Cec2_AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat ) in Cec2_AddClausesMux()
227 void Cec2_AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat ) in Cec2_AddClausesSuper()
302 void Cec2_ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat… in Cec2_ObjAddToFrontier()
320 …etCnfVar( Gia_Man_t * pGia, int iObj, Vec_Ptr_t * vFrontier, Vec_Ptr_t * vFanins, satoko_t * pSat ) in Gia_ObjGetCnfVar()
756 int Cec2_ManVerify_rec( Gia_Man_t * p, int iObj, satoko_t * pSat ) in Cec2_ManVerify_rec()
771 void Cec2_ManVerify( Gia_Man_t * p, int iObj0, int iObj1, int fPhase, satoko_t * pSat ) in Cec2_ManVerify()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/ |
| H A D | pdrInt.h | 44 #define sat_solver satoko_t
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/acb/ |
| H A D | acbFunc.c | 1325 static inline int satoko_add_xor( satoko_t * pSat, int iVarA, int iVarB, int iVarC, int fCompl ) in satoko_add_xor()
1362 satoko_t * pSat = satoko_create(); in Acb_DerivePatchSupportS()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abc.c | 25456 satoko_t * p; in Abc_CommandSatoko()
|