+ void expressions2literals() {
+ int i;
+ struct symbol *sym;
+ struct property *prop;
+
+ for_all_symbols(i, sym) {
+ if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
+ sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
+ expr2literal(sym->dir_dep.expr);
+
+ for_all_properties(sym, prop, P_SELECT) {
+ assert(prop->expr->type == E_SYMBOL);
+ prop->visible.expr = expr_eliminate_eq_yn(prop->visible.expr);
+ expr2literal(prop->visible.expr);
+ }
+ }
+ }
+ }
+
+ void expressions2clauses() {
+ // Tseitin Transformation - see https://en.wikipedia.org/wiki/Tseitin_transformation
+ // or http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
+ for (auto expr: expressions) {
+ SatExpr e = expr.first;
+ sat_id e_id = expr.second;
+ switch (e.op) {
+ case E_SYMBOL:
+ case E_NONE:
+ assert(0);
+ break;
+ case E_NOT:
+ clauses.push_back(SatClause{ e_id, e.left });
+ clauses.push_back(SatClause{ -e_id, -e.left });
+ break;
+ case E_OR:
+ clauses.push_back(SatClause{ -e.left, e_id });
+ clauses.push_back(SatClause{ -e.right, e_id });
+ clauses.push_back(SatClause{ -e_id, e.left, e.right });
+ break;
+ case E_AND:
+ clauses.push_back(SatClause{ -e_id, e.left });
+ clauses.push_back(SatClause{ -e_id, e.right });
+ clauses.push_back(SatClause{ -e.left, -e.right, e_id });
+ break;
+ case E_EQUAL:
+ clauses.push_back(SatClause{ -e_id, -e.left, e.right });
+ clauses.push_back(SatClause{ -e_id, -e.right, e.left });
+ clauses.push_back(SatClause{ -e.left, -e.right, e_id });
+ clauses.push_back(SatClause{ e.left, e.right, e_id });
+ break;
+ case E_UNEQUAL:
+ case E_LTH:
+ case E_LEQ:
+ case E_GTH:
+ case E_GEQ: {
+ fprintf(stderr, "Comparison operators not implemented\n");
+ //exit(EXIT_FAILURE);
+ break;
+ }
+ case E_LIST:
+ fprintf(stderr, "LIST not implemented\n");
+ exit(EXIT_FAILURE);
+ break;
+ case E_RANGE:
+ fprintf(stderr, "RANGE not implemented\n");
+ exit(EXIT_FAILURE);
+ break;
+ }
+ }
+
+ }
+