/**CFile**************************************************************** FileName [bmcICheck.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [SAT-based bounded model checking.] Synopsis [Performs specialized check.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: bmcICheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "bmc.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) { Cnf_Dat_t * pCnf; Aig_Man_t * pAig = Gia_ManToAigSimple( p ); pAig->nRegs = 0; pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); Aig_ManStop( pAig ); return pCnf; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus ) { Gia_Obj_t * pObj; int v; Gia_ManForEachObj( pGia, pObj, v ) if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 ) p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus; for ( v = 0; v < p->nLiterals; v++ ) p->pClauses[0][v] += 2*nVarsPlus; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pCnf, int nFramesMax, int nTimeOut, int fVerbose ) { sat_solver * pSat; Vec_Int_t * vLits; Gia_Obj_t * pObj, * pObj0, * pObj1; int i, k, iVar0, iVar1, iVarOut; int VarShift = 0; // start the SAT solver pSat = sat_solver_new(); sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) ); sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); // add one large OR clause vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); Gia_ManForEachCo( p, pObj, i ) Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) ); sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); // load the last timeframe Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) ); VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p); // add XOR clauses Gia_ManForEachPo( p, pObj, i ) { pObj0 = Gia_ManPo( pMiter, 2*i+0 ); pObj1 = Gia_ManPo( pMiter, 2*i+1 ); iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)]; iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)]; iVarOut = Gia_ManRegNum(p) + i; sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 ); } Gia_ManForEachRi( p, pObj, i ) { pObj0 = Gia_ManRi( pMiter, i ); pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) ); iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)]; iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)]; iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i; sat_solver_add_xor_and( pSat, iVarOut, iVar0, iVar1, i ); } // add timeframe clauses for ( i = 0; i < pCnf->nClauses; i++ ) if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) assert( 0 ); // add other timeframes for ( k = 0; k < nFramesMax; k++ ) { // collect variables of the RO nodes Vec_IntClear( vLits ); Gia_ManForEachRo( pMiter, pObj, i ) Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] ); // lift CNF again Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars ); VarShift += pCnf->nVars; // stitch the clauses Gia_ManForEachRi( pMiter, pObj, i ) { iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)]; iVar1 = Vec_IntEntry( vLits, i ); if ( iVar1 == -1 ) continue; sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); } // add equality clauses for the COs Gia_ManForEachPo( p, pObj, i ) { pObj0 = Gia_ManPo( pMiter, 2*i+0 ); pObj1 = Gia_ManPo( pMiter, 2*i+1 ); iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)]; iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)]; sat_solver_add_buffer( pSat, iVar0, iVar1, 0 ); } Gia_ManForEachRi( p, pObj, i ) { pObj0 = Gia_ManRi( pMiter, i ); pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) ); iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)]; iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)]; sat_solver_add_buffer_enable( pSat, iVar0, iVar1, i, 0 ); } // add timeframe clauses for ( i = 0; i < pCnf->nClauses; i++ ) if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) assert( 0 ); } // sat_solver_compress( pSat ); Cnf_DataLiftGia( pCnf, pMiter, -VarShift ); Vec_IntFree( vLits ); return pSat; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ) { int fUseOldCnf = 0; Gia_Man_t * pMiter, * pTemp; Cnf_Dat_t * pCnf; sat_solver * pSat; Vec_Int_t * vLits, * vUsed; int i, status, Lit; int nLitsUsed, nLits, * pLits; abctime clkStart = Abc_Clock(); assert( nFramesMax > 0 ); assert( Gia_ManRegNum(p) > 0 ); if ( fVerbose ) printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n", Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) ); // create miter pTemp = Gia_ManDup( p ); pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 ); Gia_ManStop( pTemp ); assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) ); assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) ); // derive CNF if ( fUseOldCnf ) pCnf = Cnf_DeriveGiaRemapped( pMiter ); else { pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 ); Gia_ManStop( pTemp ); pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; } // collect positive literals vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); for ( i = 0; i < Gia_ManRegNum(p); i++ ) Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) ); // iteratively compute a minimal M-inductive set of next-state functions nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits); vUsed = Vec_IntAlloc( Vec_IntSize(vLits) ); while ( 1 ) { int fChanges = 0; // derive SAT solver pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose ); // sat_solver_bookmark( pSat ); status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) { printf( "Timeout reached after %d seconds.\n", nTimeOut ); break; } if ( status == l_True ) { printf( "The problem is satisfiable (the current set is not M-inductive).\n" ); break; } assert( status == l_False ); // call analize_final nLits = sat_solver_final( pSat, &pLits ); // mark used literals Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 ); for ( i = 0; i < nLits; i++ ) Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 ); // check if there are any positive unused Vec_IntForEachEntry( vLits, Lit, i ) { assert( i == Abc_Lit2Var(Lit) ); if ( Abc_LitIsCompl(Lit) ) continue; if ( Vec_IntEntry(vUsed, i) ) continue; // positive literal became unused Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) ); nLitsUsed--; fChanges = 1; } // report the results if ( fVerbose ) printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat), sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) ); if ( fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); // count the number of negative literals sat_solver_delete( pSat ); if ( !fChanges || fEmpty ) break; // break; // sat_solver_rollback( pSat ); } Cnf_DataFree( pCnf ); Gia_ManStop( pMiter ); Vec_IntFree( vLits ); Vec_IntFree( vUsed ); } /**Function************************************************************* Synopsis [Collect flops starting from the POs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Bmc_PerformFindFlopOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRegs ) { if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; Gia_ObjSetTravIdCurrent(p, pObj); if ( Gia_ObjIsCi(pObj) ) { if ( Gia_ObjIsRo(p, pObj) ) Vec_IntPush( vRegs, Gia_ObjId(p, pObj) ); return; } assert( Gia_ObjIsAnd(pObj) ); Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs ); Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs ); } void Bmc_PerformFindFlopOrder( Gia_Man_t * p, Vec_Int_t * vRegs ) { Gia_Obj_t * pObj; int i, iReg, k = 0; // start with POs Vec_IntClear( vRegs ); Gia_ManForEachPo( p, pObj, i ) Vec_IntPush( vRegs, Gia_ObjId(p, pObj) ); // add flop outputs in the B Gia_ManIncrementTravId( p ); Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); Gia_ManForEachObjVec( vRegs, p, pObj, i ) { assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) ); if ( Gia_ObjIsRo(p, pObj) ) pObj = Gia_ObjRoToRi( p, pObj ); Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs ); } // add dangling flops Gia_ManForEachRo( p, pObj, i ) if ( !Gia_ObjIsTravIdCurrent(p, pObj) ) Vec_IntPush( vRegs, Gia_ObjId(p, pObj) ); // remove POs; keep flop outputs only; remap ObjId into CiId assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) ); Gia_ManForEachObjVec( vRegs, p, pObj, i ) { if ( i < Gia_ManPoNum(p) ) continue; iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p); assert( iReg >= 0 && iReg < Gia_ManRegNum(p) ); Vec_IntWriteEntry( vRegs, k++, iReg ); } Vec_IntShrink( vRegs, k ); assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t * vLits ) { int fUseOldCnf = 0; Gia_Man_t * pMiter, * pTemp; Cnf_Dat_t * pCnf; sat_solver * pSat; Vec_Int_t * vRegs = NULL; // Vec_Int_t * vLits; int i, Iter, status; int nLitsUsed, RetValue = 0; abctime clkStart = Abc_Clock(); assert( nFramesMax > 0 ); assert( Gia_ManRegNum(p) > 0 ); // create miter pTemp = Gia_ManDup( p ); pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 ); Gia_ManStop( pTemp ); assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) ); assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) ); // derive CNF if ( fUseOldCnf ) pCnf = Cnf_DeriveGiaRemapped( pMiter ); else { extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 ); //Gia_ManStop( pTemp ); //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; pCnf = Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0 ); } /* // collect positive literals vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); for ( i = 0; i < Gia_ManRegNum(p); i++ ) Vec_IntPush( vLits, Abc_Var2Lit(i, 0) ); */ // derive SAT solver pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose ); status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_True ) { printf( "I = %4d : ", nFramesMax ); printf( "Problem is satisfiable.\n" ); sat_solver_delete( pSat ); Cnf_DataFree( pCnf ); Gia_ManStop( pMiter ); return 1; } if ( status == l_Undef ) { printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut ); RetValue = 1; goto cleanup; } assert( status == l_False ); // count the number of positive literals nLitsUsed = 0; for ( i = 0; i < Gia_ManRegNum(p); i++ ) if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) ) nLitsUsed++; // try removing variables vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) ); if ( fBackTopo ) Bmc_PerformFindFlopO
/****************************************************************************
**
** Copyright (C) 2010 Nokia Corporation and/or its subsidiary(-ies).
** All rights reserved.
**
** Contact: Nokia Corporation (qt-info@nokia.com)
**
** This file is part of a Qt Solutions component.
**
** You may use this file under the terms of the BSD license as follows:
**
** "Redistribution and use in source and binary forms, with or without
** modification, are permitted provided that the following conditions are
** met:
**   * Redistributions of source code must retain the above copyright
**     notice, this list of conditions and the following disclaimer.
**   * Redistributions in binary form must reproduce the above copyright
**     notice, this list of conditions and the following disclaimer in
**     the documentation and/or other materials provided with the
**     distribution.
**   * Neither the name of Nokia Corporation and its Subsidiary(-ies) nor
**     the names of its contributors may be used to endorse or promote
**     products derived from this software without specific prior written
**     permission.
**
** THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
** "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
** LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
** A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
** OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
** SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
** LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
** DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
** THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
** (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
** OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE."
**
****************************************************************************/


#ifndef QTPROPERTYBROWSER_H
#define QTPROPERTYBROWSER_H

#include <QWidget>
#include <QtCore/QSet>

#if QT_VERSION >= 0x040400
QT_BEGIN_NAMESPACE
#endif

#if defined(Q_WS_WIN)
#  if !defined(QT_QTPROPERTYBROWSER_EXPORT) && !defined(QT_QTPROPERTYBROWSER_IMPORT)
#    define QT_QTPROPERTYBROWSER_EXPORT
#  elif defined(QT_QTPROPERTYBROWSER_IMPORT)
#    if defined(QT_QTPROPERTYBROWSER_EXPORT)
#      undef QT_QTPROPERTYBROWSER_EXPORT
#    endif
#    define QT_QTPROPERTYBROWSER_EXPORT __declspec(dllimport)
#  elif defined(QT_QTPROPERTYBROWSER_EXPORT)
#    undef QT_QTPROPERTYBROWSER_EXPORT
#    define QT_QTPROPERTYBROWSER_EXPORT __declspec(dllexport)
#  endif
#else
#  define QT_QTPROPERTYBROWSER_EXPORT
#endif


class QtAbstractPropertyManager;
class QtPropertyPrivate;

class QT_QTPROPERTYBROWSER_EXPORT QtProperty
{
public:
    virtual ~QtProperty();

    QList<QtProperty *> subProperties() const;

    QtAbstractPropertyManager *propertyManager() const;

    QString toolTip() const;
    QString statusTip() const;
    QString whatsThis() const;
    QString propertyName() const;
    QString propertyId() const;
    bool isEnabled() const;
    bool isSelectable() const;
    bool isModified() const;

    bool hasValue() const;
    QIcon valueIcon() const;
    QString valueText() const;

    virtual bool compare(QtProperty* otherProperty)const;

    void setToolTip(const QString &text);
    void setStatusTip(const QString &text);
    void setWhatsThis(const QString &text);
    void setPropertyName(const QString &text);
    void setPropertyId(const QString &text);
    void setEnabled(bool enable);
    void setSelectable(bool selectable);
    void setModified(bool modified);

    bool isSubProperty()const;
    void addSubProperty(QtProperty *property);
    void insertSubProperty(QtProperty *property, QtProperty *afterProperty);
    void removeSubProperty(QtProperty *property);
protected:
    explicit QtProperty(QtAbstractPropertyManager *manager);
    void propertyChanged();
private:
    friend class QtAbstractPropertyManager;
    QtPropertyPrivate *d_ptr;
};

class QtAbstractPropertyManagerPrivate;

class QT_QTPROPERTYBROWSER_EXPORT QtAbstractPropertyManager : public QObject
{
    Q_OBJECT
public:

    explicit QtAbstractPropertyManager(QObject *parent = 0);
    ~QtAbstractPropertyManager();

    QSet<QtProperty *> properties() const;
    void clear() const;

    QtProperty *addProperty(const QString &name = QString());
    QtProperty *qtProperty(const QString &id)const;
Q_SIGNALS:

    void propertyInserted(QtProperty *property,
                QtProperty *parent, QtProperty *after);
    void propertyChanged(QtProperty *property);
    void propertyRemoved(QtProperty *property, QtProperty *parent);
    void propertyDestroyed(QtProperty *property);
protected:
    virtual bool hasValue(const QtProperty *property) const;
    virtual QIcon valueIcon(const QtProperty *property) const;
    virtual QString valueText(const QtProperty *property) const;
    virtual void initializeProperty(QtProperty *property) = 0;
    virtual void uninitializeProperty(QtProperty *property);
    virtual QtProperty *createProperty();
private:
    friend class QtProperty;
    QtAbstractPropertyManagerPrivate *d_ptr;
    Q_DECLARE_PRIVATE(QtAbstractPropertyManager)
    Q_DISABLE_COPY(QtAbstractPropertyManager)
};

class QT_QTPROPERTYBROWSER_EXPORT QtAbstractEditorFactoryBase : public QObject
{
    Q_OBJECT
public:
    virtual QWidget *createEditor(QtProperty *property, QWidget *parent) = 0;
protected:
    explicit QtAbstractEditorFactoryBase(QObject *parent = 0)
        : QObject(parent) {}

    virtual void breakConnection(QtAbstractPropertyManager *manager) = 0;
protected Q_SLOTS:
    virtual void managerDestroyed(QObject *manager) = 0;

    friend class QtAbstractPropertyBrowser;
};

template <class PropertyManager>
class QtAbstractEditorFactory : public QtAbstractEditorFactoryBase
{
public:
    explicit QtAbstractEditorFactory(QObject *parent) : QtAbstractEditorFactoryBase(parent) {}
    QWidget *createEditor(QtProperty *property, QWidget *parent)
    {
        QSetIterator<PropertyManager *> it(m_managers);
        while (it.hasNext()) {
            PropertyManager *manager = it.next();
            if (manager == property->propertyManager()) {
                return createEditor(manager, property, parent);
            }
        }
        return 0;
    }
    void addPropertyManager(PropertyManager *manager)
    {
        if (m_managers.contains(manager))
            return;
        m_managers.insert(manager);
        connectPropertyManager(manager);
        connect(manager, SIGNAL(destroyed(QObject *)),
                    this, SLOT(managerDestroyed(QObject *)));
    }
    void removePropertyManager(PropertyManager *manager)
    {
        if (!m_managers.contains(manager))
            return;
        disconnect(manager, SIGNAL(destroyed(QObject *)),
                    this, SLOT(managerDestroyed(QObject *)));
        disconnectPropertyManager(manager);
        m_managers.remove(manager);
    }
    QSet<PropertyManager *> propertyManagers() const
    {
        return m_managers;
    }
    PropertyManager *propertyManager(QtProperty *property) const
    {
        QtAbstractPropertyManager *manager = property->propertyManager();
        QSetIterator<PropertyManager *> itManager(m_managers);
        while (itManager.hasNext()) {
            PropertyManager *m = itManager.next();
            if (m == manager) {
                return m;
            }
        }
        return 0;
    }
protected:
    virtual void connectPropertyManager(PropertyManager *manager) = 0;
    virtual QWidget *createEditor(PropertyManager *manager, QtProperty *property,
                QWidget *parent) = 0;
    virtual void disconnectPropertyManager(PropertyManager *manager) = 0;
    void managerDestroyed(QObject *manager)
    {
        QSetIterator<PropertyManager *> it(m_managers);
        while (it.hasNext()) {
            PropertyManager *m = it.next();
            if (m == manager) {
                m_managers.remove(m);
                return;
            }
        }
    }
private:
    void breakConnection(QtAbstractPropertyManager *manager)
    {
        QSetIterator<PropertyManager *> it(m_managers);
        while (it.hasNext()) {
            PropertyManager *m = it.next();
            if (m == manager) {
                removePropertyManager(m);
                return;
            }
        }
    }
private:
    QSet<PropertyManager *> m_managers;
    friend class QtAbstractPropertyEditor;
};

class QtAbstractPropertyBrowser;
class QtBrowserItemPrivate;

class QT_QTPROPERTYBROWSER_EXPORT QtBrowserItem
{
public:
    QtProperty *property() const;
    QtBrowserItem *parent() const;
    QList<QtBrowserItem *> children() const;
    QtAbstractPropertyBrowser *browser() const;
private:
    explicit QtBrowserItem(QtAbstractPropertyBrowser *browser, QtProperty *property, QtBrowserItem *parent);
    ~QtBrowserItem();
    QtBrowserItemPrivate *d_ptr;
    friend class QtAbstractPropertyBrowserPrivate;
};

class QtAbstractPropertyBrowserPrivate;

class QT_QTPROPERTYBROWSER_EXPORT QtAbstractPropertyBrowser : public QWidget
{
    Q_OBJECT
public:

    explicit QtAbstractPropertyBrowser(QWidget *parent = 0);
    ~QtAbstractPropertyBrowser();

    QList<QtProperty *> properties() const;
    QList<QtBrowserItem *> items(QtProperty *property) const;
    QtBrowserItem *topLevelItem(QtProperty *property) const;
    QList<QtBrowserItem *> topLevelItems() const;
    void clear();

    template <class PropertyManager>
    void setFactoryForManager(PropertyManager *manager,
                    QtAbstractEditorFactory<PropertyManager> *factory) {
        QtAbstractPropertyManager *abstractManager = manager;
        QtAbstractEditorFactoryBase *abstractFactory = factory;

        if (addFactory(abstractManager, abstractFactory))
            factory->addPropertyManager(manager);
    }

    void unsetFactoryForManager(QtAbstractPropertyManager *manager);

    QtBrowserItem *currentItem() const;
    void setCurrentItem(QtBrowserItem *);

Q_SIGNALS:
    void currentItemChanged(QtBrowserItem *);

public Q_SLOTS:

    QtBrowserItem *addProperty(QtProperty *property);
    QtBrowserItem *insertProperty(QtProperty *property, QtProperty *afterProperty);
    void removeProperty(QtProperty *property);

protected:

    virtual void itemInserted(QtBrowserItem *item, QtBrowserItem *afterItem) = 0;
    virtual void itemRemoved(QtBrowserItem *item) = 0;
    // can be tooltip, statustip, whatsthis, name, icon, text.
    virtual void itemChanged(QtBrowserItem *item) = 0;

    virtual QWidget *createEditor(QtProperty *property, QWidget *parent);
private:

    bool addFactory(QtAbstractPropertyManager *abstractManager,
                QtAbstractEditorFactoryBase *abstractFactory);

    QtAbstractPropertyBrowserPrivate *d_ptr;
    Q_DECLARE_PRIVATE(QtAbstractPropertyBrowser)
    Q_DISABLE_COPY(QtAbstractPropertyBrowser)
    Q_PRIVATE_SLOT(d_func(), void slotPropertyInserted(QtProperty *,
                            QtProperty *, QtProperty *))
    Q_PRIVATE_SLOT(d_func(), void slotPropertyRemoved(QtProperty *,
                            QtProperty *))
    Q_PRIVATE_SLOT(d_func(), void slotPropertyDestroyed(QtProperty *))
    Q_PRIVATE_SLOT(d_func(), void slotPropertyDataChanged(QtProperty *))

};

#if QT_VERSION >= 0x040400
QT_END_NAMESPACE
#endif

#endif // QTPROPERTYBROWSER_H