| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-03-27 | Support unicode internal representation and escape sequences (#3852) | Andrew Reynolds | |
| Work towards support for the strings standard. This updates the string solver and parser such that: The internal representation of strings is vectors of code points, Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models, The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings, Handle unicode escape sequences according to the SMT-LIB standard in String, Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary, Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points. | |||
| 2020-03-15 | Handle cases in --sygus-rr where evaluation is not constant (#4100) | Andrew Reynolds | |
| Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant. Fixes #4096 and fixes #4089. | |||
| 2020-03-13 | Fix case of non-constant value for sygus sampling (#4051) | Andrew Reynolds | |
| Fixes #4050. | |||
| 2019-12-12 | Use the node-level datatypes API (#3556) | Andrew Reynolds | |
| 2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner | |
| 2019-03-26 | Update copyright headers. | Aina Niemetz | |
| 2019-03-14 | Generalize sygus-rr-verify for fast enumerator (#2829) | Andrew Reynolds | |
| 2019-03-12 | Add option --sygus-rr-synth-rec for considering all grammar types ↵ | Andrew Reynolds | |
| recursively (#2270) | |||
| 2018-10-12 | Improvements to rewrite rules from inputs (#2625) | Andrew Reynolds | |
| 2018-08-20 | Minor improvements to the interface for sygus sampler (#2326) | Andrew Reynolds | |
| 2018-07-26 | Fix a few issues in the sygus sampler related to evaluation (#2215) | Andrew Reynolds | |
| 2018-07-08 | Add more sophisticated floating-point sampler (#2155) | Andres Noetzli | |
| This commit adds a floating-point sampler inspired by PyMPF [0]. It also creates a new Sampler class that can be used for creating random values of different sorts (currently BV and FP values). [0] https://github.com/florianschanda/PyMPF | |||
| 2018-07-04 | Minor changes to sygus-rr utilities to support floating point rewrites (#2148) | Andrew Reynolds | |
| 2018-07-04 | Reorganize candidate rewrite rule filtering (#2116) | Andrew Reynolds | |
| 2018-06-29 | Use evaluator in sygus sampler. (#2117) | Andrew Reynolds | |
| * Use evaluator for sygus sampler. * Format | |||
| 2018-06-27 | Synthesize candidate-rewrites from standard inputs (#1918) | Andrew Reynolds | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
| 2018-05-03 | Move Lazy trie datastructure to its own file (#1871) | Haniel Barbosa | |
| Preparation for further developing CegisUnif | |||
| 2018-04-21 | Improve sygus sampling for strings (#1802) | Andrew Reynolds | |
| 2018-04-20 | Reenable filtering based on ordering in sygus sampler (#1784) | Andrew Reynolds | |
| 2018-04-10 | Improve accuracy of stats for sygus sampler (#1755) | Andrew Reynolds | |
| 2018-03-27 | Fix for --sygus-rr-synth (#1723) | Andrew Reynolds | |
| 2018-03-27 | Filter candidate rewrites based on matching (#1682) | Andrew Reynolds | |
| 2018-03-20 | Minor fix and addition to sygus sampler (#1678) | Andrew Reynolds | |
| 2018-03-05 | Fix for sampler. (#1639) | Andrew Reynolds | |
| 2018-03-02 | Print candidate rewrites in terms of original grammar (#1635) | Andrew Reynolds | |
| 2018-02-27 | Improvements to sygus sampling (#1621) | Andrew Reynolds | |
| 2018-02-12 | Minor improvements to sygus sampler (#1598) | Andrew Reynolds | |
| 2018-02-09 | Class to reduce printing of redundant candidate rewrites (#1588) | Andrew Reynolds | |
| 2018-02-08 | Minor improvements to sygus sampling. (#1577) | Andrew Reynolds | |
| 2018-02-05 | Statically eliminate redundant sygus constructors (#1560) | Andrew Reynolds | |
| 2018-02-04 | Sample based on sygus grammar by default (#1558) | Andrew Reynolds | |
| 2018-02-02 | Option to use sampling for CEGIS (#1555) | Andrew Reynolds | |
| 2018-02-01 | Use sygus to synthesize/verify rewrite rules (#1547) | Andrew Reynolds | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback