summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2013-03-22compiles withDejan Jovanović
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21Better error in case of nonlinear assertions while in linear logicMorgan Deters
2013-03-21Add the ability to "mute" commands, needed for SMT-LIB compliance.Morgan Deters
2013-03-21fixing markings of internal nodes in equality engineDejan Jovanović
2013-03-21Merge branch 'master' of github.com:CVC4/CVC4Dejan Jovanović
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-21more equality constant evaluationDejan Jovanović
2013-03-21Fix for SmtEngine::expandDefinitions()---improper TypeCheckingExceptionMorgan Deters
2013-03-21fixing constant evaluation bugsDejan Jovanović
2013-03-20Better reporting of detached git state in --version and --show-configMorgan Deters
2013-03-20Fix to bug 497: make justification heuristic's ITE cache context-dependent.Morgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-03-20Some statistics for narrowing down incrementality issues (push/pop vs solve t...Morgan Deters
2013-03-19Adding evaluation of constant terms to the equality engine. Evaluation on a p...Dejan Jovanović
2013-03-19Minor cleanup of sourcesMorgan Deters
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-03-19Remove PropositionalQuery class and all CUDD-related build stuff (and referen...Morgan Deters
2013-03-19Minor fixes to build systemMorgan Deters
2013-03-15Boolean terms rewriting for quantified variables of type Bool, when quantifie...Morgan Deters
2013-03-15Merge branch '1.0.x'Morgan Deters
2013-03-15fix up build system for swig (d242c30 introduced a subtle error)1.0.xMorgan Deters
2013-03-15changed default option for quantifier instantiationAndrew Reynolds
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14Fix warning (line annotation)Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-03-13Added a rewrite for iff:Clark Barrett
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for boolean...Andrew Reynolds
2013-03-08Disallow overflow in bitvector literals (parser only)Morgan Deters
2013-03-06Best heuristics for handling decision requests from arraysClark Barrett
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive minisc...Andrew Reynolds
2013-03-05Merge branch '1.0.x'Morgan Deters
2013-03-05Bugfix for SmtEngine: proper unsubscribing for NodeManager eventsMorgan Deters
2013-03-01Merge branch '1.0.x'Morgan Deters
2013-02-26Bug fix for rep-set.Morgan Deters
2013-02-26Fix for quantifiers containing Boolean terms.Morgan Deters
2013-02-26Merge branch '1.0.x'lianah
2013-02-26Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.xlianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as datatype...Andrew Reynolds
2013-02-20Single -q quiets messages/warnings. Double -qq silences sat/unsat output too.Morgan Deters
2013-02-20Some exception specification fixes in SmtEngine/Command infrastructureMorgan Deters
2013-02-18Fix for gitinfo (resolves bug 399).Morgan Deters
2013-02-16Merge branch '1.0.x'Kshitij Bansal
2013-02-16gitinfo modifications fixKshitij Bansal
2013-02-16Merge pull request #6 from kbansal/decNewoptionsKshitij Bansal
2013-02-16decision: jh: more refactoring (.h->.cpp, xor/iff)Kshitij Bansal
2013-02-16decision/ : jh: refactor embedded ITE, other minorKshitij Bansal
2013-02-16decision/: justification: refactor ITE outKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback