1 /**CFile****************************************************************
2
3 FileName [AbcGlucose.h]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
8
9 Synopsis [Interface to Glucose.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - September 6, 2017.]
16
17 Revision [$Id: AbcGlucose.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #ifndef ABC_SAT_GLUCOSE_H_
22 #define ABC_SAT_GLUCOSE_H_
23
24 ////////////////////////////////////////////////////////////////////////
25 /// INCLUDES ///
26 ////////////////////////////////////////////////////////////////////////
27
28 #include "aig/gia/gia.h"
29
30 ////////////////////////////////////////////////////////////////////////
31 /// PARAMETERS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 #define GLUCOSE_UNSAT -1
35 #define GLUCOSE_SAT 1
36 #define GLUCOSE_UNDEC 0
37
38
39 ABC_NAMESPACE_HEADER_START
40
41 ////////////////////////////////////////////////////////////////////////
42 /// BASIC TYPES ///
43 ////////////////////////////////////////////////////////////////////////
44
45 typedef struct Glucose_Pars_ Glucose_Pars;
46 struct Glucose_Pars_ {
47 int pre; // preprocessing
48 int verb; // verbosity
49 int cust; // customizable
50 int nConfls; // conflict limit (0 = no limit)
51 };
52
Glucose_CreatePars(int p,int v,int c,int nConfls)53 static inline Glucose_Pars Glucose_CreatePars(int p, int v, int c, int nConfls)
54 {
55 Glucose_Pars pars;
56 pars.pre = p;
57 pars.verb = v;
58 pars.cust = c;
59 pars.nConfls = nConfls;
60 return pars;
61 }
62
63 typedef void bmcg_sat_solver;
64
65 ////////////////////////////////////////////////////////////////////////
66 /// MACRO DEFINITIONS ///
67 ////////////////////////////////////////////////////////////////////////
68
69 ////////////////////////////////////////////////////////////////////////
70 /// FUNCTION DECLARATIONS ///
71 ////////////////////////////////////////////////////////////////////////
72
73 extern bmcg_sat_solver * bmcg_sat_solver_start();
74 extern void bmcg_sat_solver_stop( bmcg_sat_solver* s );
75 extern void bmcg_sat_solver_reset( bmcg_sat_solver* s );
76 extern int bmcg_sat_solver_addclause( bmcg_sat_solver* s, int * plits, int nlits );
77 extern void bmcg_sat_solver_setcallback( bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) );
78 extern int bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits, int nlits );
79 extern int bmcg_sat_solver_final( bmcg_sat_solver* s, int ** ppArray );
80 extern int bmcg_sat_solver_addvar( bmcg_sat_solver* s );
81 extern void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars );
82 extern int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim );
83 extern int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v );
84 extern void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze );
85 extern int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s);
86 extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
87 extern void bmcg_sat_solver_set_stop( bmcg_sat_solver* s, int * pstop );
88 extern abctime bmcg_sat_solver_set_runtime_limit( bmcg_sat_solver* s, abctime Limit );
89 extern void bmcg_sat_solver_set_conflict_budget( bmcg_sat_solver* s, int Limit );
90 extern int bmcg_sat_solver_varnum( bmcg_sat_solver* s );
91 extern int bmcg_sat_solver_clausenum( bmcg_sat_solver* s );
92 extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
93 extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
94 extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot );
95 extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
96 extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
97 extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
98 extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
99
100 extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
101 extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
102
103 ABC_NAMESPACE_HEADER_END
104
105 #endif
106
107 ////////////////////////////////////////////////////////////////////////
108 /// END OF FILE ///
109 ////////////////////////////////////////////////////////////////////////
110
111