Commits · 124402b2d26e0dc003f5fdb467e5be7ee7c478f3 · tables / jtet · GitLab

Nov 15, 2013
- Handle variable predicates in the generators. · 124402b2
  Matthew Dawson authored Nov 15, 2013
  124402b2
- Implement subtype predicate parsing. · e26861dc
  Matthew Dawson authored Nov 15, 2013
  e26861dc
- Implement the NotEquals operator. · bfacefd7
  Matthew Dawson authored Nov 15, 2013
  bfacefd7
- Implement a parser to extract PVS subtype expressions from variable types. · c44ced20
  Matthew Dawson authored Nov 15, 2013
  c44ced20
- To test the PVS parser, make the MatlabParserOperatorParseTest generic. · 1ca5f025
  Matthew Dawson authored Nov 15, 2013
  1ca5f025
- Add a simple PVS parser for use in subtyping. · fdabb422
  Matthew Dawson authored Nov 15, 2013
  fdabb422
- Move some forgotten Matlab specific code into its parser. · 0454753a
  Matthew Dawson authored Nov 15, 2013
  0454753a
- Rename all expression pieces to not mention Matlab explicitly. · 2d0e7606
  Matthew Dawson authored Nov 15, 2013
  2d0e7606
- Similar to VariableParser, also make MatlabParser a single static method. · a5bb9d3c
  Matthew Dawson authored Nov 15, 2013
  a5bb9d3c
- Make VariableParser into a static only class. · 0d7bdaae
  Matthew Dawson authored Nov 15, 2013
  0d7bdaae
- Remove the matlab2smt, and create appropriate other packages. · 171008e5
  Matthew Dawson authored Nov 15, 2013
  171008e5
- Move all the java code to the package ca.mcmaster.cas.tabularexpressiontoolbox. · 13ee85a0
  Matthew Dawson authored Nov 15, 2013
  13ee85a0
- Add some toString methods to help debugging. · 54cf6993
  Matthew Dawson authored Nov 15, 2013
  54cf6993
Sep 30, 2013
- Handle negative and fractional outputs from SMTLIB. · 01b5369e
  Matthew Dawson authored Sep 30, 2013
  01b5369e
- When parsing SMTLibOut, parse the decimal point as a period. · 9c489c27
  Matthew Dawson authored Sep 30, 2013
  9c489c27
- Use proper grammar for SMTLIB output. · d7dd1878
  Matthew Dawson authored Sep 30, 2013
  d7dd1878
- Update antlr to version 4.1 · a744556b
  Matthew Dawson authored Sep 30, 2013
  a744556b
- Update the assembly plugin to the latest version. · cbe7569f
  Matthew Dawson authored Sep 30, 2013
  cbe7569f
Sep 27, 2013
- CVC3 doesn't allow decimal points, thus always use fractions. · d8d600e2
  Matthew Dawson authored Sep 27, 2013
  d8d600e2
- Add a system to change the start of the TCC numbering for CVC3. · 248c951a
  Matthew Dawson authored Sep 27, 2013
  248c951a
- Finish testing fixed point support for CVC3. · a09331a5
  Matthew Dawson authored Sep 27, 2013
  a09331a5
- Fix a bug when generating Binary Operations. · 96e09a93
  Matthew Dawson authored Sep 27, 2013
  96e09a93
- Start implementing fixed point back again with *all* the operators. · a4c52b62
  Matthew Dawson authored Sep 27, 2013
  a4c52b62
- Remove useless output from MatlabParser now. · 9d36304b
  Matthew Dawson authored Sep 27, 2013
  9d36304b
- Implement Real operators for CVC3 generation. · 19d00816
  Matthew Dawson authored Sep 27, 2013
  19d00816
- Implement other important math operators for SMTLIB. · 663dd0de
  Matthew Dawson authored Sep 27, 2013
  663dd0de
- Massive change for type handling in expressions. · 17e787e8
  Matthew Dawson authored Sep 27, 2013
  17e787e8
- Implement parsing for all important binary operators. · fe1891b2
  Matthew Dawson authored Sep 27, 2013
  fe1891b2
- Test simple parsing of operators. · 8b8d9c2a
  Matthew Dawson authored Sep 27, 2013
  8b8d9c2a
Sep 19, 2013
- SampleValues has to be public in CheckerRunnerResult for Matlab. · 44f9c253
  Matthew Dawson authored Sep 19, 2013
  44f9c253
- Handle the case when no complete queries exist in the grid walker. · 37749598
  Matthew Dawson authored Sep 19, 2013
  37749598
- In the smtlib grid generator test, don't mention cvc3. · 1a349538
  Matthew Dawson authored Sep 19, 2013
  1a349538
- Implement a z3 runner. · c4bae550
  Matthew Dawson authored Sep 19, 2013
  c4bae550
- Add a utility class to hold checker results. · 984056ae
  Matthew Dawson authored Sep 19, 2013
  984056ae
- When parsing Matlab code, make sure the parsed code always ends in a newline. · 6e700218
  Matthew Dawson authored Sep 19, 2013
  6e700218
- Rename smtlibgenerator to smtlibchecker. · 5a9fe5d0
  Matthew Dawson authored Sep 19, 2013
  5a9fe5d0
- First run at SMT-LIB generated table test. · 3206e6d5
  Matthew Dawson authored Sep 19, 2013
  3206e6d5
- SMT-LIB requires real literals to have a decimal point. So we do that. · 55ef62af
  Matthew Dawson authored Sep 19, 2013
  55ef62af
- Implement most of the important matlab -> smtlib generation code. · b75ffb25
  Matthew Dawson authored Sep 19, 2013
  b75ffb25
- Start implementing the SMTLIBGenerator for matlab syntax. · f2e3628a
  Matthew Dawson authored Sep 19, 2013
  f2e3628a