0

Is it possible to retract facts in Z3's datalog engine? The closest I can find in the documentation is Z3_fixedpoint_update_rule which I haven't been able to get to work the way I want.

I have seen other questions deal with retraction using check-sat-assuming (e.g. Incremental SMT solver with ability to drop specific constraint) Is there a corollary for the fixedpoint/datalog engine?

dropkick
  • 65
  • 5

1 Answers1

0

Short answer: no. Once facts are added, rules are pre-processed based on them, other facts are produced, etc, so right now there's no way of going back. I think only LogicBlox supports such feature.

Nuno Lopes
  • 868
  • 6
  • 13