summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
AgeCommit message (Collapse)Author
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.
2010-05-12Adding ParserBuilder, reducing visibility of Parser and Input constructorsChristopher L. Conway
Adding Smt2 subclass of Parser Checking for multiple calls to set-logic in SMT v2
2010-05-12true and false are only defined if the core theory is loaded in SMT v2 ↵Christopher L. Conway
strict mode
2010-05-12Adding class Smt2 to handle declaration of logic and theory symbolsChristopher L. Conway
2010-05-06Adding --strict-parsing optionChristopher L. Conway
2010-04-29Added the capability to construct expressions by passing the operator ↵Dejan Jovanović
instead of the kind, i.e. Expr op = ..."f"... em.mkExpr(op, children); Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
2010-04-28Refactoring Input/Parser code to support external manipulation of the parser ↵Christopher L. Conway
state.
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-02-27Adding --mmap option to use memory-mapped file input, which provides a ↵Christopher L. Conway
marginal improvement (<5%) on big benchmarks.
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
* configure.ac, test/unit/Makefile.am: Resolved an issue where even when not testing, one unit test was built. * Re-ran contrib/update-copyright.pl on all source files to ensure consistent and correct header comments. * contrib/get-authors: Change definition of "minor contributor" to >= 10% of lines (rather than strictly greater than 10% of lines)
2010-02-18Adding --no-checking option to disable semantic checks in parserChristopher L. Conway
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides ↵Morgan Deters
cvc4-c++-editing-mode from contrib/editing-with-emacs
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵Morgan Deters
regenerated configure script
2010-02-03Addressed many of the concerns of bug 10 (build system code review).Morgan Deters
Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested.
2010-02-01Fixing the CVC grammar for parsing Boolean expressions. All the ↵Dejan Jovanović
associativity stufff is now in the grammar. All the parser tests pass now.
2009-12-18more build system fix-upsMorgan Deters
2009-12-18Lots of parser changes to make Chris happy. Yet more to come later. Dejan Jovanović
2009-12-17update-copyright.pl now retrieves and incorporates author information from ↵Morgan Deters
repository history; re-ran update-copyright.pl; cleaned up some things with make
2009-12-11Extracted the public Expr and ExprManager interface to encapsulate the ↵Dejan Jovanović
optimized expressions and the internal expression manager.
2009-12-10killing expr into node...Dejan Jovanović
2009-12-09some fixes and organizational adjustments to assert code, parsers/lexers, ↵Morgan Deters
and build process
2009-12-07antlr parser for the cvc4 language (boolean only)Dejan Jovanović
yet to be finalized, it should work as expected
2009-12-06Big chunk of changes:Dejan Jovanović
* Fixed bugs in option parsing * Simplified the main.cpp significantly (more c++ like) * Added the null kind, expr value, and expression, with the default constructor public * Simplified commands, we need to discuss this in the meeting (what to do with command results?) * Removed all the lex/yacc files * Symbol table is now a templated class, as we will have tables for variables, predicates and functions * The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory. TODO: * add the PL grammar and unit test when the testing becomes available * with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols? * i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback