mirror of
https://github.com/YosysHQ/yosys
synced 2026-02-14 12:51:48 +00:00
53 lines
1.4 KiB
C++
53 lines
1.4 KiB
C++
#include "kernel/yosys.h"
|
|
#include "libs/ezsat/ezcmdline.h"
|
|
|
|
USING_YOSYS_NAMESPACE
|
|
PRIVATE_NAMESPACE_BEGIN
|
|
|
|
struct EzCmdlineTestPass : public Pass {
|
|
EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
|
|
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
|
{
|
|
std::string cmd;
|
|
size_t argidx = 1;
|
|
|
|
while (argidx < args.size()) {
|
|
if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
|
|
cmd = args[argidx + 1];
|
|
argidx += 2;
|
|
continue;
|
|
}
|
|
break;
|
|
}
|
|
|
|
extra_args(args, argidx, design);
|
|
|
|
if (cmd.empty())
|
|
log_error("Missing -cmd <solver> argument.\n");
|
|
|
|
ezCmdlineSAT sat(cmd);
|
|
sat.non_incremental();
|
|
|
|
// assume("A") adds a permanent CNF clause "A".
|
|
sat.assume(sat.VAR("A"));
|
|
|
|
std::vector<int> model_expressions;
|
|
std::vector<bool> model_values;
|
|
model_expressions.push_back(sat.VAR("A"));
|
|
|
|
// Expect SAT with A=true.
|
|
if (!sat.solve(model_expressions, model_values))
|
|
log_error("ezCmdlineSAT SAT case failed.\n");
|
|
if (model_values.size() != 1 || !model_values[0])
|
|
log_error("ezCmdlineSAT SAT model mismatch.\n");
|
|
|
|
// Passing NOT("A") here adds a temporary unit clause for this solve call,
|
|
// so the solver sees A && !A and must return UNSAT.
|
|
if (sat.solve(model_expressions, model_values, sat.NOT("A")))
|
|
log_error("ezCmdlineSAT UNSAT case failed.\n");
|
|
|
|
log("ezcmdline_test passed!\n");
|
|
}
|
|
} EzCmdlineTestPass;
|
|
|
|
PRIVATE_NAMESPACE_END
|