Age | Commit message (Expand) | Author |
2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett |
2017-04-05 | Fix bug 698. | ajreynol |
2017-04-05 | Fixes for nlAlgSolveSubs. | ajreynol |
2017-04-05 | Caching for fun def process, add regression. | ajreynol |
2017-04-05 | Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON... | ajreynol |
2017-04-05 | Fix several spelling errors | Fabian Wolff |
2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol |
2017-04-04 | Simplify Theory::collectModelInfo interface to not take deprecated fullModel ... | ajreynol |
2017-04-04 | Do not solve for 0-ary non-constant symbols (for which isVar returns true), a... | ajreynol |
2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
2017-03-31 | Add option multi-trigger-linear, minor optimization to E-matching. | ajreynol |
2017-03-30 | Minor fixes for trigger selection max. | ajreynol |
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol |
2017-03-28 | Refactor the standard effort of relational solver | Paul Meng |
2017-03-28 | Fix for bug 733 | Clark Barrett |
2017-03-28 | Minor refactoring sygus. | ajreynol |
2017-03-28 | More work on sygus. Add regress4 to Makefile. | ajreynol |
2017-03-27 | Fixing a bug for checking whether a node was visited. | Tim King |
2017-03-27 | Minor cleanups to ExtTheory. | Tim King |
2017-03-27 | Removing the friend class modifier from ExtTheory to Theory. | Tim King |
2017-03-27 | Merge pull request #137 from 4tXJ7f/throw_quals | Clark Barrett |
2017-03-27 | Making the ExtTheory object a private member of Theory. | Tim King |
2017-03-27 | Making ppNotifyAssertions take a const vector. | Tim King |
2017-03-27 | Moving the CareGraph into its own file. | Tim King |
2017-03-27 | Moving the theory::Assertion struct into its own file. | Tim King |
2017-03-27 | Remove throw qualifiers in type enumerators | Andres Notzli |
2017-03-24 | Add some regressions. Minor. | ajreynol |
2017-03-24 | Refactor model building for quantifiers to be a single pass, simplification. ... | ajreynol |
2017-03-22 | Fix more cases of rewritten explanations in strings for bug 784. Minor. | ajreynol |
2017-03-22 | Minor fix for bounded integers. | ajreynol |
2017-03-22 | Work on new approach for sygus involving conditional solutions. Refactoring o... | ajreynol |
2017-03-21 | Improve computeCareGraph functions to check shared term equality status once ... | ajreynol |
2017-03-18 | Fix for bug 707. | Clark Barrett |
2017-03-18 | Fix to help with bug 717 | Clark Barrett |
2017-03-10 | Minor fix for cbqi-all. | ajreynol |
2017-03-07 | More fixes for printing/parsing sets, fix kind name. | ajreynol |
2017-03-06 | Do not eagerly construct explanations in relation solver. | ajreynol |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil no... | ajreynol |
2017-03-06 | Adding support for bool-to-bv | Clark Barrett |
2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. Generaliz... | ajreynol |
2017-03-03 | Another minor fix for sets related to sharing + finite element types. | ajreynol |
2017-03-02 | Fixes related to sets. | ajreynol |
2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2017-02-16 | Minor fixes for relations, quantifiers dsplit. | ajreynol |
2017-02-16 | Fixes for sets+rels check. Minor. | ajreynol |
2017-02-15 | Minimization modes for fmf bound. | ajreynol |
2017-02-07 | Generalize finite bound inference to unifiable variables in set membership li... | ajreynol |
2017-01-30 | Fix regexp cache issue in strings, add regression. | ajreynol |
2017-01-18 | Fix non-idempotent rewrite in Array rewriter | Andres Noetzli |