import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public Netlist(BDDFactory fac, StateGraph sg, Reset reset) {
    this.fac = fac;
    this.reset = reset;
    this.nameVarMap = new HashMap<>();
    this.idVarMap = new HashMap<>();
    this.terms = new TreeMap<>(new BDDComparator());
    this.unmappedTerms = new HashSet<>();
    this.mappedTerms = new HashMap<>();
    this.quasiSignals = new HashMap<>();
    this.tmpid = 0;

    this.sigVarMap = HashBiMap.create();
    for(Signal sig : sg.getAllSignals()) {
        sigVarMap.put(sig, getNetlistVariableByName(sig.getName()));
    }

    initReset();
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
private static TechLibrary readTechnology(File optTech, String cfgTech, BDDFactory storage) {
    if(optTech != null) {
        if(optTech.exists()) {
            logger.debug("Using options technology file: " + optTech.getAbsolutePath());
            return TechLibrary.importFromFile(optTech, storage);
        } else {
            logger.warn("Options technology file " + optTech.getAbsolutePath() + " not found. Trying default from config");
        }
    }

    if(cfgTech != null) {
        File cfgTechFile = BasedirHelper.replaceBasedirAsFile(cfgTech);
        if(cfgTechFile.exists()) {
            logger.debug("Using config technology file: " + cfgTechFile.getAbsolutePath());
            return TechLibrary.importFromFile(cfgTechFile, storage);
        } else {
            logger.warn("Config technology file " + cfgTechFile.getAbsolutePath() + " not found.");
        }
    } else {
        logger.warn("No default technology in config file defined");
    }

    return null;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public void addStats(BDDFactory bddFactory, BDD bdd, String[] varOrder) {
		if (pathCount == -1 ) {
			pathCount = bdd.pathCount();
		}
		int bddNodeCount = bdd.nodeCount();		

		if ( bddNodeCount < bvoCountNodes ) {
			bvoCountNodes = bddNodeCount;
			bvoIndex = index;
		}
		if ( bddNodeCount > wvoCountNodes ) {
			wvoCountNodes = bddNodeCount; 
			wvoIndex = index;
		}
		stats.add(index, new BDDGenerationStatisticsRecord(bddFactory, bdd, varOrder, bddNodeCount));
		index++;
				
//		System.out.print("\n" + index +"-Count: "); 
//		for ( int i = 0 ; i < varOrder.length ; i++ ) {
//			System.out.print(varOrder[i] + ",");			
//		}
//		System.out.print("\nBest: " + bvoIndex +"(" + bvoCountNodes + ")" + "Worst: " + wvoIndex + "(" + wvoCountNodes + ")");
	}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
/**
   * Constructs a new BDD solver.  Also initializes the BDD library.
   */
  public BDDSolver() {
      super();
      if (BDDCACHE == 0) BDDCACHE = BDDNODES / 4;
if (VERBOSE >= 2)
      	out.println("Initializing BDD library (" + BDDNODES + " nodes, cache size " + BDDCACHE + ", min free " + BDDMINFREE + "%)");
      bdd = BDDFactory.init(1000, BDDCACHE);
      if (VERBOSE >= 2) out.println("Using BDD library "+bdd.getVersion());
      fielddomainsToBDDdomains = new GenericMultiMap(ListFactory.linkedListFactory);
      bdd.setMinFreeNodes(BDDMINFREE);
      try {
          fbo = new FindBestDomainOrder(this);
      } catch (NoClassDefFoundError x) {
          if (VERBOSE >= 2) out.println("No machine learning library found, learning disabled.");
      }
  }
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public PerformanceResult answer(Reasoner r) {
	if(r==null){
		throw new FAMAParameterException("Reasoner :Not specified");
	}
	JavaBDDResult res = new JavaBDDResult();
	JavaBDDReasoner bddr = (JavaBDDReasoner)r;
	long before=System.currentTimeMillis();
	BDD sol=bddr.getBDD().satOne();
	long time=System.currentTimeMillis() - before;
	
	if (!sol.isZero())
		valid = true;
	
	// Save results
	res.setTime(time);
	
	// Consultar este fallo
	res.fillFields((BDDFactory) bddr.getBDDFactory());
	
	return res;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public PerformanceResult answer(Reasoner r)  {
	if(r==null){
		throw new FAMAParameterException("Reasoner :Not specified");
	}
	JavaBDDResult res = new JavaBDDResult();
	JavaBDDReasoner bddr = (JavaBDDReasoner)r;
	
	long before=System.currentTimeMillis();	
	Iterator it=bddr.getBDD().allsat().iterator();
	while (it.hasNext()) {
		// Save product
		saveProduct((byte[])it.next(),r);
	}
	long time=System.currentTimeMillis() - before;

	// Save results
	res.setTime(time);
	res.fillFields((BDDFactory) bddr.getBDDFactory());
       
       return res;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public PerformanceResult answer(Reasoner r)  {
	if(r==null){
		throw new FAMAParameterException("Reasoner :Not specified");
	}
	JavaBDDResult res = new JavaBDDResult();
	JavaBDDReasoner bddr = (JavaBDDReasoner)r;
	
	long before=System.currentTimeMillis();
	numberOfProducts=bddr.getBDD().satCount();
	long time=System.currentTimeMillis() - before;

	// Save results
	res.setTime(time);
	res.fillFields((BDDFactory) bddr.getBDDFactory());
	
       return res;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Override
public void update(int fieldIndex, StoneColor color) {
	Field field = FieldGenerator.create(
			color.getPrimitive(),
			PositionHexagon.get(fieldIndex / board.getRows(), fieldIndex
					% board.getColumns()), fieldIndex);
	board.setField(field);
	BDDFactory fac = win.getFactory();
	Logging logUpdate;
	String capPrefix = this.color + "'s situation updated for ";
	String capSuffix = "'s move";
	if (StoneColor.WHITE.equals(color)) {
		logUpdate = Logging.create(capPrefix + color + capSuffix);
		win = logUpdate.restrictLog(win, fac.ithVar(field.getIndex()));
	} else {
		logUpdate = Logging.create(capPrefix + color + capSuffix);
		win = logUpdate.restrictLog(win, fac.nithVar(field.getIndex()));
	}
	logUpdate.log();

}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Test
public void testModelCountChanging() {

	// there are 260 possible paths from bottom left to top right on a 4x4
	// board
	int expectedModelCount = 260;

	Position p = PositionSquare.get(3, 0);
	Position q = PositionSquare.get(0, 3);

	BoardAnalizerPrototype analizer = new BoardAnalizerPrototype(
			PRIMITIVE_BOARD_PATHS_ALL);
	BDD path = analizer.getPath(p, q);
	int actual = path.allsat().size();
	assertEquals(expectedModelCount, actual);

	expectedModelCount = 58;
	BDDFactory fac = path.getFactory();
	BDD restricted = path.restrict(fac.ithVar(2).not());
	actual = restricted.allsat().size();
	analizer.done();
	path.free();
	restricted.free();
	assertEquals(expectedModelCount, actual);
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Override
protected void initialize(int nodenum, int cachesize) {
	factory = Factory.mk(nodenum, cachesize);
	//factory = Factory.mkER(nodenum, cachesize);
	// we set the default call-backs

	try {
		Method m = JavaBDDAdapterFactory.class.getDeclaredMethod
			("defaultResizeCallback", new Class[] { int.class, int.class });
		registerResizeCallback(this, m);

		m = JavaBDDAdapterFactory.class.getDeclaredMethod
			("defaultGCCallback", new Class[] { int.class, BDDFactory.GCStats.class });
		registerGCCallback(this, m);
	}
	catch (SecurityException | NoSuchMethodException e) {
		throw new RuntimeException("Unexpected exception " + e);
	}
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
/**
 * Constructs a {@link JBDDProvider} with the {@link Type} of the BDD library to use, a given number of variables,
 * the growth rate of the number of variables, and the initial number of nodes.
 * 
 * @param type
 *            the type of the BDD library
 * @param vars
 *            the number of variables
 * @param variableGrowthFactor
 *            the factor by which to extend the number of variables if required
 * @param initialNumberofNodes
 *            the initial number of nodes reserved in the BDD factory
 */
public JBDDProvider(Type type, int vars, int variableGrowthFactor, int initialNumberofNodes) {
	switch (type) {
	case JDD:
		factory = JDDFactory.init(initialNumberofNodes, initialNumberofNodes);
		break;
	default:
		factory = JFactory.init(initialNumberofNodes, initialNumberofNodes);
		factory.autoReorder(BDDFactory.REORDER_SIFT);
	}

	factory.setVarNum(vars);
	this.vars = vars;
	this.variableGrowthFactor = variableGrowthFactor;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
/**
 * Calls the logic synthesis flow
 * 
 * @return Status code:
 *         0: Everything okay
 *         1: Something failed
 */
private static int execute() {
    BDDFactory storage = JFactory.init(netlistNodesize, netlistNodesize / 4);
    storage.setCacheRatio(4f);

    TechLibrary tech = readTechnology(options.getTechnology(), config.defaultTech, storage);
    if(tech == null) {
        logger.error("No technology found");
        return 1;
    }

    Flow flow = new Flow(options, tech, storage);
    return flow.execute();
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Override
public BDD toBDD(BDDFactory fac, Map<TechVariable, Integer> map) {
    if(name.equals("0") || name.equals("CONST0")) {
        return fac.zero();
    } else if(name.equals("1") || name.equals("CONST1")) {
        return fac.one();
    } else if(!map.containsKey(this)) {
        int id = fac.extVarNum(1);
        map.put(this, id);
    }
    return fac.ithVar(map.get(this));
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Override
public BDD toBDD(BDDFactory fac, Map<TechVariable, Integer> map) {
    BDD tb = t.toBDD(fac, map);
    switch(op) {
        case not:
            return tb.not();
        default:
            System.err.println("Fehler BDD Unary OP unknown");
            return null;
    }
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
@Override
public BDD toBDD(BDDFactory fac, Map<TechVariable, Integer> map) {
    BDD t1b = t1.toBDD(fac, map);
    BDD t2b = t2.toBDD(fac, map);
    switch(op) {
        case and:
            return t1b.and(t2b);
        case or:
            return t1b.or(t2b);
        default:
            System.err.println("Fehler BDD Binary OP unknown");
            return null;
    }
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public PF2BDDParser(BDDFactory bddFactory, Map<String,Integer> variable2indexMap, long maxParsingTimeAllowed) {
	this.bddFactory = bddFactory;
	this.variable2indexMap = variable2indexMap;
	variables = new ArrayList<BooleanVariableInterface>();
	this.maxParsingTimeAllowed = maxParsingTimeAllowed;
	this.parsingTime = -1;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
public BDDGenerationStatisticsRecord(BDDFactory bddFactory , BDD bdd, String[] varOrder, int nodesCount) {
	this.bddFactory = bddFactory;
	this.bdd = bdd;
	this.varOrder = new String[varOrder.length];
	System.arraycopy(varOrder, 0, this.varOrder, 0, varOrder.length);
	this.nodesCount = nodesCount;
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
protected BDD createBDD(BDDFactory bddFactory, String orderingFormulasStrategy) throws Exception {
		
		if ( reorderMethod != BDDFactory.REORDER_NONE ) {
			super.initBDDReorder(getFeatureModel().countNodes());
		}
		
		BDD bdd = null;
		
		long start = System.currentTimeMillis();
		// create BDD based on Statistics (eg., best order, worst order)
		if ( searchType != null ) {
			if ( searchType == BEST_VARIABLE_ORDER || searchType == WORST_VARIABLE_ORDER) {
				bdd = createBDDBasedOnStatistics(searchType);
				this.heuristicRunningTime = 0;
			}
		}
		// create BDD based on FEATURE TREE TRAVERSAL HEURISTICS
		else if ( variableOrderingHeuristic != null ){
//			bddFactory.setVarNum(countFMNodes);
			varIndex2NameMap = variableOrderingHeuristic.run(toCNF());
			varName2IndexMap = VariableOrderingHeuristic.variableOrderingAsHashMap(varIndex2NameMap);
			bdd = createBDDStructure(start - (long)getHeuristicRunningTime(), orderingFormulasStrategy);
		}
		
		// root node is always true
		bdd.andWith(bddFactory.ithVar(varName2IndexMap.get(featureModel.getRoot().getID())));

		this.bddBuildingTime = System.currentTimeMillis() - start;
		
//		theOriginalBDD = bdd; 		
//		theWorkingBDD = theOriginalBDD;		
		return bdd;
	}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
protected void initBDDReorder(int countNodes) {		
	if ( reorderMethod != BDDFactory.REORDER_NONE ) {
		bddFactory.enableReorder();
		bddFactory.autoReorder(reorderMethod);
		// define each level of the BDD as an eligible SIFTING block
		if ( reorderMethod == BDDFactory.REORDER_SIFT || 
			 reorderMethod == BDDFactory.REORDER_SIFTITE || 
			 reorderMethod == BDDFactory.REORDER_RANDOM ){
			for( int i = 0 ; i < countNodes ; i++ ) {
				bddFactory.addVarBlock(bddFactory.ithVar(i), false);
			}
		}
	}
}
 

import net.sf.javabdd.BDDFactory; //导入依赖的package包/类
/**
 * Create a new presence condition manager.
 */
public PresenceConditionManager() {
  this.B = BDDFactory.init(5000000, 50000);
  this.vars = new Variables(B);
  this.stack = new LinkedList<BDD>();
  this.global = B.one();
  this.branch = null;
  this.notBranches = null;
  this.current = null;
}