projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2013-04-17 Kshitij Bansalbool flatten: node num_children workaround commit | commitdiff | tree
2013-04-17 Kshitij Bansalboolean flatten: bug fix in dfs search commit | commitdiff | tree
2013-04-17 Kshitij Bansalboolean flatten rewrite: dont re-rewrite commit | commitdiff | tree
2013-04-17 Kshitij Bansalgeneralize to handle and commit | commitdiff | tree
2013-04-16 Kshitij Bansalflatten or nodes commit | commitdiff | tree
2013-04-11 Clark BarrettImproved speed of no redundant lemma assertion by using... commit | commitdiff | tree
2013-04-11 Clark BarrettFixes for getModelVal in bv theory commit | commitdiff | tree
2013-04-11 Clark BarrettAdded check for infinite lemma loop commit | commitdiff | tree
2013-04-11 lianahfixed getModelValue to only query the value of leaves... commit | commitdiff | tree
2013-04-09 Morgan DetersChange TPTP parser to not use the STRING type; this... commit | commitdiff | tree
2013-04-05 Morgan DetersFix unit test (compile error) for new SatSolver interface commit | commitdiff | tree
2013-04-03 Dejan Jovanović* changing the bitblast-eager to bitblast on pre-register commit | commitdiff | tree
2013-04-03 Morgan DetersPrerelease versioning for master. commit | commitdiff | tree
2013-04-03 Morgan DetersPre-release versioning commit | commitdiff | tree
2013-04-03 Morgan DetersCutting release 1.1. commit | commitdiff | tree
2013-04-03 Morgan DetersSome final minor changes before cutting 1.1. commit | commitdiff | tree
2013-04-03 Liana Hadareanupdated NEWS to include inequality solver commit | commitdiff | tree
2013-04-03 Andrew Reynoldsabort quantifiers check if master equality engine is... commit | commitdiff | tree
2013-04-02 Tim KingMaking arithmetic model reversion on unsat checks an... commit | commitdiff | tree
2013-04-02 Morgan DetersRegenerated copyrights: canonicalized names, no emails commit | commitdiff | tree
2013-04-02 Morgan DetersRemove old README file from rewrite-rules left over... commit | commitdiff | tree
2013-04-02 Morgan DetersFix get-authors script to not extract email addresses... commit | commitdiff | tree
2013-04-02 Morgan DetersOne final fix to "make submission" rule commit | commitdiff | tree
2013-04-02 Morgan Detersupdate copyrights commit | commitdiff | tree
2013-04-02 Morgan DetersAdjust release Makefile rules, new run script commit | commitdiff | tree
2013-04-02 Clark BarrettFix regression error by turning off model-based solver... commit | commitdiff | tree
2013-04-02 Clark BarrettTurning on model based array solver for QF_AX commit | commitdiff | tree
2013-04-02 Clark BarrettMade eager lemmas an option, enabled for QF_AX commit | commitdiff | tree
2013-04-02 Clark BarrettDisabling eager array index splitting for QF_AX commit | commitdiff | tree
2013-04-02 Morgan DetersFixes for two bugs: commit | commitdiff | tree
2013-04-01 Tim KingCleaning up the demand restart code. commit | commitdiff | tree
2013-04-01 Tim KingAdding a restart test strategy to integers. commit | commitdiff | tree
2013-04-01 Tim KingAdding demand restart. commit | commitdiff | tree
2013-04-01 Tim KingAdding tests for the previous commit. commit | commitdiff | tree
2013-04-01 Morgan DetersMerging some cleanup work: commit | commitdiff | tree
2013-04-01 Tim KingFix for iff terms over equalities between the same... commit | commitdiff | tree
2013-04-01 Morgan DetersFix bug 491 and related issues with checkModel() and... commit | commitdiff | tree
2013-04-01 lianahfixed TheoryBool rewriter bug commit | commitdiff | tree
2013-04-01 lianahfixed bug 502; now the core bv solver only gives the... commit | commitdiff | tree
2013-03-31 Liana Hadareanchanged option to run inequality solver by default commit | commitdiff | tree
2013-03-31 Clark BarrettDisabling eager array index splitting for QF_AUFLIA commit | commitdiff | tree
2013-03-30 Andrew Reynoldsdo simple ite rewriting within quantifiers commit | commitdiff | tree
2013-03-29 Morgan Detersmake Boolean term conversion partially non-recursive... commit | commitdiff | tree
2013-03-29 Dejan JovanovićMerge branch 'master' of github.com:CVC4/CVC4 commit | commitdiff | tree
2013-03-29 Dejan Jovanovićremoving cryptominisat since we're not using it commit | commitdiff | tree
2013-03-28 Morgan Detersfix memory corruption in arrays destructor commit | commitdiff | tree
2013-03-28 Morgan Deterssome Java bindings fixes (fixes Debian build problems) commit | commitdiff | tree
2013-03-28 Clark BarrettFixed a warning, made eager-index default to true ... commit | commitdiff | tree
2013-03-28 Clark BarrettFixed bug in arrays commit | commitdiff | tree
2013-03-28 Clark BarrettAdded assertion commit | commitdiff | tree
2013-03-28 Clark BarrettUpdates to model-based array solver commit | commitdiff | tree
2013-03-28 Clark BarrettNew model-based array procedure commit | commitdiff | tree
2013-03-27 lianahreverted the core solver to do static slicing, added... commit | commitdiff | tree
2013-03-27 lianahfixed inequality checkDisequalities inefficiency commit | commitdiff | tree
2013-03-27 lianahMerge branch 'master' into bv-core commit | commitdiff | tree
2013-03-27 lianahfixed some model stuff commit | commitdiff | tree
2013-03-27 lianahfixed model generation bug; commented out attempt... commit | commitdiff | tree
2013-03-27 lianahinequality solver now only splits on disequalities... commit | commitdiff | tree
2013-03-27 lianahadded model generation for bv subtheories and bv-inequa... commit | commitdiff | tree
2013-03-26 Morgan DetersFixes for warnings from clang++, from -std=gnu++0x... commit | commitdiff | tree
2013-03-26 Morgan DetersMake --incremental the default when running interactively commit | commitdiff | tree
2013-03-26 lianahcore theory currently disabled commit | commitdiff | tree
2013-03-26 Dejan JovanovićgetModelValue implementation in bitvectors commit | commitdiff | tree
2013-03-26 Dejan Jovanovićadding commit | commitdiff | tree
2013-03-26 Dejan JovanovićMerge branch 'master' of git@github.com:CVC4/CVC4.git commit | commitdiff | tree
2013-03-26 Dejan Jovanovićmoving bv before arrays commit | commitdiff | tree
2013-03-26 lianahfixed inequality bugs due to improper explanation commit | commitdiff | tree
2013-03-26 lianahcleaned up the bv subtheory interface; added check... commit | commitdiff | tree
2013-03-26 Morgan Detersjava input stream adapters working commit | commitdiff | tree
2013-03-25 lianahgetEqualityStatus now also queries the inequality solver commit | commitdiff | tree
2013-03-25 Morgan DetersFix for SCM detection commit | commitdiff | tree
2013-03-25 Kshitij BansalMerge pull request #7 from kbansal/portfolio commit | commitdiff | tree
2013-03-25 Kshitij Bansalfinish removal of separateOutput commit | commitdiff | tree
2013-03-25 Liana Hadareanadded support for disequalities in the inequality solver commit | commitdiff | tree
2013-03-24 lianahincremental inequality solver implemented commit | commitdiff | tree
2013-03-24 Morgan DetersFix bug in portfolio executor output; fixes nightly... commit | commitdiff | tree
2013-03-23 lianahnon-incremental inequality solver seems to be bug-free... commit | commitdiff | tree
2013-03-23 lianahfixed some explanation problems for the core theory... commit | commitdiff | tree
2013-03-23 Dejan JovanovićMerge remote-tracking branch 'dddejan/c++11' commit | commitdiff | tree
2013-03-23 Dejan Jovanovićchanging string hash function to use the gnu namespace commit | commitdiff | tree
2013-03-22 Morgan DetersSupport for Boolean term conversion in datatypes. commit | commitdiff | tree
2013-03-22 Dejan Jovanovićcompiles with commit | commitdiff | tree
2013-03-22 lianahMerge branch 'master' into bv-core commit | commitdiff | tree
2013-03-22 Dejan Jovanovićanother typo/bugfix for equality constant evaluation commit | commitdiff | tree
2013-03-21 lianahMerge branch 'master' into bv-core commit | commitdiff | tree
2013-03-21 lianahfixed more equality stuff commit | commitdiff | tree
2013-03-21 Morgan DetersBetter error in case of nonlinear assertions while... commit | commitdiff | tree
2013-03-21 Morgan DetersAdd the ability to "mute" commands, needed for SMT... commit | commitdiff | tree
2013-03-21 Dejan Jovanovićfixing markings of internal nodes in equality engine commit | commitdiff | tree
2013-03-21 lianahfixed compilation problem commit | commitdiff | tree
2013-03-21 lianahincorporated dejan's constant evaluation; now getting... commit | commitdiff | tree
2013-03-21 lianahMerge branch 'master' into bv-core commit | commitdiff | tree
2013-03-21 lianahdisabled ineq commit | commitdiff | tree
2013-03-21 Dejan JovanovićMerge branch 'master' of github.com:CVC4/CVC4 commit | commitdiff | tree
2013-03-21 Morgan DetersSome model and printing fixes for defined functions... commit | commitdiff | tree
2013-03-21 Dejan Jovanovićmore equality constant evaluation commit | commitdiff | tree
2013-03-21 Morgan DetersFix for SmtEngine::expandDefinitions()---improper TypeC... commit | commitdiff | tree
2013-03-21 lianahadded regression test for constant eval commit | commitdiff | tree
2013-03-21 lianahMerge branch 'master' into bv-core commit | commitdiff | tree
2013-03-21 Dejan Jovanovićfixing constant evaluation bugs commit | commitdiff | tree
next