summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
AgeCommit message (Collapse)Author
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
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type. 2. CVC language parser supports datatypes. 3. CVC language printer now functional. 4. Minor other cleanups. No performance impact is expected outside of datatypes. I'm verifying that that is the case with a cluster job this morning.
2011-04-10merge from replay branchMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some ↵Morgan Deters
documentation, and make it possible to "make doc" on a clean source tree (post-configure)
2010-10-26Cleaning up some header filesChristopher L. Conway
2010-10-23Adding Parser::setInput and using it in InteractiveShell (Fixes: #225)Christopher L. Conway
Removing ParserBuilder::withStateFrom
2010-10-20Adding support for interactive modeChristopher L. Conway
2010-10-09reverting some changes to parser from last commitMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback