summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
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
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-04-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fm...ajreynol
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for --...ajreynol
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-04-22Merge pull request #73 from kbansal/parser-dont-tokenizeKshitij Bansal
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable del...ajreynol
2015-04-16update commentKshitij Bansal
2015-04-15string parser builtinop changesKshitij Bansal
2015-04-15bv parserchanges cleanupKshitij Bansal
2015-04-15fp builtinop parser changesKshitij Bansal
2015-04-15fp reorder tokens to match other occurencesKshitij Bansal
2015-04-15THEORY_INTS parser changesKshitij Bansal
2015-04-15THEORY_REAL_INTS parser changesKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback