summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
2017-07-10Merge ntExt branch. Adds support for transcendental functions. Refactoring of...ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-06-28Enable non-linear solve by default, update regressions.ajreynol
2017-05-30print only labeled assertions as part of the unsat coreguykatzz
2017-05-12Adding VPATH back inmakaimann
2017-05-12Conditional coverage buildmakaimann
2017-05-05Do not eliminate extended arithmetic symbols when finite model finding is on,...ajreynol
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback