# Boolector C API documentation¶

## Interface¶

## 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 typeBooleanand typebit 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 < 100Given 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 ywhich 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 Awhere 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 viaboolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1);or via setting the environment variable:

BTORMODELGEN=1For 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; }