SMT-LIB2 commands and proof checker, imperative style

Functions
void	start_smt2 ()
	Starting a proof. More...
void	declare_sort (SORT s)
	Declaring a sort. More...
void	declare_fun (FUNSYM f)
	Declaring a function or predicate symbol. More...
void	assertf (EXPR f)
	Asserting a formula. More...
int	check_proof (CERTIF proof)
	Checking a certificate with the certified checker. More...
void	debug_check_proof (CERTIF proof)
	Checking a certificate with the uncertified debugging checker. More...

Detailed Description

The imperative style directly correspond to SMT-LIB2 commands. A proof starts with start_smt2(), then sorts, function and predicate symbols, and assertions are declared. Finally, the proof is checked, using either the certified checker check_proof or the uncertified checker for debugging debug_check_proof.

Function Documentation

assertf()

void assertf

(

EXPR

f

)

Asserting a formula.

This function asserts the formula f.

Parameters

f	The formula that is asserted.

check_proof()

int check_proof

(

CERTIF

proof

)

Checking a certificate with the certified checker.

This function calls the certified checker on the problem that was input in the imperative style.

Parameters

proof

The certificate.

Returns

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

debug_check_proof()

void debug_check_proof

(

CERTIF

proof

)

Checking a certificate with the uncertified debugging checker.

This function calls the uncertified debugging checker on the problem that was input in the imperative style. Step by step proof checking is printed in the standard output.

Parameters

proof

The certificate.

declare_fun()

void declare_fun

(

FUNSYM

f

)

Declaring a function or predicate symbol.

This function declares the uninterpreted function or predicate symbol f.

Parameters

f	The uninterpreted function or predicate symbol to declare.

declare_sort()

void declare_sort

(

SORT

s

)

Declaring a sort.

This function declares the uninterpreted sort s.

Warning

The sorts sort("Bool") and sort("Int") are interpreted and should not be declared.

Parameters

s	The uninterpreted sort to declare.

start_smt2()

void start_smt2

(

)

Starting a proof.

This function starts the imperative proof mode.