projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Updates to theory preprocess equality (#5776)
[cvc5.git]
/
src
/
theory
/
uf
/
theory_uf.h
2020-12-03
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
2020-11-23
Andrew Reynolds
Change UF ho to ppRewrite instead of expand definition...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-15
Andrew Reynolds
Standard equality engine notify class for Theory (...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-11
Andrew Reynolds
Move finite model minimization to UF last call effort...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-02
Andrew Reynolds
(proof-new) Add proof support in TheoryUF (#5002)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-27
Andrew Reynolds
(new theory) Update TheoryUF to new interface (#4944)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-24
Andrew Reynolds
Extend the standard Theory template based on equality...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Remove spurious theory methods calls (#4931)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-21
Andrew Reynolds
Simplify and fix care graph for ufHo (#4924)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
blob
|
commitdiff
|
raw
|
diff to current
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
blob
|
commitdiff
|
raw
|
diff to current
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
blob
|
commitdiff
|
raw
|
diff to current
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
blob
|
commitdiff
|
raw
|
diff to current
2020-02-25
yoni206
remove redundant includes (#3815)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-12
Andrew Reynolds
Rename UF with cardinality extension (#3241)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-02
Andrew Reynolds
Use unique_ptr for UF modules (#3080)
blob
|
commitdiff
|
raw
|
diff to current
2019-07-01
Andrew Reynolds
Split higher-order UF solver (#2890)
blob
|
commitdiff
|
raw
|
diff to current
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-11-27
Andrew Reynolds
Make (T)NodeTrie a general utility (#2489)
blob
|
commitdiff
|
raw
|
diff to current
2018-09-17
Andrew Reynolds
Decision strategy: incorporate UF with cardinality...
blob
|
commitdiff
|
raw
|
diff to current
2018-06-25
Aina Niemetz
Updated copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-04-11
Andrew Reynolds
Properly implement function extensionality based on...
blob
|
commitdiff
|
raw
|
diff to current
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
blob
|
commitdiff
|
raw
|
diff to current
2018-02-06
Tim King
Resolving warnings from -Winconsistent-missing-override...
blob
|
commitdiff
|
raw
|
diff to current
2017-12-08
Andrew Reynolds
Make collect model info return a Bool (#1421)
blob
|
commitdiff
|
raw
|
diff to current
2017-09-21
Andrew Reynolds
Extend quantifier-free UF solver to higher-order. This...
blob
|
commitdiff
|
raw
|
diff to current
2017-07-07
Mathias Preiner
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2017-04-04
ajreynol
Simplify Theory::collectModelInfo interface to not...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-21
ajreynol
Improve computeCareGraph functions to check shared...
blob
|
commitdiff
|
raw
|
diff to current
2017-03-02
ajreynol
Eliminate Boolean term conversion. Generalizes removeIT...
blob
|
commitdiff
|
raw
|
diff to current
2016-11-03
ajreynol
Add priorities to getNextDecision. Properly handle...
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-05-26
Clark Barrett
Merge branch 'master' of https://github.com/CVC4/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2016-05-26
ajreynol
Use term indexing in TheoryUF::computeCareGraph. Do...
blob
|
commitdiff
|
raw
|
diff to current
2016-05-20
ajreynol
Improvements to theory combination + strings: do not...
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-03-23
guykatzz
Merge pull request #82 from CVC4/master_for_merge
blob
|
commitdiff
|
raw
|
diff to current
2016-03-23
Guy
squash-merge from proof branch
blob
|
commitdiff
|
raw
|
diff to current
2016-01-28
Tim King
Adding listeners to Options.
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-06
Tim King
Add SmtGlobals Class
blob
|
commitdiff
|
raw
|
diff to current
2015-10-26
ajreynol
Promote InstStrategyCbqi to quantifier module. Cleanup...
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-30
Morgan Deters
Fix compiler warning re: TheoryUF destructor.
blob
|
commitdiff
|
raw
|
diff to current
2014-04-30
Morgan Deters
Mostly resolves bug #561 memory leaks, and more.
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-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-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-22
Tianyi Liang
Merge branch 'master' of github.com:tiliang/CVC4
blob
|
commitdiff
|
raw
|
diff to current
2014-01-22
Morgan Deters
Delay QuantifiersEngine and UF strong solver initializa...
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-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-03-15
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-14
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-13
lianah
post failed attempts at getting the incremental solver...
blob
|
commitdiff
|
raw
|
diff to current
2013-03-05
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-03-01
Morgan Deters
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-26
lianah
Merge branch '1.0.x'
blob
|
commitdiff
|
raw
|
diff to current
2013-02-24
Andrew Reynolds
added option --model-u-dt-enum for outputting uninterpr...
blob
|
commitdiff
|
raw
|
diff to current
2012-12-01
Morgan Deters
remove instantiator framework
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-10-11
Morgan Deters
Standardizing copyright notice. Touches **ALL** source...
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-07-12
Andrew Reynolds
merged fmf-devel branch, includes support for SMT2...
blob
|
commitdiff
|
raw
|
diff to current
2012-07-06
Tim King
Added virtual destructor to PpRewrite.
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-06
Dejan Jovanović
Changes to the combination mechanism, lots of details...
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-09
Dejan Jovanović
* simplifying equality engine interface
blob
|
commitdiff
|
raw
|
diff to current
2012-05-03
Dejan Jovanović
Some cleanup starting off from trying to understand...
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-02
Dejan Jovanović
CDMap -> CDHashMap
blob
|
commitdiff
|
raw
|
diff to current
2012-02-24
Dejan Jovanović
Theory interface changes:
blob
|
commitdiff
|
raw
|
diff to current
2011-11-30
Morgan Deters
fix linking errors on oneiric
blob
|
commitdiff
|
raw
|
diff to current
2011-10-17
Dejan Jovanović
Sharing work
blob
|
commitdiff
|
raw
|
diff to current
2011-09-29
Morgan Deters
Some base infrastructure for user push/pop; a few bugfi...
blob
|
commitdiff
|
raw
|
diff to current
2011-09-15
Dejan Jovanović
additional stuff for sharing,
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-07-11
Dejan Jovanović
adding disequality propagation
blob
|
commitdiff
|
raw
|
diff to current
2011-07-11
Morgan Deters
merge from symmetry branch
blob
|
commitdiff
|
raw
|
diff to current
next