Add LastEffort, when no more decisions
Quantifiers instantiate not eager triggers during LastEffort
Showing
- src_colibri2/core/demon.ml 20 additions, 18 deletionssrc_colibri2/core/demon.ml
- src_colibri2/core/demon.mli 10 additions, 10 deletionssrc_colibri2/core/demon.mli
- src_colibri2/core/egraph.ml 3 additions, 0 deletionssrc_colibri2/core/egraph.ml
- src_colibri2/core/egraph.mli 3 additions, 0 deletionssrc_colibri2/core/egraph.mli
- src_colibri2/core/events.ml 12 additions, 7 deletionssrc_colibri2/core/events.ml
- src_colibri2/core/events.mli 9 additions, 2 deletionssrc_colibri2/core/events.mli
- src_colibri2/solver/scheduler.ml 22 additions, 5 deletionssrc_colibri2/solver/scheduler.ml
- src_colibri2/theories/bool/boolean.ml 3 additions, 3 deletionssrc_colibri2/theories/bool/boolean.ml
- src_colibri2/theories/bool/equality.ml 5 additions, 5 deletionssrc_colibri2/theories/bool/equality.ml
- src_colibri2/theories/bool/uninterp.ml 2 additions, 2 deletionssrc_colibri2/theories/bool/uninterp.ml
- src_colibri2/theories/quantifier/quantifier.ml 61 additions, 19 deletionssrc_colibri2/theories/quantifier/quantifier.ml
Loading
Please register or sign in to comment