I would like to add a “save knowledgebase” and “load knowledgebase” functionality to my program.
I would like to be able to save the knowledgebase of my program (contains both dynamic and thread_local predicates) to a list e.g. knowledgebase_snapshot(I, L)
where L is a list of all predicates in the knowledgebase when knowledgebase_snapshot/2 is asserted, and I being an ID.
I then would like to be able to load a knowledgebase which overwrites the current knowledgebase using the already-saved knowledgebase_snapshot(I, L).
My program’s execution is roughly the following:
Load the graph-based problem to solve, and perform some work resulting in asserting new predicates in the knowledgebase.
“Save the knowledgebase”.
Make some “smart” manipulations of the graph, discover useful facts, and assert them in the knowledgebase.
Attempt solving the problem: if problem is solved or a timeout is reached, we are done; else “Load the knowledgebase” and go back to the previous step.
It is quite late for me to change my program logic and avoid using assertions, and I am not even sure if I can do that with my Prolog skills.
So what is available in SWI’s toolbox to enable me to do the save and load functionality?
I thought about exporting the result of listing/0 to a file (save) and consulting it (load), but I cannot afford a lot of file IO wasted time since the number of my “smart” manipulations requiring load and save is not exactly small.
I also thought about creating lists that store the arguments of my dynamic predicates (the save functionality); and when I want to load the knowledgebase, I retract all my dynamic predicates and re-assert them by looking up the saved lists (the load functionality).
You can do that using transaction/1 Does require the development versions.
That works, but better simply use write_canonical/1 to dump the facts and just read_term/2 with assertz/1 to restore the data. That is a lot faster. In theory we could provide access to the primitives that write .qlf files to dump the clauses as VM code and load it. The save is about as expensive (rough guess), but the loading is about 20 times faster.
The program program basically does stuff until the point goal. Then it makes a single assert, after which it continues execution (calls p2/1).
What I need is that if the first choice of goal/0 fails, the second choice starts with only p1(a) and p2(b) asserted. However, in this case, p1(c) is also asserted as shown in the the following.
As can be seen, the knowledgebase – when executing the second choice of goal/0 – already contains p1(c), but I want it to discard all asserts made in the first choice of goal/0.
I was more thinking about the code below. Note that the first clause commits as you cannot decide to accept a transaction and later roll it back anyway.
It doesn’t deal with saving a snapshot and returning to this. It targets at tracking the changes to a dynamic predicate and maintain a file that allows for restoring the final state.
P.s. It should probably also be extended to use the assert/retract hooks to simply track normal assert/retract instead of defining its own modification operations. That would simplify adding/removing persistency.
Wow, awesome, you guys thought about implementing everything Transaction is working for my purposes!
I have a few of questions:
Does transaction work with both dynamic and thread_local predicates?
Can it co-exist with tabling? Maybe the answer here is obvious, but because of my lack of a solid background on tabling and transactions, I am imagining them as two beasts put next to each other and I wonder if they can work together.
Does “Run Goal as once/1 in a transaction” in the help page on transaction/1 mean that I can only get one solution for the goal inside the transaction? Why is that?
I am also keen on the assert_backtrackable/1 you kindly suggested:
The page on assertz/2 says that when assertion is made, a reference is created and unified with some handle that can be used to access the clause through e.g. erase/1. But when I attempt to use it, I get a warning about singleton Ref at consult-time and and error about “Arguments are not sufficiently instantiated” in erase/1 at runtime. Any thoughts?
I may be blanking here on something – but how (or why) is Ref bound when the execution thread gets to erase after backtracking away from assertz(Term, Ref) …
What is the general mechanism of variable binding doing here
Edit:
There are a few things going on – at least in theory:
assertz has a side effect – an asserted Term w/ an allocated reference, that is not undone upon backtracking
Ref is bound to that reference and the binding is not undone
erase undoes the term referred to by the bound Ref
What is the status of Ref after erase – is it still bound to the now, non-existing Term? – say, if yet another backtracking branch is disjointedly added.
AFAIK, yes. Transactions are thread-specific anyway, so this is more or less automatic.
Not yet. Well, there are some bits and pieces I’m exploring with people at CMU. Ultimately I’d like that to work seamlessly. There are quite a few scenarios though and it isn’t all that clear how these should be handled.
Yes. Why? Well, the interaction between going in/out of the transaction and rollback/commit seem pretty complicated. It might be doable but it certainly wasn’t the original intend with transactions. They are primarily there to get atomic state transitions. But, there are alternatives: start a thread running a transaction and while inside the transaction, make it talk to a thread outside the transaction. Now we can exchange answers and ask the thread inside the transaction to backtrack, finish with success or failure, etc.
Another option might be combining engines and transactions. That might not be possible right now though