projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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-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-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
2013-03-21 lianahadded more tests commit | commitdiff | tree
2013-03-21 lianahgeneralized bv inequality reasoning to handle both... commit | commitdiff | tree
2013-03-21 Morgan DetersBetter reporting of detached git state in --version... commit | commitdiff | tree
2013-03-21 Morgan DetersFix to bug 497: make justification heuristic's ITE... commit | commitdiff | tree
2013-03-21 Morgan DetersRemove unintentionally-committed-to-master README from... commit | commitdiff | tree
2013-03-20 Morgan DetersInteractive mode support for multiline input commit | commitdiff | tree
2013-03-20 Morgan DetersProperly |quote| symbols in SMT-LIBv2 output. commit | commitdiff | tree
2013-03-20 Morgan DetersSome statistics for narrowing down incrementality issue... commit | commitdiff | tree
2013-03-20 Liana Hadareanone more ineq regression commit | commitdiff | tree
2013-03-20 Liana Hadareanfixed reversed concat in core theory commit | commitdiff | tree
2013-03-20 Liana Hadareanmerged dejan's stuff commit | commitdiff | tree
2013-03-20 Liana Hadareanmerged master with dejan's constant evaluating equality... commit | commitdiff | tree
2013-03-20 Liana Hadareaninequality reasoning works on small examples added... commit | commitdiff | tree
2013-03-20 Dejan JovanovićAdding evaluation of constant terms to the equality... commit | commitdiff | tree
2013-03-19 Morgan DetersMinor cleanup of sources commit | commitdiff | tree
2013-03-19 Morgan DetersFixes for miplib-trick application (and a new testcase) commit | commitdiff | tree
2013-03-19 Morgan DetersRemove PropositionalQuery class and all CUDD-related... commit | commitdiff | tree
2013-03-19 Morgan DetersMinor fixes to build system commit | commitdiff | tree
2013-03-19 Liana Hadareanadded the cpp file for the inequality graph commit | commitdiff | tree
2013-03-19 Liana Hadareanimplementing more inequality graph stuff; work in progr... commit | commitdiff | tree
2013-03-18 lianahmore work on inequality reasoning for bv commit | commitdiff | tree
2013-03-16 lianahstarted work on the inequality bv subtheory commit | commitdiff | tree
2013-03-15 Morgan DetersBoolean terms rewriting for quantified variables of... commit | commitdiff | tree
2013-03-15 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-03-15 Morgan Detersfix up build system for swig (d242c30 introduced a... commit | commitdiff | tree
2013-03-15 Andrew Reynoldschanged default option for quantifier instantiation commit | commitdiff | tree
2013-03-14 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-03-14 Morgan DetersFix warning (line annotation) commit | commitdiff | tree
2013-03-14 Morgan Detersfix to build system: #include the proper file when... commit | commitdiff | tree
2013-03-14 Clark BarrettAdded a rewrite for iff: commit | commitdiff | tree
2013-03-13 lianahpost failed attempts at getting the incremental solver... commit | commitdiff | tree
2013-03-11 Andrew Reynoldsite removal option for quantifiers --ite-remove-quant... commit | commitdiff | tree
2013-03-09 Morgan DetersDisallow overflow in bitvector literals (parser only) commit | commitdiff | tree
2013-03-06 lianahmore slicer changes for incremental commit | commitdiff | tree
2013-03-06 Clark BarrettBest heuristics for handling decision requests from... commit | commitdiff | tree
2013-03-06 Andrew Reynoldsfixed two bugs for the new E-matching implementation... commit | commitdiff | tree
2013-03-05 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-03-05 Morgan DetersBugfix for SmtEngine: proper unsubscribing for NodeMana... commit | commitdiff | tree
2013-03-01 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-02-26 Morgan DetersBug fix for rep-set. commit | commitdiff | tree
2013-02-26 Morgan DetersFix for quantifiers containing Boolean terms. commit | commitdiff | tree
2013-02-26 lianahMerge branch '1.0.x' commit | commitdiff | tree
2013-02-26 lianahMerge branch '1.0.x' of https://github.com/CVC4/CVC4... commit | commitdiff | tree
2013-02-26 lianahfix for bv crash in incremental mode; this is a tempora... commit | commitdiff | tree
2013-02-24 Andrew Reynoldsadded option --model-u-dt-enum for outputting uninterpr... commit | commitdiff | tree
2013-02-20 Morgan DetersSingle -q quiets messages/warnings. Double -qq silence... commit | commitdiff | tree
2013-02-20 Morgan DetersSome exception specification fixes in SmtEngine/Command... commit | commitdiff | tree
2013-02-18 Morgan DetersFix for gitinfo (resolves bug 399). commit | commitdiff | tree
2013-02-17 Kshitij BansalMerge branch '1.0.x' commit | commitdiff | tree
2013-02-17 Kshitij Bansalgitinfo modifications fix commit | commitdiff | tree
2013-02-17 Kshitij BansalMerge pull request #6 from kbansal/decNewoptions commit | commitdiff | tree
2013-02-17 Kshitij Bansaldecision: jh: more refactoring (.h->.cpp, xor/iff) commit | commitdiff | tree
2013-02-17 Kshitij Bansaldecision/ : jh: refactor embedded ITE, other minor commit | commitdiff | tree
2013-02-17 Kshitij Bansaldecision/: justification: refactor ITE out commit | commitdiff | tree
2013-02-17 Kshitij Bansalrefactoring justification_heuristic code commit | commitdiff | tree
2013-02-16 Kshitij Bansalrm decision jh GiveUp related code commit | commitdiff | tree
2013-02-16 Morgan DetersSome cleanup and copyright updating commit | commitdiff | tree
2013-02-16 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-02-16 Morgan DetersFix version identification for new git repository. commit | commitdiff | tree
2013-02-16 Morgan DetersFix typo in error message commit | commitdiff | tree
2013-02-15 Kshitij BansalMerge branch '1.0.x' commit | commitdiff | tree
2013-02-15 Kshitij Bansalprvs commit: lower warning to notice commit | commitdiff | tree
2013-02-15 Kshitij BansalMerge branch '1.0.x' commit | commitdiff | tree
2013-02-15 Kshitij Bansalmake incremental+portfolio experimental commit | commitdiff | tree
2013-02-15 Kshitij BansalMerge pull request #5 from kbansal/1.0.x commit | commitdiff | tree
2013-02-15 Kshitij Bansalmake incremental+portfolio experimental commit | commitdiff | tree
2013-02-15 Morgan DetersMerge branch '1.0.x' commit | commitdiff | tree
2013-02-15 Morgan DetersFix builds/ links to survive configuring twice with... commit | commitdiff | tree
2013-02-15 Morgan DetersFix ECHO command in CVC language parser to not output... commit | commitdiff | tree
2013-02-15 Tim KingMerge branch '1.0.x' commit | commitdiff | tree
2013-02-15 Tianyi Liangrepairs a bug in rewriterule engine: constructor cannot... commit | commitdiff | tree
2013-02-14 Dejan JovanovićMerge pull request #4 from tiliang/master commit | commitdiff | tree
2013-02-14 Tim KingRemoving BVDebug and replacing with Debug. commit | commitdiff | tree
2013-02-14 Tianyi Liangrepairs a bug in rewriterule engine: constructor cannot... commit | commitdiff | tree
2013-02-14 lianahstarted working on incremental slicer - not compiling commit | commitdiff | tree
2013-02-13 Morgan DetersFix a preprocessing performance issue. commit | commitdiff | tree
2013-02-11 lianahundid the caching that actually hurt performance commit | commitdiff | tree
2013-02-08 Morgan DetersFix user-values in SMT-LIB v1.2 commit | commitdiff | tree
next