projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Improve arithmetic proofs (#6106)
[cvc5.git] / src / expr / node.cpp
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... blob | commitdiff | raw | diff to current
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2019-12-15 Andrew ReynoldsSimple optimizations for the core rewriter (#3569) blob | commitdiff | raw | diff to current
2019-03-26 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2018-08-16 Andres NoetzliMove node algorithms to separate file (#2311) blob | commitdiff | raw | diff to current
2018-07-27 Andrew ReynoldsFix Node::hasFreeVar for function variables (#2216) blob | commitdiff | raw | diff to current
2018-06-25 Aina NiemetzUpdated copyright headers. blob | commitdiff | raw | diff to current
2018-04-08 Andrew ReynoldsCheck free variables in assertions (#1737) blob | commitdiff | raw | diff to current
2018-04-02 yoni206Do not call toString() on malformed node when throwing... blob | commitdiff | raw | diff to current
2018-01-10 Tim KingCleaning up throw specifiers on Exception and subclasse... blob | commitdiff | raw | diff to current
2017-10-20 Andrew ReynoldsMake Sygus conjectures higher-order (#1244) blob | commitdiff | raw | diff to current
2017-10-10 Andrew ReynoldsSplit term database (#1206) blob | commitdiff | raw | diff to current
2017-07-10 ajreynolSeparate sygus term utilities to new file, minor cleanu... blob | commitdiff | raw | diff to current
2017-07-10 ajreynolMerge datatype shared selectors/sygus comp 2017 branch... blob | commitdiff | raw | diff to current
2017-07-07 Mathias PreinerUpdate copyright headers. blob | commitdiff | raw | diff to current
2016-04-20 PaulMengupdate from the master blob | commitdiff | raw | diff to current
2016-04-09 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 blob | commitdiff | raw | diff to current
2016-04-04 Tim KingUpdating the copyright headers and scripts. blob | commitdiff | raw | diff to current
2016-01-05 Tim KingAdding a new class LastExceptionBuffer for the purpose... blob | commitdiff | raw | diff to current
2015-12-15 Tim KingRefactoring Options Handler & Library Cycle Breaking blob | commitdiff | raw | diff to current
2014-07-10 Kshitij BansalMerge remote-tracking branch 'origin/master' into segfa... blob | commitdiff | raw | diff to current
2014-07-01 Morgan DetersUpdate copyrights. blob | commitdiff | raw | diff to current
2014-04-01 Tim KingMerge branch '1.3.x' blob | commitdiff | raw | diff to current
2014-03-26 Morgan DetersMerge branch '1.3.x' blob | commitdiff | raw | diff to current
2014-03-21 Kshitij BansalMerge pull request #22 from kbansal/sets-model blob | commitdiff | raw | diff to current
2014-03-11 Morgan DetersMerge branch '1.3.x' blob | commitdiff | raw | diff to current
2014-03-11 Morgan DetersMerge branch '1.3.x' blob | commitdiff | raw | diff to current
2014-03-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 blob | commitdiff | raw | diff to current
2014-03-08 Tim KingMerge remote-tracking branch 'CVC4root/master' blob | commitdiff | raw | diff to current
2014-03-08 Morgan DetersRemove --ite-remove-quant; support pulling ground ITEs... blob | commitdiff | raw | diff to current
2013-12-05 Morgan DetersUpdate copyrights, add missing file-level documentation... blob | commitdiff | raw | diff to current
2013-11-26 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4 blob | commitdiff | raw | diff to current
2013-11-25 Tim KingMerge remote-tracking branch 'CVC4root/master' blob | commitdiff | raw | diff to current
2013-11-25 Tim KingSubstantial Changes: blob | commitdiff | raw | diff to current
2013-11-11 Morgan DetersFlatten libcvc4 build structure; remove some #include... blob | commitdiff | raw | diff to current
2013-11-07 Morgan DetersFlatten libcvc4 build structure; remove some #include... blob | commitdiff | raw | diff to current
2013-04-02 Morgan DetersRegenerated copyrights: canonicalized names, no emails blob | commitdiff | raw | diff to current
2013-04-02 Morgan Detersupdate copyrights blob | commitdiff | raw | diff to current
2012-12-01 Morgan Detersfix memory corruption issue in debug builds that led... blob | commitdiff | raw | diff to current
2012-11-27 Morgan DetersTuples and records merge. Resolves bug 270. blob | commitdiff | raw | diff to current
2012-10-11 Morgan DetersStandardizing copyright notice. Touches **ALL** source... blob | commitdiff | raw | diff to current
2012-10-10 Morgan DetersAbstract values for SMT-LIB. blob | commitdiff | raw | diff to current
2012-03-01 Morgan DetersPartial merge from kind-backend branch, including Minis... blob | commitdiff | raw | diff to current
2011-11-22 Morgan DetersMore language bindings work: blob | commitdiff | raw | diff to current
2011-04-20 Morgan DetersMinor mixed-bag commit. Expected performance impact... blob | commitdiff | raw | diff to current
2011-03-25 Morgan DetersThis is a merge from the "theoryfixes+cdattrhash" branc... blob | commitdiff | raw | diff to current
2010-10-31 Morgan Detersenable dependence graphs in doxygen; fix lots of doxyge... blob | commitdiff | raw | diff to current
2010-10-06 Morgan Detersdeclare-sort, define-sort working but not thoroughly... blob | commitdiff | raw | diff to current
2010-06-30 Morgan Deters* theory "tree" rewriting implemented and works blob | commitdiff | raw | diff to current
2010-06-04 Morgan Deters** Don't fear the files-changed list, almost all change... blob | commitdiff | raw | diff to current
2010-05-04 Dejan JovanovićType-checking classes and hooks (not tested yet). blob | commitdiff | raw | diff to current
2010-03-30 Morgan DetersHighlights of this commit are: blob | commitdiff | raw | diff to current
2010-02-26 Tim KingTheoryUFWhite tests are added. There are also accompany... blob | commitdiff | raw | diff to current
2010-02-25 Morgan Deters* src/expr/node_builder.h: fixed some overly-aggressive... blob | commitdiff | raw | diff to current
2010-02-22 Dejan Jovanovićfinally works blob | commitdiff | raw
2010-02-22 Dejan JovanovićMerging from branch branches/Liana r241 blob | commitdiff | raw | diff to current
2010-02-22 Christopher L. ConwaySwitching to types-as-attributes in parser blob | commitdiff | raw | diff to current
2010-02-22 Morgan Deters* configure.ac: Remove doc/ from search path for Makefi... blob | commitdiff | raw | diff to current
2010-02-22 Morgan DetersRe-committing revision 232 properly: blob | commitdiff | raw | diff to current
2010-02-22 Morgan Detersundoing improperly-committed revision 232; will re... blob | commitdiff | raw | diff to current
2010-02-22 Cesare Tinelli* Add virtual destructors to CnfStream, Theory, OutputC... blob | commitdiff | raw | diff to current
2010-02-22 Morgan Detersfix bug 22 (remove tracing from non-trace builds; remov... blob | commitdiff | raw | diff to current
2010-02-12 Dejan JovanovićChanges to hashing that solve the xinetd boolean benchm... blob | commitdiff | raw | diff to current
2010-02-04 Dejan Jovanovićbeautification of the prop engine blob | commitdiff | raw | diff to current
2010-02-04 Morgan Detersremove -*- c++ -*- emacs tag from source files (it... blob | commitdiff | raw | diff to current
2010-02-04 Morgan Detersminor fix for update-copyright.pl; ran update-copyright... blob | commitdiff | raw | diff to current
2010-02-04 Tim KingFixes to the cnf converter. Also a barebones utility... blob | commitdiff | raw | diff to current
2010-02-03 Dejan Jovanovićsimple ITE parsing blob | commitdiff | raw | diff to current
2010-02-03 Tim KingWithin node I added printAst(..) for general purpose... blob | commitdiff | raw | diff to current
2009-12-18 Morgan Detersnumerous fixes to nodes; more coming blob | commitdiff | raw | diff to current
2009-12-17 Morgan Detersupdate-copyright.pl now retrieves and incorporates... blob | commitdiff | raw | diff to current
2009-12-17 Morgan Deters+ test infrastructure fixes blob | commitdiff | raw | diff to current
2009-12-16 Morgan Deters+ refactoring fixes for expr package based on code... blob | commitdiff | raw | diff to current
2009-12-16 Tim KingSmall refactoring changes for the expr package. blob | commitdiff | raw | diff to current
2009-12-16 Morgan DetersFixes to the build system: blob | commitdiff | raw | diff to current
2009-12-11 Dejan JovanovićExtracted the public Expr and ExprManager interface... blob | commitdiff | raw | diff to current
2009-12-10 Dejan Jovanovićkilling expr into node... blob | commitdiff | raw | diff to current