Augmentation consistent with model and incrementality / undoing augmentations

[salmans]

The current implementation of augmentation doesn't preserve the facts that are already true in the model that is being augmented. For example consider the following theory: exists x . P(x) | exists x . Q(x)

A model containing a single fact P(e^0) satisfies the theory. Now, if we augment this model with a fact P(e^1), the SMT solver may find a model containing P(e^1) and Q(e^1), which is a model of the theory; however, the new model is not in the homomorphism cone of the first model, containing P(e^0).

@ryandanas , the solve this problem, we must send all facts in the current model as new constraints to the SMT solver. In the example above, we must add a new constraint Truth -> P(e^0) that requires P(e^0) to be true in the returning model. This makes the augmentation process more complicated; so, it may be a good idea to push some of the complexities in REPL down to the SMT solver. One idea is to add a new function satAugment to the interface of SAT, which captures the interaction with the SMT solver during augmentation. Alternatively, we may still want the REPL to coordinate everything, in which case, we can add a function satAddModelConstraints: since the SAT layer already saves the last returned solution, we can use the last solution to generate the extra constrains. Accordingly, satAddModelConstraint accepts the current iterator and returns a new iterator after adding the additional constraints. I personally like the first solution. Any ideas?

[thedotmatrix]

@salmans I added the satAugment function to the SAT.Data/SAT.Impl definitions.

However, in both SBV and SMTLib2, I am unsure how to assert the constraint to include the clauses of the last result in the next result. I did define the function addResultToContext in both libraries; right now it just returns the same context/container.

I'm assuming making the change would be trivial for you to do. Would you be willing to checkout my feature branch, make the change, and commit/push it if you have the time?

Thanks.

[salmans]

No problem. I'll write the function.

[thedotmatrix]

Right now, we really don't have functions to support the process of augmentation incrementally in the chase / sat implementations...

Given a current model, augment the current base, G, and provenance with a user observation Resume the chase to get the *differences in the original propositional theory AND the fully updated base, G, provenance, etc Then add *only the changes to the prop theory to the SAT iterator and also have that SAT iterator respect the clauses in the previously generated solution.

[salmans]

OK, the Chase and SAT interfaces are now ready for fixing this bug. The thing that is left to do is to implement the augmentation and backtracking functions. Other features seem to be working fine.

[thedotmatrix]

@salmans I updated the aug repl command to call the changes. Right now, no augmented models are being returned. I tried to mark exactly where the issue is inside the API.Surface module. Issue related functions in API.Core are augmentChase, augmentBase, and upModel.

I can't tell if I updated the ChaseState/Iterator inproperly, or if there is a bug with the augmentation core implementation. If you have any questions, feel free to email me.

[salmans]

I found the bug. It is in the additional constraints that are added to enforce consistency with the model being augmented. I am working on it.

[salmans]

The bug is fixed now. It took me a while to figure out what was going wrong: a false had to be changed to true!

[thedotmatrix]

Similar to satAugment, satBacktrack does not seem to be returning models with the augmentations removed. If you need to go over the code together, let me know.

[salmans]

@ryandanas I guess I know what is going wrong here but because you are more familiar with the design of REPL and API, I think you can fix the bug more quickly and in a way that is consistent with the overall design:

1. I didn't see any calls to satPop before calling satBacktrack. If I remember correctly, the last time that we talked, we decided to temporarily call satPush and satPop outside of SAT.
2. After I added satPopto modelDown (I am not sure if that's the right place to call the function considering the design of REPL and API) I get an error message from the SAT layer that suggests that the iterator being passed to modelDown is not the previous iterator, before applying augmentation.

I am not sure if the second bug is exactly caused because of using the wrong iterator but I think you should have a look at the code before I start working on the wrong way of fixing it! Notice that although iterators share the same pipe to interact with the solver, each iterator has an internal state (which is mostly used to translate SMT results to Razor models) which has to be kept track of inside the augmentation stack.

[thedotmatrix]

I think I fixed this issue, but I want to discuss exactly which iterators are being pushed / augmented / popped / backtracked before closing this.

[salmans]

I totally agree

[thedotmatrix]

So undo can actually support undoing the last augmentation, and any next commands. I have to update it to actually backtrack that far.