Skip to content
Snippets Groups Projects
Commit 5343fad5 authored by Colin Eles's avatar Colin Eles
Browse files

fixed a bug with trig libraries

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6916 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 6c8b4b81
No related branches found
No related tags found
No related merge requests found
...@@ -21,7 +21,7 @@ function [ check, seqs ] = cvc_check( object ) ...@@ -21,7 +21,7 @@ function [ check, seqs ] = cvc_check( object )
waitbar(.10,box,'Running Proof'); waitbar(.10,box,'Running Proof');
% run the cvc command % run the cvc command
[status, result] = system(['cvc3 ' filename ' +model']); [status, result] = system(['cvc3 ' filename ' +model'])
% check return status for errors % check return status for errors
if (status ~= 0) if (status ~= 0)
......
...@@ -42,7 +42,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel'))) ...@@ -42,7 +42,7 @@ if (exists == 1 && (isempty(button) || strcmp(button,'Cancel')))
output = 'canceled'; output = 'canceled';
return; return;
elseif (exists == 1 && (strcmp(button,'Open PVS'))); elseif (exists == 1 && (strcmp(button,'Open PVS')));
[status, result] = system(['pvs ' function_name '.pvs']); [status, result] = system(['pvs ' function_name '.pvs'])
output = 'canceled'; output = 'canceled';
elseif (exists == 0 || strcmp(button,'Attempt to prove')) elseif (exists == 0 || strcmp(button,'Attempt to prove'))
box = waitbar(0,'Generating Proof Script'); box = waitbar(0,'Generating Proof Script');
......
...@@ -22,7 +22,8 @@ function string = pvs_check_for_imports(object) ...@@ -22,7 +22,8 @@ function string = pvs_check_for_imports(object)
hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}}; hashtable = {{'sqrt', 'reals@sqrt'} {'sin', 'trig@trig_basic'} {'cos', 'trig@trig_basic'} {'tan', 'trig@trig_basic'}};
for k=1:size(hashtable,2) for k=1:size(hashtable,2)
if ~isempty(regexp(object.data.function_inputs,hashtable{k}(1),'once')) functions = regexp(object.data.function_inputs,hashtable{k}(1),'once')
if ~isempty(functions{1})
if (~any(ismember(found,hashtable{k}(1)))) if (~any(ismember(found,hashtable{k}(1))))
string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')]; string = [string 'IMPORTING ' char(hashtable{k}(2)) sprintf('\n')];
found = [found hashtable{k}(1)]; found = [found hashtable{k}(1)];
......
...@@ -11,6 +11,6 @@ function [] = init(object) ...@@ -11,6 +11,6 @@ function [] = init(object)
object.pvs_includes = []; object.pvs_includes = [];
object.counter_trials = 1000; object.counter_trials = 1000;
object.counter_range = 100; object.counter_range = 100;
object.exception = 0; object.except = 0;
end end
...@@ -15,7 +15,6 @@ object.counter_range = settings.range; ...@@ -15,7 +15,6 @@ object.counter_range = settings.range;
if ~isfield(settings,'except') if ~isfield(settings,'except')
settings.except = 0; settings.except = 0;
end end
%object.except = settings.except; object.except = settings.except;
object.except = 1;
end end
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment