projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2010-06-29
Tim King
This commit merges the decaying-rows branch into the...
commit
|
commitdiff
|
tree
2010-06-29
Tim King
Update to stats.h is now back into the trunk. The...
commit
|
commitdiff
|
tree
2010-06-29
Tim King
Merging the unate-propagator branch into the trunk...
commit
|
commitdiff
|
tree
2010-06-29
Morgan Deters
* Add CDMap<>::insertAtContextLevelZero(k, d) for inser...
commit
|
commitdiff
|
tree
2010-06-24
Tim King
Added post_mortem.py a statistics collector for user...
commit
|
commitdiff
|
tree
2010-06-22
Tim King
Made ~Stat() virtual. Added some additional statistics...
commit
|
commitdiff
|
tree
2010-06-18
Morgan Deters
"statistics" and "staticbinary" are now tags on the...
commit
|
commitdiff
|
tree
2010-06-18
Tim King
Merging the statistics branch into the main trunk....
commit
|
commitdiff
|
tree
2010-06-18
Morgan Deters
bug fix (unreported on bugzilla): skolem variables...
commit
|
commitdiff
|
tree
2010-06-17
Morgan Deters
fix some minor annoyances in the regression test Makefi...
commit
|
commitdiff
|
tree
2010-06-16
Tim King
Added the experimental. +bool TheoryArith::AssertEquali...
commit
|
commitdiff
|
tree
2010-06-16
Tim King
More assorted changes to arithmetic in preparation...
commit
|
commitdiff
|
tree
2010-06-16
Tim King
This commit just contains miscellaneous arithmetic...
commit
|
commitdiff
|
tree
2010-06-15
Morgan Deters
fix last commit gcc options (-wunknown-pragmas ==>...
commit
|
commitdiff
|
tree
2010-06-15
Morgan Deters
remove warnings about unknown #pragma GCC diagnostic...
commit
|
commitdiff
|
tree
2010-06-15
Tim King
I made a documentation change to get() to make explicit...
commit
|
commitdiff
|
tree
2010-06-15
Morgan Deters
(minor) fix for file documentation
commit
|
commitdiff
|
tree
2010-06-14
Christopher...
Adding array select/store to SMT v1 and v2 parsers
commit
|
commitdiff
|
tree
2010-06-14
Tim King
Fix to arith to make sure it only attempts to report...
commit
|
commitdiff
|
tree
2010-06-14
Clark Barrett
Started work on array theory
commit
|
commitdiff
|
tree
2010-06-06
Tim King
Some assorted fixes and local optimizations for theory...
commit
|
commitdiff
|
tree
2010-06-06
Tim King
Adding += and *= to Rational.
commit
|
commitdiff
|
tree
2010-06-04
Tim King
Changed how assignments are saved during check. These...
commit
|
commitdiff
|
tree
2010-06-04
Tim King
Changed several arguments to const references.
commit
|
commitdiff
|
tree
2010-06-04
Christopher...
Adding QF_SAT to SMT parsers
commit
|
commitdiff
|
tree
2010-06-04
Christopher...
Reimplementing AntlrInputStream::newStreamInputStream
commit
|
commitdiff
|
tree
2010-06-04
Morgan Deters
** Don't fear the files-changed list, almost all change...
commit
|
commitdiff
|
tree
2010-06-04
Christopher...
Missing files in last commit
commit
|
commitdiff
|
tree
2010-06-04
Christopher...
Enabling RDL/IDL in SMT v1 and adding some simple tests
commit
|
commitdiff
|
tree
2010-06-03
Christopher...
Implementing input from stdin (Fixes: #144)
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Fixes 2 issues with assignments. The first is construct...
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Adds toString to DeltaRational
commit
|
commitdiff
|
tree
2010-06-03
Tim King
Fixes a bug where registration occurs before preregistr...
commit
|
commitdiff
|
tree
2010-06-03
Christopher...
Changing ANTLR3 detection in configure (Fixes #147)
commit
|
commitdiff
|
tree
2010-06-03
Morgan Deters
* Added NodeBuilder<>::getChild() to make interface...
commit
|
commitdiff
|
tree
2010-06-03
Morgan Deters
resolving bug 139: metaKindOf() warnings still exist...
commit
|
commitdiff
|
tree
2010-06-02
Morgan Deters
added a handful of debugTagIsOn("context") checks to...
commit
|
commitdiff
|
tree
2010-06-02
Morgan Deters
more VERBOSE test failures
commit
|
commitdiff
|
tree
2010-06-01
Christopher...
Fixing test failures in production build
commit
|
commitdiff
|
tree
2010-06-01
Tim King
This commit adds a debugTagIsOn() guard around some...
commit
|
commitdiff
|
tree
2010-06-01
Tim King
This commit is a fix for a bug in removeITEs(). The...
commit
|
commitdiff
|
tree
2010-06-01
Christopher...
Adding SMT v2 parsing support for: QF_IDL, QF_NIA,...
commit
|
commitdiff
|
tree
2010-06-01
Christopher...
Checking for executable permission on antlr3 script
commit
|
commitdiff
|
tree
2010-06-01
Tim King
Fixed a bug in partial_model.cpp where the data was...
commit
|
commitdiff
|
tree
2010-06-01
Christopher...
Fixing failing test in r521
commit
|
commitdiff
|
tree
2010-06-01
Dejan Jovanović
In order for splitting on demand to be able to retract...
commit
|
commitdiff
|
tree
2010-05-31
Christopher...
First draft implementation of mkAssociative
commit
|
commitdiff
|
tree
2010-05-29
Tim King
Adding a couple of example from fuzzsmt to regress1.
commit
|
commitdiff
|
tree
2010-05-29
Tim King
Couple of fixes to theory arith. pivotAndUpdate now...
commit
|
commitdiff
|
tree
2010-05-29
Tim King
After blasting the disjuncts, TheoryEngine rewrite...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
This update enables TheoryArith to accept assertions...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Bug fixes for combining coefficients of rewritten nodes.
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Added printModel() to src/theory/arith/partial_model...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
A few changes to the organization of TheoryEngine rewri...
commit
|
commitdiff
|
tree
2010-05-28
Tim King
Moving the ITE removal from CnfStream to TheoryEngine...
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
fix bug #134: infinite deallocation loop
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
small cosmetic change to tests summary output
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
Remove isAtomic() as per 4/27/2010 meeting. Add commen...
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
fix compiler comparison-signedness warnings
commit
|
commitdiff
|
tree
2010-05-27
Tim King
Reverting this file to not include any comments. (Morga...
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
added the ability to add custom expected stdout, stderr...
commit
|
commitdiff
|
tree
2010-05-27
Tim King
Preregistration has been turned on. Highly experimental...
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
Use the newer automake test driver "parallel-tests...
commit
|
commitdiff
|
tree
2010-05-27
Christopher...
Adding debug assertions on most TNode operations
commit
|
commitdiff
|
tree
2010-05-27
Christopher...
Adding NodeManager::prepareToBeDestroyed() (Fixes:...
commit
|
commitdiff
|
tree
2010-05-27
Christopher...
Adding .cvc4_config to .gitignore
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
fix bug #111: errors in building lcov-all
commit
|
commitdiff
|
tree
2010-05-27
Morgan Deters
fix bug 120; competition mode regression failures for...
commit
|
commitdiff
|
tree
2010-05-26
Tim King
. '+Outstanding case split in theory arith'
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Adding CnfStreamBlack tests for all Boolean connectives
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Fixing test failures in CnfStreamBlack (it was the...
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Adding documentation to my-configure
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Fixing my-configure
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Adding contrib/my-configure
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Adding CnfStream unit tests
commit
|
commitdiff
|
tree
2010-05-26
Morgan Deters
CDMap<> and CDOmap<> fixes to resolve bug 123
commit
|
commitdiff
|
tree
2010-05-26
Tim King
Fix for bug 131. Added some additional debugging assert...
commit
|
commitdiff
|
tree
2010-05-26
Morgan Deters
CDMap: fix bug 130
commit
|
commitdiff
|
tree
2010-05-26
Christopher...
Prevent lexer errors being raised if a parser error...
commit
|
commitdiff
|
tree
2010-05-25
Tim King
Added Rational constructors that only take a numerator...
commit
|
commitdiff
|
tree
2010-05-25
Dejan Jovanović
Some initial changes to allow for lemmas on demand.
commit
|
commitdiff
|
tree
2010-05-21
Tim King
Small fixes to TheoryArith. Added a hack to make Integ...
commit
|
commitdiff
|
tree
2010-05-20
Tim King
Added the division symbol to the parser, and minimal...
commit
|
commitdiff
|
tree
2010-05-19
Tim King
Significant revision to theory/arith. The new draft...
commit
|
commitdiff
|
tree
2010-05-14
Christopher...
Adding debugging code in PropEngine/CnfStream
commit
|
commitdiff
|
tree
2010-05-14
Christopher...
Adding ITE tests
commit
|
commitdiff
|
tree
2010-05-14
Christopher...
Adding rudimentary ITE handling in CnfStream
commit
|
commitdiff
|
tree
2010-05-14
Christopher...
Virtualizing interface between CnfStream and SatSolver
commit
|
commitdiff
|
tree
2010-05-13
Christopher...
Minor refactorings to PropEngine, SatSolver
commit
|
commitdiff
|
tree
2010-05-13
Christopher...
Minor refactorings and corrections to comments
commit
|
commitdiff
|
tree
2010-05-12
Christopher...
Adding ParserBuilder, reducing visibility of Parser...
commit
|
commitdiff
|
tree
2010-05-12
Christopher...
true and false are only defined if the core theory...
commit
|
commitdiff
|
tree
2010-05-12
Christopher...
Refactoring parser tests
commit
|
commitdiff
|
tree
2010-05-12
Christopher...
Adding class Smt2 to handle declaration of logic and...
commit
|
commitdiff
|
tree
2010-05-07
Christopher...
Tightening lexer rules for numerals in SMT v2
commit
|
commitdiff
|
tree
2010-05-07
Morgan Deters
make CVC4::Rational public (fixes broken build)
commit
|
commitdiff
|
tree
2010-05-06
Christopher...
Adding --strict-parsing option
commit
|
commitdiff
|
tree
2010-05-06
Christopher...
Adding AntlrInput::tokenTextSubstr
commit
|
commitdiff
|
tree
2010-05-06
Christopher...
Adding tests for Rational::fromDecimal
commit
|
commitdiff
|
tree
2010-05-06
Christopher...
Adding tests for Integer::pow
commit
|
commitdiff
|
tree
next