projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2013-03-26
lianah
cleaned up the bv subtheory interface; added check...
commit
|
commitdiff
|
tree
2013-03-25
lianah
getEqualityStatus now also queries the inequality solver
commit
|
commitdiff
|
tree
2013-03-25
Liana Hadarean
added support for disequalities in the inequality solver
commit
|
commitdiff
|
tree
2013-03-24
lianah
incremental inequality solver implemented
commit
|
commitdiff
|
tree
2013-03-23
lianah
non-incremental inequality solver seems to be bug-free...
commit
|
commitdiff
|
tree
2013-03-23
lianah
fixed some explanation problems for the core theory...
commit
|
commitdiff
|
tree
2013-03-22
lianah
Merge branch 'master' into bv-core
commit
|
commitdiff
|
tree
2013-03-22
Dejan Jovanović
another typo/bugfix for equality constant evaluation
commit
|
commitdiff
|
tree
2013-03-21
lianah
Merge branch 'master' into bv-core
commit
|
commitdiff
|
tree
2013-03-21
lianah
fixed more equality stuff
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Better error in case of nonlinear assertions while...
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Add the ability to "mute" commands, needed for SMT...
commit
|
commitdiff
|
tree
2013-03-21
Dejan Jovanović
fixing markings of internal nodes in equality engine
commit
|
commitdiff
|
tree
2013-03-21
lianah
fixed compilation problem
commit
|
commitdiff
|
tree
2013-03-21
lianah
incorporated dejan's constant evaluation; now getting...
commit
|
commitdiff
|
tree
2013-03-21
lianah
Merge branch 'master' into bv-core
commit
|
commitdiff
|
tree
2013-03-21
lianah
disabled ineq
commit
|
commitdiff
|
tree
2013-03-21
Dejan Jovanović
Merge branch 'master' of github.com:CVC4/CVC4
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Some model and printing fixes for defined functions...
commit
|
commitdiff
|
tree
2013-03-21
Dejan Jovanović
more equality constant evaluation
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Fix for SmtEngine::expandDefinitions()---improper TypeC...
commit
|
commitdiff
|
tree
2013-03-21
lianah
added regression test for constant eval
commit
|
commitdiff
|
tree
2013-03-21
lianah
Merge branch 'master' into bv-core
commit
|
commitdiff
|
tree
2013-03-21
Dejan Jovanović
fixing constant evaluation bugs
commit
|
commitdiff
|
tree
2013-03-21
lianah
added more tests
commit
|
commitdiff
|
tree
2013-03-21
lianah
generalized bv inequality reasoning to handle both...
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Better reporting of detached git state in --version...
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Fix to bug 497: make justification heuristic's ITE...
commit
|
commitdiff
|
tree
2013-03-21
Morgan Deters
Remove unintentionally-committed-to-master README from...
commit
|
commitdiff
|
tree
2013-03-20
Morgan Deters
Interactive mode support for multiline input
commit
|
commitdiff
|
tree
2013-03-20
Morgan Deters
Properly |quote| symbols in SMT-LIBv2 output.
commit
|
commitdiff
|
tree
2013-03-20
Morgan Deters
Some statistics for narrowing down incrementality issue...
commit
|
commitdiff
|
tree
2013-03-20
Liana Hadarean
one more ineq regression
commit
|
commitdiff
|
tree
2013-03-20
Liana Hadarean
fixed reversed concat in core theory
commit
|
commitdiff
|
tree
2013-03-20
Liana Hadarean
merged dejan's stuff
commit
|
commitdiff
|
tree
2013-03-20
Liana Hadarean
merged master with dejan's constant evaluating equality...
commit
|
commitdiff
|
tree
2013-03-20
Liana Hadarean
inequality reasoning works on small examples added...
commit
|
commitdiff
|
tree
2013-03-20
Dejan Jovanović
Adding evaluation of constant terms to the equality...
commit
|
commitdiff
|
tree
2013-03-19
Morgan Deters
Minor cleanup of sources
commit
|
commitdiff
|
tree
2013-03-19
Morgan Deters
Fixes for miplib-trick application (and a new testcase)
commit
|
commitdiff
|
tree
2013-03-19
Morgan Deters
Remove PropositionalQuery class and all CUDD-related...
commit
|
commitdiff
|
tree
2013-03-19
Morgan Deters
Minor fixes to build system
commit
|
commitdiff
|
tree
2013-03-19
Liana Hadarean
added the cpp file for the inequality graph
commit
|
commitdiff
|
tree
2013-03-19
Liana Hadarean
implementing more inequality graph stuff; work in progr...
commit
|
commitdiff
|
tree
2013-03-18
lianah
more work on inequality reasoning for bv
commit
|
commitdiff
|
tree
2013-03-16
lianah
started work on the inequality bv subtheory
commit
|
commitdiff
|
tree
2013-03-15
Morgan Deters
Boolean terms rewriting for quantified variables of...
commit
|
commitdiff
|
tree
2013-03-15
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-03-15
Morgan Deters
fix up build system for swig (d242c30 introduced a...
commit
|
commitdiff
|
tree
2013-03-15
Andrew Reynolds
changed default option for quantifier instantiation
commit
|
commitdiff
|
tree
2013-03-14
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-03-14
Morgan Deters
Fix warning (line annotation)
commit
|
commitdiff
|
tree
2013-03-14
Morgan Deters
fix to build system: #include the proper file when...
commit
|
commitdiff
|
tree
2013-03-14
Clark Barrett
Added a rewrite for iff:
commit
|
commitdiff
|
tree
2013-03-13
lianah
post failed attempts at getting the incremental solver...
commit
|
commitdiff
|
tree
2013-03-11
Andrew Reynolds
ite removal option for quantifiers --ite-remove-quant...
commit
|
commitdiff
|
tree
2013-03-09
Morgan Deters
Disallow overflow in bitvector literals (parser only)
commit
|
commitdiff
|
tree
2013-03-06
lianah
more slicer changes for incremental
commit
|
commitdiff
|
tree
2013-03-06
Clark Barrett
Best heuristics for handling decision requests from...
commit
|
commitdiff
|
tree
2013-03-06
Andrew Reynolds
fixed two bugs for the new E-matching implementation...
commit
|
commitdiff
|
tree
2013-03-05
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-03-05
Morgan Deters
Bugfix for SmtEngine: proper unsubscribing for NodeMana...
commit
|
commitdiff
|
tree
2013-03-01
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-26
Morgan Deters
Bug fix for rep-set.
commit
|
commitdiff
|
tree
2013-02-26
Morgan Deters
Fix for quantifiers containing Boolean terms.
commit
|
commitdiff
|
tree
2013-02-26
lianah
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-26
lianah
Merge branch '1.0.x' of https://github.com/CVC4/CVC4...
commit
|
commitdiff
|
tree
2013-02-26
lianah
fix for bv crash in incremental mode; this is a tempora...
commit
|
commitdiff
|
tree
2013-02-24
Andrew Reynolds
added option --model-u-dt-enum for outputting uninterpr...
commit
|
commitdiff
|
tree
2013-02-20
Morgan Deters
Single -q quiets messages/warnings. Double -qq silence...
commit
|
commitdiff
|
tree
2013-02-20
Morgan Deters
Some exception specification fixes in SmtEngine/Command...
commit
|
commitdiff
|
tree
2013-02-18
Morgan Deters
Fix for gitinfo (resolves bug 399).
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
gitinfo modifications fix
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
Merge pull request #6 from kbansal/decNewoptions
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
decision: jh: more refactoring (.h->.cpp, xor/iff)
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
decision/ : jh: refactor embedded ITE, other minor
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
decision/: justification: refactor ITE out
commit
|
commitdiff
|
tree
2013-02-17
Kshitij Bansal
refactoring justification_heuristic code
commit
|
commitdiff
|
tree
2013-02-16
Kshitij Bansal
rm decision jh GiveUp related code
commit
|
commitdiff
|
tree
2013-02-16
Morgan Deters
Some cleanup and copyright updating
commit
|
commitdiff
|
tree
2013-02-16
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-16
Morgan Deters
Fix version identification for new git repository.
commit
|
commitdiff
|
tree
2013-02-16
Morgan Deters
Fix typo in error message
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
prvs commit: lower warning to notice
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
make incremental+portfolio experimental
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
Merge pull request #5 from kbansal/1.0.x
commit
|
commitdiff
|
tree
2013-02-15
Kshitij Bansal
make incremental+portfolio experimental
commit
|
commitdiff
|
tree
2013-02-15
Morgan Deters
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-15
Morgan Deters
Fix builds/ links to survive configuring twice with...
commit
|
commitdiff
|
tree
2013-02-15
Morgan Deters
Fix ECHO command in CVC language parser to not output...
commit
|
commitdiff
|
tree
2013-02-15
Tim King
Merge branch '1.0.x'
commit
|
commitdiff
|
tree
2013-02-15
Tianyi Liang
repairs a bug in rewriterule engine: constructor cannot...
commit
|
commitdiff
|
tree
2013-02-14
Dejan Jovanović
Merge pull request #4 from tiliang/master
commit
|
commitdiff
|
tree
2013-02-14
Tim King
Removing BVDebug and replacing with Debug.
commit
|
commitdiff
|
tree
2013-02-14
Tianyi Liang
repairs a bug in rewriterule engine: constructor cannot...
commit
|
commitdiff
|
tree
2013-02-14
lianah
started working on incremental slicer - not compiling
commit
|
commitdiff
|
tree
2013-02-13
Morgan Deters
Fix a preprocessing performance issue.
commit
|
commitdiff
|
tree
next