Adding an option to the equality engine constructor to treat all constants as
[cvc5.git] / src / theory / theory_engine.cpp
2014-12-27 Dejan JovanovicAdding an option to the equality engine constructor...
2014-12-03 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2014-12-03 Kshitij BansalRevert "Disable constants sharing in eq engine, disable...
2014-11-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-11-20 ajreynolDisable constants sharing in eq engine, disable hack...
2014-11-19 Kshitij BansalMerge pull request #70 from kbansal/sets-for-merge...
2014-11-19 Kshitij BansalSet Constant's normal form and other short fixes
2014-11-17 Liana HadareanResource-limiting work.
2014-11-11 Kshitij BansalMerge pull request #64 from mdeters/theorysets-hashset...
2014-11-10 Tianyi LiangMerge pull request #63 from mdeters/theorystrings-hashs...
2014-11-10 ajreynolDo not eliminate variables only occurring in patterns...
2014-11-10 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-07 Morgan DetersMerge branch '1.4.x'
2014-11-05 Morgan DetersMerge branch '1.4.x'
2014-10-30 Clark BarrettAdded new, much faster, care graph computation for...
2014-10-17 Morgan DetersMerge branch '1.4.x'
2014-10-16 Morgan DetersMerge branch '1.4.x'
2014-10-11 Morgan DetersMerge branch '1.4.x'
2014-10-10 Kshitij BansalMerge remote-tracking branch 'origin/1.4.x'
2014-10-09 Morgan DetersMerge branch '1.4.x'
2014-10-07 Morgan DetersMerge branch '1.4.x'
2014-10-06 Morgan DetersMerge branch '1.4.x'
2014-10-06 Morgan DetersMerge branch '1.4.x'
2014-10-03 Morgan DetersMerge branch '1.4.x'
2014-10-03 Morgan DetersMerge branch '1.4.x'
2014-10-02 Clark BarrettAdded internal support for constant arrays.
2014-10-02 Morgan DetersMerge branch '1.4.x'.
2014-10-02 Clark BarrettMore model-based combination for arrays
2014-10-02 Clark BarrettBetter getEqualityStatus for arrays, smarter combinatio...
2014-09-30 Morgan DetersMerge branch '1.4.x'
2014-09-30 Morgan DetersProofs- and cores-related segfault fixes (mainly a...
2014-09-27 Morgan DetersMerge branch '1.4.x'
2014-09-26 Morgan DetersMerge branch '1.4.x'
2014-09-18 Morgan DetersResource spending support in theories (and especially...
2014-09-17 Kshitij BansalMerge branch '1.4.x' while ignoring commit 8d5eb49.
2014-09-17 Kshitij BansalMerge branch '1.4.x'
2014-08-24 Kshitij Bansalimprovements to sets sharing
2014-08-22 Morgan DetersUnsat core infrastruture and API (SMT-LIB compliance...
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-22 Morgan DetersMerge branch '1.4.x'
2014-08-19 Morgan DetersMerge branch '1.4.x'
2014-08-18 Morgan DetersMerge branch '1.4.x'
2014-08-18 ajreynolAdd support for quantifier-specific instantiation level...
2014-07-10 Kshitij BansalMerge remote-tracking branch 'origin/master' into segfa...
2014-07-01 Morgan DetersUpdate copyrights.
2014-06-10 lianahMerging CAV14 paper bit-vector work.
2014-05-12 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-05-11 Andrew ReynoldsMore preparation for CASC proofs. Minor fix for sort...
2014-05-01 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-30 Tim KingT-entailment work, and QCF (quant conflict find) work...
2014-04-01 Tim KingMerge branch '1.3.x'
2014-03-26 Morgan DetersMerge branch '1.3.x'
2014-03-21 Kshitij BansalMerge pull request #22 from kbansal/sets-model
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Morgan DetersFix for rewriterules build breakage.
2014-03-11 Morgan DetersMerge branch '1.3.x'
2014-03-11 Andrew ReynoldsInitial refactor of rewrite rules, make theory_rewriter...
2014-03-10 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-08 Tim KingMerge pull request #18 from timothy-king/master
2014-03-08 Tim KingFixing name changes that cam in from the merge.
2014-03-08 Tim KingMerge remote-tracking branch 'CVC4root/master'
2014-03-07 Tim KingMerging a squash of the branch timothy-king/CVC4/glpkne...
2014-03-07 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-03-07 Tianyi Liangadds incremental for strings; clean-up codes
2014-03-07 Tianyi Liangadds incremental for strings; clean-up codes
2014-03-04 Morgan DetersDon't theory-preprocess under quantifiers; but DO theor...
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Morgan DetersMerge branch '1.3.x'
2014-02-21 Kshitij BansalMerge pull request #10 from kbansal/sets-for-merge
2014-02-21 Kshitij Bansaladd new theory (sets)
2014-02-19 Tim KingMerge branch '1.3.x'
2014-01-27 Morgan DetersMerge branch '1.3.x'
2014-01-22 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-01-22 Morgan DetersDelay QuantifiersEngine and UF strong solver initializa...
2014-01-18 Tianyi Liangstrings with new ideas
2014-01-18 Morgan DetersMerge branch '1.3.x'
2014-01-17 Tianyi Liangstrings with new ideas
2014-01-17 Kshitij BansalMerge branch '1.3.x'
2014-01-10 Andrew ReynoldsAdd new method --quant-cf for finding conflicts eagerly...
2014-01-09 Morgan DetersMerge branch '1.3.x'
2014-01-08 Morgan DetersMerge branch '1.3.x'
2014-01-02 Morgan DetersMerge branch '1.3.x'
2013-12-27 Morgan DetersMerge branch '1.3.x'
2013-12-26 Tianyi LiangMerge branch 'master' of https://github.com/CVC4/CVC4
2013-12-24 Morgan DetersMerge branch '1.3.x'
2013-12-24 Morgan DetersMerge branch '1.3.x'
2013-12-23 Morgan DetersProof-checking code; fixups of segfaults and missing...
2013-12-05 Morgan DetersUpdate copyrights, add missing file-level documentation...
2013-12-03 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-11-27 Morgan DetersGeneral pre-release cleanup commit
2013-11-26 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-11-25 Tim KingMerge remote-tracking branch 'CVC4root/master'
2013-11-25 Tim KingSubstantial Changes:
2013-11-06 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-11-04 lianahMerge branch 'master' of https://github.com/CVC4/CVC4
2013-10-08 Liana Hadareanfixed some bugs
2013-09-30 Liana Hadareanmerged golden
2013-09-27 Morgan DetersSome fixes to recent strings commits.
next