summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
AgeCommit message (Collapse)Author
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
2010-10-09support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ↵Morgan Deters
define-fun; several set-info, set-option, get-option, get-info improvementss
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ↵Morgan Deters
working (just need to decide where to expand)
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, ↵Morgan Deters
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
2010-07-02re-generated comment headers of source filesMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
** file-level documentation at the top of the sources. ** This is the "make bugzilla stop bugging me" bugfix commit. * Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy. Updated documentation in the file. Resolves bug #99. * Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.) moved into a separate file. Partially resolves bug #100. * Moved isAssociative(Kind) into kind.h (and into the CVC4::kind namespace) instead of metakind.h (where it was in CVC4::metakind). This clears up a warning (private #inclusion) from the SMT and SMT2 parsers, and maybe makes more sense anyways, since this is based on the kind (and not the metakind) of an operator. * Documentation improvement; doxygen top-level \file gestures, \brief gestures for files, etc. Changed contrib/update-copyright.pl for this change, and post-processed to add \brief. Resolves bug #98. * Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind). They no longer made sense. Resolves bug #91.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback