Isat3 Manual
User Manual:
Open the PDF directly: View PDF 
.
Page Count: 13
iSAT3 Manual (isat3 0.02-20140409)∗
Karsten Scheibler
April 9, 2014
1 Introduction
This document provides a brief introduction into the usage of the iSAT3 binary and the iSAT3
library. iSAT3 is a satisfiability checker for Boolean combinations of arithmetic constraints over
real- and integer-valued variables. Those constraints may contain linear and non-linear arith-
metic as well as transcendental functions. iSAT3 is the third implementation of the iSAT algo-
rithm [FHT+07]. All three implementations (with HySAT [FH06, HEFT08] and iSAT [EKKT08]
being the first two) share the same major core principles of tightly integrating ICP into the CDCL
framework. But while the core solvers of HySAT and iSAT operate on simple bounds, the core
of iSAT3 uses literals and additionally utilizes an ASG for more advanced formula preprocess-
ing [SKB13].
2 The iSAT3 Binary
2.1 Modes of Operation
The command-line tool iSAT3 has two different modes of operation: It can be used a) as a
satisfiability checker for a single formula or b) for finding a trace of a hybrid system via bounded
model checking (BMC). In the following the usage of iSAT3 is illustrated by means of some
examples. iSAT3 understands the same input language as HySAT and iSAT.
2.1.1 Single Formula Mode
Assume you want to find a pythagorean triple, i.e. a triple (a, b, c) of integer values which satisfies
a2+b2=c2. To use iSAT3 for this purpose, create a file, say sample1.hys, containing the
following lines (without the line numbers).
1DECL
2-- The r an ge of eac h va r ia bl e ha s to be bo un de d .
3in t [1 , 100 ] a , b , c ;
4
5EXPR
6-- Co ns trai nt to be sol ved .
7a*a + b*b = c*c;
In single formula mode the input file has two sections: The first section, starting with the keyword
DECL, contains declarations of all variables occuring in the formula to be solved. The second
∗This work has been partially funded by the German Research Council (DFG) as part of the Transregional
Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS,
http://www.avacs.org/).
1
section, starting with EXPR, contains the formula itself, in this case consisting of a single arithmetic
constraint only. After calling iSAT3 the following output is generated, reporting a= 3, b = 4 and
c= 5 as a satisfying valuation.
1# i sat 3 - I -v sa mp le1 . h ys
2opening ’sample1.hys’ for reading
3pa rsi ng ( use r t ime 0 .00 00 00 s eco nds )
4re wri te ( use r t ime 0 .00 00 00 s eco nds )
5cnf g en era ti on ( use r t ime 0 .00 00 00 s eco nds )
6st art ing to s ol ve
7a:
8[3 , 3] -- p o in t i n t erv a l
9b:
10 [4 , 4] -- p o in t i n t erv a l
11 c:
12 [5 , 5] -- p o in t i n t erv a l
13 SA T ISF IAB L E [ sa t isf iab l e wi th all val ue s in the g iv en inte rva l s ]
You might have noticed, that iSAT3 writes the result in form of intervals instead of single values.
This is due to the fact that calculations in iSAT3 are carried out in interval arithmetic. In contrast
to the examples presented in this brief introduction, the solution intervals computed by iSAT3
will in general be non-point intervals.
2.1.2 Bounded Model Checking Mode
Bounded model checking (BMC) of a hybrid system aims at finding a run of bounded length k
which
•starts in an initial state of the system,
•obeys the system’s transition relation, and
•ends in a state in which a certain (desired or undesired) property holds.
The idea of BMC is to construct a formula which is satisfiable if and only if a trace with above
properties exists. In case of satisfiability, any satisfying valuation of this formula corresponds to
such a trace.
For specifying BMC tasks, iSAT3 has a second input file format which consists of four parts:
•DECL: As above, this part contains declarations of all variables. Furthermore, you can define
symbolic constants in this section (see the definition of fin line 2 in the example below).
•INIT: This part is a formula describing the initial state(s) of the system to be investigated.
In the example below, xis initialized to 0.5, and jump is set to false, since this is the only
valuation which satisfies the constraint !jump, where ’!’ stands for ’not’.
•TRANS: This formula describes the transition relation of the system. Variables may occur in
primed (x’) or unprimed (x) form. A primed variable represents the value of that variable
in the successor step, i.e. after the transition has taken place. Thus, line 14 of the example
states, that if jump is false in the current state, then the value of xin the next state is given
by its current value plus 2. The semicolon which terminates each constraint can be read as
an AND-operator. Hence, TRANS in the example is a conjunction of three constraints.
•TARGET: This formula characterises the state(s) whose reachability is to be checked. In the
example below, we want to find out if a state is reachable in which x > 3.5 holds.
2
1DECL
2de fi ne f = 2.0 ;
3float [0 , 1000] x;
4bo ole ju mp ;
5
6INIT
7x = 0 .5;
8! ju mp ;
9
10 TRANS
11 jump ’ < -> ! jum p ;
12
13 jump -> f * x ’ = x ;
14 ! jump -> x’ = x + 2;
15
16 TARGET
17 x > 3.5;
When calling iSAT3 with the input file above, it successively unwinds the transition relation
k= 0,1,2, . . . times, conjoins the resulting formula with the formulae describing the initial state
and the target states, and thereafter solves the formula thus obtained.
From the excerpts of the tool ouput below you can see that for k= 0,1,2,3,4,the formulae are
all unsatisfiable, for k= 5 however, a solution is found. Note, that iSAT3 reports the values of
jump and xfor each step kof the system. After the last transition, as required, x > 3.5 holds.
1# isat3 -I - v -v sa mple2 . hys
2opening ’sample2.hys’ for reading
3pa rsi ng ( use r t ime 0 .00 00 00 s eco nds )
4re wri te ( use r t ime 0 .00 00 00 s eco nds )
5cnf g en era ti on ( use r t ime 0 .00 00 00 s eco nds )
6st art ing to s ol ve
7de pth 0 is UN SA TI SF IAB LE ( use r time 0. 000 00 0 sec on ds )
8de pth 1 is UN SA TI SF IAB LE ( use r time 0. 000 00 0 sec on ds )
9de pth 2 is UN SA TI SF IAB LE ( use r time 0. 000 00 0 sec on ds )
10 de pth 3 is UN SA TI SF IAB LE ( use r time 0. 000 00 0 sec on ds )
11 de pth 4 is UN SA TI SF IAB LE ( use r time 0. 000 00 0 sec on ds )
12 depth 5 is SA TIS FIA B LE [ sa tis fia b le with all value s in the given i n ter val s ] ...
13 jump@0:
14 false
15 x@0 :
16 [0.5 , 0. 5] -- poi nt in t e rva l
17 x@1 :
18 [2.5 , 2. 5] -- poi nt in t e rva l
19 jump@1:
20 true
21 x@2 :
22 [1.25 , 1.25] -- p o in t i n t erv a l
23 jump@2:
24 false
25 x@3 :
26 [3.25 , 3.25] -- p o in t i n t erv a l
27 jump@3:
28 true
29 x@4 :
30 [1.625 , 1.62 5] -- po i nt in t e rv a l
31 jump@4:
32 false
33 x@5 :
34 [3.625 , 3.62 5] -- po i nt in t e rv a l
35 jump@5:
36 true
37 UN SAF E [ ta rge t is r eac hab le with al l v alu es in the gi ven i nte rv als ]
2.2 Input Language: Types, Operators, and Expressions
2.2.1 Types
•Types supported by iSAT3 are float,int, and boole.
3
•When declaring a float or an integer variable you have to specify the range of this variable.
Due to the internal working of iSAT3 these ranges have to be bounded, i.e. you have to
specify a lower and an upper bound. To reduce solving time, ranges should be chosen as
small as possible.
•Integer and float variables can be mixed within the same arithmetic constraint.
2.2.2 Operators
•Boolean operators:
Operator Type Num. Args. Meaning
and infix 2 conjunction
or infix 2 disjunction
nand infix 2 negated and
nor infix 2 negated or
xor infix 2 exclusive or
nxor infix 2 negated xor, i.e. equivalence
<-> infix 2 alternative notation for ’nxor’
impl infix 2 implication
-> infix 2 alternative notation for ’impl’
not prefix 1 negation
!prefix 1 alternative notation for ’not’
•Arithmetic operators:
Operator Type Num. Args. Meaning
+infix 1 or 2 unary ’plus’ and addition
-infix 1 or 2 unary ’minus’ and subtraction
*infix 2 multiplication
abs prefix 1 absolute value
min prefix 2 minimum
max prefix 2 maximum
exp prefix 1 exponential function regarding base e
exp2 prefix 1 exponential function regarding base 2
exp10 prefix 1 exponential function regarding base 10
log prefix 1 logarithmic function regarding base e
log2 prefix 1 logarithmic function regarding base 2
log10 prefix 1 logarithmic function regarding base 10
sin prefix 1 sine (unit: radian)
cos prefix 1 cosine (unit: radian)
pow prefix 2 nth power, n(2nd argument) has to be an integer, n≥0
^infix 2 nth power, n(2nd argument) has to be an integer, n≥0
nrt prefix 2 nth root, n(2nd argument) has to be an integer, n≥1
Operators abs,min,max,exp,exp2,exp10,log,log2,log10,sin,cos,pow and nrt have
to be called with their arguments being separated by commas and enclosed in brackets.
Example: min(x, y)
•Relational operators:
>,>=,<,<=,=,!= (all infix)
•Precedence of operators: The following list shows all operators ordered by their precedence,
starting with the one that binds strongest. You can use brackets in the input file to modify
the order of term evaluation induced by these precedence rules.
4
unary not, ^
unary plus, unary minus
multiplication
plus, minus
abs,min,max,exp,exp2,exp10,log,log2,log10,sin,cos,pow,nrt
>,>=,<,<=,=,!=
and,nand
xor,nxor
or,nor
impl
2.2.3 Expressions
•Let aand bbe Boolean variables and xand ybe float variables. Examples for expressions
are:
[x*y+2*(x-4)>=5-2*(x-4)]
(x > 20 and !b) xor a
b<->{3.18*(-5-y*y*y)=7}
sin(x + max(3, y)) < 0.4
abs(3.1 * min(x^2 + y^2, -x)) <= 10.3
•Note that the individual constraints occurring in a formula have to be conjoined using the
’;’-operator. In addition, the last line of each formula has to be terminated with a semicolon.
2.3 How iSAT3 works
To be able to interprete iSAT3’s output and the tool options presented in the next section you
need some basic understanding of how the tool works internally. For further details regarding the
iSAT algorithm refer to [FHT+07] and regarding iSAT3 internals refer to [SKB13]. The iSAT3
solver performs a backtrack search to prune the search space until it is left with a ‘sufficiently
small’ portion of the search space for which it cannot derive any contradiction with respect to the
constraints occuring in the input formula.
Initially, the search space consists of the cartesian product of the ranges of all variables occuring
in the formula to be solved. Just like an ordinary (purely Boolean) SAT solver, iSAT3 operates
by alternating between two steps:
•The decision step involves selecting a variable ‘blindly’, splitting its current interval (e.g. by
using the midpoint of the interval as split point) and temporarily discarding either the lower
or the upper part of the interval from the search. The solver will ignore the discarded part
of the search space until the decision is undone by backtracking.
•Each decision is followed by a deduction step in which the solver applies a set of deduction
rules that explore all the consequences of the previous decision. Informally speaking, the
deduction rules carve away portions of the search space that contain non-solutions only.
Assume, for example, that the input formula consists of the single constraint x·y= 8 and initially
x∈[2,4] and y∈[2,4] holds. The solver might now decide to split the interval of xby assigning
the new lower bound x≥3 to x. In the subsequent deduction phase, the solver will deduce that,
5
due to the increased lower bound of x, the upper bound of ycan be reduced to 8
3because for all
other values of ythe constraint x·y= 8 is violated. After asserting y≤8
3, thereby contracting
the search space to [3,4] ×[2,8
3], no further deductions are possible, and the solver goes on with
taking the next decision. Deduction may also yield a conflict, i.e. a variable whose interval is
empty, indicating the need to backtrack.
To enforce termination of the algorithm, the solver only selects a variable xfor splitting if the
width x−xof its interval [x, x] is above a certain threshold ε, which we call minimal splitting width.
Furthermore, the solver discards a (non-conflicting) deduced bound if it only yields a comparatively
small progress with respect to the bound already in place. More precisely, a deduced lower (upper)
bound bdis ignored if |bc−bd| ≤ δabs, where bcis the current lower (upper) bound of the respective
variable and δabs is a parameter which we call minimum progress. The values of εand δcan be
set with the command-line options --msw and --mpr.
These measures taken to enforce termination have some consequences which are important to
understand:
•If iSAT3 terminates with result ‘UNSATISFIABLE’, then – assuming that there are no bugs
in the implementation – you can be sure, that the formula is actually unsatisfiable.
•If the tool outputs result ‘SATISFIABLE’, then the input formula is satisfiable.
We note however that iSAT3 is in general not able to compute a definite answer for all input
formulae. This is due to the fact that interval arithmetic combined with splitting (floating-
point) intervals yields a highly incomplete deduction calculus. We are currently working on
techniques to certify satisfiability in more cases.
•As mentioned before, iSAT3 cannot decide all given formulae due to the methods employed.
To nevertheless provide termination with at least some quantitative result, the tool may stop
with result CANDIDATE SOLUTION. This means that for the given parameters εand δabs the
solver could not detect any conflicts within the reported interval valuation. It does not mean,
however, that the box actually contains a solution, but it can be seen as an approximative
solution wrt. parameters εand δabs. Actually, in most cases there will be a solution within
the box or at least nearby. If you think that iSAT3 has reported a spurious solution you
should re-run the solver with smaller εand δabs in order to confirm (or to refute) the previous
result.
2.4 Tool Options
The options influence the solver behavior and thereby its performance. Understanding the solving
algorithm on the abstract level described in the previous section is important when using most of
the options listed below.
2.4.1 General Options
These options are the ones you will most certainly want to experiment with when solving your
models.
--msw Set the minimum splitting width, i.e. iSAT3 will not split intervals if their current width
is below this threshold.
--mpr Set the absolute progress. Deduced consistent bounds that refine the valuation by less than
this value are neglected.
--extended-hys-syntax Enable support for exp2,exp10,log,log2 and log10. Without this
option these strings are treated as variable names.
6
2.4.2 Print Options
Print options only affect the output of the solver, not the actual solving process.
-v increase verbosity level (without -v iSAT3 will only give a very brief output).
--print-hex all numbers are outputted in hexadecimal format. This might be interesting to get
the exact bit representation of floating point numbers. You may also use such numbers in
the input files given to iSAT3.
2.4.3 BMC-related Options
The BMC-related options refer only to input formulae in the bounded model checking format.
They have no influence on the solver’s behavior if the formula is given in the EXPR format.
--start-depth The first unwinding depth for which a BMC formula is generated and checked for
satisfiability.
--max-depth The last unwinding depth for which a BMC formula is generated and checked for
satisfiability.
3 The iSAT3 Library
The iSAT3 library provides a C-API (also usable in C++). The following code snippets will give
an idea how the API should be used. Please look also at the example program example.c which
is contained in the isat3.tar.bz2 file.
3.1 Creating a solver instance
Before using the library you have to call isat3_setup() once. Before your program exits, you
should call isat3_cleanup() once. The function isat3_init() will return a new instance of
iSAT3. An solver instance is needed to create a formula, solve it and asking for a solution –
if there is any. A formula is created with the help of isat3_nodes. Every solver instance is
independent of other already created instances. If you use multiple instances at the same time, be
careful to not mix isat3_nodes from different instances. If an instance is not needed any more,
use isat3_deinit() to destroy it. The following listing shows the basic steps of setting up the
iSAT3 library and creating an iSAT3 instance.
7
1# i nc lu de < st di o .h >
2
3# in clu de " isa t3 .h "
4
5vo id do _s om et hi ng ( i nt pa ra me ter )
6{
7st ru ct is at3 * is3 = i sa t3_ in it ( N ULL ) ;
8
9/* ... c re ate a fo rmu la and solve it ... */
10
11 isat3_deinit(is3);
12 }
13
14 int ma in ( vo id )
15 {
16 is a t3_ set u p ();
17 do_something(0);
18 do_something(1);
19 do_something(2);
20
21 /* ... */
22
23 is a t3_ c lea n up ();
24 re tu rn (0);
25 }
3.2 Creating a formula
A formula is created with the help of isat3_nodes. Starting with the variables the formula is
build bottom-up. For example the constraint x+y*z<7;can be created with these four
steps:
1. create sub-formula for (y * z), the associated isat3_node is t1
2. create sub-formula for (x + t1), the associated isat3_node is t2
3. create an integer constant 7, the associated isat3_node is c1
4. create sub-formula for (t2 < c1), the associated isat3_node is t3
If sub-formulas are no longer needed you may destroy the reference to them with isat3_node_destroy().
8
1st ru ct is at3 * is3 ;
2s tru ct i s at 3_ no de *b , * x , * y , * z;
3st ru ct isa t3_ nod e * t1 , *t2 , * t3 , * t4 , *t5 , * t6 ;
4st ru ct isa t3_ nod e * c1 , *c2 , * c3 ;
5st ruc t is at 3_n od e * expr ;
6
7is3 = i sa t3_ in it ( N ULL );
8
9/*
10 * DEC L
11 * boole b;
12 * i nt [ - 10 , 10] x , y ,z ;
13 */
14
15 b = isat3_node_create_variable_boole(is3, "b");
16
17 x = isat3_node_create_variable_integer(is3, "x", -10, 10);
18 y = isat3_node_create_variable_integer(is3, "y", -10, 10);
19 z = isat3_node_create_variable_integer(is3, "z", -10, 10);
20
21 /*
22 * EXP R
23 *x+y*z<7;
24 * b or (x ^2 = 4);
25 */
26
27 t1 = i sa t 3_ n od e_ c re a te _ bi na r y_ o pe r at io n ( i s3 , IS AT 3_ NO DE _B OP _M UL , y , z ) ;
28 t2 = is a t3_n o d e _cre a t e _bin a r y_ope r a tion ( is3 , ISAT 3_N ODE _BO P_A DD , x , t1 );
29 c1 = isat3_node_create_constant_integer(is3, 7);
30 t3 = i s at 3 _ no d e_ c r ea t e _b i na r y _o p er a t io n ( i s3 , IS AT 3 _N OD E _B OP _ LE SS , t2 , c 1 );
31
32 c2 = isat3_node_create_constant_integer(is3, 2);
33 t4 = i s at 3 _ no d e_ c r ea t e _b i na r y _o p er a t io n ( i s3 , IS A T3 _N O DE _B OP _ PO WE R , x , c 2 );
34 c3 = isat3_node_create_constant_integer(is3, 4);
35 t5 = is a t3_n o d e _cre a t e _bin a r y_ope r a tion ( is3 , ISAT 3 _NO DE_ BOP _ EQ U AL , t4 , c3 );
36 t6 = is a t3_n o d e _cre a t e _bin a r y_ope r a tion ( is3 , I S AT 3_N ODE _BO P_O R , b, t5 );
37
38 e xpr = i s a t3 _ n od e _c r e at e _ bi n ar y _ op e r at i on ( is3 , I SA T 3_ NO DE _ BO P_ AN D , t3 , t 6 );
39
40 /* de st roy temp ora ry nodes , not ne ed ed any mo re */
41
42 i s at 3 _n o de _ de s tr o y ( is3 , t6 );
43 i s at 3 _n o de _ de s tr o y ( is3 , t5 );
44 i s at 3 _n o de _ de s tr o y ( is3 , t4 );
45 i s at 3 _n o de _ de s tr o y ( is3 , t3 );
46 i s at 3 _n o de _ de s tr o y ( is3 , t2 );
47 i s at 3 _n o de _ de s tr o y ( is3 , t1 );
48 i s at 3 _n o de _ de s tr o y ( is3 , c3 );
49 i s at 3 _n o de _ de s tr o y ( is3 , c2 );
50 i s at 3 _n o de _ de s tr o y ( is3 , c1 );
51
52 /* ... s olvin g ... */
53
54 isat3_deinit(is3);
The function isat3_node_create_unary_operation() creates unary operations of the following
types:
Parameter Operation
ISAT3_NODE_UOP_PRIME to create a primed variable in TRANS (for example x’)
ISAT3_NODE_UOP_NOT boolean negation
ISAT3_NODE_UOP_ABS absolute value
ISAT3_NODE_UOP_MINUS unary minus
ISAT3_NODE_UOP_SIN sine (unit: radian)
ISAT3_NODE_UOP_COS cosine (unit: radian)
ISAT3_NODE_UOP_EXP exponential function regarding base e
ISAT3_NODE_UOP_EXP2 exponential function regarding base 2
ISAT3_NODE_UOP_EXP10 exponential function regarding base 10
ISAT3_NODE_UOP_LOG logarithmic function regarding base e
ISAT3_NODE_UOP_LOG2 logarithmic function regarding base 2
ISAT3_NODE_UOP_LOG10 logarithmic function regarding base 10
9
The function isat3_node_create_binary_operation() creates binary operations of the following
types:
Parameter Operation
ISAT3_NODE_BOP_AND conjunction
ISAT3_NODE_BOP_NAND negated and
ISAT3_NODE_BOP_OR disjunction
ISAT3_NODE_BOP_NOR negated or
ISAT3_NODE_BOP_XOR exclusive or
ISAT3_NODE_BOP_XNOR negated xor, i.e. equivalence
ISAT3_NODE_BOP_IMPLIES implication
ISAT3_NODE_BOP_IFF equivalence
ISAT3_NODE_BOP_LESS <
ISAT3_NODE_BOP_LESS_EQUAL <=
ISAT3_NODE_BOP_GREATER >
ISAT3_NODE_BOP_GREATER_EQUAL >=
ISAT3_NODE_BOP_EQUAL =
ISAT3_NODE_BOP_NOT_EQUAL !=
ISAT3_NODE_BOP_MIN minimum
ISAT3_NODE_BOP_MAX maximum
ISAT3_NODE_BOP_ADD addition
ISAT3_NODE_BOP_SUB subtraction
ISAT3_NODE_BOP_MULT multiplication
ISAT3_NODE_BOP_POWER nth power, n(2nd argument) has to be an integer n≥0
ISAT3_NODE_BOP_ROOT nth root, n(2nd argument) has to be an integer n≥1
For easier creation of nodes with three (ternary) to nine (nonary) arguments, the functions
isat3_node_create_ternary_operation(), . . . , isat3_node_create_nonary_operation() may
be used. The created nodes are of the following types:
Parameter Operation
ISAT3_NODE_NOP_AND conjunction
ISAT3_NODE_NOP_NAND negated and
ISAT3_NODE_NOP_OR disjunction
ISAT3_NODE_NOP_NOR negated or
ISAT3_NODE_NOP_XOR exclusive or
ISAT3_NODE_NOP_XNOR negated xor, i.e. equivalence
ISAT3_NODE_NOP_ADD addition
ISAT3_NODE_NOP_MULT multiplication
Please consult isat3.h for the detailed function declarations.
10
3.3 Solving
The two different operation modes of the binary, namely a) satisfiability checking of a single
formula or b) finding a trace of a hybrid system via bounded model checking (BMC) are also
supported through the library interface.
3.3.1 Single Formula Mode
1st ru ct is at3 * is3 ;
2st ruc t is at 3_n od e * expr ;
3i3 _typ e_t re sul t ;
4i3 _typ e_t re sul t ;
5i3 _t rut hval _t tr uth val ;
6i3 _bo ol_ t lb _is_str ict , u b_is _str ict ;
7i 3_ do ub le _t lb , u b ;
8
9is3 = i sa t3_ in it ( N ULL );
10
11 /* de cla re va ria ble s */
12
13 b = isat3_node_create_variable_boole(is3, "b");
14 x = isat3_node_create_variable_float(is3, "x", -100, 1000);
15
16 /* ... c re ate expr ... */
17
18 /*
19 * expr is the node re p res e nti ng the f orm ula to be so lved
20 * c orr es po nd in g to E XPR in a . hy s f ile s
21 * ti me out in micro - s eco nd s
22 * r esult could be ISAT 3_R E SUL T_U NKN O WN , I S AT 3 _RE SUL T_U NSA T ,
23 * IS AT3 _R ESU LT_ SAT , ...
24 */
25
26 r es ul t = i sa t3 _ so l ve _ ex p r ( is3 , expr , t im eo ut ) ;
27
28 /* get s olu tio n or c an d ida te s olu tio n */
29
30 if (( i s a t3_r e s u lt_c o n t ains _ p o ssibl e _ s olut i o n ( resu lt )) ||
31 (isat3_result_contains_solution(result)))
32 {
33 t ru th v al = i s at 3 _ ge t _t r ut h _v a lu e ( is3 , b , 0 );
34
35 /*
36 * t rut hva l could be I3 _ TR UTH VAL _FA LSE , I3_ T R UTH V AL_ T RUE or
37 * I3_TRUTHVAL_UNDEF
38 */
39
40 l b_ i s_ s tr ic t = i s a t3 _ is _ l ow e r_ b o un d _s t r ic t ( i s3 , x , 0 );
41 u b_ i s_ s tr ic t = i s a t3 _ is _ u pp e r_ b o un d _s t r ic t ( i s3 , x , 0 );
42 lb = i s at 3 _g e t_ l o we r _b o u nd ( is3 , x , 0 );
43 ub = i s at 3 _g e t_ u p pe r _b o u nd ( is3 , x , 0 );
44
45 /* print the res ul t for x */
46
47 pr in tf ( " % s : %s %1. 40 f , %1.40 f % s \ n " ,
48 i s at 3 _n o d e_ g et _ v ar i ab l e _n a me ( is3 , x ) ,
49 lb_is_strict ? "(" : "[",
50 lb ,
51 ub ,
52 ub _ is_ stri ct ? ") " : " ] " );
53 }
54
55 /* ... */
56
57 isat3_deinit(is3);
11
3.3.2 Bounded Model Checking Mode
1st ru ct is at3 * is3 ;
2s tru ct i s at 3_ no de *b , * x ;
3st ruc t is at 3_n od e * expr ;
4i3 _t rut hval _t tr uth val ;
5i3 _bo ol_ t lb _is_str ict , u b_is _str ict ;
6i 3_ do ub le _t lb , u b ;
7i 3_ tf ra me _t t , t fr am e ;
8
9is3 = i sa t3_ in it ( N ULL );
10
11 /* de cla re va ria ble s */
12
13 b = isat3_node_create_variable_boole(is3, "b");
14 x = isat3_node_create_variable_float(is3, "x", -100, 1000);
15
16 /* ... c re ate init , trans , targ et ... */
17
18 /*
19 * init , trans , targ et nodes rep r ese n tin g the sub - for mu las of INIT , TRANS ,
20 * TARGET
21 * sta r t_t fra m e b efore s olvin g unroll up to this time fra me
22 * max_ tfr ame unrol l not more tha n this n um ber of tim e frame s
23 * ti me out in micro - s eco nd s
24 * r esult cou ld be ISA T3_ R ESU LT_ UNK N OWN , IS AT3 _RE SUL T_U N SA T ,
25 * IS AT3 _RE SU L T_ SAT , ...
26 */
27
28 re su lt = is a t3_s o lve _ bmc ( is3 , init , trans , target , s ta rt_tf ra me , end_tframe , t imeou t );
29
30 /* get s olu tio n or c an d ida te s olu tio n */
31
32 if (( i s a t3_r e s u lt_c o n t ains _ p o ssibl e _ s olut i o n ( resu lt )) ||
33 (isat3_result_contains_solution(result)))
34 {
35 tf ra me = i sa t3 _g et _t fr am e ( is3 ) ;
36 for (t = 0; t <= tfr am e ; t ++)
37 {
38 t ru th va l = is a t3 _g e t_ tr u th _v a lu e ( is3 , b , t );
39
40 /*
41 * t rut hva l could be I3 _ TR UTH VAL _FA LSE , I3_ T R UTH V AL_ T R UE or
42 * I3_TRUTHVAL_UNDEF
43 */
44
45 l b_ is _s tr i ct = i s at 3 _i s _l ow e r_ bo u nd _ st ri c t ( is3 , x , t );
46 u b_ is _s tr i ct = i s at 3 _i s _u pp e r_ bo u nd _ st ri c t ( is3 , x , t );
47 lb = i sa t3 _ ge t _l ow e r_ bo u nd ( i s3 , x , t ) ;
48 ub = i sa t3 _ ge t _u pp e r_ bo u nd ( i s3 , x , t ) ;
49
50 /* print the res ul t for x */
51
52 pr in tf ( " % s@ %d: % s %1.40 f , % 1. 40 f % s\n" ,
53 i s at 3 _ no d e_ g e t_ v a ri a b le _ na m e ( i s3 , x ) ,
54 tframe ,
55 lb _ is_ stri ct ? "( " : " [ " ,
56 lb ,
57 ub ,
58 ub _ is_ stri ct ? ") " : " ] " );
59 }
60 }
61
62 /* ... */
63
64 isat3_deinit(is3);
3.3.3 Incremental Solving
The functions isat3_solve_expr() and isat3_solve_bmc() start the solver every time from
scratch. If you want to solve a set of formulas with common sub-formulas, it is more beneficial to
use incremental solving. You create constraints as before. With the function isat3_add_constraint()
you add the them to the set of constraints to be solved with isat3_solve_constraints(). Every
call to isat3_solve_constraints() will re-use conflict-clauses learnt during previous calls.
12
Additionally backtrack-points are supported. Imagine the set of constraints as a stack. New
constraints are added to the top. A backtrack-point is a marker in this stack. Going back
to a backtrack-point removes (pops) the constraints above this backtrack-point. The function
isat3_push_btpoint() will set a backtrack-point – in other words it will set a marker in the
stack of the constraints. The function isat3_pop_btpoint() will remove all constraints until the
top-most backtrack-point. Please consult example.c for an example illustrating the usage of the
incremental interface.
References
[EKKT08] Andreas Eggers, Natalia Kalinnik, Stefan Kupferschmid, and Tino Teige. Challenges
in constraint-based analysis of hybrid systems. In Angelo Oddi, Fran¸cois Fages, and
Francesca Rossi, editors, CSCLP, volume 5655 of Lecture Notes in Computer Science,
pages 51–65. Springer, 2008.
[FH06] Martin Fr¨anzle and Christian Herde. HySAT: An efficient proof engine for bounded
model checking of hybrid systems. Formal Methods in System Design, 2006.
[FHT+07] Martin Fr¨anzle, Christian Herde, Tino Teige, Stefan Ratschan, and Tobias Schubert.
Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex
Boolean Structure. Journal on Satisfiability, Boolean Modeling, and Computation,
1(2007):209–236, 2007.
[HEFT08] Christian Herde, Andreas Eggers, Martin Fr¨anzle, and Tino Teige. Analysis of hybrid
systems using hysat. In ICONS, pages 196–201. IEEE Computer Society, 2008.
[SKB13] Karsten Scheibler, Stefan Kupferschmid, and Bernd Becker. Recent improvements in
the smt solver isat. In Christian Haubelt and Dirk Timmermann, editors, MBMV,
pages 231–241. Institut f¨ur Angewandte Mikroelektronik und Datentechnik, Fakult¨at
f¨ur Informatik und Elektrotechnik, Universit¨at Rostock, 2013.
13
