summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
2016-06-01Merging proof branchGuy
2016-05-24Merged cryptominisat from experimental branch.Liana Hadarean
2016-05-24Improvements to symmetry breaking in sygus search. Minor fix for getting inst...ajreynol
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino...ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En...ajreynol
2016-05-12Add casc scripts. Improvements to qcf related to nested quantifiers and varia...ajreynol
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizatio...ajreynol
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize irre...ajreynol
2016-04-28More work on inst propagate. Optimization for qcf to check instances eagerly...ajreynol
2016-04-14Add option --snorm-infer-eq to infer equalities based on normalization in Ari...ajreynol
2016-04-13Handle parametric datatypes with --quant-ind. Minor updates.ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ...ajreynol
2016-04-04New options for trigger selection, add option --strict-triggers. Do not infer...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-04-01Improvements to equality inference module: add missing cases for solvable var...ajreynol
2016-03-31Improvements to trigger selection, min triggers by default. Optimizations for...ajreynol
2016-03-30Updates to E-matching to avoid entailed instantiations earlier. Minor updates...ajreynol
2016-03-23squash-merge from proof branchGuy
2016-03-23Fixed help for tear-down-incremental optionClark Barrett
2016-03-21New version of the recursive options parsing strategy.Tim King
2016-03-12Add options related to interleaving quantifiers and theory combination, chang...ajreynol
2016-03-10Faster conditional rewriting for and/or beneath quantifiers. Improvements to ...ajreynol
2016-03-01Shorter explanations for strings based on tracking which parts of normal form...ajreynol
2016-02-29Minor options to datatypes.ajreynol
2016-02-26Refactoring of inferences in strings. Add several options.ajreynol
2016-02-25Minor improvement to partial qe. Add options for representative selection in ...ajreynol
2016-02-24Add entailment checks between length terms to reduce splitting in strings sol...ajreynol
2016-02-18Implement dynamic splitting for quantified formulas. Minor refactoring of re...ajreynol
2016-02-05Add two optimizations for datatypes, currently disabled. Bug fix rewriter for...ajreynol
2016-02-03Added --omit-dont-cares option which doesn't print model values forClark Barrett
2016-02-01Making the references to std more explicit in didyoumean.cpp.Tim King
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-05Add SmtGlobals ClassTim King
2015-12-30Modified tear-down-incremental option to take an integer - the integer is theClark Barrett
2015-12-30Shuffling around public vs. private headersTim King
2015-12-26Merged my changes from experimental branch (new array decision procedure,Clark Barrett
2015-12-24Miscellaneous fixesTim King
2015-12-18Modifying emptyset.h and sexpr. Adding SetLanguage.Tim King
2015-12-15Making logic_info_forward.h a public header for now.Tim King
2015-12-15Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.ajreynol
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-03Modifying the src/options/Makefile.am for travis.Tim King
2015-12-02Modifying options/Makefile.am to pass distcheck. There is an unpleasant hack ...Tim King
2015-12-02Separating the steps of the old mkoptions script into smaller phases.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback