summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2013-03-26core theory currently disabledlianah
2013-03-26fixed inequality bugs due to improper explanationlianah
2013-03-25cleaned up the bv subtheory interface; added check for inequality theory comp...lianah
2013-03-25getEqualityStatus now also queries the inequality solverlianah
2013-03-24added support for disequalities in the inequality solverLiana Hadarean
2013-03-24incremental inequality solver implementedlianah
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-23fixed some explanation problems for the core theory; still slowlianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21fixed more equality stufflianah
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-21fixed compilation problemlianah
2013-03-21incorporated dejan's constant evaluation; now getting destruction seg faultlianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21disabled ineqlianah
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-21added regression test for constant evallianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21fixing constant evaluation bugsDejan Jovanović
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
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-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19merged dejan's stuffLiana Hadarean
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
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-19added the cpp file for the inequality graphLiana Hadarean
2013-03-19implementing more inequality graph stuff; work in progress doesn't compileLiana Hadarean
2013-03-18more work on inequality reasoning for bvlianah
2013-03-16started work on the inequality bv subtheorylianah
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback