SMT-LIB2 commands and proof checker, functional style

Functions
SORTS	sorts (size_t nb, SORT *data)
	Listing the uninterpreted sorts. More...
FUNSYMS	funsyms (size_t nb, FUNSYM *data)
	Listing the uninterpreted function and predicate symbols. More...
ASSERTIONS	assertions (size_t nb, EXPR *data)
	Listing the assertions. More...
SMTLIB2	smtlib2 (SORTS s, FUNSYMS f, ASSERTIONS a)
	Representing an SMT-LIB2 problem. More...
int	checker (SMTLIB2 smt, CERTIF proof)
	Checking a certificate with the certified checker. More...
void	debug_checker (SMTLIB2 smt, CERTIF proof)
	Checking a certificate with the uncertified debugging checker. More...

Detailed Description

The functional style calls the checker on lists of sorts, symbols and assertions declarations, as well as the certificate. The proof can be checked using either the certified checker checker or the uncertified checker for debugging debug_checker.

Function Documentation

assertions()

ASSERTIONS assertions	(	size_t	nb,
		EXPR *	data
	)

Listing the assertions.

This function lists the assertions, whose conjunction will be checked for unsatisfiability.

Parameters

nb	The number of assertions.
data	A pointer to the assertions.

Returns

The list of assertions.

checker()

int checker	(	SMTLIB2	smt,
		CERTIF	proof
	)

Checking a certificate with the certified checker.

This function calls the certified checker on the problem and the certificate.

Parameters

smt	The SMT-LIB2 problem.
proof	The certificate.

Returns

Any non-zero number means that the certificate is valid.

debug_checker()

void debug_checker	(	SMTLIB2	smt,
		CERTIF	proof
	)

Checking a certificate with the uncertified debugging checker.

This function calls the uncertified debugging checker on the problem and the certificate. Step by step proof checking is printed in the standard output.

Parameters

smt	The SMT-LIB2 problem.
proof	The certificate.

funsyms()

FUNSYMS funsyms	(	size_t	nb,
		FUNSYM *	data
	)

Listing the uninterpreted function and predicate symbols.

This function lists the uninterpreted function and predicate symbols.

Parameters

nb	The number of uninterpreted function and predicate symbols to declare.
data	A pointer to the uninterpreted function and predicate symbols to declare.

Returns

The list of uninterpreted function and predicate symbols.

smtlib2()

SMTLIB2 smtlib2	(	SORTS	s,
		FUNSYMS	f,
		ASSERTIONS	a
	)

Representing an SMT-LIB2 problem.

This function groups together the lists of sorts, symbols and assertions.

Parameters

s	The list of uninterpreted sorts.
f	The list of uninterpreted function and predicate symbols.
a	The list of assertions.

Returns

The SMT-LIB2 problem.

sorts()

SORTS sorts	(	size_t	nb,
		SORT *	data
	)

Listing the uninterpreted sorts.

This function lists the uninterpreted sorts.

Warning

The sorts sort("Bool") and sort("Int") are interpreted and should not appear in the list.

Parameters

nb	The number of uninterpreted sorts to declare.
data	A pointer to the uninterpreted sorts to declare.

Returns

The list of uninterpreted sorts.