| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
| 2018-10-18 | Introducing internal commands for SyGuS commands (#2627) | Haniel Barbosa | |
| 2018-10-02 | Allow (_ to_fp ...) in strict parsing mode (#2566) | Andres Noetzli | |
| When parsing with `--strict-parsing`, we are checking whether the operators that we encounter have been explicitly added to the `d_logicOperators` set in the `Parser` class. We did not do that for the indexed operator `(_ to_fp ...)` (which is represented by the kind `FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator. | |||
| 2018-09-26 | Makes SyGuS parsing more robust in invariant problems (#2509) | Haniel Barbosa | |
| 2018-09-22 | cmake: Enable -Wall. | Mathias Preiner | |
| 2018-09-22 | cmake: Add support for cross-compiling for Windows. | Mathias Preiner | |
| 2018-09-22 | cmake: More documentation, clean up. | Aina Niemetz | |
| 2018-09-22 | cmake: FindANTLR: Check if antlr3FileStreamNew is available. | Mathias Preiner | |
| 2018-09-22 | cmake: Add make install rule. | Mathias Preiner | |
| 2018-09-22 | cmake: Only build libcvc4 and libcvc4parser as libraries. | Mathias Preiner | |
| The sources of all previous libraries are now added to libcvc4 and built as libcvc4. This removes circular dependencies between libcvc4 and libexpr. Further, we now only have one parser library and don't build additional libraries for each language. | |||
| 2018-09-22 | cmake: Move find_package to where it is actually needed. | Mathias Preiner | |
| 2018-09-22 | cmake: Add library versioning for libcvc4.so. | Mathias Preiner | |
| 2018-09-22 | cmake: Fix some includes. | Mathias Preiner | |
| 2018-09-22 | cmake: Cleanup CMakeLists.txt files, remove SHARED. | Mathias Preiner | |
| 2018-09-22 | cmake: Working build infrastructure. | Mathias Preiner | |
| TODO: cvc4autoconfig.h | |||
| 2018-09-22 | cmake: Antlr parser generation done. | Mathias Preiner | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-11 | Fixe compiler warning in line_buffer.cpp. (#2453) | Aina Niemetz | |
| 2018-08-27 | Make division chainable in the smt2 parser (#2367) | Andrew Reynolds | |
| 2018-08-23 | Use "filename" instead of "name" in SmtEngine::setInfo() (#2361) | Andres Noetzli | |
| 2018-08-21 | Fix processing of nested Variable construct in sygus let bodies (#2351) | Andrew Reynolds | |
| 2018-08-21 | Warn and enable quantifiers when using sygus + logics with QF (#2352) | Andrew Reynolds | |
| 2018-08-20 | Remove support for prototype (non-sygus) synthesis (#2338) | Andrew Reynolds | |
| 2018-08-17 | Split sygus grammar to its own ANTLR grammar (#2307) | Andrew Reynolds | |
| 2018-08-08 | Plug solver API object into parser. (#2240) | Aina Niemetz | |
| 2018-08-07 | Simplify and improve the sygus parser (#2266) | Andrew Reynolds | |
| Currently, there is code duplication for parsing constants in sygus grammars, e.g.: https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048 https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304 This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g. As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants. It also removes some unnecessary code for converting builtin kinds to their total versions. This is work towards #2197. We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols. | |||
| 2018-08-07 | Delete functions instead of using CVC4_UNDEFINED (#1794) | Andres Noetzli | |
| C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable. | |||
| 2018-08-06 | Add RegLan to smt2/sygus parsers. (#2276) | Andrew Reynolds | |
| 2018-08-06 | Remove support for Enum sygus syntax. (#2264) | Andrew Reynolds | |
| 2018-08-02 | Parse standard separation logic inputs (#2257) | Andrew Reynolds | |
| 2018-08-01 | Fix issues with printing parametric datatypes in smt2 (#2213) | Andrew Reynolds | |
| 2018-07-14 | sygusComp2018: update semantics for declare-fun in sygus. (#2102) | Andrew Reynolds | |
| 2018-07-02 | Improve error message. (#2124) | Andrew Reynolds | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-06-04 | Only enable transcendentals if logic is N[I]RAT (#2052) | Andres Noetzli | |
| 2018-05-29 | Make user's SMT2 version override file version (#2004) | Andres Noetzli | |
| 2018-05-29 | Track input language in a single place (#2003) | Andres Noetzli | |
| 2018-05-22 | Parse error for sygus grammar term with multiple let bodies (#1961) | Andrew Reynolds | |
| 2018-05-21 | Improvements in parsing and printing related to mixed int/real (#1879) | Andrew Reynolds | |
| This eliminates some hacks for dealing with Int/Real. - Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA. - Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant. - Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852. - Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml). | |||
| 2018-05-08 | Support for str.<= and str.< (#1882) | Andrew Reynolds | |
| 2018-05-07 | Add support for str.code (#1821) | Andrew Reynolds | |
| 2018-05-03 | Fix redundant internalPush calls. (#1865) | Mathias Preiner | |
| The SMT2 parser by default passes a true expression to the CheckSatCommand, which results in checkSatisfiability (in SmtEngine) to always do an internal push. As a consequence, the work of each check-sat was reset even though no user level push/pop happened. | |||
| 2018-05-02 | Support HORN logic string (#1849) | Andrew Reynolds | |
| 2018-05-02 | Initial support for string standard in smt lib 2.6 (#1848) | Andrew Reynolds | |
| 2018-04-08 | Check free variables in assertions (#1737) | Andrew Reynolds | |
| 2018-04-08 | Do not introduce uinterpreted constants in TPTP parser (#1743) | Andrew Reynolds | |
| 2018-04-06 | Add define rec fun to cvc parser (#1738) | Arjun Viswanathan | |
| 2018-04-02 | Remove references to nyu (#1721) | Clark Barrett | |
| 2018-03-09 | Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653) | Aina Niemetz | |
| 2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
| * Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
 |
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