Skip to content

Commit

Permalink
update(fildesh): with planned v0.2.0 deprecations
Browse files Browse the repository at this point in the history
  • Loading branch information
grencez committed Dec 12, 2023
1 parent f04342d commit 97dbaad
Show file tree
Hide file tree
Showing 18 changed files with 143 additions and 141 deletions.
5 changes: 5 additions & 0 deletions MODULE.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,11 @@ bazel_dep(name = "rules_license", version = "0.0.7")
bazel_dep(name = "mdd-glu", version = "2.4.0")
bazel_dep(name = "rules_peg", version = "0.1.18")

git_override(
module_name = "fildesh",
remote = "https://github.com/fildesh/fildesh.git",
commit="3d991055f1f5a8ebb77578fe2d5623c96a50480e",
)
git_override(
module_name = "mdd-glu",
remote = "https://github.com/ProtocolConvergence/mdd-glu.git",
Expand Down
2 changes: 1 addition & 1 deletion dep/cmake_fetchcontent/fildesh.cmake
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
FetchContent_Declare(
Fildesh
GIT_REPOSITORY "https://github.com/fildesh/fildesh.git"
GIT_TAG "80f50ea9d3f7439a92c6d627113a9a71e83505e6"
GIT_TAG "3d991055f1f5a8ebb77578fe2d5623c96a50480e"
)
FetchContent_MakeAvailable(Fildesh)
10 changes: 10 additions & 0 deletions src/cx/alphatab.h
Original file line number Diff line number Diff line change
Expand Up @@ -201,6 +201,16 @@ ccstr_of_AlphaTab (const AlphaTab* ts)
return ts->s;
}

static inline void put_AlphaTab_FildeshO(FildeshO* out, const AlphaTab* a) {
size_t n = a->sz;
if (n > 0 && a->s[n-1] == '\0') {
n -= 1;
}
if (n > 0) {
put_bytestring_FildeshO(out, (const unsigned char*)a->s, n);
}
}

qual_inline
void
copy_AlphaTab (AlphaTab* a, const AlphaTab* b)
Expand Down
6 changes: 3 additions & 3 deletions src/cx/sesp.c
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
SespCtx*
make_SespCtx ()
{
const FildeshKV empty_map = DEFAULT_FildeshKV_SINGLE_LIST;
const FildeshKV empty_map = DEFAULT_FildeshKV;
SespCtx* ctx = AllocT( SespCtx, 1 );
ctx->kindmap = empty_map;
ctx->nil.base.kind = 0;
Expand All @@ -17,7 +17,7 @@ make_SespCtx ()
void
free_SespCtx (SespCtx* ctx)
{
FildeshKV_id_t id;
FildeshKV_id id;
FildeshKV* map = &ctx->kindmap;
for (id = any_id_FildeshKV(map);
!fildesh_nullid(id);
Expand All @@ -42,7 +42,7 @@ ctx_of_Sesp (const Sesp a)
SespKind*
ensure_kind_SespCtx (SespCtx* ctx, const SespVT* vt)
{
FildeshKV_id_t id = ensuref_FildeshKV(&ctx->kindmap, vt, sizeof(*vt));
FildeshKV_id id = ensuref_FildeshKV(&ctx->kindmap, vt, sizeof(*vt));
SespKind* kind = (SespKind*) value_at_FildeshKV(&ctx->kindmap, id);
if (!kind) {
kind = make_SespKind(vt);
Expand Down
4 changes: 2 additions & 2 deletions src/pfmla.c
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
void
init1_PFmlaCtx (PFmlaCtx* ctx, const PFmlaVT* vt)
{
const FildeshKV empty_map = DEFAULT_FildeshKV_SINGLE_LIST;
const FildeshKV empty_map = DEFAULT_FildeshKV;
assert(vt->vbl_base_offset == 0);
init_FildeshAT(ctx->vbls);
ctx->vbl_map = empty_map;
Expand Down Expand Up @@ -827,7 +827,7 @@ add_vbl_PFmlaCtx (PFmlaCtx* ctx, const char* name, uint domsz)

{
char* key = strdup_FildeshAlloc(ctx->alloc, name);
const FildeshKV_id_t id = ensuref_FildeshKV(
const FildeshKV_id id = ensuref_FildeshKV(
&ctx->vbl_map, key, strlen(key)+1);
assign_memref_at_FildeshKV(&ctx->vbl_map, id, x);
x->name = key;
Expand Down
10 changes: 5 additions & 5 deletions src/pla.cc
Original file line number Diff line number Diff line change
Expand Up @@ -186,11 +186,11 @@ oput_protocon_pc_acts_espresso_spawn(std::ostream& out, const Xn::PcSymm& pc_sym
const char* const* argv)
{
int istat = 0;
fildesh_fd_t to_espresso_fd = -1;
fildesh_fd_t in_espresso_fd = -1;
fildesh_fd_t out_espresso_fd = -1;
fildesh_fd_t from_espresso_fd = -1;
fildesh_compat_pid_t pid = -1;
Fildesh_fd to_espresso_fd = -1;
Fildesh_fd in_espresso_fd = -1;
Fildesh_fd out_espresso_fd = -1;
Fildesh_fd from_espresso_fd = -1;
FildeshCompat_pid pid = -1;

// Names for variables.
std::vector<std::string> guard_vbls;
Expand Down
10 changes: 5 additions & 5 deletions src/satsyn/dimacs.h
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
oput_dimacs_CnfFmla(FildeshO* out, const CnfFmla* fmla)
{
CnfDisj clause[] = {DEFAULT_CnfDisj};
puts_FildeshO(out, "p cnf ");
putstrlit_FildeshO(out, "p cnf ");
print_int_FildeshO(out, (int)fmla->nvbls);
putc_FildeshO(out, ' ');
print_int_FildeshO(out, (int)fmla->idcs.sz);
Expand All @@ -19,7 +19,7 @@ oput_dimacs_CnfFmla(FildeshO* out, const CnfFmla* fmla)
print_int_FildeshO(out, (int)(1+clause->lits.s[j].vbl));
putc_FildeshO(out, ' ');
}
puts_FildeshO(out, "0\n");
putstrlit_FildeshO(out, "0\n");
}
lose_CnfDisj(clause);
}
Expand Down Expand Up @@ -67,10 +67,10 @@ extl_solve_CnfFmla (CnfFmla* fmla, bool* sat, BitTable evs)
const char* const z3_argv[] = {"z3", "-dimacs", "sat.in", NULL};
const char* const minisat_argv[] = {"minisat", "-verb=0", "sat.in", "sat.out", NULL};
const char* const* argv = (SatSolve_Z3 ? z3_argv : minisat_argv);
fildesh_fd_t out_solver_fd = -1;
fildesh_fd_t from_solver_fd = -1;
Fildesh_fd out_solver_fd = -1;
Fildesh_fd from_solver_fd = -1;
int istat = 0;
fildesh_compat_pid_t pid = -1;
FildeshCompat_pid pid = -1;
if (istat != 0) {
fildesh_log_error("Failed to create pipe for solver.");
}
Expand Down
8 changes: 4 additions & 4 deletions src/satsyn/encodesat.c
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ encode_sat(FMem_synsearch* tape)
DeclTableT( State, struct { TableT(XnSz) tx; TableT(XnSz) to; } );

FildeshAlloc* alloc = open_FildeshAlloc();
FildeshKV lstate_map[1] = {DEFAULT_FildeshKV_SINGLE_LIST};
FildeshKV xnmap[1] = {DEFAULT_FildeshKV_SINGLE_LIST};
FildeshKV pathmap[1] = {DEFAULT_FildeshKV_SINGLE_LIST};
FildeshKV lstate_map[1] = {DEFAULT_FildeshKV};
FildeshKV xnmap[1] = {DEFAULT_FildeshKV};
FildeshKV pathmap[1] = {DEFAULT_FildeshKV};

DeclTable( State, states );
CnfFmla fmla[] = {DEFAULT_CnfFmla};
Expand All @@ -109,7 +109,7 @@ encode_sat(FMem_synsearch* tape)
const XnSys* restrict sys = tape->sys;
XnRule* g;
TableT(XnSz)* may_rules;
FildeshKV_id_t kvid;
FildeshKV_id kvid;

lstate_map->alloc = alloc;
xnmap->alloc = alloc;
Expand Down
4 changes: 2 additions & 2 deletions src/satsyn/inst-sat3.h
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ inst_sat3_XnSys (const CnfFmla* fmla)
XnVbl sat = dflt_XnVbl ();
sat.domsz = 2;
truncate_FildeshO(name);
puts_FildeshO(name, "sat");
putstrlit_FildeshO(name, "sat");
putc_FildeshO(name, '\0');
assign_cstr_AlphaTab(&sat.name, name->at);
sat_idx = sys->vbls.sz;
Expand Down Expand Up @@ -302,7 +302,7 @@ inst_sat3_ring_XnSys (const CnfFmla* fmla, const bool use_sat)
sat->domsz = 2;

truncate_FildeshO(name);
puts_FildeshO(name, "sat");
putstrlit_FildeshO(name, "sat");
print_int_FildeshO(name, (int)r);
putc_FildeshO(name, '\0');
assign_cstr_AlphaTab(&sat->name, name->at);
Expand Down
4 changes: 2 additions & 2 deletions src/satsyn/instance.c
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ inst_bit3_XnSys(unsigned npcs)

ready_vbl.domsz = 2;
truncate_FildeshO(name);
puts_FildeshO(name, "ready");
putstrlit_FildeshO(name, "ready");
print_int_FildeshO(name, (int)r);
putc_FildeshO(name, '\0');
assign_cstr_AlphaTab(&ready_vbl.name, name->at);
Expand Down Expand Up @@ -312,7 +312,7 @@ inst_dijkstra4state_XnSys(unsigned npcs)

up_vbl.domsz = 2;
truncate_FildeshO(name);
puts_FildeshO(name, "up");
putstrlit_FildeshO(name, "up");
print_int_FildeshO(name, (int)r);
putc_FildeshO(name, '\0');
assign_cstr_AlphaTab(&up_vbl.name, name->at);
Expand Down
20 changes: 10 additions & 10 deletions src/satsyn/pla.c
Original file line number Diff line number Diff line change
Expand Up @@ -25,26 +25,26 @@ oput_pla_state_XnSys(FildeshO* out, const XnSys* sys, const luint sidx)
oput_pla_XnEVbl(out, &x);
}
putc_FildeshO(out, ' ');
puts_FildeshO(out, legit ? "01" : "10");
putstr_FildeshO(out, legit ? "01" : "10");
}

static
void
oput_pla_legit(FildeshO* out, const XnSys* sys)
{
puts_FildeshO(out, ".mv ");
putstrlit_FildeshO(out, ".mv ");
print_int_FildeshO(out, (int)sys->vbls.sz + 1);
puts_FildeshO(out, " 0");
putstrlit_FildeshO(out, " 0");
for (unsigned i = 0; i < sys->vbls.sz; ++i) {
putc_FildeshO(out, ' ');
print_int_FildeshO(out, (int)sys->vbls.s[i].domsz);
}
puts_FildeshO(out, " 2\n");
putstrlit_FildeshO(out, " 2\n");
for (unsigned i = 0; i < sys->nstates; ++i) {
oput_pla_state_XnSys(out, sys, i);
putc_FildeshO(out, '\n');
}
puts_FildeshO(out, ".e\n");
putstrlit_FildeshO(out, ".e\n");
}

static
Expand Down Expand Up @@ -74,9 +74,9 @@ oput_pla_pc(FildeshO* out, const XnPc* pc, const XnSys* sys,
const TableT(XnRule) rules)
{
const unsigned pcidx = IdxEltTable (sys->pcs, pc);
puts_FildeshO(out, ".mv ");
putstrlit_FildeshO(out, ".mv ");
print_int_FildeshO(out, (int)pc->vbls.sz + pc->nwvbls);
puts_FildeshO(out, " 0");
putstrlit_FildeshO(out, " 0");
for (unsigned i = 0; i < pc->vbls.sz; ++i) {
putc_FildeshO(out, ' ');
print_int_FildeshO(out, (int)sys->vbls.s[pc->vbls.s[i]].domsz);
Expand All @@ -90,11 +90,11 @@ oput_pla_pc(FildeshO* out, const XnPc* pc, const XnSys* sys,
putc_FildeshO(out, '#');
for (unsigned i = 0; i < pc->vbls.sz; ++i) {
putc_FildeshO(out, ' ');
puts_FildeshO(out, ccstr_of_AlphaTab(&sys->vbls.s[pc->vbls.s[i]].name));
print_name_of_XnVbl_FildeshO(out, &sys->vbls.s[pc->vbls.s[i]]);
}
for (unsigned i = 0; i < pc->nwvbls; ++i) {
putc_FildeshO(out, ' ');
puts_FildeshO(out, ccstr_of_AlphaTab(&sys->vbls.s[pc->vbls.s[i]].name));
print_name_of_XnVbl_FildeshO(out, &sys->vbls.s[pc->vbls.s[i]]);
putc_FildeshO(out, '\'');
}
putc_FildeshO(out, '\n');
Expand All @@ -107,7 +107,7 @@ oput_pla_pc(FildeshO* out, const XnPc* pc, const XnSys* sys,
putc_FildeshO(out, '\n');
}
}
puts_FildeshO(out, ".e\n");
putstrlit_FildeshO(out, ".e\n");
}

bool
Expand Down
Loading

0 comments on commit 97dbaad

Please sign in to comment.