projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Adding an option to the equality engine constructor to treat all constants as
2014-12-27
Dejan Jovanovic
Adding an option to the equality engine constructor...
commit
|
commitdiff
|
tree
2014-05-08
Dejan Jovanovic
Adding encoding of sha1 collision for the hashing example
commit
|
commitdiff
|
tree
2013-02-14
Dejan Jovanović
Merge pull request #4 from tiliang/master
commit
|
commitdiff
|
tree
2012-12-12
Dejan Jovanović
Merge pull request #2 from CVC4/1.0.x
commit
|
commitdiff
|
tree
2012-12-12
Dejan Jovanović
Merge pull request #1 from lianah/1.0.x
commit
|
commitdiff
|
tree
2012-11-26
Dejan Jovanović
fixup for incremental solving
commit
|
commitdiff
|
tree
2012-11-26
Dejan Jovanović
Adding support for a master equality engine. Each theory...
commit
|
commitdiff
|
tree
2012-11-16
Dejan Jovanović
fixing and refactoring the equality iterator
commit
|
commitdiff
|
tree
2012-10-30
Dejan Jovanović
delta of a model-building failure case
commit
|
commitdiff
|
tree
2012-10-24
Dejan Jovanović
fix for bug 429
commit
|
commitdiff
|
tree
2012-10-24
Dejan Jovanović
two smaller random pure LRA push-pop cases that fail
commit
|
commitdiff
|
tree
2012-10-10
Dejan Jovanović
fixing the cvc bv parser and typechecker
commit
|
commitdiff
|
tree
2012-10-09
Dejan Jovanović
fix for bug 415
commit
|
commitdiff
|
tree
2012-10-09
Dejan Jovanović
adding mergePredicates method to the equality engine...
commit
|
commitdiff
|
tree
2012-10-05
Dejan Jovanović
BoolExpr removed and replaced with Expr
commit
|
commitdiff
|
tree
2012-10-03
Dejan Jovanović
adding ::getBooleanVariables to the PropEngine
commit
|
commitdiff
|
tree
2012-09-24
Dejan Jovanović
some api changes
commit
|
commitdiff
|
tree
2012-09-22
Dejan Jovanović
another fix for the equality class iterator
commit
|
commitdiff
|
tree
2012-09-19
Dejan Jovanović
fix for bug 370.
commit
|
commitdiff
|
tree
2012-09-19
Dejan Jovanović
Changing the equality engines's euivalence class iterator...
commit
|
commitdiff
|
tree
2012-08-07
Dejan Jovanović
small fixes
commit
|
commitdiff
|
tree
2012-08-06
Dejan Jovanović
removing the sat solver inmterface from being public
commit
|
commitdiff
|
tree
2012-08-06
Dejan Jovanović
fix constant printing for datatypes
commit
|
commitdiff
|
tree
2012-07-14
Dejan Jovanović
an example that uses bitvectors to simulate sha1 computation...
commit
|
commitdiff
|
tree
2012-07-10
Dejan Jovanović
* fixing the simple_vc_cxx.cpp compile issue (no more...
commit
|
commitdiff
|
tree
2012-07-10
Dejan Jovanović
going back to 1. being a non decimal
commit
|
commitdiff
|
tree
2012-07-10
Dejan Jovanović
small changes:
commit
|
commitdiff
|
tree
2012-06-17
Dejan Jovanović
fixing a problem due to lemmas produced while backtracking
commit
|
commitdiff
|
tree
2012-06-17
Dejan Jovanović
enabling theoryof=term for quantifiers with sharing
commit
|
commitdiff
|
tree
2012-06-17
Dejan Jovanović
fixing wrong assertion
commit
|
commitdiff
|
tree
2012-06-17
Dejan Jovanović
fixing makefile error that brakes build
commit
|
commitdiff
|
tree
2012-06-16
Dejan Jovanović
small change to equality assertions so that one doesn...
commit
|
commitdiff
|
tree
2012-06-16
Dejan Jovanović
changing theoryOf in shared mode with arrays to move...
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
fixing the problems with the bvminisat. there was a...
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
enabling fixed bug345 case
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
fixes for the hasTerm issues in the shared database...
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
fix for clark's bug
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
changing to a more natural propagation order in uf...
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
some changes to the uf engine
commit
|
commitdiff
|
tree
2012-06-14
Dejan Jovanović
* removing rewriteEquality from the rewriter
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
removing bug233 until morgan commits the actual file
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
fix for bug 354
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
enabling regressions from last night, all fixed
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
!(*child_it).isConst() assertion fail
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
r2.node == response.node failure
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
r2.node == response.node failure
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
!current[0].isConst() failure
commit
|
commitdiff
|
tree
2012-06-13
Dejan Jovanović
benchmark to show that we don't rewrite bvsmod correctly
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
missing problems
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong answer for bv
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
bufixes and the bugs
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
conflicts from theories are removable
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
more breakage in aufbv
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong answer benchmarks
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
wrong result benchmark
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
tests for the
commit
|
commitdiff
|
tree
2012-06-12
Dejan Jovanović
test cases for the
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
another benchmark that used to fail
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
fixing bitvector bugs
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
failing bv examples
commit
|
commitdiff
|
tree
2012-06-11
Dejan Jovanović
some failing examples
commit
|
commitdiff
|
tree
2012-06-10
Dejan Jovanović
adding an assertion to trigger the problem of bug349...
commit
|
commitdiff
|
tree
2012-06-10
Dejan Jovanović
fixes for bug347
commit
|
commitdiff
|
tree
2012-06-08
Dejan Jovanović
very small fast example for the bv fail
commit
|
commitdiff
|
tree
2012-06-08
Dejan Jovanović
small fuzz examples where bv fails
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
fixing the wrong results. arrays equality adaptor had...
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
cleaning up the expample for the future
commit
|
commitdiff
|
tree
2012-06-07
Dejan Jovanović
fixing some bugs in propagation of disequalities
commit
|
commitdiff
|
tree
2012-06-06
Dejan Jovanović
disabling a super-expensive assertions to speed up...
commit
|
commitdiff
|
tree
2012-06-06
Dejan Jovanović
Changes to the combination mechanism, lots of details...
commit
|
commitdiff
|
tree
2012-05-27
Dejan Jovanović
some reordering to keep invariants
commit
|
commitdiff
|
tree
2012-05-27
Dejan Jovanović
Committing the work on equality engine, I need to see...
commit
|
commitdiff
|
tree
2012-05-24
Dejan Jovanović
Separating the subtheory implementations in the bitvector...
commit
|
commitdiff
|
tree
2012-05-24
Dejan Jovanović
Significant changes to the internals of the equality...
commit
|
commitdiff
|
tree
2012-05-21
Dejan Jovanović
Updating equality manager to handle tagged trigger...
commit
|
commitdiff
|
tree
2012-05-18
Dejan Jovanović
removing failing regression
commit
|
commitdiff
|
tree
2012-05-17
Dejan Jovanović
Queueing up asserted literals in the proxy instead...
commit
|
commitdiff
|
tree
2012-05-16
Dejan Jovanović
adding simple-minded handling of (dis-)equalities where...
commit
|
commitdiff
|
tree
2012-05-16
Dejan Jovanović
testcase for bug 337
commit
|
commitdiff
|
tree
2012-05-16
Dejan Jovanović
Changes to SAT solver:
commit
|
commitdiff
|
tree
2012-05-16
Dejan Jovanović
equality status for bitvectors can now look into the...
commit
|
commitdiff
|
tree
2012-05-16
Dejan Jovanović
removing duplicate literals in explanations of propagations
commit
|
commitdiff
|
tree
2012-05-15
Dejan Jovanović
(no commit message)
commit
|
commitdiff
|
tree
2012-05-15
Dejan Jovanović
test cases
commit
|
commitdiff
|
tree
2012-05-15
Dejan Jovanović
fixing warnings, grr
commit
|
commitdiff
|
tree
2012-05-14
Dejan Jovanović
fixes for shared term registration. previously the...
commit
|
commitdiff
|
tree
2012-05-14
Dejan Jovanović
fixing up preregistration again
commit
|
commitdiff
|
tree
2012-05-13
Dejan Jovanović
fixing build warnings
commit
|
commitdiff
|
tree
2012-05-09
Dejan Jovanović
* simplifying equality engine interface
commit
|
commitdiff
|
tree
2012-05-09
Dejan Jovanović
Fixing the debug tags generation and related methods...
commit
|
commitdiff
|
tree
2012-05-03
Dejan Jovanović
Some cleanup starting off from trying to understand...
commit
|
commitdiff
|
tree
2012-04-18
Dejan Jovanović
disabling the problematic pragma in node_manager.h...
commit
|
commitdiff
|
tree
2012-04-17
Dejan Jovanović
Fix for thos annoying "array index" warnings in production...
commit
|
commitdiff
|
tree
2012-04-06
Dejan Jovanović
processing assertions in bit-vectors even when in fullcheck...
commit
|
commitdiff
|
tree
2012-04-04
Dejan Jovanović
some settings in bvminisat
commit
|
commitdiff
|
tree
2012-03-30
Dejan Jovanović
some more build system fixes
commit
|
commitdiff
|
tree
2012-03-30
Dejan Jovanović
fixing some build systme warnings
commit
|
commitdiff
|
tree
2012-03-29
Dejan Jovanović
bringing cryptominisat into the main branch
commit
|
commitdiff
|
tree
2012-03-28
Dejan Jovanović
enabling the --disable-arithmetic-propagation option...
commit
|
commitdiff
|
tree
2012-03-28
Dejan Jovanović
Some renaming and refactoring in SAT
commit
|
commitdiff
|
tree
next