summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2015-01-08switch ascii encoding to unsigned charTianyi Liang
2015-01-07patch to the last commitTianyi Liang
2015-01-07bug fix, thanks to Pierre's reportTianyi Liang
2015-01-07added initial AX rules;Tianyi Liang
2014-12-28Disable prenex by default when using fmf bound int, minor improvement to data...ajreynol
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-22bug fix for constant regular expression model buildingTianyi Liang
2014-12-22Do not collapse wrongly applied selectors for non-well-founded codatatypes pr...ajreynol
2014-12-22Add misc trigger options.ajreynol
2014-12-16Fix oversight in dumping assertions in preprocessing.Morgan Deters
2014-12-12Add cvc parsing support for cardinality constraints. Bug fix for enumerating...ajreynol
2014-12-11Minor fixes to language bindings. (Resolves #607.)Morgan Deters
2014-12-11Option to enable/disable cyclicity check in datatypes.ajreynol
2014-12-10bug fix, thanks to Guy's example.Tianyi Liang
2014-12-09Better error description (related to bug 605).Morgan Deters
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-06Fix dt.size care graph.ajreynol
2014-12-04Relaxed the constant requirement for regular expression loop;Tianyi Liang
2014-12-04clean up and improve intersectionTianyi Liang
2014-12-04Fix valgrind-flagged error about uninitialized value.Morgan Deters
2014-12-04Fix segfault in lambdas when constructed via API.Morgan Deters
2014-12-03Fix UnsatCore in language bindings.Morgan Deters
2014-12-03Floating point infrastructure.Martin Brain
2014-12-03Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2014-12-03Revert "Disable constants sharing in eq engine, disable hack in theory engine."Kshitij Bansal
2014-12-02disable inter cacheTianyi Liang
2014-11-28Synchronize conjecture generation with E-matching. Minor fix to --full-satur...ajreynol
2014-11-26add intersection rewritingTianyi Liang
2014-11-26add more regexp rewritingTianyi Liang
2014-11-26add more functions for regular expressionsTianyi Liang
2014-11-25Fix bug in --term-db-mode=relevant with variable triggers. Support inst-clos...ajreynol
2014-11-22added number of resource units used as a statlianah
2014-11-21Throw error when pattern is not list of terms.ajreynol
2014-11-21Change default option to --inst-when=full-last-call (interleave instantiation...ajreynol
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. Chang...ajreynol
2014-11-20Fix #lines in template.Morgan Deters
2014-11-19Making construction of trigger sets not use the global engine state.Dejan Jovanović
2014-11-19Distribute UnsafeInterruptException interface file for SWIG.Morgan Deters
2014-11-18Merge pull request #70 from kbansal/sets-for-merge-squashedKshitij Bansal
2014-11-18Set Constant's normal form and other short fixesKshitij Bansal
2014-11-18clear model cache in BVQuickCheck clearSolver() (fixes bug 587)Liana Hadarean
2014-11-18All Minisat solve calls now return lbool (fixes bug 599)lianah
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ho...ajreynol
2014-11-17added command line option for extractArith bv rewritelianah
2014-11-17Short-circuit in TheoryArithPrivate::check(), care of Tim.Morgan Deters
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-17Resource-limiting work.Liana Hadarean
2014-11-16Add term db mode. Minor changes to quantifiers rewriter: split ITE's where e...ajreynol
2014-11-14Be lazier to consider EQC in UF+cardinality solver. Minor cleanup.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback