Termination callback and boolector_pop()

[cdisselkoen]

It seems that the result from the termination callback is "sticky"/"permanent" even across push/pop. Meaning that if the termination callback ever returns nonzero (indicating to terminate), then all future calls to boolector_sat() will terminate without even bothering to call the termination callback - even if boolector_pop() is used to revert to a previous state. I'm not sure if this is an intended feature or not. For my use case, I would prefer if boolector_pop() would reset the termination state, so that the termination callback would be checked again for future operations after the pop.

Here's a code example of the behavior I'm observing:

#include <boolector.h>
#include <stdio.h>
#include <stdint.h>
#include <stdlib.h>

int32_t myterm(void* arg) {
  static bool first_time = true;
  if (first_time) {
    first_time = false;
    printf("returning 1\n");
    return 1;  // terminate the first time
  } else {
    printf("returning 0\n");
    return 0;  // then let it run indefinitely
  }
}

const char* describe_satresult(int32_t satresult) {
  switch (satresult) {
    case BOOLECTOR_SAT: return "SAT";
    case BOOLECTOR_UNSAT: return "UNSAT";
    case BOOLECTOR_UNKNOWN: return "UNKNOWN";
    default: return "unrecognized return code";
  }
}

int main(int argc, char* argv[]) {
  Btor* btor = boolector_new();
  boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
  boolector_set_term(btor, &myterm, NULL);

  printf("Boolector version: %s\n", boolector_version(btor));

  // just a bunch of nonsense so that the sat() query is nontrivial
  BoolectorSort sort = boolector_bitvec_sort(btor, 1024);
  BoolectorNode* bv0 = boolector_var(btor, sort, "bv0");
  BoolectorNode* bv1 = boolector_var(btor, sort, "bv1");
  BoolectorNode* sum = boolector_var(btor, sort, "sum");
  BoolectorNode* zero = boolector_zero(btor, sort);
  boolector_assert(btor, boolector_not(btor, boolector_eq(btor, sum, zero)));
  boolector_assert(btor, boolector_eq(btor, sum, boolector_add(btor, bv0, bv1)));
  BoolectorNode* bv2 = boolector_slice(btor, bv0, 1023, 512);
  BoolectorNode* bv3 = boolector_slice(btor, bv0, 511, 0);
  boolector_assert(btor, boolector_ugt(btor, bv2, bv3));
  BoolectorNode* bv4 = boolector_concat(btor, bv2, boolector_add(btor, bv2, bv3));

  boolector_push(btor, 1);
  boolector_assert(btor, boolector_ugt(btor, bv4, bv1));
  printf("first result: %s\n", describe_satresult(boolector_sat(btor)));
  boolector_pop(btor, 1);

  printf("second result: %s\n", describe_satresult(boolector_sat(btor)));
}

In this example, we have a termination callback which terminates the first query, but (theoretically) lets all future queries continue indefinitely. In main(), we make two calls to boolector_sat(), expecting the first to be terminated. After the first call is terminated, we use boolector_pop() to return to an earlier state and check for satisfiability there.

The output I get from running this code is

Boolector version: 3.2.0
returning 1
first result: UNKNOWN
second result: UNKNOWN

which indicates that both queries were terminated. Furthermore, the termination callback only prints once, indicating that the second call to boolector_sat() never even checked the termination callback. This is the behavior I'm wondering whether it's intended or a bug.

My intended use case is to implement per-sat()-call query timeouts. So, even if one query times out and is terminated by the callback, I'd like the ability to boolector_pop() and continue working with a different set of constraints. It's possible that the termination callback mechanism is not the correct tool for this purpose - if there's a different tool that would work better, I'd love to hear about it.

[mpreiner]

When we initially implemented termination support, we didn't think about incremental usage. As soon as the termination function returns true, we internally set a termination flag to true. We don't reset the flag. Having the termination callback per check-sat makes sense.
There are three options to add support for this:

• Add an option to enable reset after each check-sat call
• Add an additional reset flag to boolector_set_term to indicate whether the termination flag should be reset after check-sat
• Do not set a flag at all and only rely on the return value of the termination function

[aniemetz]

@mpreiner @andrewvaughanj do we plan to include this in #62? Is this already supported by #62?