From b3d3f7dd3aeb5c7648caf9c424f6dc341ad27ac0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 12 Nov 2020 23:57:46 -0800 Subject: Duplicating Glucose package. --- src/sat/glucose2/AbcGlucose2.h | 111 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 src/sat/glucose2/AbcGlucose2.h (limited to 'src/sat/glucose2/AbcGlucose2.h') diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h new file mode 100644 index 00000000..8fc774cd --- /dev/null +++ b/src/sat/glucose2/AbcGlucose2.h @@ -0,0 +1,111 @@ +/**CFile**************************************************************** + + FileName [AbcGlucose.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.] + + Synopsis [Interface to Glucose.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 6, 2017.] + + Revision [$Id: AbcGlucose.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC_SAT_GLUCOSE_H_ +#define ABC_SAT_GLUCOSE_H_ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig/gia/gia.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define GLUCOSE_UNSAT -1 +#define GLUCOSE_SAT 1 +#define GLUCOSE_UNDEC 0 + + +ABC_NAMESPACE_HEADER_START + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Glucose2_Pars_ Glucose2_Pars; +struct Glucose2_Pars_ { + int pre; // preprocessing + int verb; // verbosity + int cust; // customizable + int nConfls; // conflict limit (0 = no limit) +}; + +static inline Glucose2_Pars Glucose_CreatePars(int p, int v, int c, int nConfls) +{ + Glucose2_Pars pars; + pars.pre = p; + pars.verb = v; + pars.cust = c; + pars.nConfls = nConfls; + return pars; +} + +typedef void bmcg2_sat_solver; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern bmcg2_sat_solver * bmcg2_sat_solver_start(); +extern void bmcg2_sat_solver_stop( bmcg2_sat_solver* s ); +extern void bmcg2_sat_solver_reset( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_addclause( bmcg2_sat_solver* s, int * plits, int nlits ); +extern void bmcg2_sat_solver_setcallback( bmcg2_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*) ); +extern int bmcg2_sat_solver_solve( bmcg2_sat_solver* s, int * plits, int nlits ); +extern int bmcg2_sat_solver_final( bmcg2_sat_solver* s, int ** ppArray ); +extern int bmcg2_sat_solver_addvar( bmcg2_sat_solver* s ); +extern void bmcg2_sat_solver_set_nvars( bmcg2_sat_solver* s, int nvars ); +extern int bmcg2_sat_solver_eliminate( bmcg2_sat_solver* s, int turn_off_elim ); +extern int bmcg2_sat_solver_var_is_elim( bmcg2_sat_solver* s, int v ); +extern void bmcg2_sat_solver_var_set_frozen( bmcg2_sat_solver* s, int v, int freeze ); +extern int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s); +extern int * bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int ); +extern void bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop ); +extern abctime bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit ); +extern void bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit ); +extern int bmcg2_sat_solver_varnum( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_clausenum( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_learntnum( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s ); +extern int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot ); +extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); +extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); +extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); +extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); + +extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars ); +extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars ); + +ABC_NAMESPACE_HEADER_END + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + -- cgit v1.2.3 From 22388f901a88dddfe629dd3c1406b06fafa9675d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Nov 2020 10:29:31 -0800 Subject: Adding and integrating new SAT solver APIs. --- src/sat/glucose2/AbcGlucose2.h | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/sat/glucose2/AbcGlucose2.h') diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 8fc774cd..28304e52 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -97,6 +97,11 @@ extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVa extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); +extern int bmcg2_sat_solver_jftr( bmcg2_sat_solver * s ); +extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jftr ); +extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 ); +extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s ); +extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var ); extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars ); extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars ); -- cgit v1.2.3 From dd07ec57be48b79d07b39d4e5607f4178a32dc1b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Nov 2020 19:02:41 -0800 Subject: Extending sweeper to handle XORs. --- src/sat/glucose2/AbcGlucose2.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/sat/glucose2/AbcGlucose2.h') diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 28304e52..7c060ccc 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -94,6 +94,7 @@ extern int bmcg2_sat_solver_learntnum( bmcg2_sat_solver* s ); extern int bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s ); extern int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); +extern int bmcg2_sat_solver_add_xor( bmcg2_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl ); extern int bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); extern Vec_Str_t * bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); -- cgit v1.2.3 From 5f8a8a596a009046896acd8af6397acecc1e36a9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Apr 2021 14:46:05 -0700 Subject: Upgrade to the circuit-based solver. --- src/sat/glucose2/AbcGlucose2.h | 1 + 1 file changed, 1 insertion(+) (limited to 'src/sat/glucose2/AbcGlucose2.h') diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h index 7c060ccc..9299d290 100644 --- a/src/sat/glucose2/AbcGlucose2.h +++ b/src/sat/glucose2/AbcGlucose2.h @@ -103,6 +103,7 @@ extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jf extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 ); extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s ); extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var ); +extern void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ); extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars ); extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars ); -- cgit v1.2.3