Newer
Older
Colin Eles
committed
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
function [ check, seqs ] = cvc_check( object )
%CVC_CHECK Summary of this function goes here
% Detailed explanation goes here
box = waitbar(0,'Generating Proof Script');
[filename, queries] = object.generate_file;
waitbar(.10,box,'Running Proof');
[status, result] = system(['cvc3 ' filename])
waitbar(.70,box,'Parsing Results');
seqs = [];
for i = 1:size(queries,2)
asserts = [];
% find results of individual queries, using regexp and notations in
% output begin1 ... end1
query_result = regexp(result,['(?<=begin' num2str(i) ').*(?=end' num2str(i) ')'],'match');
invalid_found = regexp(char(query_result),'Invalid.');
if ~isempty(invalid_found)
% formula was found to be invalid
% look for a counter example
asserts = regexp(char(query_result),'(?<=ASSERT[ ]*\()[^\n]*(?==)|(?<==)[^\n]*(?=\);)','match');
% for j = 1:size(asserts,2)
% splits = {splits regexp(asserts(j),'=','split')};
%
% end
seqs = [seqs struct('id', '1234a', 'TCC', 'test', 'seq', queries(i), 'ce', {asserts})];
end
end
if isempty(seqs)
check = 1
else
check = 0;
end
waitbar(1,box,'Deleting Proof Script');
delete(box);
end