summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2013-03-27New model-based array procedureClark Barrett
2013-03-27reverted the core solver to do static slicing, added option --bv-core-solverlianah
2013-03-27fixed inequality checkDisequalities inefficiencylianah
2013-03-27Merge branch 'master' into bv-corelianah
2013-03-27fixed some model stufflianah
2013-03-27fixed model generation bug; commented out attempt at inequality propagationlianah
2013-03-26inequality solver now only splits on disequalities when completelianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-26Make --incremental the default when running interactivelyMorgan Deters
2013-03-26core theory currently disabledlianah
2013-03-26getModelValue implementation in bitvectorsDejan Jovanović
2013-03-26addingDejan Jovanović
* getModelValue to valuation * getModelValue to theory engine * getModelValue to theory implemented getModelValue in bitvector the purpose of getModelValue is to ask for a concrete value of a shared term
2013-03-26Merge branch 'master' of git@github.com:CVC4/CVC4.gitDejan Jovanović
2013-03-26moving bv before arraysDejan Jovanović
2013-03-26fixed inequality bugs due to improper explanationlianah
2013-03-25cleaned up the bv subtheory interface; added check for inequality theory ↵lianah
completeness
2013-03-25java input stream adapters workingMorgan Deters
2013-03-25getEqualityStatus now also queries the inequality solverlianah
2013-03-25Fix for SCM detectionMorgan Deters
2013-03-25finish removal of separateOutputKshitij Bansal
2013-03-24added support for disequalities in the inequality solverLiana Hadarean
2013-03-24incremental inequality solver implementedlianah
2013-03-23Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.Morgan Deters
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-23Merge remote-tracking branch 'dddejan/c++11'Dejan Jovanović
Conflicts: src/smt/boolean_terms.cpp
2013-03-23changing string hash function to use the gnu namespaceDejan Jovanović
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-22compiles withDejan Jovanović
export CXXFLAGS='-std=gnu++0x' before configure fails all regressions in the parser
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 ↵lianah
inequalities
2013-03-20Better reporting of detached git state in --version and --show-configMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback