Age | Commit message (Expand) | Author |
2015-11-03 | Adding a test to ensure the <build>/src/theory directory is available to the ... | Tim King |
2015-10-27 | Adding the new mkdirs script to EXTRA_DIST. This should fix the failing night... | Tim King |
2015-10-26 | This commit removes using absolute paths in the generation of the .subdirs fi... | Tim King |
2015-10-22 | Enable counterexample-guided quantifier instantiation by default for quantifi... | ajreynol |
2015-09-09 | Working towards a fair enumerator for codatatypes. | ajreynol |
2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix for... | ajreynol |
2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol |
2015-06-29 | Module to infer alpha equivalence of quantified formulas. Minor clean up of ... | ajreynol |
2015-02-11 | Move si solution reconstruction to own file, make more robust. Other refactor... | ajreynol |
2015-02-02 | Single invocation module for counterexample guided quantifier instantiation -... | ajreynol |
2015-01-29 | Restrict LtePartialInst instantiations based on E-matching, promote to quanti... | ajreynol |
2015-01-21 | Initial work on sygusNormalForm. | ajreynol |
2014-12-03 | Floating point infrastructure. | Martin Brain |
2014-11-13 | Remove two obsolete versions of MBQI. | ajreynol |
2014-11-07 | Remove some dead code. | Morgan Deters |
2014-10-28 | Initial infrastructure for function definition quantifiers, internal parsing ... | ajreynol |
2014-10-19 | Finish sets type enumerator implementation. | Kshitij Bansal |
2014-10-10 | Add owner map to better manage QuantifiersModules. Initial infrastructure fo... | ajreynol |
2014-07-31 | New module for generating candidate equality conjectures used in inductive pr... | ajreynol |
2014-06-21 | fixed build failure | lianah |
2014-06-19 | get-glpk-cut-log script, and configure code. | Morgan Deters |
2014-06-14 | Evil bitvector preprocessing pass for simplifying powers of two. | lianah |
2014-06-11 | Fix an omission in bv sources. | Morgan Deters |
2014-06-11 | Some clean-up, post bv-merge. | Morgan Deters |
2014-06-10 | Merging Tim's pseudoboolean work from his fmcad14 branch. | Tim King |
2014-06-10 | Merging CAV14 paper bit-vector work. | lianah |
2014-05-26 | Separating an implicit inclusion of smt_engine.h from theory.h. | Tim King |
2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
2014-05-06 | First draft of ambqi_builder (new implementation of MBQI based on disjoint se... | Andrew Reynolds |
2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
2014-04-09 | some debugging changes | Kshitij Bansal |
2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
2014-03-11 | Fix for rewriterules build breakage. | Morgan Deters |
2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
2014-03-07 | Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into m... | Tim King |
2014-02-21 | disable test cvc3_main, attempt to fix dist_check | Kshitij Bansal |
2014-02-21 | add new theory (sets) | Kshitij Bansal |
2014-02-14 | Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp... | Andrew Reynolds |
2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters |
2013-11-27 | General pre-release cleanup commit | Morgan Deters |
2013-11-25 | Substantial Changes: | Tim King |
2013-11-12 | Minor build system cleanup | Morgan Deters |
2013-11-11 | Some fixes to build system with dependency-tracking is off; should fix RPM/De... | Morgan Deters |
2013-11-08 | Fix "make distclean", which should fix some of the build issues from last night | Morgan Deters |
2013-11-07 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
2013-08-09 | Clean up "make install"-produced intermediate files (resolves bug 526) | Morgan Deters |
2013-04-26 | FCSimplex branch merge | Tim King |