summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2017-04-21Handle subtypes in sets. Bug fixes for tuples with subtypes.ajreynol
2017-04-20Minor fixes.ajreynol
2017-04-18Coverage fixmakaimann
2017-04-07Change option names for nl.ajreynol
2017-04-05Merge pull request #143 from FabianWolff/masterClark Barrett
2017-04-05Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON...ajreynol
2017-04-05Fix several spelling errorsFabian Wolff
2017-04-04Enable multi-trigger-linear by default, add option.ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-03-31Add option multi-trigger-linear, minor optimization to E-matching.ajreynol
2017-03-29Add quantifiers options related to model and master equality engine.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring o...ajreynol
2017-03-16Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ...ajreynol
2017-03-06Adding support for bool-to-bvClark Barrett
2017-03-02Minor cleanup and reorganization related to last commit.ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2017-02-15Minimization modes for fmf bound.ajreynol
2017-02-07Generalize finite bound inference to unifiable variables in set membership li...ajreynol
2016-12-29Changing getTearDownIncremental() to return the type of options::tearDownIncr...Tim King
2016-12-07Refactoring, generalization of bounded inference module. Simplification of re...ajreynol
2016-11-21Refactoring related to track instantiation option.ajreynol
2016-11-11Add simple inferences for extended bitvector functions, add a few related opt...ajreynol
2016-11-10Add option for enabling/disabling lazy extended function reduction in bitvect...ajreynol
2016-11-08Add a few options to separation logic and sets. Minor changes to separation l...ajreynol
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver as...ajreynol
2016-10-05Added an option that allow empty dependencies when attempting to minimize pre...guykatzz
2016-09-20More refactoring of cbqi. Add a few regressions. Add option for qcf.ajreynol
2016-09-16Use matching heuristics for EPR instantiation.ajreynol
2016-09-15Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul...ajreynol
2016-09-12Refactor prenex modes.ajreynol
2016-09-12Remove old implementation of cbqiajreynol
2016-09-09Support for separation logic + EPR. Refactor preprocessing of sep.nil, only a...ajreynol
2016-09-03Option for prenex normal formajreynol
2016-09-01Fix boolean term issue in invariants from sygus. Minor default options change...ajreynol
2016-09-01Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier...ajreynol
2016-08-31Removing typeof from didyoumean.cpp.Tim King
2016-08-26Basic support for EPR+CBQI. Minor cleanup.ajreynol
2016-08-25Options for counterexample guided instantiation.ajreynol
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for bounde...ajreynol
2016-08-11Add support for fewer preprocessing holesAndres Notzli
2016-07-27Added an option for a more aggressive weakest implicant optimizationGuy
2016-07-26Add option to minimize sygus solutions based on using weakest implicants of i...ajreynol
2016-07-26Minor improvements to strings related to constant splitting, including a few ...ajreynol
2016-07-20Print only instantiations that are in the unsat core when --proof is enabled....ajreynol
2016-07-19Add infrastructure for tracking instantiation lemmas (for proofs, and minimiz...ajreynol
2016-07-16Refactor strings extf evaluation info. Ensure strings eager preprocess elimin...ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ...ajreynol
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback