summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Collapse)Author
2018-09-22cmake: Cleanup CMakeLists.txt files, remove SHARED.Mathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
TODO: cvc4autoconfig.h
2018-09-22cmake: Antlr parser generation done.Mathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-21 Fix processing of nested Variable construct in sygus let bodies (#2351)Andrew Reynolds
2018-08-21Warn 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-17Split sygus grammar to its own ANTLR grammar (#2307)Andrew Reynolds
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-07Simplify 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-06Add RegLan to smt2/sygus parsers. (#2276)Andrew Reynolds
2018-08-06Remove support for Enum sygus syntax. (#2264)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-07-14sygusComp2018: update semantics for declare-fun in sygus. (#2102)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-04Only 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-29Track input language in a single place (#2003)Andres Noetzli
2018-05-22Parse error for sygus grammar term with multiple let bodies (#1961)Andrew Reynolds
2018-05-21Improvements 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-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-03Fix 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-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-06Make 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-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-03-05Add 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-27Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)Aina Niemetz
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
Also adds parsing support for PI in smt2 with syntax "real.pi".
2018-02-07Fixing more inconsistent usages of override. (#1575)Tim King
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-01-06Removing throw specifiers from src/parser/. (#1486)Tim King
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-10Fix issue 1433. (#1435)Andrew Reynolds
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-12-01Fix 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-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-19Removing an unused variable from SygusInput. Resolves CID 1362932. (#1392)Tim King
2017-11-05Make higher-order a flag in logic info. (#1318)Andrew Reynolds
* Make higher-order a flag in logic info. * Format * Minor * Format
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks. * Minor fix * Fix bug in Node::hasBoundVar for non-ground operators. * Add regression. * Address review. * Apply clang format.
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
* Argument for strings class to specify whether to process escape sequences. * Change default value on string constructor. * Make CVC4::String::toString symmetric to the constructor for CVC4::String, document. * Clang format.
2017-10-12Sygus logics (#1226)Andrew Reynolds
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions. * Minor * Add case for reals, comment. * Fix regress1.
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand. * Comment * Pass expression names by reference. * Update throw specifiers. * Minor * Switch expression names to CDMap, simplify interface for printing unsat core names. * Revert throw specifier change. * Minor simplifcations
2017-10-09Split term database (#1206)Andrew Reynolds
* Move equality query to own file, move equality inference to quantifiers engine. * Move quantifiers attributes out of TermDb and into QuantAttribute. * Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header. * Split term database into term util. * Partial fix for #1205 that eliminates need for dependency in node.cpp. * Add more references to github issues.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback