Boolector C API documentation

Interface

• C Interface
  • Macros
  • Typedefs
  • Functions
  • Deprecated

Quickstart

First, create a Boolector instance:

Btor *btor = boolector_new ();

You can configure this instance via boolector_set_opt() E.g., if you want to enable model generation:

boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);

For a detailed description of all configurable options, see boolector_set_opt().

Next you can either parse an input file, and/or generate expressions to be either asserted via boolector_assert(), or, if incremental usage is enabled, assumed via boolector_assume() (analogously to MiniSAT). Note that Boolector’s internal design is motivated by hardware design, hence we do not distinguish between type Boolean and type bit vector of length 1.

E.g., if you want to parse an input file “example.btor”, you can either use boolector_parse() or boolector_parse_btor():

char *error_msg;
int status;
int result;
FILE *fd = fopen ("example.btor", "r");
result = boolector_parse_btor (btor, fd, "example.btor", &error_msg, &status);

Incremental usage is not enabled, hence, if the parser does not encounter an error, it returns BOOLECTOR_UNKNOWN (for a more detailed description of the parsers return values, see boolector_parse()). However, if the parser encounters an error, it returns BOOLECTOR_PARSE_ERROR and an explanation of that error is stored in error_msg. If the input file specifies a (known) status of the input formula (either satisfiable or unsatisfiable), that status is stored in status.

As an example for generating and asserting expressions via boolector_assert(), consider the following example:

0 < x <= 100, 0 < y <= 100, x * y < 100

Given the Boolector instance created above, we generate and assert the following expressions:

BtorNode *x = boolector_var (btor, 8, "x");
BtorNode *y = boolector_var (btor, 8, "y");
BtorNode *zero = boolector_zero (btor, 8);
BtorNode *hundred = boolector_int (btor, 100, 8);

// 0 < x
BoolectorNode *ult_x = boolector_ult (btor, zero, x);
boolector_assert (btor, ult_x);

// x <= 100
BtorNode *ulte_x = boolector_ulte (btor, x, hundred);
boolector_assert (btor, ulte_x);

// 0 < y
BtorNode *ult_y = boolector_ult (btor, zero, y);
boolector_assert (btor, ult_y);

// y <= 100
BtorNode *ulte_y = boolector_ulte (btor, y, hundred);
boolector_assert (btor, ulte_y);

// x * y
BtorNode *mul = boolector_mul (btor, x, y);

// x * y < 100
BtorNode *ult = boolector_ult (btor, mul, hundred);
boolector_assert (btor, ult);
BtorNode *umulo = boolector_umulo (btor, x, y);
BtorNode *numulo = boolector_not (btor, umulo);  // prevent overflow
boolector_assert (btor, numulo)

After parsing an input file and/or asserting/assuming expressions, the satisfiability of the resulting formula can be determined via boolector_sat(). If the resulting formula is satisfiable and model generation has been enabled via boolector_set_opt(), you can either print the resulting model via boolector_print_model(), or query assignments of bit vector and array variables or uninterpreted functions via boolector_bv_assignment(), boolector_array_assignment() and boolector_uf_assignment(). Note that querying assignments is not limited to variables—you can query the assignment of any arbitrary expression.

E.g., given the example above, we first determine if the formula is satisfiable via boolector_sat() (which it is):

int result = boolector_sat (btor);

Now you can either query the assignments of variables x and y:

char *xstr = boolector_bv_assignment (btor, x);  // returns "00000100"
char *ystr = boolector_bv_assignment (btor, y);  // returns "00010101"

or print the resulting model via boolector_print_model(). Boolector supports printing models in its own format (“btor”) or in SMT-LIB v2 format (“smt2”). Printing the resulting model in Boolector’s own format:

boolector_print_model (btor, "btor", stdout);

A possible model would be:

2 00000100 x
3 00010101 y

which in this case indicates the assignments of bit vector variables x and y. Note that the first column indicates the id of an input, the second column its assignment, and the third column its name (or symbol) if any. In the case that the formula includes arrays as input, their values at a certain index are indicated as follows:

4[00] 01 A

where A has id 4 and is an array with index and element bit width of 2, and its value at index 0 is 1.

Printing the above model in SMT-LIB v2 format:

boolector_print_model (btor, "smt2", stdout);

A possible model would be:

(model
  (define-fun x () (_ BitVec 8) #b00000100)
  (define-fun y () (_ BitVec 8) #b00010101)
  (define-fun y (
   (y_x0 (_ BitVec 2)))
   (ite (= y_x0 #b00) #b01
     #00))
)

Note that Boolector internally represents arrays as uninterpreted functions, hence array models are printed as models for UF (without an explicit typecast).

Finally, in case that you generated expressions, you have to clean up, i.e., release those expressions (see Internals and boolector_release()), and delete Boolector instance btor via boolector_delete(). E.g., following from the example above, we proceed as follows:

boolector_release (btor, x);
boolector_release (btor, y);
boolector_release (btor, zero);
boolector_release (btor, hundred);
boolector_release (btor, ult_x);
boolector_release (btor, ulte_x);
boolector_release (btor, ult_y);
boolector_release (btor, ulte_y);
boolector_release (btor, mul);
boolector_release (btor, ult);
boolector_release (btor, numulo);
boolector_release (btor, umulo);
boolector_delete (btor);

Note that in case you generated assignment strings you have to release them as well:

boolector_free_bv_assignment (btor, xstr);
boolector_free_bv_assignment (btor, ystr);

Options

Boolector can be configured either via boolector_set_opt(), or via environment variables of the form:

BTOR<capitalized option name without '_' and ':'>=<value>

E.g., given a Boolector instance btor, model generation is enabled either via

boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);

or via setting the environment variable:

BTORMODELGEN=1

For a list and detailed descriptions of all available options, see boolector_set_opt().

API Tracing

API tracing allows to record every call to Boolector’s public API. The resulting trace can be replayed and the replayed sequence behaves exactly like the original Boolector run. This is particularly useful for debugging purposes, as it enables replaying erroneous behaviour. API tracing can be enabled either via boolector_set_trapi() or by setting the environment variable BTORAPITRACE=<filename>.

E.g., given a Boolector instance btor, enabling API tracing is done as follows:

FILE *fd = fopen ("error.trace", "r");
boolector_set_trapi (btor, fd);

or

BTORAPITRACE="error.trace"

Internals

Boolector internally maintains a directed acyclic graph (DAG) of expressions. As a consequence, each expression maintains a reference counter, which is initially set to 1. Each time an expression is shared, i.e. for each API call that returns an expression (a BoolectorNode), its reference counter is incremented by 1. Not considering API calls that generate expressions, this mainly applies to boolector_copy(), which simply increments the reference counter of an expression, and boolector_match_node() resp. boolector_match_node_by_id(), which retrieve nodes of a given Boolector instance by id resp. a given node’s id. Expressions are released via boolector_release(), and if its reference counter is decremented to zero, it is deleted from memory. Note that by asserting an expression, it will be permanently added to the formula, i.e. Boolector internally holds its reference until it is either eliminated via rewriting, or the Boolector instance is deleted. Following from that, it is safe to release an expression as soon as you asserted it, as long as you don’t need it for further querying.

Operators

Boolector internally describes expressions by means of a set of base operators as documented in BTOR. Boolector’s API, however, provides a richer set of operators for convenience, where non-base operators are internally rewritten to use base operators only. E.g., two’s complement (boolector_neg()) is rewritten as one’s complement and addition of 1. Note that this behaviour is not influenced by the rewrite level chosen.

Rewriting

Boolector simplifies expressions and the expression DAG by means of rewriting and supports three so-called rewrite levels. Increasing rewrite levels increase the extent of rewriting performed, and a rewrite level of 0 is equivalent to disabling rewriting at all. Note that Boolector not only simplifies expressions during construction of the expression DAG—for each call to boolector_sat(), various simplification techniques and rewriting phases are initiated. You can force Boolector to initiate rewriting and simplify the expression DAG via boolector_simplify(). The rewrite level can be configured via boolector_set_opt().

Examples

Bit vector examples

#include "boolector.h"
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

#define BV1_EXAMPLE_NUM_BITS 8

/* We verify the XOR swap algorithm. The XOR bitwise operation can
 * be used to swap variables without using a temporary variable:
 * int x, y;
 * ...
 * x = x ^ y
 * y = x ^ y
 * x = x ^ y
 */

int
main (void)
{
  Btor *btor;
  BoolectorNode *x, *y, *temp, *old_x, *old_y, *eq1, *eq2, *and, *formula;
  BoolectorSort s;
  int result;

  btor = boolector_new ();
  s = boolector_bitvec_sort (btor, BV1_EXAMPLE_NUM_BITS);
  x = boolector_var (btor, s, NULL);
  y = boolector_var (btor, s, NULL);

  /* remember initial values of x and y */
  old_x = boolector_copy (btor, x);
  old_y = boolector_copy (btor, y);

  /* x = x ^ y */
  temp = boolector_xor (btor, x, y);
  boolector_release (btor, x);
  x = temp;

  /* y = x ^ y */
  temp = boolector_xor (btor, x, y);
  boolector_release (btor, y);
  y = temp;

  /* x = x ^ y */
  temp = boolector_xor (btor, x, y);
  boolector_release (btor, x);
  x = temp;

  /* Now, we have to show that old_x = y and old_y = x */
  eq1 = boolector_eq (btor, old_x, y);
  eq2 = boolector_eq (btor, old_y, x);
  and = boolector_and (btor, eq1, eq2);

  /* In order to prove that this is a theorem, we negate the whole
   * formula and show that the negation is unsatisfiable */
  formula = boolector_not (btor, and);

  /* We assert the formula and call Boolector */
  boolector_assert (btor, formula);
  result = boolector_sat (btor);
  if (result == BOOLECTOR_UNSAT)
    printf ("Formula is unsatisfiable\n");
  else
    abort ();

  /* cleanup */
  boolector_release (btor, x);
  boolector_release (btor, old_x);
  boolector_release (btor, y);
  boolector_release (btor, old_y);
  boolector_release (btor, eq1);
  boolector_release (btor, eq2);
  boolector_release (btor, and);
  boolector_release (btor, formula);
  boolector_release_sort (btor, s);
  assert (boolector_get_refs (btor) == 0);
  boolector_delete (btor);
  return 0;
}

#include "boolector.h"
#include "btoropt.h"
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

#define BV2_EXAMPLE_NUM_BITS 8

/* We try to show the following theorem:
 * v1 > 0 & v2 > 0  =>  v1 + v2 > 0
 *
 * The theorem is valid if v1 and v2 are naturals, but not if they
 * are two's complement bit-vectors as addition can overflow.
 */

int
main (void)
{
  Btor *btor;
  BoolectorNode *v1, *v2, *add, *zero, *vars_sgt_zero, *impl;
  BoolectorNode *v1_sgt_zero, *v2_sgt_zero, *add_sgt_zero, *formula;
  BoolectorSort s;
  const char *assignments[10];
  int result, i;

  btor = boolector_new ();
  sort = boolector_bitvec_sort (btor, BV2_EXAMPLE_NUM_BITS);
  boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);

  s = boolector_bitvec_sort (btor, BV2_EXAMPLE_NUM_BITS);
  v1 = boolector_var (btor, s, NULL);
  v2 = boolector_var (btor, s, NULL);
  zero = boolector_zero (btor, s);

  v1_sgt_zero = boolector_sgt (btor, v1, zero);
  v2_sgt_zero = boolector_sgt (btor, v2, zero);
  vars_sgt_zero = boolector_and (btor, v1_sgt_zero, v2_sgt_zero);

  add = boolector_add (btor, v1, v2);
  add_sgt_zero = boolector_sgt (btor, add, zero);

  impl = boolector_implies (btor, vars_sgt_zero, add_sgt_zero);

  /* We negate the formula and try to show that the negation is unsatisfiable */
  formula = boolector_not (btor, impl);

  /* We assert the formula and call Boolector */
  boolector_assert (btor, formula);
  result = boolector_sat (btor);
  if (result == BOOLECTOR_SAT)
    printf ("Instance is satisfiable\n");
  else
    abort ();

  /* The formula is not valid, we have found a counter-example.
   * Now, we are able to obtain assignments to arbitrary expressions */
  i = 0;
  assignments[i++] = boolector_bv_assignment (btor, zero);
  assignments[i++] = boolector_bv_assignment (btor, v1);
  assignments[i++] = boolector_bv_assignment (btor, v2);
  assignments[i++] = boolector_bv_assignment (btor, add);
  assignments[i++] = boolector_bv_assignment (btor, v1_sgt_zero);
  assignments[i++] = boolector_bv_assignment (btor, v2_sgt_zero);
  assignments[i++] = boolector_bv_assignment (btor, vars_sgt_zero);
  assignments[i++] = boolector_bv_assignment (btor, add_sgt_zero);
  assignments[i++] = boolector_bv_assignment (btor, impl);
  assignments[i++] = boolector_bv_assignment (btor, formula);

  i = 0;
  printf ("Assignment to 0: %s\n", assignments[i++]);
  printf ("Assignment to v1: %s\n", assignments[i++]);
  printf ("Assignment to v2: %s\n", assignments[i++]);
  printf ("Assignment to v1 + v2: %s\n", assignments[i++]);
  printf ("Assignment to v1 > 0: %s\n", assignments[i++]);
  printf ("Assignment to v2 > 0: %s\n", assignments[i++]);
  printf ("Assignment to v1 > 0 & v2 > 0: %s\n", assignments[i++]);
  printf ("Assignment to v1 + v2 > 0: %s\n", assignments[i++]);
  printf ("Assignment to v1 > 0 & v2 > 0  => v1 + v2 > 0: %s\n",
	  assignments[i++]);
  printf ("Assignment to !(v1 > 0 & v2 > 0  => v1 + v2 > 0): %s\n",
	  assignments[i++]);
  for (i = 0; i < 10; i++)
    boolector_free_bv_assignment (btor, assignments[i]);

  /* cleanup */
  boolector_release (btor, zero);
  boolector_release (btor, v1);
  boolector_release (btor, v2);
  boolector_release (btor, add);
  boolector_release (btor, impl);
  boolector_release (btor, formula);
  boolector_release (btor, v1_sgt_zero);
  boolector_release (btor, v2_sgt_zero);
  boolector_release (btor, vars_sgt_zero);
  boolector_release (btor, add_sgt_zero);
  boolector_release_sort (btor, s);
  assert (boolector_get_refs (btor) == 0);
  boolector_delete (btor);
  return 0;
}

Array examples

#include "boolector.h"
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

#define ARRAY1_EXAMPLE_ELEM_BW 8
#define ARRAY1_EXAMPLE_INDEX_BW 3
#define ARRAY1_EXAMPLE_ARRAY_SIZE (1 << ARRAY1_EXAMPLE_INDEX_BW)

/* We verify the following linear search algorithm. We iterate over an array
 * and compute a maximum value as the following pseudo code shows:
 *
 * unsigned int array[ARRAY_SIZE];
 * unsigned int max;
 * int i;
 * ...
 * max = array[0];
 * for (i = 1; i < ARRAY_SIZE; i++)
 *   if (array[i] > max)
 *     max = array[i]
 *
 * Finally, we prove that it is not possible to find an array position
 * such that the value stored at this position is greater than 'max'.
 * If we can show this, we have proved that this algorithm indeed finds
 * a maximum value. Note that we prove that the algorithm finds an
 * arbitrary maximum (multiple maxima are possible), not necessarily
 * the first maximum.
 */

int
main (void)
{
  Btor *btor;
  BoolectorNode *array, *read, *max, *temp, *ugt, *formula, *index;
  BoolectorNode *indices[ARRAY1_EXAMPLE_ARRAY_SIZE];
  BoolectorSort sort_elem, sort_index, sort_array;
  int i, result;

  btor = boolector_new ();
  sort_index = boolector_bitvec_sort (btor, ARRAY1_EXAMPLE_INDEX_BW);
  sort_elem = boolector_bitvec_sort (btor, ARRAY1_EXAMPLE_ELEM_BW);
  sort_array = boolector_array_sort (btor, sort_index, sort_elem);

  /* We create all possible constants that are used as read indices */
  for (i = 0; i < ARRAY1_EXAMPLE_ARRAY_SIZE; i++)
    indices[i] = boolector_int (btor, i, sort_index);

  array = boolector_array (btor, sort_array, 0);
  /* Current maximum is first element of array */
  max = boolector_read (btor, array, indices[0]);
  /* Symbolic loop unrolling */
  for (i = 1; i < ARRAY1_EXAMPLE_ARRAY_SIZE; i++)
    {
      read = boolector_read (btor, array, indices[i]);
      ugt = boolector_ugt (btor, read, max);
      /* found a new maximum? */
      temp = boolector_cond (btor, ugt, read, max);
      boolector_release (btor, max);
      max = temp;
      boolector_release (btor, read);
      boolector_release (btor, ugt);
    }

  /* Now we show that 'max' is indeed a maximum */
  /* We read at an arbitrary position */
  index = boolector_var (btor, sort_index, NULL);
  read = boolector_read (btor, array, index);

  /* We assume that it is possible that the read value is greater than 'max' */
  formula = boolector_ugt (btor, read, max);

  /* We assert the formula and call Boolector */
  boolector_assert (btor, formula);
  result = boolector_sat (btor);
  if (result == BOOLECTOR_UNSAT)
    printf ("Formula is unsatisfiable\n");
  else
    abort ();

  /* clean up */
  for (i = 0; i < ARRAY1_EXAMPLE_ARRAY_SIZE; i++)
    boolector_release (btor, indices[i]);
  boolector_release (btor, formula);
  boolector_release (btor, read);
  boolector_release (btor, index);
  boolector_release (btor, max);
  boolector_release (btor, array);
  boolector_release_sort (btor, sort_array);
  boolector_release_sort (btor, sort_index);
  boolector_release_sort (btor, sort_elem);
  assert (boolector_get_refs (btor) == 0);
  boolector_delete (btor);
  return 0;
}

#include "boolector.h"
#include "btoropt.h"
#include <stdlib.h>
#include <stdio.h>
#include <assert.h>

#define ARRAY2_EXAMPLE_ELEM_BW 8
#define ARRAY2_EXAMPLE_INDEX_BW 1

/* We demonstrate Boolector's ability to obtain Array models.
 * We check the following formula for satisfiability:
 * write (array1, 0, 3) = write (array2, 1, 5)
 */

int
main (void)
{
  Btor *btor;
  BoolectorNode *array1, *array2, *zero, *one, *val1, *val2;
  BoolectorNode *write1, *write2, *formula;
  BoolectorSort sort_index, sort_elem, sort_array;
  char **indices, **values;
  int result, size, i;

  btor = boolector_new ();
  sort_index = boolector_bitvec_sort (btor, ARRAY2_EXAMPLE_INDEX_BW);
  sort_elem = boolector_bitvec_sort (btor, ARRAY2_EXAMPLE_ELEM_BW);
  sort_array = boolector_array_sort (btor, sort_index, sort_elem);
  boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);

  zero = boolector_zero (btor, sort_index);
  one = boolector_one (btor, sort_index);
  val1 = boolector_int (btor, 3, sort_elem);
  val2 = boolector_int (btor, 5, sort_elem);
  array1 = boolector_array (btor, sort_array, 0);
  array2 = boolector_array (btor, sort_array, 0);
  write1 = boolector_write (btor, array1, zero, val1);
  write2 = boolector_write (btor, array2, one, val2);
  /* Note: we compare two arrays for equality ---> needs extensional theory */
  formula = boolector_eq (btor, write1, write2);
  boolector_assert (btor, formula);
  result = boolector_sat (btor);
  if (result == BOOLECTOR_SAT)
    printf ("Formula is satisfiable\n");
  else
    abort ();

  /* Formula is satisfiable, we can obtain array models: */
  boolector_array_assignment (btor, array1, &indices, &values, &size);
  if (size > 0)
    {
      printf ("Array1:\n");
      for (i = 0; i < size; i++)
	printf ("Array1[%s] = %s\n", indices[i], values[i]);
      boolector_free_array_assignment (btor, indices, values, size);
    }

  boolector_array_assignment (btor, array2, &indices, &values, &size);
  if (size > 0)
    {
      printf ("\nArray2:\n");
      for (i = 0; i < size; i++)
	printf ("Array2[%s] = %s\n", indices[i], values[i]);
      boolector_free_array_assignment (btor, indices, values, size);
    }

  boolector_array_assignment (btor, write1, &indices, &values, &size);
  if (size > 0)
    {
      printf ("\nWrite1:\n");
      for (i = 0; i < size; i++)
	printf ("Write1[%s] = %s\n", indices[i], values[i]);
      boolector_free_array_assignment (btor, indices, values, size);
    }

  boolector_array_assignment (btor, write2, &indices, &values, &size);
  if (size > 0)
    {
      printf ("\nWrite2:\n");
      for (i = 0; i < size; i++)
	printf ("Write2[%s] = %s\n", indices[i], values[i]);
      boolector_free_array_assignment (btor, indices, values, size);
    }

  /* clean up */
  boolector_release (btor, formula);
  boolector_release (btor, write1);
  boolector_release (btor, write2);
  boolector_release (btor, array1);
  boolector_release (btor, array2);
  boolector_release (btor, val1);
  boolector_release (btor, val2);
  boolector_release (btor, zero);
  boolector_release (btor, one);
  boolector_release_sort (btor, sort_array);
  boolector_release_sort (btor, sort_index);
  boolector_release_sort (btor, sort_elem);
  assert (boolector_get_refs (btor) == 0);
  boolector_delete (btor);
  return 0;
}

#include "boolector.h"
#include "btoropt.h"
#include <assert.h>
#include <limits.h>

#define ARRAY3_EXAMPLE_ELEM_BW 8
#define ARRAY3_EXAMPLE_INDEX_BW 1

int
main ()
{
  int sat_result;
  BoolectorNode *array, *index1, *index2, *read1, *read2, *eq, *ne;
  BoolectorSort sort_index, sort_elem, sort_array;
  Btor *btor;

  btor = boolector_new ();
  sort_index = boolector_bitvec_sort (btor, ARRAY3_EXAMPLE_INDEX_BW);
  sort_elem = boolector_bitvec_sort (btor, ARRAY3_EXAMPLE_ELEM_BW);
  sort_array = boolector_array_sort (btor, sort_index, sort_elem);
  boolector_set_opt (btor, BTOR_OPT_INCREMENTAL, 1);

  array = boolector_array (btor, sort_array, 0);
  index1 = boolector_var (btor, sort_index, 0);
  index2 = boolector_var (btor, sort_index, 0);
  read1 = boolector_read (btor, array, index1);
  read2 = boolector_read (btor, array, index2);
  eq = boolector_eq (btor, index1, index2);
  ne = boolector_ne (btor, read1, read2);

  /* we enforce that index1 is equal to index 2 */
  boolector_assert (btor, eq);
  sat_result = boolector_sat (btor);
  assert (sat_result == BOOLECTOR_SAT);
  /* now we additionally assume that the read values differ
   * the instance is now unsatasfiable as read congruence is violated */
  boolector_assume (btor, ne);
  sat_result = boolector_sat (btor);
  assert (sat_result == BOOLECTOR_UNSAT);
  /* after the SAT call the assumptions are gone
   * the instance is now satisfiable again */
  sat_result = boolector_sat (btor);
  assert (sat_result == BOOLECTOR_SAT);
  boolector_release (btor, array);
  boolector_release (btor, index1);
  boolector_release (btor, index2);
  boolector_release (btor, read1);
  boolector_release (btor, read2);
  boolector_release (btor, eq);
  boolector_release (btor, ne);
  boolector_release_sort (btor, sort_array);
  boolector_release_sort (btor, sort_index);
  boolector_release_sort (btor, sort_elem);
  boolector_delete (btor);
  return 0;
}