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

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
2012-11-15	Tim King	Fix for bug 447.	commit \| commitdiff \| tree
2012-11-15	Tim King	Fixing comments in print_lambda.cvc.	commit \| commitdiff \| tree
2012-11-14	Tim King	Fix for bug 407. mkAnonymousFunction() in the parser...	commit \| commitdiff \| tree
2012-11-14	Tim King	Fixed a typo in r4576	commit \| commitdiff \| tree
2012-11-14	Tim King	Beautifying smt_engine.cpp.	commit \| commitdiff \| tree
2012-11-14	Tim King	Fix to bug449. Adds shared constants to the set of...	commit \| commitdiff \| tree
2012-11-13	Tim King	SmtEngine::checkModel() should only be called if the...	commit \| commitdiff \| tree
2012-11-12	Tim King	Improved error reporting for improperly using non-linear...	commit \| commitdiff \| tree
2012-11-12	Tim King	Delta is now generated in arithmetic to keep consistent...	commit \| commitdiff \| tree
2012-11-11	Tim King	Fixes for the arithmetic normal form and rewriter to...	commit \| commitdiff \| tree
2012-11-10	Tim King	Beautifying integer_cln_imp.h	commit \| commitdiff \| tree
2012-11-10	Tim King	Fix to quantifier rewritting not being idempotent....	commit \| commitdiff \| tree
2012-11-10	Tim King	Removing rewriter call in SmtEngine::addFormula().	commit \| commitdiff \| tree
2012-11-10	Tim King	Fix for bug 439. Delta computation now includes disequality...	commit \| commitdiff \| tree
2012-11-09	Tim King	Test that breaks arithmetic model building due to disequalit...	commit \| commitdiff \| tree
2012-11-09	Tim King	Arithmetic problem that fails --check-models due incompleten...	commit \| commitdiff \| tree
2012-11-08	Tim King	Turns on TheoryUF when non-linear arithmetic is turned...	commit \| commitdiff \| tree
2012-11-08	Tim King	Improved support for division by zero. This adds the...	commit \| commitdiff \| tree
2012-11-07	Tim King	Fix to a bug in integer mod lemmas.	commit \| commitdiff \| tree
2012-11-05	Tim King	Fix to the context dependent static learning code.	commit \| commitdiff \| tree
2012-10-26	Tim King	Fix for bug 430. d_delta in PartialModel was never...	commit \| commitdiff \| tree
2012-10-24	Tim King	Updated the ArithStaticLearner to be user context dependent.	commit \| commitdiff \| tree
2012-10-24	Tim King	Fix for systems that do not have the MAP_FILE macro...	commit \| commitdiff \| tree
2012-10-23	Tim King	The contrib/get-antlr-3.4 script:	commit \| commitdiff \| tree
2012-10-19	Tim King	Fix for model building with shared terms for arithmetic.	commit \| commitdiff \| tree
2012-09-29	Tim King	Calling the setIncompleteness() flag on all full checks...	commit \| commitdiff \| tree
2012-09-29	Tim King	This commit add interpretation by lemma for INTS_DIVISION...	commit \| commitdiff \| tree
2012-09-11	Tim King	Partially reverting the changes made in 4308. There...	commit \| commitdiff \| tree
2012-09-10	Tim King	Fixed an error in the rewriter Pascal pointed out....	commit \| commitdiff \| tree
2012-08-14	Tim King	Implements TheoryArith::collectModelInfo(). The current...	commit \| commitdiff \| tree
2012-08-14	Tim King	Adds substituteDelta() to DeltaRational which given...	commit \| commitdiff \| tree
2012-08-14	Tim King	Switched TheoryModel assertEqualityEngine to use const...	commit \| commitdiff \| tree
2012-08-14	Tim King	Switched a number of EqClassIterator operations to...	commit \| commitdiff \| tree
2012-07-06	Tim King	Adding std namespace to a couple of make_pair instances.	commit \| commitdiff \| tree
2012-07-06	Tim King	Added include unistd to main/util.cpp	commit \| commitdiff \| tree
2012-07-06	Tim King	Added virtual destructor to PpRewrite.	commit \| commitdiff \| tree
2012-06-27	Tim King	Fixing a bug in proof production for the DioSolver.	commit \| commitdiff \| tree
2012-06-27	Tim King	This adds TheoryArith::safeToReset(). This fixes bug...	commit \| commitdiff \| tree
2012-06-27	Tim King	Adding access to simplex's ArithPriorityQueue to TheoryArith...	commit \| commitdiff \| tree
2012-06-27	Tim King	Improved debugging output.	commit \| commitdiff \| tree
2012-06-27	Tim King	Improved debugging output.	commit \| commitdiff \| tree
2012-06-27	Tim King	Adding reduce() to the ArithPriorityQueue. This reduces...	commit \| commitdiff \| tree
2012-06-25	Tim King	Added a warning to arithmetic for a known dio solver...	commit \| commitdiff \| tree
2012-06-16	Tim King	Fixing if condition for trivial equalities in arithmetic...	commit \| commitdiff \| tree
2012-06-15	Tim King	Fixing mac compilation issues.	commit \| commitdiff \| tree
2012-06-14	Tim King	Fixing a case for explanation of non-normal form equalities.	commit \| commitdiff \| tree
2012-06-14	Tim King	Fixing a bug related to explaining propagations with...	commit \| commitdiff \| tree
2012-06-14	Tim King	Fixed arithmetic consistency issue. The simplex conflict...	commit \| commitdiff \| tree
2012-06-14	Tim King	Brings the tuning branch into trunk. This includes...	commit \| commitdiff \| tree
2012-06-13	Tim King	Added witnesses to Constraints.	commit \| commitdiff \| tree
2012-06-13	Tim King	- Added a loop to internally assert constraints that...	commit \| commitdiff \| tree
2012-06-13	Tim King	Fixed whitespace warning on Makefile.	commit \| commitdiff \| tree
2012-06-13	Tim King	Adds debugging output to theory_engine.cpp.	commit \| commitdiff \| tree
2012-06-12	Tim King	Fix to yesterday's change in arithmetic.	commit \| commitdiff \| tree
2012-06-12	Tim King	Adding incorrect qf_lia result.	commit \| commitdiff \| tree
2012-06-11	Tim King	Fix to term normalization of integer equalities. Adds...	commit \| commitdiff \| tree
2012-06-11	Tim King	Fixing type comparision assertion in getEqualityStatus().	commit \| commitdiff \| tree
2012-05-22	Tim King	This commit merges in the branch arithmetic/cprop.	commit \| commitdiff \| tree
2012-05-19	Tim King	Adding regress test for bug 341.	commit \| commitdiff \| tree
2012-05-19	Tim King	- The array type rules were fixed to use isSubtypeOf.	commit \| commitdiff \| tree
2012-05-18	Tim King	This commit adds TypeNode::leastCommonTypeNode(). ...	commit \| commitdiff \| tree
2012-05-18	Tim King	This commit removes the dead psuedoboolean code.	commit \| commitdiff \| tree
2012-05-18	Tim King	Removing long unsigned operator+ from CDList's const_iterator.	commit \| commitdiff \| tree
2012-05-17	Tim King	This fixes a fascinating segfault. This is the sequence...	commit \| commitdiff \| tree
2012-05-17	Tim King	Adding failing regression for ite type computation.	commit \| commitdiff \| tree
2012-05-15	Tim King	Fix to shared terms visitor.	commit \| commitdiff \| tree
next

RSS Atom