summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Collapse)Author
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-02Support HORN logic string (#1849)Andrew Reynolds
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-04-08Do not introduce uinterpreted constants in TPTP parser (#1743)Andrew Reynolds
2018-04-06Add define rec fun to cvc parser (#1738)Arjun Viswanathan
2018-04-02Remove references to nyu (#1721)Clark Barrett
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-08Inlining line_buffered_input to avoid warning about unused variables in ↵Tim King
production builds. (#1584)
2018-02-07Fixing more inconsistent usages of override. (#1575)Tim King
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
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-29Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)Tim King
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-07Initializing Smt1::d_logic in all cases. This was resolved by extending the ↵Tim King
Logic enum with an UNSET value. (#1329)
2017-11-07 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)Tim King
* Removing an unused member from Tptp. Initializing members of Tptp. * Removing delcaration for myPopCharStream.
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-11-03Suppport SAT logic (#1310)Andrew Reynolds
* Support SAT logic. * Add lustre example. * Add to smt1 as well. * Fix. * Fix. * Fix for new option.
2017-10-27Modify LDFLAGS to support shared libraries for Win (#1280)Andres Noetzli
* Use uintptr_t for pointer casts in Swig files CVC4's Swig interface files were casting pointers to longs in multiple instances. The problem with that is that on certain platforms *cough* Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit executable (they use the LLP64 data model). This made the compilation of language bindings fail with MinGW. This commit changes the types to uintptr_t defined in Swig's stdint.i. * Modify LDFLAGS to support shared libraries for Win This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which is required for building DLLs (shared libraries on Windows). It also adds "--export-all-symbols" to the linker flags of the parser to ensure that there are no unresolved symbols when linking against it (see comment in the Makefile.am for details). * Fix for non-Windows builds * add no-undefined to libcvc4compatjni
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-18Tptp unsat cores (#1228)Andrew Reynolds
* Support unsat cores for TPTP. * Fix assertion
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.
2017-10-05Fix typo in comment.Clark Barrett
2017-10-05Minor change to how SyGus commands are translated to SmtEngine commands. ↵Andrew Reynolds
This ensures a single success is printed for synth-fun and synth-inv. (#1193)
2017-10-03Op overload parser (#1162)Andrew Reynolds
* Update parser for operator overloading. * Improvements * Updates * Add assert
2017-09-27Fix seeking for buffered input (#1145)Andres Noetzli
CVC4's implementation of seek was calculating the pointer difference between the current position in the input and the seek point to determine how many characters to consume. This was causing problems when ANTLR was seeking to a pointer on a line after the current line because it would result in a big number of characters to consume because each line is allocated separately. This resulted in issue #1113, where CVC4 was computing a large number of characters to consume and would block until it received all of them. This commit fixes and simplifies the code by simply consuming characters until the seek point is reached without computing a count beforehand.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback