projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Switching EqProof to use shared_ptr everywhere. (#1217)
[cvc5.git]
/
src
/
theory
/
uf
/
equality_engine.h
2017-10-25
Tim King
Switching EqProof to use shared_ptr everywhere. (...
blob
|
commitdiff
|
raw
2017-09-13
Andrew Reynolds
Modify equality engine to allow operators to be marked...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Merge branch 'master' into cleanup-regexp
blob
|
commitdiff
|
raw
|
diff to current
2017-07-21
Tim King
Moving from the gnu extensions for hash maps to the...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-03-02
ajreynol
Eliminate Boolean term conversion. Generalizes removeIT...
blob
|
commitdiff
|
raw
|
diff to current
2016-10-11
Paul Meng
Merge branch 'origin' of https://github.com/CVC4/CVC4.git
blob
|
commitdiff
|
raw
|
diff to current
2016-09-02
Tim King
Merge pull request #91 from timothy-king/no-throw
blob
|
commitdiff
|
raw
|
diff to current
2016-09-01
Tim King
Relaxing the throw specifiers for the destructors for...
blob
|
commitdiff
|
raw
|
diff to current
2016-07-05
PaulMeng
Merge branch 'master' of https://github.com/CVC4/CVC4.git
blob
|
commitdiff
|
raw
|
diff to current
2016-06-06
guykatzz
Merge pull request #85 from CVC4/master_for_proof_merge
blob
|
commitdiff
|
raw
|
diff to current
2016-06-02
Guy
Merge from proof branch
blob
|
commitdiff
|
raw
|
diff to current
2016-06-02
Guy
Revert "Merging proof branch"
blob
|
commitdiff
|
raw
|
diff to current
2016-06-02
Guy
Merging proof branch
blob
|
commitdiff
|
raw
|
diff to current
2016-04-20
PaulMeng
update from the master
blob
|
commitdiff
|
raw
|
diff to current
2016-04-09
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-04-04
Tim King
Updating the copyright headers and scripts.
blob
|
commitdiff
|
raw
|
diff to current
2016-04-03
Guy
Removed the theory-specific merge reason types. Instead...
blob
|
commitdiff
|
raw
|
diff to current
2016-03-24
Guy
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-03-24
Guy
Refactored the equality engine in order to remove theor...
blob
|
commitdiff
|
raw
|
diff to current
2016-01-27
Liana Hadarean
Merged bit-vector and uf proof branch.
blob
|
commitdiff
|
raw
|
diff to current
2016-01-09
Tim King
Removing StatisticsRegistry's static functions current...
blob
|
commitdiff
|
raw
|
diff to current
2015-12-15
Tim King
Refactoring Options Handler & Library Cycle Breaking
blob
|
commitdiff
|
raw
|
diff to current
2015-01-07
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-12-27
Dejan Jovanovic
Adding an option to the equality engine constructor...
blob
|
commitdiff
|
raw
|
diff to current
2014-11-27
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-11-20
Dejan Jovanović
Making construction of trigger sets not use the global...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-10
Kshitij Bansal
Merge remote-tracking branch 'origin/master' into segfa...
blob
|
commitdiff
|
raw
|
diff to current
2014-07-01
Morgan Deters
Update copyrights.
blob
|
commitdiff
|
raw
|
diff to current
2014-04-01
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-26
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-21
Kshitij Bansal
Merge pull request #22 from kbansal/sets-model
blob
|
commitdiff
|
raw
|
diff to current
2014-03-17
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-03-14
Andrew Reynolds
Add ability to provide theory-specific proof rules...
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-03-11
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Kshitij Bansal
Merge pull request #10 from kbansal/sets-for-merge
blob
|
commitdiff
|
raw
|
diff to current
2014-02-21
Kshitij Bansal
add new theory (sets)
blob
|
commitdiff
|
raw
|
diff to current
2014-02-19
Tim King
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-27
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-18
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-17
Kshitij Bansal
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-09
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-08
Morgan Deters
Merge branch '1.3.x'
blob
|
commitdiff
|
raw
|
diff to current
2014-01-03
Andrew Reynolds
Added support for proof production in Equality Engine...
blob
|
commitdiff
|
raw
|
diff to current
2013-12-05
Morgan Deters
Update copyrights, add missing file-level documentation...
blob
|
commitdiff
|
raw
|
diff to current
2013-11-11
Morgan Deters
Flatten libcvc4 build structure; remove some #include...
blob
|
commitdiff
|
raw
|
diff to current
2013-11-07
Morgan Deters
Flatten libcvc4 build structure; remove some #include...
blob
|
commitdiff
|
raw
|
diff to current
2013-09-30
Liana Hadarean
merged golden
blob
|
commitdiff
|
raw
|
diff to current
2013-09-13
Morgan Deters
Documentation fixes, some code typo fixes, file perms...
blob
|
commitdiff
|
raw
|
diff to current
2013-08-26
Kshitij Bansal
Merge branch '1.2.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-07-19
Dejan Jovanovic
possible fix for bug 521
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
Regenerated copyrights: canonicalized names, no emails
blob
|
commitdiff
|
raw
|
diff to current
2013-04-02
Morgan Deters
update copyrights
blob
|
commitdiff
|
raw
|
diff to current
2013-04-01
Morgan Deters
Merging some cleanup work:
blob
|
commitdiff
|
raw
|
diff to current
2013-03-21
lianah
Merge branch 'master' into bv-core
blob
|
commitdiff
|
raw
|
diff to current
2013-03-21
Dejan Jovanović
fixing markings of internal nodes in equality engine
blob
|
commitdiff
|
raw
|
diff to current
2013-03-21
lianah
Merge branch 'master' into bv-core
blob
|
commitdiff
|
raw
|
diff to current
2013-03-21
Dejan Jovanović
fixing constant evaluation bugs
blob
|
commitdiff
|
raw
|
diff to current
2013-03-20
Liana Hadarean
merged master with dejan's constant evaluating equality...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-20
Dejan Jovanović
Adding evaluation of constant terms to the equality...
blob
|
commitdiff
|
raw
|
diff to current
2012-11-26
Dejan Jovanović
Adding support for a master equality engine. Each theor...
blob
|
commitdiff
|
raw
|
diff to current
2012-11-16
Dejan Jovanović
fixing and refactoring the equality iterator
blob
|
commitdiff
|
raw
|
diff to current
2012-10-11
Morgan Deters
Standardizing copyright notice. Touches **ALL** source...
blob
|
commitdiff
|
raw
|
diff to current
2012-10-09
Dejan Jovanović
fix for bug 415
blob
|
commitdiff
|
raw
|
diff to current
2012-10-09
Dejan Jovanović
adding mergePredicates method to the equality engine...
blob
|
commitdiff
|
raw
|
diff to current
2012-09-22
Morgan Deters
Separate public-facing and internal-facing interfaces...
blob
|
commitdiff
|
raw
|
diff to current
2012-09-19
Dejan Jovanović
Changing the equality engines's euivalence class iterat...
blob
|
commitdiff
|
raw
|
diff to current
2012-08-31
Andrew Reynolds
merge from fmf-devel branch. more updates to models...
blob
|
commitdiff
|
raw
|
diff to current
2012-08-29
Morgan Deters
* Numerous documentation fixes (fix doxygen warnings...
blob
|
commitdiff
|
raw
|
diff to current
2012-08-14
Tim King
Switched a number of EqClassIterator operations to...
blob
|
commitdiff
|
raw
|
diff to current
2012-07-27
François Bobot
Merge quantifiers2-trunk:
blob
|
commitdiff
|
raw
|
diff to current
2012-07-07
Morgan Deters
Various fixes to documentation---typos, some incomplete...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-14
Dejan Jovanović
changing to a more natural propagation order in uf...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-12
Morgan Deters
minor cleanup, and replace a "private:" in equality...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-11
Morgan Deters
Merge from quantifiers2-trunkmerge branch.
blob
|
commitdiff
|
raw
|
diff to current
2012-06-10
Dejan Jovanović
fixes for bug347
blob
|
commitdiff
|
raw
|
diff to current
2012-06-07
Dejan Jovanović
fixing the wrong results. arrays equality adaptor had...
blob
|
commitdiff
|
raw
|
diff to current
2012-06-07
Dejan Jovanović
fixing some bugs in propagation of disequalities
blob
|
commitdiff
|
raw
|
diff to current
2012-06-06
Dejan Jovanović
Changes to the combination mechanism, lots of details...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-27
Dejan Jovanović
Committing the work on equality engine, I need to see...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-24
Dejan Jovanović
Significant changes to the internals of the equality...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-21
Dejan Jovanović
Updating equality manager to handle tagged trigger...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-16
Dejan Jovanović
adding simple-minded handling of (dis-)equalities where...
blob
|
commitdiff
|
raw
|
diff to current
2012-05-09
Dejan Jovanović
* simplifying equality engine interface
blob
|
commitdiff
|
raw
|
diff to current
2012-05-08
Liana Hadarean
Merging in bvprop branch, with proper bit-vector propag...
blob
|
commitdiff
|
raw
|
diff to current
2012-04-11
Morgan Deters
merge from arrays-clark branch
blob
|
commitdiff
|
raw
|
diff to current
2012-03-22
Dejan Jovanović
some improvements to the sharing mechanism/interface
blob
|
commitdiff
|
raw
|
diff to current
2012-03-06
Dejan Jovanović
updating the equality engine to be able to give explana...
blob
|
commitdiff
|
raw
|
diff to current
2012-02-21
Dejan Jovanović
Fix for bug303. The problem was with function applicati...
blob
|
commitdiff
|
raw
|
diff to current
2012-02-08
Dejan Jovanović
fixing a bug in uf_engine application lookup backtracking
blob
|
commitdiff
|
raw
|
diff to current
2011-12-12
Dejan Jovanović
* merging some uf stuff from incremental_work branch...
blob
|
commitdiff
|
raw
|
diff to current
2011-10-17
Dejan Jovanović
Sharing work
blob
|
commitdiff
|
raw
|
diff to current
2011-09-07
Dejan Jovanović
fixes for uf/equality engine from the quantifiers branc...
blob
|
commitdiff
|
raw
|
diff to current
2011-09-02
Morgan Deters
Merge from my post-smtcomp branch. Includes:
blob
|
commitdiff
|
raw
|
diff to current
2011-09-02
Dejan Jovanović
* Changing pre-registration to be context dependent...
blob
|
commitdiff
|
raw
|
diff to current
2011-08-23
Dejan Jovanović
some uf cleanup
blob
|
commitdiff
|
raw
|
diff to current
2011-07-09
Dejan Jovanović
surprize surprize
blob
|
commitdiff
|
raw
|
diff to current