My favorites | Sign in
Project Home Downloads Wiki Issues Source
Checkout   Browse   Changes    
 
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
CSIsat is an open-source interpolating decision procedure for LA+EUF.

Usage:
Reads the query from stdin and writes the result to stdout.

If the input formula is satisfiable,
CSIsat writes "Satisfiable: <formula>" on stderr.
'formula' implies the conjunction of the two input formula.
Otherwise it writes an interpolant to stdout.
The computed interpolant can be verified with option -check.

Options:
--------
-debug Print debug information.
-check Check the computed interpolant (consumes additional runtime).
-sat Check for satisfiability only (no interpolation).
Writes only "satisfiable" or "unsatisfiable" to stdout.
-LAsolver Choose the LA solver to use.
Options: simplex, simplex_wo_presolve, interior, exact (default: simplex).
WARNING: exact solver integration is still experimental.
-SATsolver Choose the SAT solver to use.
Options: csi_dpll, pico (default: csi_dpll). The PicoSAT integration is experimental.
-help Display this list of options.
-syntax Choose the syntax to use.
Options: foci, infix (default: try foci first then infix if it fails).
-round Try to round the coefficient to integer values. WARNING: has a limited precision.


Input language:
---------------
The language is similar to Foci.

query :: formula ; formula ; ... ; formula

formula :: '=' term term
| '<=' term term
| '&' '[' formula ... formula ']'
| '|' '[' formula ... formula ']'
| '~' formula

term :: variable
| '+' '[' term ... term ']'
| '*' number term
| function_symbol '[' term ... term ']'

'number' is an integer, floating point, or a ratio (number '/' number).

There is also an infix syntax:

query :: formula ; formula ; ... ; formula

formula :: term '=' term
| term '<=' term
| term '<' term
| term '>=' term
| term '>' term
| formula '->' formula
| formula '<->' formula
| formula '&' formula
| formula '|' formula
| 'not' formula

term :: variable
| term '+' term
| term '-' term
| number '*' term
| '-' term
| function_symbol '(' term , ... , term ')'

(precedence levels are [->,<->], [&,|], [not]. They are parsed as
left-associative.)

Change log

r132 by DirkBeyer7201 on Dec 18, 2008   Diff
Removed some exec props.
Go to: 
Project members, sign in to write a code review

Older revisions

r129 by DirkBeyer7201 on Dec 18, 2008   Diff
Authors.txt added in order to
acknowledge people.
r125 by DirkBeyer7201 on Oct 25, 2008   Diff
comment about -check
r98 by Rilaak on Jul 8, 2008   Diff
[No log message]
All revisions of this file

File info

Size: 2308 bytes, 71 lines

File properties

svn:eol-style
native
Powered by Google Project Hosting