From 565fefec7a730ac34c7a6dbffe97bf3e38ce5003 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 6 Dec 2011 21:11:18 -0800 Subject: Proof-logging in the updated solver. --- src/sat/bsat/satProof.c | 185 ++++++++++++++++++++++++++++++++++++---------- src/sat/bsat/satSolver2.c | 30 +++----- src/sat/bsat/satSolver2.h | 13 ++-- 3 files changed, 163 insertions(+), 65 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 8fa17e94..a06dd412 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -64,10 +64,11 @@ static inline int Proof_NodeSize (int nEnts) { return sizeo #define Proof_ForeachNodeVec( pVec, p, pNode, i ) \ for ( i = 0; (i < Vec_IntSize(pVec)) && ((pNode) = Proof_NodeRead(p, Vec_IntEntry(pVec,i))); i++ ) #define Proof_NodeForeachFanin( p, pNode, pFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), 1); i++ ) -#define Proof_NodeForeachFanin2( p, pNode, pFanin, iFanin, i ) \ - for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = ((pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 1))), ((iFanin) = ((pNode->pEnts[i] & 1) ? pNode->pEnts[i] >> 1 : 0)), 1); i++ ) - + for ( i = 0; (i < (int)pNode->nEnts) && (((pFanin) = (pNode->pEnts[i] & 1) ? NULL : Proof_NodeRead(p, pNode->pEnts[i] >> 2)), 1); i++ ) +#define Proof_NodeForeachLeaf( pLeaves, pNode, pLeaf, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && (((pLeaf) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : NULL), 1); i++ ) +#define Proof_NodeForeachFaninRoot( p, pLeaves, pNode, pFanin, i ) \ + for ( i = 0; (i < (int)pNode->nEnts) && ((pFanin) = (pNode->pEnts[i] & 1) ? Proof_NodeRead(pLeaves, pNode->pEnts[i] >> 2) : Proof_NodeRead(p, pNode->pEnts[i] >> 2)); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -125,7 +126,7 @@ void Proof_CleanCollected( Vec_Int_t * vProof, Vec_Int_t * vUsed ) SeeAlso [] ***********************************************************************/ -void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) +void Proof_CollectUsed_iter( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec_Int_t * vStack ) { satset * pNext; int i, hNode; @@ -167,7 +168,37 @@ void Proof_CollectUsedInt( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed, Vec SeeAlso [] ***********************************************************************/ -void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) +Vec_Int_t * Proof_CollectUsedIter( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) +{ + Vec_Int_t * vUsed, * vStack; + assert( (hRoot > 0) ^ (vRoots != NULL) ); + vUsed = Vec_IntAlloc( 1000 ); + vStack = Vec_IntAlloc( 1000 ); + if ( hRoot ) + Proof_CollectUsed_iter( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack ); + else + { + satset * pNode; + int i; + Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) + Proof_CollectUsed_iter( vProof, pNode, vUsed, vStack ); + } + Vec_IntFree( vStack ); + return vUsed; +} + +/**Function************************************************************* + + Synopsis [Recursively visits useful proof nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Proof_CollectUsed_rec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) { satset * pNext; int i; @@ -176,7 +207,7 @@ void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) pNode->Id = 1; Proof_NodeForeachFanin( p, pNode, pNext, i ) if ( pNext && !pNext->Id ) - Proof_CollectUsedRec( p, pNext, vUsed ); + Proof_CollectUsed_rec( p, pNext, vUsed ); Vec_IntPush( vUsed, Proof_NodeHandle(p, pNode) ); } @@ -191,22 +222,20 @@ void Proof_CollectUsedRec( Vec_Int_t * p, satset * pNode, Vec_Int_t * vUsed ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Proof_CollectUsed( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) +Vec_Int_t * Proof_CollectUsedRec( Vec_Int_t * vProof, Vec_Int_t * vRoots, int hRoot ) { Vec_Int_t * vUsed, * vStack; assert( (hRoot > 0) ^ (vRoots != NULL) ); vUsed = Vec_IntAlloc( 1000 ); vStack = Vec_IntAlloc( 1000 ); if ( hRoot ) -// Proof_CollectUsedInt( vProof, Proof_NodeRead(vProof, hRoot), vUsed, vStack ); - Proof_CollectUsedRec( vProof, Proof_NodeRead(vProof, hRoot), vUsed ); + Proof_CollectUsed_rec( vProof, Proof_NodeRead(vProof, hRoot), vUsed ); else { satset * pNode; int i; Proof_ForeachNodeVec( vRoots, vProof, pNode, i ) -// Proof_CollectUsedInt( vProof, pNode, vUsed, vStack ); - Proof_CollectUsedRec( vProof, pNode, vUsed ); + Proof_CollectUsed_rec( vProof, pNode, vUsed ); } Vec_IntFree( vStack ); return vUsed; @@ -279,9 +308,9 @@ satset * Proof_CheckReadOne( Vec_Int_t * vClauses, Vec_Int_t * vProof, Vec_Int_t { satset * pAnt; if ( iAnt & 1 ) - return Proof_NodeRead( vClauses, iAnt >> 1 ); + return Proof_NodeRead( vClauses, iAnt >> 2 ); assert( iAnt > 0 ); - pAnt = Proof_NodeRead( vProof, iAnt >> 1 ); + pAnt = Proof_NodeRead( vProof, iAnt >> 2 ); assert( pAnt->Id > 0 ); return Proof_NodeRead( vResolves, pAnt->Id ); } @@ -303,7 +332,7 @@ void Proof_Check( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot ) satset * pSet, * pSet0, * pSet1; int i, k, Counter = 0, clk = clock(); // collect visited clauses - vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); // perform resolution steps vTemp = Vec_IntAlloc( 1000 ); @@ -433,6 +462,8 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) Vec_IntShrink( p, nSize ); } + + /**Function************************************************************* Synopsis [Computes UNSAT core.] @@ -444,29 +475,31 @@ void Sat_ProofReduce( Vec_Int_t * p, Vec_Int_t * vRoots ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots ) +Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, Vec_Int_t * vRoots ) { - unsigned * pSeen; Vec_Int_t * vCore, * vUsed; - satset * pNode; - int i, * pBeg; + satset * pNode, * pFanin; + int i, k, clk = clock();; // collect visited clauses - vUsed = Proof_CollectUsed( vProof, vRoots, 0 ); - // find the core + vUsed = Proof_CollectUsedIter( vProof, vRoots, 0 ); + // collect core clauses vCore = Vec_IntAlloc( 1000 ); - pSeen = ABC_CALLOC( unsigned, Aig_BitWordNum(nRoots) ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { pNode->Id = 0; - for ( pBeg = pNode->pEnts; pBeg < pNode->pEnts + pNode->nEnts; pBeg++ ) - if ( (*pBeg & 1) && !Aig_InfoHasBit((unsigned *)pBeg, *pBeg>>1) ) + Proof_NodeForeachLeaf( vRoots, pNode, pFanin, k ) + if ( pFanin && !pFanin->mark ) { - Aig_InfoSetBit( (unsigned *)pBeg, *pBeg>>1 ); - Vec_IntPush( vCore, (*pBeg>>1)-1 ); + pFanin->mark = 1; + Vec_IntPush( vCore, Proof_NodeHandle(vRoots, pFanin) ); } } + // clean core clauses + Proof_ForeachNodeVec( vCore, vRoots, pNode, i ) + pNode->mark = 0; Vec_IntFree( vUsed ); - ABC_FREE( pSeen ); + printf( "Collected %d core clauses. ", Vec_IntSize(vCore) ); + Abc_PrintTime( 1, "Time", clock() - clk ); return vCore; } @@ -474,7 +507,7 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots ) Synopsis [Computes interpolant of the proof.] - Description [Aassuming that global vars and A-clauses are marked.] + Description [Aassuming that vars/clause of partA are marked.] SideEffects [] @@ -483,19 +516,81 @@ Vec_Int_t * Sat_ProofCore( Vec_Int_t * vProof, int nRoots, Vec_Int_t * vRoots ) ***********************************************************************/ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int hRoot, Vec_Int_t * vGlobVars ) { - Vec_Int_t * vUsed; + Vec_Int_t * vUsed, * vCore, * vVarMap; + Vec_Int_t * vUsedNums, * vCoreNums; + satset * pNode, * pFanin; Aig_Man_t * pAig; - int i; + Aig_Obj_t * pObj; + int i, k, iVar, Entry; + // collect core clauses + vCore = Sat_ProofCore( vProof, vClauses ); // collect visited clauses - vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); // start the AIG pAig = Aig_ManStart( 10000 ); pAig->pName = Aig_UtilStrsav( "interpol" ); for ( i = 0; i < Vec_IntSize(vGlobVars); i++ ) Aig_ObjCreatePi( pAig ); - + + // map variables into their global numbers + vVarMap = Vec_IntStartFull( Vec_IntFindMax(vGlobVars) + 1 ); + Vec_IntForEachEntry( vGlobVars, Entry, i ) + Vec_IntWriteEntry( vVarMap, Entry, i ); + + // copy the numbers out and derive interpol for clause + vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) ); + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + { + if ( pNode->partA ) + { + pObj = Aig_ManConst0( pAig ); + satset_foreach_var( pNode, iVar, k ) + if ( iVar < Vec_IntSize(vVarMap) && Vec_IntEntry(vVarMap, iVar) >= 0 ) + pObj = Aig_Or( pAig, pObj, Aig_IthVar(pAig, iVar) ); + } + else + pObj = Aig_ManConst1( pAig ); + // remember the interpolant + Vec_IntPush( vCoreNums, pNode->Id ); + pNode->Id = Aig_ObjToLit(pObj); + } + Vec_IntFree( vVarMap ); + + // copy the numbers out and derive interpol for resolvents + vUsedNums = Vec_IntAlloc( Vec_IntSize(vUsed) ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + { + assert( pNode->nEnts > 1 ); + Proof_NodeForeachFaninRoot( vProof, vClauses, pNode, pFanin, k ) + { + if ( k == 0 ) + pObj = Aig_ObjFromLit(pAig, pFanin->Id); + else if ( pNode->pEnts[k] & 2 ) // variable of A + pObj = Aig_Or( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + else + pObj = Aig_And( pAig, pObj, Aig_ObjFromLit(pAig, pFanin->Id) ); + } + // remember the interpolant + Vec_IntPush( vUsedNums, pNode->Id ); + pNode->Id = Aig_ObjToLit(pObj); + } + // save the result + Aig_ObjCreatePo( pAig, pObj ); + Aig_ManCleanup( pAig ); + + // move the results back + Proof_ForeachNodeVec( vCore, vClauses, pNode, i ) + pNode->Id = Vec_IntEntry( vCoreNums, i ); + Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) + pNode->Id = Vec_IntEntry( vUsedNums, i ); + // cleanup + Vec_IntFree( vCore ); + Vec_IntFree( vUsed ); + Vec_IntFree( vCoreNums ); + Vec_IntFree( vUsedNums ); return pAig; } @@ -503,7 +598,6 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int Sat_ProofTest( &s->clauses, // clauses &s->proof_clas, // proof clauses - &s->proof_vars, // proof variables NULL, // proof roots veci_begin(&s->claProofs)[clause_read(s, s->iLearntLast)->Id)], // one root &s->glob_vars ); // global variables (for interpolation) @@ -520,23 +614,35 @@ Aig_Man_t * Sat_ProofInterpolant( Vec_Int_t * vClauses, Vec_Int_t * vProof, int SeeAlso [] ***********************************************************************/ -void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ) +void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot ) { Vec_Int_t * vClauses = (Vec_Int_t *)pClauses; Vec_Int_t * vProof = (Vec_Int_t *)pProof; - Vec_Int_t * vVars = (Vec_Int_t *)pVars; Vec_Int_t * vRoots = (Vec_Int_t *)pRoots; - Vec_Int_t * vGlobVars = (Vec_Int_t *)pGlobVars; - Vec_Int_t * vUsed; + Vec_Int_t * vUsed, * vCore; // int i, Entry; // collect visited clauses - vUsed = Proof_CollectUsed( vProof, NULL, hRoot ); + vUsed = Proof_CollectUsedRec( vProof, NULL, hRoot ); Proof_CleanCollected( vProof, vUsed ); + printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + + // collect visited clauses + vUsed = Proof_CollectUsedIter( vProof, NULL, hRoot ); + Proof_CleanCollected( vProof, vUsed ); + printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); + Vec_IntFree( vUsed ); + + vCore = Sat_ProofCore( vProof, vClauses ); + Vec_IntFree( vCore ); + + + // Vec_IntForEachEntry( vUsed, Entry, i ) // printf( "%d ", Entry ); // printf( "\n" ); - +/* printf( "Found %d useful resolution nodes.\n", Vec_IntSize(vUsed) ); Vec_IntFree( vUsed ); vUsed = Proof_CollectAll( vProof ); @@ -544,6 +650,7 @@ void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, Vec_IntFree( vUsed ); Proof_Check( vClauses, vProof, hRoot ); +*/ } //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 1c9e9dbb..cde37116 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -85,13 +85,13 @@ struct varinfo_t { unsigned val : 2; // variable value unsigned pol : 1; // last polarity - unsigned glo : 1; // global variable + unsigned partA : 1; // partA variable unsigned tag : 4; // conflict analysis tags unsigned lev : 24; // variable level }; -int var_is_global (sat_solver2* s, int v) { return s->vi[v].glo; } -void var_set_global(sat_solver2* s, int v, int glo) { s->vi[v].glo = glo; if (glo) veci_push(&s->glob_vars, v); } +int var_is_partA (sat_solver2* s, int v) { return s->vi[v].partA; } +void var_set_partA(sat_solver2* s, int v, int partA) { s->vi[v].partA = partA; } static inline int var_value (sat_solver2* s, int v) { return s->vi[v].val; } static inline int var_polar (sat_solver2* s, int v) { return s->vi[v].pol; } @@ -145,7 +145,7 @@ static inline void solver2_clear_marks(sat_solver2* s) { static inline satset* clause_read (sat_solver2* s, cla h) { return satset_read( &s->clauses, h ); } static inline cla clause_handle (sat_solver2* s, satset* c) { return satset_handle( &s->clauses, c ); } static inline int clause_check (sat_solver2* s, satset* c) { return satset_check( &s->clauses, c ); } -static inline int clause_proofid(sat_solver2* s, satset* c) { return c->learnt ? veci_begin(&s->claProofs)[c->Id]<<1 : (clause_handle(s,c)<<1) | 1; } +static inline int clause_proofid(sat_solver2* s, satset* c, int partA) { return c->learnt ? (veci_begin(&s->claProofs)[c->Id]<<2) | (partA<<1) : (clause_handle(s,c)<<2) | 1; } //static inline int var_reason (sat_solver2* s, int v) { return (s->reasons[v]&1) ? 0 : s->reasons[v] >> 1; } //static inline int lit_reason (sat_solver2* s, int l) { return (s->reasons[lit_var(l)&1]) ? 0 : s->reasons[lit_var(l)] >> 1; } @@ -180,10 +180,7 @@ static inline void proof_chain_start( sat_solver2* s, satset* c ) s->iStartChain = veci_size(&s->proof_clas); veci_push(&s->proof_clas, 0); veci_push(&s->proof_clas, 0); - veci_push(&s->proof_clas, clause_proofid(s, c) ); - veci_push(&s->proof_vars, 0); - veci_push(&s->proof_vars, 0); - veci_push(&s->proof_vars, 0); + veci_push(&s->proof_clas, clause_proofid(s, c, 0) ); } } @@ -192,8 +189,7 @@ static inline void proof_chain_resolve( sat_solver2* s, satset* cls, int Var ) if ( s->fProofLogging ) { satset* c = cls ? cls : var_unit_clause( s, Var ); - veci_push(&s->proof_clas, clause_proofid(s, c) ); - veci_push(&s->proof_vars, Var); + veci_push(&s->proof_clas, clause_proofid(s, c, var_is_partA(s,Var)) ); // printf( "%d %d ", clause_proofid(s, c), Var ); } } @@ -1225,9 +1221,7 @@ sat_solver2* sat_solver2_new(void) veci_new(&s->mark_levels); veci_new(&s->min_lit_order); veci_new(&s->min_step_order); - veci_new(&s->glob_vars); veci_new(&s->proof_clas); veci_push(&s->proof_clas, -1); - veci_new(&s->proof_vars); veci_push(&s->proof_vars, -1); veci_new(&s->claActs); veci_push(&s->claActs, -1); veci_new(&s->claProofs); veci_push(&s->claProofs, -1); @@ -1256,8 +1250,6 @@ sat_solver2* sat_solver2_new(void) { s->proof_clas.cap = (1 << 20); s->proof_clas.ptr = ABC_REALLOC( int, s->proof_clas.ptr, s->proof_clas.cap ); - s->proof_vars.cap = (1 << 20); - s->proof_vars.ptr = ABC_REALLOC( int, s->proof_vars.ptr, s->proof_clas.cap ); } return s; } @@ -1306,16 +1298,14 @@ void sat_solver2_delete(sat_solver2* s) { satset * c = clause_read(s, s->iLearntLast); // report statistics - assert( veci_size(&s->proof_clas) == veci_size(&s->proof_vars) ); - printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 8.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits ); + printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proof_clas) / (1<<20), s->nUnits ); Sat_ProofTest( &s->clauses, // clauses &s->proof_clas, // proof clauses - &s->proof_vars, // proof variables NULL, // proof roots - veci_begin(&s->claProofs)[c->Id], // one root - &s->glob_vars ); // global variables (for interpolation) + veci_begin(&s->claProofs)[c->Id] // one root + ); // delete vectors veci_delete(&s->order); @@ -1328,9 +1318,7 @@ void sat_solver2_delete(sat_solver2* s) veci_delete(&s->mark_levels); veci_delete(&s->min_lit_order); veci_delete(&s->min_step_order); - veci_delete(&s->glob_vars); veci_delete(&s->proof_clas); - veci_delete(&s->proof_vars); veci_delete(&s->claActs); veci_delete(&s->claProofs); veci_delete(&s->clauses); diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index 1cdc8bd9..e091d488 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -68,8 +68,8 @@ extern void sat_solver2_store_mark_clauses_a( sat_solver2 * s ); extern void * sat_solver2_store_release( sat_solver2 * s ); // global variables -extern int var_is_global (sat_solver2* s, int v); -extern void var_set_global(sat_solver2* s, int v, int glo); +extern int var_is_partA (sat_solver2* s, int v); +extern void var_set_partA(sat_solver2* s, int v, int partA); // clause grouping (these two only work after creating a clause before the solver is called) extern int clause_is_partA (sat_solver2* s, int handle); extern void clause_set_partA(sat_solver2* s, int handle, int partA); @@ -143,7 +143,6 @@ struct sat_solver2_t // proof logging veci proof_clas; // sequence of proof clauses - veci proof_vars; // sequence of proof variables int iStartChain; // temporary variable to remember beginning of the current chain in proof logging int nUnits; // the total number of unit clauses @@ -177,9 +176,13 @@ static inline void satset_print (satset * c) { printf( "}\n" ); } - #define satset_foreach_entry( p, c, h, s ) \ for ( h = s; (h < veci_size(p)) && (((c) = satset_read(p, h)), 1); h += satset_size(c->nEnts) ) +#define satset_foreach_var( p, var, i ) \ + for ( i = 0; (i < (int)(p)->nEnts) && ((var) = lit_var((p)->pEnts[i])); i++ ) +#define satset_foreach_lit( p, lit, i ) \ + for ( i = 0; (i < (int)(p)->nEnts) && ((lit) = (p)->pEnts[i]); i++ ) + //================================================================================================= // Public APIs: @@ -245,7 +248,7 @@ static inline int sat_solver2_set_random(sat_solver2* s, int fNotUseRandom) return fNotUseRandomOld; } -extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pVars, veci * pRoots, int hRoot, veci * pGlobVars ); +extern void Sat_ProofTest( veci * pClauses, veci * pProof, veci * pRoots, int hRoot ); ABC_NAMESPACE_HEADER_END -- cgit v1.2.3