Track inference id for pending facts in strings (#4331)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 18 Apr 2020 22:47:31 +0000 (17:47 -0500)
committerGitHub <noreply@github.com>
Sat, 18 Apr 2020 22:47:31 +0000 (17:47 -0500)
commit15be4ec678fc59760add75c675efd81c32b8573b
tree2f1542fb4e72c8a31bc92530f658da24c3c31dc4
parent55497dfdff15f4bb3d839f64a7baa46c3aa84266
Track inference id for pending facts in strings (#4331)

This improves our tracking of pending inferences in strings so that we record pending inferences as a triple (id, fact, exp). This will ensure that proof steps can be constructed at the time we decide to process facts. It also inlines the sendInfer method into sendInference for simplicity.

This also improves the policy for reference counting facts and their explanations: we add them to d_keep when they are added to the equality engine. Previously, we were adding them when they were registered as pending. This means we would collect facts in this pending set that were added but later abandoned, which is unnecessary.
src/theory/strings/inference_manager.cpp
src/theory/strings/inference_manager.h