summaryrefslogtreecommitdiffstats
path: root/src/proof/cec
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/cec')
-rw-r--r--src/proof/cec/cec.h1
-rw-r--r--src/proof/cec/cecSatG2.c102
2 files changed, 73 insertions, 30 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index c5c5dbb7..3414842c 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -95,6 +95,7 @@ struct Cec_ParSmf_t_
typedef struct Cec_ParFra_t_ Cec_ParFra_t;
struct Cec_ParFra_t_
{
+ int jType; // solver type
int nWords; // the number of simulation words
int nRounds; // the number of simulation rounds
int nItersMax; // the maximum number of iterations of SAT sweeping
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 3b942f4f..0b3bf58b 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -28,33 +28,45 @@
#include "sat/glucose2/AbcGlucose2.h"
-#define sat_solver bmcg2_sat_solver
-#define sat_solver_start bmcg2_sat_solver_start
-#define sat_solver_stop bmcg2_sat_solver_stop
-#define sat_solver_addclause bmcg2_sat_solver_addclause
-#define sat_solver_addvar bmcg2_sat_solver_addvar
-#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
-#define sat_solver_reset bmcg2_sat_solver_reset
-#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
-#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
-#define sat_solver_solve bmcg2_sat_solver_solve
-#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver bmcg2_sat_solver
+#define sat_solver_start bmcg2_sat_solver_start
+#define sat_solver_stop bmcg2_sat_solver_stop
+#define sat_solver_addclause bmcg2_sat_solver_addclause
+#define sat_solver_addvar bmcg2_sat_solver_addvar
+#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_reset bmcg2_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg2_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg2_sat_solver_conflictnum
+#define sat_solver_solve bmcg2_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg2_sat_solver_read_cex
+#define sat_solver_jftr bmcg2_sat_solver_jftr
+#define sat_solver_set_jftr bmcg2_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg2_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg2_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg2_sat_solver_mark_cone
#else
#include "sat/glucose/AbcGlucose.h"
-#define sat_solver bmcg_sat_solver
-#define sat_solver_start bmcg_sat_solver_start
-#define sat_solver_stop bmcg_sat_solver_stop
-#define sat_solver_addclause bmcg_sat_solver_addclause
-#define sat_solver_addvar bmcg_sat_solver_addvar
-#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
-#define sat_solver_reset bmcg_sat_solver_reset
-#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
-#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
-#define sat_solver_solve bmcg_sat_solver_solve
-#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver bmcg_sat_solver
+#define sat_solver_start bmcg_sat_solver_start
+#define sat_solver_stop bmcg_sat_solver_stop
+#define sat_solver_addclause bmcg_sat_solver_addclause
+#define sat_solver_addvar bmcg_sat_solver_addvar
+#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_reset bmcg_sat_solver_reset
+#define sat_solver_set_conflict_budget bmcg_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum bmcg_sat_solver_conflictnum
+#define sat_solver_solve bmcg_sat_solver_solve
+#define sat_solver_read_cex_varvalue bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex bmcg_sat_solver_read_cex
+#define sat_solver_jftr bmcg_sat_solver_jftr
+#define sat_solver_set_jftr bmcg_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit bmcg_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round bmcg_sat_solver_start_new_round
+#define sat_solver_mark_cone bmcg_sat_solver_mark_cone
#endif
@@ -134,7 +146,8 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
p->timeStart = Abc_Clock();
p->pPars = pPars;
p->pAig = pAig;
- p->pSat = sat_solver_start();
+ p->pSat = sat_solver_start();
+ sat_solver_set_jftr( p->pSat, pPars->jType );
p->vFrontier = Vec_PtrAlloc( 1000 );
p->vFanins = Vec_PtrAlloc( 100 );
p->vCexMin = Vec_IntAlloc( 100 );
@@ -422,11 +435,19 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
{
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
- Vec_PtrClear( p->vFanins );
- Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
- Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
- Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
+ if( sat_solver_jftr( p->pSat ) < 2 )
+ {
+ Vec_PtrClear( p->vFanins );
+ Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
+ Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
+ Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
+ }
+ if( 0 < sat_solver_jftr( p->pSat ) )
+ sat_solver_set_var_fanin_lit( p->pSat\
+ , Cec4_ObjSatId( p->pNew, pObj )\
+ , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin0(pObj) ), Gia_ObjFaninC0(pObj) )\
+ , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin1(pObj) ), Gia_ObjFaninC1(pObj) ) );
return Cec4_ObjSatId( p->pNew, pObj );
}
// start the frontier
@@ -1064,6 +1085,12 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
clk = Abc_Clock();
iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
+ if( sat_solver_jftr( p->pSat ) )
+ {
+ sat_solver_start_new_round( p->pSat );
+ sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
+ sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj1)) );
+ }
p->timeCnf += Abc_Clock() - clk;
// perform solving
Lits[0] = Abc_Var2Lit(iVar0, 1);
@@ -1135,20 +1162,35 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
{
abctime clk = Abc_Clock();
- int i, IdAig, IdSat, status, fEasy, RetValue = 1;
+ int i, iLit, IdAig, IdSat, status, fEasy, RetValue = 1;
Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
if ( status == GLUCOSE_SAT )
{
+ int * pCex;
//printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
p->nSatSat++;
p->nPatterns++;
p->pAig->iPatsPi++;
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
- Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
- Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
+ //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
+ // Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
+ pCex = sat_solver_read_cex( p->pSat );
+ Vec_IntClear( p->vPat );
+ if ( pCex == NULL )
+ {
+ Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
+ Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
+ }
+ else
+ {
+ for ( i = 0; i < pCex[0]; )
+ Vec_IntPush( p->vPat, Abc_LitNot(pCex[++i]) );
+ }
+ Vec_IntForEachEntry( p->vPat, iLit, i )
+ Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
if ( fEasy )
p->timeSatSat0 += Abc_Clock() - clk;
else
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-19 01:53:00 +0000