%%%%%%%%%%%  ARCA_SAT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


Arca_sat produces an smt-lib2 file specifying a problem equisatisfiable with the problem described in the input file, but not  containing 
cardinality constraints anymore. The default name of the output file is "TEST.smt2", but the user can specify an alternative name via 
the -O option. Type -h for the list of valid options.

The input file must be written according to the following instructions. 

Free arithmetic constants are allowed and should be declared (see below); free function symbols of domain Int and codomain are allowed 
too and should be declared; however functional application f(t) is allowed only when t is the unique bound variable (named 'x') and must 
be written as 'f<x>' (not as '(f x)' like in smt-lib2 standard).


The input file must consists of blocks, where each block must be a constant declaration set, an array declation set, an  arithmetic 
assertions set, a cardinality assetions set or a quantified assertion set. It is possible to specify many instances of the same kind of 
block. Blocks are independant from each other, but constants and functions must be declared only once and inside only one block.
The syntax of these  blocks is specified below; lines beginning with ';;' are comments and will be disregarded by the application.

WARNING:
Cardinality assertions (and also quantified assertions) must be simple flat (in a very strict sense): this means that  in such assertions 
the bound variable (which must be the variable x) must always occur only as an argument of a free function symbol and the only argument 
of a free function symbol must be this variable x. Arcasat does not check that this restriction is satisfied, but violating it produces 
complaints for undeclared symbols by the SMT-solver.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


(1) Constant declaration sets: these blocks must begin with the line

"CONSTANT_DECLARATIONS"

and end with the line

"Number_of_constant_declarations XX"

where XX is the number of the constant declarations in the block. Each other line in the block must be of the kind

"(declare-const <identifier> Int)"

where <identifier> is a valid SMT-LIB2 identifier (e.g. a <aA_zZ>* string). The very first declaration in the first constant declaration block 
must be 

"(declare-const N Int)"

Here N is used to indicate the dimension of the system (in other words, the bound variable x is assumed to range in the interval [0,N]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


(2) Array declaration sets: these blocks must begin with the line

"ARRAY_DECLARATIONS"

and end with the line

"Number_of_array_declarations XX"

where XX is the number of the array declarations in the block. Each other line in the block must be of the kind

(declare-fun <identifier> (Int) Int)

where <identifier> is a valid SMT-LIB2 identifier (e.g. a <aA_zZ>* string).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


(3) Arithmetic assertions sets: these must begin with the line

"ARITHMETIC_ASSERTIONS"

and end with the line

"Number_of_arithmetic_assertions XX"

where XX is the number of the assertions in the block. Each other line in the block must be of the kind

(assert <formula>  )

where <formula> is a valid smt-lib2 formula containing linear integer aritmetic operations and the declared constants. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


(4) Quantified assertions sets: these must begin with the line

"QUANTIFIED_ASSERTIONS"

and end with the line

"Number_of_quantified_assertions XX"

where XX is the number of the assertions in the block. Each other line in the block must be of the kind

(assert (forall ((x Int))  <formula>  ) )

where <formula> is a valid smt-lib2 simple flat formula containing linear integer aritmetic operations, the declared constants and the terms 
of the kind 'f<x>' where f is a declared array. Arcasat assumes that the universal quantifier is relativized to the interval [0,N)
(that is, '(forall ((x Int))' means 'for all x such that 0 <= x < N').


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


(5) Cardinality assertions sets: these must begin with the line

"CARDINALITY_ASSERTIONS"

and end with the line

"Number_of_cardinality_assertions XX"

where XX is the number of the assertions in the block. Each other line in the block must be of the kind

"(assert (= <constant_identifier> (card ((x Int)) <formula>))"

or of the kind

"(assert (= <constant_identifier> #{x | <formula> }))"

where <constant_identifier> is the identifier of a declared constant and <formula> is a valid smt-lib2 simple flat formula containing linear 
integer aritmetic operations, the declared constants and the terms of the kind 'f<x>' where f is a declared array. Notice that the constant
identifier must be the first argument of the equality predicate in a cardinality assertion.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OPTIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The current release of arcasat supplies the following command line options:

-h  display options;
-s  run the tool in silent mode;
-vN (where N=1,2,3): increasing verbosity level (default value is 1, it is possible to use -v0 with the same effect as -s);
-y  produces a Yices proof obbligations file (named .yices-log);
-O  (followed by "<name>") writes output proof obbligations in file <name>.smt2 (default name is "TEST").