Isat3 Manual
User Manual:
Open the PDF directly: View PDF 
.
Page Count: 13
| Download | |
| Open PDF In Browser | View PDF |
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 arithmetic as well as transcendental functions. iSAT3 is the third implementation of the iSAT algorithm [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 preprocessing [SKB13].
2
2.1
The iSAT3 Binary
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).
1
DECL
-- The range of each v a ri a b l e has to be bounded .
int [1 , 100] a , b , c ;
2
3
4
5
6
7
EXPR
-- C o n s t r a i n t to be solved .
a*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
2
3
4
5
6
7
8
9
10
11
12
13
# isat3 -I -v sample1 . hys
opening ’ sample1 . hys ’ for reading
parsing ( user time 0.000000 seconds )
rewrite ( user time 0.000000 seconds )
cnf generation ( user time 0.000000 seconds )
starting to solve
a:
[3 , 3] -- point i n t e r v a l
b:
[4 , 4] -- point i n t e r v a l
c:
[5 , 5] -- point i n t e r v a l
SATISFIABLE [ satisfiable with all values in the given intervals ]
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 f in 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, x is 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 x in 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
1
DECL
define f = 2.0;
float [0 , 1000] x ;
boole jump ;
2
3
4
5
6
7
8
INIT
x = 0.5;
! jump ;
9
10
11
TRANS
jump ’ <-> ! jump ;
12
13
14
jump -> f * x ’ = x ;
! jump -> x ’ = x + 2;
15
16
17
TARGET
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 x for each step k of the system. After the last transition, as required, x > 3.5 holds.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
2.2
2.2.1
# isat3 -I -v -v sample2 . hys
opening ’ sample2 . hys ’ for reading
parsing ( user time 0.000000 seconds )
rewrite ( user time 0.000000 seconds )
cnf generation ( user time 0.000000 seconds )
starting to solve
depth 0 is UNSATISFIABLE ( user time 0.000000 seconds )
depth 1 is UNSATISFIABLE ( user time 0.000000 seconds )
depth 2 is UNSATISFIABLE ( user time 0.000000 seconds )
depth 3 is UNSATISFIABLE ( user time 0.000000 seconds )
depth 4 is UNSATISFIABLE ( user time 0.000000 seconds )
depth 5 is SATISFIABLE [ satisfiable with all values in the given intervals ] ...
jump@0 :
false
x@0 :
[0.5 , 0.5] -- point i n t er v a l
x@1 :
[2.5 , 2.5] -- point i n t er v a l
jump@1 :
true
x@2 :
[1.25 , 1.25] -- point i nt e r v a l
jump@2 :
false
x@3 :
[3.25 , 3.25] -- point i n t e r v a l
jump@3 :
true
x@4 :
[1.625 , 1.625] -- point i n t e r v a l
jump@4 :
false
x@5 :
[3.625 , 3.625] -- point i n t e r v a l
jump@5 :
true
UNSAFE [ target is reachable with all values in the given intervals ]
Input Language: Types, Operators, and Expressions
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
and
or
nand
nor
xor
nxor
<->
impl
->
not
!
Type
infix
infix
infix
infix
infix
infix
infix
infix
infix
prefix
prefix
Num. Args.
2
2
2
2
2
2
2
2
2
1
1
Meaning
conjunction
disjunction
negated and
negated or
exclusive or
negated xor, i.e. equivalence
alternative notation for ’nxor’
implication
alternative notation for ’impl’
negation
alternative notation for ’not’
• Arithmetic operators:
Operator
+
*
abs
min
max
exp
exp2
exp10
log
log2
log10
sin
cos
pow
^
nrt
Type
infix
infix
infix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
prefix
infix
prefix
Num. Args.
1 or 2
1 or 2
2
1
2
2
1
1
1
1
1
1
1
1
2
2
2
Meaning
unary ’plus’ and addition
unary ’minus’ and subtraction
multiplication
absolute value
minimum
maximum
exponential function regarding base e
exponential function regarding base 2
exponential function regarding base 10
logarithmic function regarding base e
logarithmic function regarding base 2
logarithmic function regarding base 10
sine (unit: radian)
cosine (unit: radian)
nth power, n (2nd argument) has to be an integer, n ≥ 0
nth power, n (2nd argument) has to be an integer, n ≥ 0
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 a and b be Boolean variables and x and y be 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 x by 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 y can be reduced to 38 because for all
other values of y the constraint x · y = 8 is violated. After asserting y ≤ 83 , thereby contracting
the search space to [3, 4] × [2, 83 ], 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 x for splitting if the
width x−x of 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 bd is ignored if |bc −bd | ≤ δabs , where bc is 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 (floatingpoint) 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
# include < stdio .h >
2
3
# include " isat3 . h "
4
5
6
7
void do_something ( int parameter )
{
struct isat3 * is3 = isat3_init ( NULL );
8
/* ... create a formula and solve it ... */
9
10
isat3_deinit ( is3 );
}
11
12
13
14
15
16
17
18
19
int main ( void )
{
isat3_setup ();
do_something (0);
do_something (1);
do_something (2);
20
21
/* ... */
22
23
24
25
3.2
isat3_cleanup ();
return (0);
}
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
1
2
3
4
5
struct
struct
struct
struct
struct
isat3
isat3_node
isat3_node
isat3_node
isat3_node
* is3 ;
*b , *x , *y , * z ;
* t1 , * t2 , * t3 , * t4 , * t5 , * t6 ;
* c1 , * c2 , * c3 ;
* expr ;
6
7
is3 = isat3_init ( NULL );
8
9
10
11
12
13
/*
* DECL
* boole b ;
* int [ -10 ,10] x ,y , z ;
*/
14
15
b = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ b o o l e ( is3 , " b " );
16
17
18
19
x = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ i n t e g e r ( is3 , " x " , -10 , 10);
y = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ i n t e g e r ( is3 , " y " , -10 , 10);
z = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ i n t e g e r ( is3 , " z " , -10 , 10);
20
21
22
23
24
25
/*
* EXPR
* x + y * z < 7;
* b or ( x ^2 = 4);
*/
26
27
28
29
30
t1
t2
c1
t3
=
=
=
=
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ c o n s t a n t _ i n t e g e r ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
ISAT3_NODE_BOP_MUL , y , z );
ISAT3_NODE_BOP_ADD , x , t1 );
7);
ISAT3_NODE_BOP_LESS , t2 , c1 );
c2
t4
c3
t5
t6
=
=
=
=
=
i s a t 3 _ n o d e _ c r e a t e _ c o n s t a n t _ i n t e g e r ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ c o n s t a n t _ i n t e g e r ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 ,
2);
ISAT3_NODE_BOP_POWER , x , c2 );
4);
ISAT3_NODE_BOP_EQUAL , t4 , c3 );
ISAT3_NODE_BOP_OR , b , t5 );
31
32
33
34
35
36
37
38
expr = i s a t 3 _ n o d e _ c r e a t e _ b i n a r y _ o p e r a t i o n ( is3 , ISAT3_NODE_BOP_AND , t3 , t6 );
39
40
/* destroy temporary nodes , not needed any more */
41
42
43
44
45
46
47
48
49
50
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
i s a t 3 _ n o d e _ d e s t r o y ( is3 ,
t6 );
t5 );
t4 );
t3 );
t2 );
t1 );
c3 );
c2 );
c1 );
51
52
/* ... solving ... */
53
54
isat3_deinit ( is3 );
The function isat3_node_create_unary_operation() creates unary operations of the following
types:
Parameter
ISAT3_NODE_UOP_PRIME
ISAT3_NODE_UOP_NOT
ISAT3_NODE_UOP_ABS
ISAT3_NODE_UOP_MINUS
ISAT3_NODE_UOP_SIN
ISAT3_NODE_UOP_COS
ISAT3_NODE_UOP_EXP
ISAT3_NODE_UOP_EXP2
ISAT3_NODE_UOP_EXP10
ISAT3_NODE_UOP_LOG
ISAT3_NODE_UOP_LOG2
ISAT3_NODE_UOP_LOG10
Operation
to create a primed variable in TRANS (for example x’)
boolean negation
absolute value
unary minus
sine (unit: radian)
cosine (unit: radian)
exponential function regarding base e
exponential function regarding base 2
exponential function regarding base 10
logarithmic function regarding base e
logarithmic function regarding base 2
logarithmic function regarding base 10
9
The function isat3_node_create_binary_operation() creates binary operations of the following
types:
Parameter
ISAT3_NODE_BOP_AND
ISAT3_NODE_BOP_NAND
ISAT3_NODE_BOP_OR
ISAT3_NODE_BOP_NOR
ISAT3_NODE_BOP_XOR
ISAT3_NODE_BOP_XNOR
ISAT3_NODE_BOP_IMPLIES
ISAT3_NODE_BOP_IFF
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
ISAT3_NODE_BOP_MAX
ISAT3_NODE_BOP_ADD
ISAT3_NODE_BOP_SUB
ISAT3_NODE_BOP_MULT
ISAT3_NODE_BOP_POWER
ISAT3_NODE_BOP_ROOT
Operation
conjunction
negated and
disjunction
negated or
exclusive or
negated xor, i.e. equivalence
implication
equivalence
<
<=
>
>=
=
!=
minimum
maximum
addition
subtraction
multiplication
nth power, n (2nd argument) has to be an integer n ≥ 0
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
ISAT3_NODE_NOP_AND
ISAT3_NODE_NOP_NAND
ISAT3_NODE_NOP_OR
ISAT3_NODE_NOP_NOR
ISAT3_NODE_NOP_XOR
ISAT3_NODE_NOP_XNOR
ISAT3_NODE_NOP_ADD
ISAT3_NODE_NOP_MULT
Operation
conjunction
negated and
disjunction
negated or
exclusive or
negated xor, i.e. equivalence
addition
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
1
2
3
4
5
6
7
Single Formula Mode
struct isat3
struct isat3_node
i3_type_t
i3_type_t
i3_truthval_t
i3_bool_t
i3_double_t
* is3 ;
* expr ;
result ;
result ;
truthval ;
lb_is_strict , ub_is_strict ;
lb , ub ;
8
9
is3 = isat3_init ( NULL );
10
11
/* declare variables */
12
13
14
b = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ b o o l e ( is3 , " b " );
x = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ f l o a t ( is3 , " x " , -100 , 1000);
15
16
/* ... create expr ... */
17
18
19
20
21
22
23
24
/*
* expr
*
* timeout
* result
*
*/
is the node representing the formula to be solved
corresponding to EXPR in a . hys files
in micro - seconds
could be ISAT3_RESULT_UNKNOWN , ISAT3_RESULT_UNSAT ,
ISAT3_RESULT_SAT , ...
25
26
result = i s a t 3 _ s o l v e _ e x p r ( is3 , expr , timeout );
27
28
/* get solution or candidate solution */
29
30
31
32
33
if (( i s a t 3 _ r e s u l t _ c o n t a i n s _ p o s s i b l e _ s o l u t i o n ( result )) ||
( i s a t 3 _ r e s u l t _ c o n t a i n s _ s o l u t i o n ( result )))
{
truthval = i s a t 3 _ g e t _ t r u t h _ v a l u e ( is3 , b , 0);
34
35
36
37
38
/*
* truthval could be I3_TRUTHVAL_FALSE , I 3 _ T R U T H V A L _ T RU E or
* I3_TRUTHVAL_UNDEF
*/
39
40
41
42
43
lb_is_strict = i s a t 3 _ i s _ l o w e r _ b o u n d _ s t r i c t ( is3 , x , 0);
ub_is_strict = i s a t 3 _ i s _ u p p e r _ b o u n d _ s t r i c t ( is3 , x , 0);
lb = i s a t 3 _ g e t _ l o w e r _ b o u n d ( is3 , x , 0);
ub = i s a t 3 _ g e t _ u p p e r _ b o u n d ( is3 , x , 0);
44
45
/* print the result for x */
46
47
48
49
50
51
52
53
printf ( " % s : % s %1.40 f , %1.40 f % s \ n " ,
i s a t 3 _ n o d e _ g e t _ v a r i a b l e _ n a m e ( is3 , x ) ,
lb_is_strict ? " ( " : " [ " ,
lb ,
ub ,
ub_is_strict ? " ) " : " ] " );
}
54
55
/* ... */
56
57
isat3_deinit ( is3 );
11
3.3.2
1
2
3
4
5
6
7
Bounded Model Checking Mode
struct isat3
struct isat3_node
struct isat3_node
i3_truthval_t
i3_bool_t
i3_double_t
i3_tframe_t
* is3 ;
*b , * x ;
* expr ;
truthval ;
lb_is_strict , ub_is_strict ;
lb , ub ;
t , tframe ;
8
9
is3 = isat3_init ( NULL );
10
11
/* declare variables */
12
13
14
b = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ b o o l e ( is3 , " b " );
x = i s a t 3 _ n o d e _ c r e a t e _ v a r i a b l e _ f l o a t ( is3 , " x " , -100 , 1000);
15
16
/* ... create init , trans , target ... */
17
18
19
20
21
22
23
24
25
26
/*
* init , trans , target
*
* start_tframe
* max_tframe
* timeout
* result
*
*/
nodes representing the sub - formulas of INIT , TRANS ,
TARGET
before solving unroll up to this time frame
unroll not more than this number of time frames
in micro - seconds
could be ISAT3_RESULT_UNKNOWN , ISAT3_RESULT_UNSAT ,
ISAT3_RESULT_SAT , ...
27
28
result = i sa t3 _ so lv e_ b mc ( is3 , init , trans , target , start_tframe , end_tframe , timeout );
29
30
/* get solution or candidate solution */
31
32
33
34
35
36
37
38
if (( i s a t 3 _ r e s u l t _ c o n t a i n s _ p o s s i b l e _ s o l u t i o n ( result )) ||
( i s a t 3 _ r e s u l t _ c o n t a i n s _ s o l u t i o n ( result )))
{
tframe = i s at 3 _ g e t _ t f r a m e ( is3 );
for ( t = 0; t <= tframe ; t ++)
{
truthval = i s a t 3 _ g e t _ t r u t h _ v a l u e ( is3 , b , t );
39
/*
* truthval could be I3_TRUTHVAL_FALSE , I 3 _ T R U T H V A L _ T R U E or
* I3_TRUTHVAL_UNDEF
*/
40
41
42
43
44
lb_is_strict = i s a t 3 _ i s _ l o w e r _ b o u n d _ s t r i c t ( is3 , x , t );
ub_is_strict = i s a t 3 _ i s _ u p p e r _ b o u n d _ s t r i c t ( is3 , x , t );
lb = i s a t 3 _ g e t _ l o w e r _ b o u n d ( is3 , x , t );
ub = i s a t 3 _ g e t _ u p p e r _ b o u n d ( is3 , x , t );
45
46
47
48
49
/* print the result for x */
50
51
printf ( " % s@ % d : % s %1.40 f , %1.40 f % s \ n " ,
i s a t 3 _ n o d e _ g e t _ v a r i a b l e _ n a m e ( is3 , x ) ,
tframe ,
lb_is_strict ? " ( " : " [ " ,
lb ,
ub ,
ub_is_strict ? " ) " : " ] " );
}
52
53
54
55
56
57
58
59
60
}
61
62
/* ... */
63
64
3.3.3
isat3_deinit ( is3 );
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çois Fages, and
Francesca Rossi, editors, CSCLP, volume 5655 of Lecture Notes in Computer Science,
pages 51–65. Springer, 2008.
[FH06]
Martin Fränzle 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änzle, 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änzle, 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ür Angewandte Mikroelektronik und Datentechnik, Fakultät
für Informatik und Elektrotechnik, Universität Rostock, 2013.
13
Source Exif Data:
File Type : PDF File Type Extension : pdf MIME Type : application/pdf PDF Version : 1.4 Linearized : No Page Count : 13 Producer : pdfTeX-1.40.10 Creator : TeX Create Date : 2014:04:09 10:30:54+02:00 Modify Date : 2014:04:09 10:30:54+02:00 Trapped : False PTEX Fullbanner : This is pdfTeX, Version 3.1415926-1.40.10-2.2 (TeX Live 2009/Debian) kpathsea version 5.0.0EXIF Metadata provided by EXIF.tools