mirror of https://github.com/YosysHQ/yosys.git
Merge branch 'YosysHQ:main' into main
This commit is contained in:
commit
d1f0c38bac
2
Makefile
2
Makefile
|
|
@ -169,7 +169,7 @@ ifeq ($(OS), Haiku)
|
|||
CXXFLAGS += -D_DEFAULT_SOURCE
|
||||
endif
|
||||
|
||||
YOSYS_VER := 0.51+17
|
||||
YOSYS_VER := 0.51+46
|
||||
YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
|
||||
YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1)
|
||||
YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)
|
||||
|
|
|
|||
|
|
@ -676,10 +676,10 @@ void ezSAT::preSolverCallback()
|
|||
bool ezSAT::solver(const std::vector<int>&, std::vector<bool>&, const std::vector<int>&)
|
||||
{
|
||||
preSolverCallback();
|
||||
fprintf(stderr, "************************************************************************\n");
|
||||
fprintf(stderr, "ERROR: You are trying to use the solve() method of the ezSAT base class!\n");
|
||||
fprintf(stderr, "*************************************************************************\n");
|
||||
fprintf(stderr, "ERROR: You are trying to use the solver() method of the ezSAT base class!\n");
|
||||
fprintf(stderr, "Use a dervied class like ezMiniSAT instead.\n");
|
||||
fprintf(stderr, "************************************************************************\n");
|
||||
fprintf(stderr, "*************************************************************************\n");
|
||||
abort();
|
||||
}
|
||||
|
||||
|
|
@ -1332,7 +1332,7 @@ void ezSAT::printInternalState(FILE *f) const
|
|||
fprintf(f, "\n");
|
||||
}
|
||||
if (cnfConsumed)
|
||||
fprintf(f, " *** more clauses consumed via cnfConsume() ***\n");
|
||||
fprintf(f, " *** more clauses consumed via consumeCnf() ***\n");
|
||||
|
||||
fprintf(f, "--8<-- snap --8<--\n");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1325,8 +1325,8 @@ struct ShareWorker
|
|||
|
||||
qcsat.ez->assume(qcsat.ez->AND(sub1, sub2));
|
||||
|
||||
log(" Size of SAT problem: %d variables, %d clauses\n",
|
||||
qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
|
||||
log(" Size of SAT problem: %zu cells, %d variables, %d clauses\n",
|
||||
qcsat.imported_cells.size(), qcsat.ez->numCnfVariables(), qcsat.ez->numCnfClauses());
|
||||
|
||||
if (qcsat.ez->solve(sat_model, sat_model_values)) {
|
||||
log(" According to the SAT solver this pair of cells can not be shared.\n");
|
||||
|
|
|
|||
Loading…
Reference in New Issue