| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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"). | |||
| 2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2018-03-05 | Add support for check-sat-assuming. (#1637) | Aina Niemetz | |
| This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). | |||
| 2018-02-27 | Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627) | Aina Niemetz | |
| 2018-02-20 | Minor fixes and additions for transcendental functions (#1612) | Andrew Reynolds | |
| Also adds parsing support for PI in smt2 with syntax "real.pi". | |||
| 2018-02-08 | Inlining line_buffered_input to avoid warning about unused variables in ↵ | Tim King | |
| production builds. (#1584) | |||
| 2018-02-07 | Fixing more inconsistent usages of override. (#1575) | Tim King | |
| 2018-02-07 | Add remaining transcendental functions (#1551) | Andrew Reynolds | |
| 2018-01-09 | Cleaning up throw specifiers on Exception and subclasses. (#1475) | Tim King | |
| 2018-01-06 | Removing throw specifiers from src/parser/. (#1486) | Tim King | |
| 2017-12-27 | Rel smt parser (#1446) | Arjun Viswanathan | |
| 2017-12-10 | Fix issue 1433. (#1435) | Andrew Reynolds | |
| 2017-12-06 | Add command for define-fun-rec and add to API (#1412) | Andrew Reynolds | |
| 2017-12-01 | Fix reset-assertions (#1413) | Andres Noetzli | |
| This commit fixes two issues with reset-assertions: - pending pops were not done in SmtEngine, resulting in the following assertion failure: d_userLevels.size() == 0 && d_userContext->getLevel() == 1 - all definitions were erased on reset-assertion in an SMT2 file, leading to errors about undefined types | |||
| 2017-12-01 | Refactor and generalize PBE strategies (#1410) | Andrew Reynolds | |
| 2017-11-29 | Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372) | Tim King | |
| 2017-11-23 | Ho parsing and regressions (#1350) | Andrew Reynolds | |
| 2017-11-22 | Sygus Lambda Grammars (#1390) | 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