summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
AgeCommit message (Collapse)Author
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-01-06Removing throw specifiers from src/parser/. (#1486)Tim King
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-10-05Fix typo in comment.Clark Barrett
2017-10-03Op overload parser (#1162)Andrew Reynolds
* Update parser for operator overloading. * Improvements * Updates * Add assert
2017-07-07Update copyright headers.Mathias Preiner
2016-11-11Deleting the remaining commands in the Parser's queue within ~Parser().Tim King
2016-11-01Revert change to Datatypes API to return vector of DatatypeTypes, as before. ↵ajreynol
ASAN failures with datatypes should now be mostly fixed.
2016-11-01Revert change to datatypes API for passing pointers, instead make deep copy ↵ajreynol
during call to mkMutualDatatypes.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-04-20update from the masterPaulMeng
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2014-11-17Resource-limiting work.Liana Hadarean
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-06Support for RESET command in CVC native language (and infrastructure for ↵Morgan Deters
support elsewhere).
2014-07-01Update copyrights.Morgan Deters
2014-06-21API documentation improvements.Morgan Deters
2014-06-06Sets translate, and other short fixesKshitij Bansal
- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine
2014-04-29Fix for --force-logic to extend its reach to the parser.Morgan Deters
2013-09-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵Morgan Deters
segfault in smt2 printer
2013-06-19Fix to the "include" extended feature of the SMT-LIB parserMorgan Deters
2013-06-19Give a more useful parse error message for "undeclared variable -1".Morgan Deters
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
2013-06-07Allow disabling include-file featureMorgan Deters
2013-05-20Detect multiply-defined :named annotations and issue an error.Morgan Deters
Thanks to David Cok for pointing out this issue. Conflicts: library_versions
2013-05-20Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵Morgan Deters
mode. Thanks to David Cok for raising this issue.
2013-05-20Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵Morgan Deters
in some places Thanks to David Cok for reporting these issues.
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-12-11Ignore unknown term annotations (giving a warning). Resolves bug 479.Morgan Deters
2012-11-28Bug fix:Morgan Deters
* Fix creation of bound variables in CVC native language parser * This corrects a problem with misleading model output (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-28Public interface review items:Morgan Deters
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
* rename DeclarationScope to SymbolTable * rename all HashStrategy -> HashFunction (which we often have anyways) * remove CDCircList (no one is currently using it)
2012-06-22Parser: add the possibility to bind at level 0.François Bobot
2012-06-07LogicInfo locking implemented, and some initialization-order issues in ↵Morgan Deters
SmtEngine resolved. ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2011-10-04compat layer cleanupMorgan Deters
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-14add AscriptionType stuff to support nullary parameterized datatypes; also, ↵Morgan Deters
review of Andy's earlier commit, with some minor code clean-up and documentation
2011-05-13added support for parametric datatypes, updated cvc parser to handle ↵Andrew Reynolds
parametric datatypes, type ascriptions are not implemented yet
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
* work around a lexer ambiguity in CVC grammar * add support for tracing antlr parser/lexer * add parsing support for more language features * initial parameterized types parsing work to support Andy's work
2011-04-20numerous bugfixesMorgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
Expected performance impact outside of datatypes/CVC parser is negligible. * CVC language LAMBDA, functional LET, type LET, precedence fixes, bitvectors, and arrays, with partial parsing support also for quantifiers, tuples, subranges, subtypes, and records * support for complex recursive DATATYPE selectors, e.g. tree = node(children:ARRAY INT OF tree) | leaf(data:INT) these are complicated because they have to be left unresolved at parse time and dealt with in a second pass. * bugfix for Exprs/Types that occurred when setting them to null (not Nodes/TypeNodes, just Exprs/Types). * Cleanup/code review items
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback