summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
2016-09-25Closing an open file descriptor in MemoryMapFile.Tim King
2016-09-25Freeing memory in error handling code for bounded_token_buffer.Tim King
2016-09-14Support for unique variable generation in node manager.ajreynol
2016-06-17Cleanup from last commit, treat sep.nil as variable kind.ajreynol
2016-06-17Support for separation logic. Enable cbqi by default for pure BV.ajreynol
2016-05-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En...ajreynol
2016-05-06Minor clean up, fixes related to sygus.ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-05-05Removing a null pointer reference that was found by -fsanitize=null.Tim King
2016-04-13Update native language support for strings.ajreynol
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-08Extend synthesis solver to handle single invocation with additional universal...ajreynol
2016-02-16Public interface for quantifier elimination. Minor changes to datatypes rewr...ajreynol
2016-02-15Minor change to last commitajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-02-01Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build p...Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Disabling the RESTART command.Tim King
2016-01-06Improving the documentation of the CVC command CONTINUE.Tim King
2015-12-30Shuffling around public vs. private headersTim King
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-15Breaking the include cycle between Record and Expr.Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-03Removing the generated directory from the parsers.Tim King
2015-11-26Front-end support for get-value of sort cardinality, minor fixes for sygus so...ajreynol
2015-11-23Isolating the dependencies on CVC4_ANTLR3_OLD_INPUT_STREAM. Also freeing more...Tim King
2015-09-24Counterexample-guided instantiation for datatypes. Make sygus parsing more l...ajreynol
2015-09-18More work mixing UF and sygus.ajreynol
2015-09-18Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quan...ajreynol
2015-08-01Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datat...ajreynol
2015-08-01Support for default grammar for datatypes in sygus. Support vts for infinity.ajreynol
2015-07-31Sygus support for inductive datatypes.ajreynol
2015-07-25Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-12Make sygus an output language. Parse declare-fun in sygus. Minor improvemen...ajreynol
2015-06-12Accelerate sygus solution reconstruction for constants and id functions. Min...ajreynol
2015-06-11Avoid naming conflicts in sygus, refactor. Add missing regression. Detect St...ajreynol
2015-06-11Handle duplicate operators in sygus grammars. Parse sygus quoted literals. A...ajreynol
2015-06-11Update experimental scripts. Support top-level non-terminals in sygus gramma...ajreynol
2015-06-10Bug fix parsing constant constructor sygus.ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-10Parse support for sygus LetGTerm.ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-06-02Flatten sygus grammars during parsing. Remove duplicate operators from grammars.ajreynol
2015-06-02Add casc 25 tfn script. Change tff script to output instantiations. Work tow...ajreynol
2015-05-28added options for controlling resource step-count for various solving stagesLiana Hadarean
2015-05-11Allow sygus with no syntactic restrictions for LIA. Add regressions.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback