git.libre-soc.org Git - cvc5.git/search

2014-06-25	Tim King	Merge branch 'master' of github.com:CVC3/CVC4	commit \| commitdiff \| tree
2014-06-25	Tim King	Fixing the previous bugfix.	commit \| commitdiff \| tree
2014-06-24	Tim King	Alternative lazier heuristic for assertion rewriting.	commit \| commitdiff \| tree
2014-06-24	Tim King	Fixing a soundness bug in arithmetic and a roubustness...	commit \| commitdiff \| tree
2014-06-19	Tim King	This commit adds a priority queue implementation. ...	commit \| commitdiff \| tree
2014-06-17	Tim King	Merge pull request #33 from mdeters/arith-proposal	commit \| commitdiff \| tree
2014-06-17	Tim King	This commit adds a priority queue implementation. ...	commit \| commitdiff \| tree
2014-06-10	Tim King	Merging Tim's pseudoboolean work from his fmcad14 branch.	commit \| commitdiff \| tree
2014-06-06	Tim King	Patch for the subtype theoryof mode to make the equalities...	commit \| commitdiff \| tree
2014-05-26	Tim King	Separating an implicit inclusion of smt_engine.h from...	commit \| commitdiff \| tree
2014-05-26	Tim King	Fixing a soundness bug due to the default implmentation...	commit \| commitdiff \| tree
2014-05-19	Tim King	More documentation fixes. Apologies for multiple commits.	commit \| commitdiff \| tree
2014-05-19	Tim King	Fixing documentation for glpk configuration.	commit \| commitdiff \| tree
2014-05-12	Tim King	Merge remote-tracking branch 'timothy-king/master'	commit \| commitdiff \| tree
2014-05-12	Tim King	Merging in additional glpk options and statistics from...	commit \| commitdiff \| tree
2014-05-05	Tim King	Improving documentation for glpk-cut-log switch.	commit \| commitdiff \| tree
2014-04-30	Tim King	T-entailment work, and QCF (quant conflict find) work...	commit \| commitdiff \| tree
2014-04-06	Tim King	Reduced example from pcc's bug report.	commit \| commitdiff \| tree
2014-04-06	Tim King	Merge pull request #21 from pcc/ite-fix	commit \| commitdiff \| tree
2014-04-01	Tim King	Merge branch '1.3.x'	commit \| commitdiff \| tree
2014-04-01	Tim King	Fixing bug 552. There was a bug when integers are...	commit \| commitdiff \| tree
2014-03-26	Tim King	Merging in a fix from 1.3.x.	commit \| commitdiff \| tree
2014-03-26	Tim King	Fixes an idempotency issue for non-linear multiplication...	commit \| commitdiff \| tree
2014-03-08	Tim King	Merge pull request #18 from timothy-king/master	commit \| commitdiff \| tree
2014-03-08	Tim King	Fixing name changes that cam in from the merge.	commit \| commitdiff \| tree
2014-03-08	Tim King	Merge remote-tracking branch 'CVC4root/master'	commit \| commitdiff \| tree
2014-03-08	Tim King	Fixing a SWIG problem for RationalFromDoubleException.	commit \| commitdiff \| tree
2014-03-07	Tim King	Merging a squash of the branch timothy-king/CVC4/glpknecfix...	commit \| commitdiff \| tree
2014-03-05	Tim King	Improving support for POW in arithmetic. Resolves bug...	commit \| commitdiff \| tree
2014-02-19	Tim King	Merge branch 'master' of github.com:CVC4/CVC4	commit \| commitdiff \| tree
2014-02-19	Tim King	Merge branch '1.3.x'	commit \| commitdiff \| tree
2014-02-19	Tim King	Stopping non-linear terms from entering the dio solver...	commit \| commitdiff \| tree
2013-11-25	Tim King	Merge remote-tracking branch 'CVC4root/master'	commit \| commitdiff \| tree
2013-11-25	Tim King	Substantial Changes:	commit \| commitdiff \| tree
2013-11-21	Tim King	Adding the changes needed to delete rewriter attributes...	commit \| commitdiff \| tree
2013-11-20	Tim King	Changing the number of bits allocated per field in...	commit \| commitdiff \| tree
2013-05-09	Tim King	Changing the integer normal form to increase matching.	commit \| commitdiff \| tree
2013-05-07	Tim King	Fixes a bug with arithmetic's new attempt solution...	commit \| commitdiff \| tree
2013-05-07	Tim King	Improving arithmetic debugging output.	commit \| commitdiff \| tree
2013-05-07	Tim King	Disabling an incorrect prototyping line from the simplex...	commit \| commitdiff \| tree
2013-05-06	Tim King	Adding a heuristic for guessing an optimization function...	commit \| commitdiff \| tree
2013-05-06	Tim King	Disables justification stop only for LRA if the problem...	commit \| commitdiff \| tree
2013-05-05	Tim King	Adding cut offs for likely integer infeasible paths.	commit \| commitdiff \| tree
2013-05-04	Tim King	Adding a smarter technique for pivoting in solutions...	commit \| commitdiff \| tree
2013-05-03	Tim King	Fixing compilation of unit tests. These problems were...	commit \| commitdiff \| tree
2013-05-03	Tim King	More misc. arithmetic cleanup. Removing unused files...	commit \| commitdiff \| tree
2013-05-03	Tim King	Code cleanup. Reducing misc. warnings in arithmetic.	commit \| commitdiff \| tree
2013-05-03	Tim King	Removing arithmetic legacy code and unifying functions.	commit \| commitdiff \| tree
2013-05-03	Tim King	Fixing a debug typo.	commit \| commitdiff \| tree
2013-05-03	Tim King	Merging branch 'soiquickexplain'.	commit \| commitdiff \| tree
2013-05-03	Tim King	Merge branch 'fcexplanations'	commit \| commitdiff \| tree
2013-05-02	Tim King	Adding quick explain for soi simplex.	commit \| commitdiff \| tree
2013-05-01	Tim King	Working on the new explanation system.	commit \| commitdiff \| tree
2013-04-30	Tim King	Making propagation more conversative.	commit \| commitdiff \| tree
2013-04-30	Tim King	Draft of the new propagation code.	commit \| commitdiff \| tree
2013-04-30	Tim King	Adding has bound counts and tracking for rows.	commit \| commitdiff \| tree
2013-04-28	Tim King	Fixing the failure for make distcheck.	commit \| commitdiff \| tree
2013-04-26	Tim King	FCSimplex branch merge	commit \| commitdiff \| tree
2013-04-02	Tim King	Making arithmetic model reversion on unsat checks an...	commit \| commitdiff \| tree
2013-04-01	Tim King	Cleaning up the demand restart code.	commit \| commitdiff \| tree
2013-04-01	Tim King	Adding a restart test strategy to integers.	commit \| commitdiff \| tree
2013-04-01	Tim King	Adding demand restart.	commit \| commitdiff \| tree
2013-04-01	Tim King	Adding tests for the previous commit.	commit \| commitdiff \| tree
2013-04-01	Tim King	Fix for iff terms over equalities between the same...	commit \| commitdiff \| tree
2013-02-15	Tim King	Merge branch '1.0.x'	commit \| commitdiff \| tree
2013-02-14	Tim King	Removing BVDebug and replacing with Debug.	commit \| commitdiff \| tree
2013-01-31	Tim King	Adding a heuristic to more eagerly split bounded integer...	commit \| commitdiff \| tree
2013-01-23	Tim King	Adding miplibtrick option.	commit \| commitdiff \| tree
2013-01-23	Tim King	Adding substitution size cap.	commit \| commitdiff \| tree
2012-12-15	Tim King	Merging in patch from branch '1.0.x'.	commit \| commitdiff \| tree
2012-12-15	Tim King	Adding unit test for different versions of division.	commit \| commitdiff \| tree
2012-12-15	Tim King	Merge remote-tracking branch 'main-repo/1.0.x' into...	commit \| commitdiff \| tree
2012-12-15	Tim King	Changing the rewriter to use Boute's Euclidean definition...	commit \| commitdiff \| tree
2012-12-05	Tim King	Improved garbage collection for TheoryArith. The merges...	commit \| commitdiff \| tree
2012-12-05	Tim King	Cleanup of arithmetic, and some new utility functions...	commit \| commitdiff \| tree
2012-12-05	Tim King	This commit merges in CDTrailHashMap and CDInsertHashMap...	commit \| commitdiff \| tree
2012-12-01	Tim King	Fix for a CLN related bug on 32 bit systems. Integer...	commit \| commitdiff \| tree
2012-12-01	Tim King	Polishing API examples.	commit \| commitdiff \| tree
2012-12-01	Tim King	Adding SmtEngine::setLogic(const char* logic) so that...	commit \| commitdiff \| tree
2012-11-30	Tim King	Fixes for stricter compilers Andy brought to my attention.	commit \| commitdiff \| tree
2012-11-30	Tim King	Changing the documentation of ARR_TABLE_FUN to say...	commit \| commitdiff \| tree
2012-11-30	Tim King	Updating the combination.cpp example.	commit \| commitdiff \| tree
2012-11-30	Tim King	Committing tests to potentially discover an obscure...	commit \| commitdiff \| tree
2012-11-30	Tim King	Changes to SExpr to accept autoconversion from bool...	commit \| commitdiff \| tree
2012-11-30	Tim King	Adding smtname level options for tlimit, rlimit, etc...	commit \| commitdiff \| tree
2012-11-28	Tim King	Adding the helloworld.cpp example.	commit \| commitdiff \| tree
2012-11-27	Tim King	Adding an example to show how to use arithmetic.	commit \| commitdiff \| tree
2012-11-26	Tim King	Improved implementation of Integer::length() with CLN...	commit \| commitdiff \| tree
2012-11-26	Tim King	Removing DioSolver::acceptableOriginalNodes(). This...	commit \| commitdiff \| tree
2012-11-26	Tim King	Improving arithmetic debugging output.	commit \| commitdiff \| tree
2012-11-26	Tim King	Disabling test/regress/regress0/push-pop/bug396.smt2...	commit \| commitdiff \| tree
2012-11-25	Tim King	Adding a regression test from bug 462.	commit \| commitdiff \| tree
2012-11-25	Tim King	This commit fixes two incompleteness bugs (461, 459...	commit \| commitdiff \| tree
2012-11-24	Tim King	Adds ensureConstraint(...) to ConstraintDatabase. This...	commit \| commitdiff \| tree
2012-11-21	Tim King	- Removes getDeltaValueWithNonlinear() entirely	commit \| commitdiff \| tree
2012-11-21	Tim King	Adds a number of new capabilities to DeltaRational...	commit \| commitdiff \| tree
2012-11-21	Tim King	Added debugging output to --check-models. I've found...	commit \| commitdiff \| tree
2012-11-19	Tim King	Adding hand minimized test for bug 450.	commit \| commitdiff \| tree
2012-11-19	Tim King	Changed the splitting-on-demand lemmas of arithmetic...	commit \| commitdiff \| tree
2012-11-19	Tim King	Fix for bug452.	commit \| commitdiff \| tree
next

RSS Atom