added directory for examples as well as some examples pulled from FPGA presentation, added example for quadratic roots problem solved using predicate subtyping which typechecks and appears to give proper answers when compared to matlab roots fcn

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6762 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6759 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

added support to look for known functions and import their associated pvs libraries automatically, currently only have sqrt, but can add more as they come up

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6742 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6716 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6715 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6714 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

fixed a small but major bug which I didn't notice before affected checking table with subgrids in cvc

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6713 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6667 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6653 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6638 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6621 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6620 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

added a utility file for checking for unsuppressed output, ie stuff that will print to the command window. thinking of putting it on file exchange because its fairly useful

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6619 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6612 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6611 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6600 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6599 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6594 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6593 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6590 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6589 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6588 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6587 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

updated GUI to generalize the typecheck procedure, default prover is now CVC, although this can be changed, currently not saved to the block, so each time you open it will go back to CVC, may want to change this in the future. need to fix some stuff in validation report

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6562 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

no longer runs COUNTERMODEL everytime, actually didn't even need to do the running twice idea as dissucessed earlier, actually a command line flag +model, that will automatically display the countermodel for na invalid query.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6561 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6560 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

added support for dependant subtypes, seems to work well with ones like the power conditioning example, if you try to give a specific type, ie. {x:real|x>5}, cvc is not able to prove unless you provide a witness of the type. Currently translates from pvs style typing to the cvc style so that user only needs to know one way, the pvs way is cleaner

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6559 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6558 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6556 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6525 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6524 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6523 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6521 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6520 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

begnining of application of SMT solver, using CVC3 solver. only works for 1D vertical grids right now, although easy to add more dimensions, etc. ALOT faster than PVS.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6519 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6360 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6352 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6351 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6319 57e6efec-57d4-0310-aeb1-a6c144bb1a8b

have a mode working where tool will generate a theory using the simulink types, as well as an constraints expressed in the pvs types. for example if input is x:real, but in simulink diagram input is int8, will create a theory where input is of type int8, copies a pvs theory of the types to the pwd, currently using integer subranges for types, and real for floating pt types, not sure if I should use IEEE754, might lose test case generation with this. Typechecker forces proving that no over/under flow for outputs, this is not always automatic, and grind seems to have trouble with it sometimes.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/trunk/TableTool@6318 57e6efec-57d4-0310-aeb1-a6c144bb1a8b