projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2016-09-26 Tim KingDeleting the intermediate command singleton. commit | commitdiff | tree
2016-09-26 Tim KingDisambiguating a type issue. Coverity scan reported... commit | commitdiff | tree
2016-09-25 Tim KingAdding virtual destructors to several classes in expr.h . commit | commitdiff | tree
2016-09-25 Tim KingRemoving an unused iterator. commit | commitdiff | tree
2016-09-25 Tim KingFixing a potential use after free coming from a pop_bac... commit | commitdiff | tree
2016-09-25 Tim KingIntegrating a working coverity_scan travis rule back... commit | commitdiff | tree
2016-09-21 ajreynolRemove duplicate code from my last commit commit | commitdiff | tree
2016-09-21 Tim KingFixing an error in the previous travis commit. commit | commitdiff | tree
2016-09-21 Tim KingUpdating the travis file for coverity scan. commit | commitdiff | tree
2016-09-20 ajreynolRefactor, separate theory-specific counterexample-guide... commit | commitdiff | tree
2016-09-20 ajreynolMore refactoring of cbqi. Add a few regressions. Add... commit | commitdiff | tree
2016-09-19 Tim KingMerge pull request #92 from timothy-king/travis-cpp11 commit | commitdiff | tree
2016-09-18 Tim KingAdding a gnu++11 rule to travis. commit | commitdiff | tree
2016-09-18 ajreynolMinor fix for strings commit | commitdiff | tree
2016-09-17 guykatzzIn a ROW guard proof, if the transitivity proof does... commit | commitdiff | tree
2016-09-17 guykatzzMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2016-09-17 ajreynolUse matching heuristics for EPR instantiation. commit | commitdiff | tree
2016-09-16 GuyHandling a corner case where a ROW's guard is a constan... commit | commitdiff | tree
2016-09-16 GuyLet arith_proof print its own terms commit | commitdiff | tree
2016-09-16 ajreynolMore refactoring of cbqi, start developing new interface. commit | commitdiff | tree
2016-09-15 ajreynolFurther refactor cbqi. commit | commitdiff | tree
2016-09-15 ajreynolBegin refactoring of cbqi, remove a few dead options... commit | commitdiff | tree
2016-09-15 ajreynolMake sep pto a trigger kind, track in equality engines... commit | commitdiff | tree
2016-09-15 ajreynolRefactor setIncomplete in quantifiers. commit | commitdiff | tree
2016-09-14 ajreynolSupport for unique variable generation in node manager. commit | commitdiff | tree
2016-09-14 ajreynolLemma cache in theory sep. Minor optimization for sets... commit | commitdiff | tree
2016-09-13 ajreynolMinor changes to sep logic, epr, quantifier splitting. commit | commitdiff | tree
2016-09-12 ajreynolRefactor prenex modes. commit | commitdiff | tree
2016-09-12 ajreynolRemove old implementation of cbqi commit | commitdiff | tree
2016-09-12 ajreynolPrefer non-cardinality constants in term models for... commit | commitdiff | tree
2016-09-12 ajreynolEnsure sep.nil is unique per type at NodeManager level... commit | commitdiff | tree
2016-09-09 ajreynolFix bug in unconstrained simplifier related to sep... commit | commitdiff | tree
2016-09-09 ajreynolSupport for separation logic + EPR. Refactor preprocess... commit | commitdiff | tree
2016-09-08 ajreynolRefactor seplog preprocess. Handle case where sep data... commit | commitdiff | tree
2016-09-03 ajreynolMiniscope top level conjunctions for prenex normal... commit | commitdiff | tree
2016-09-03 ajreynolOption for prenex normal form commit | commitdiff | tree
2016-09-02 Tim KingMerge pull request #91 from timothy-king/no-throw commit | commitdiff | tree
2016-09-01 ajreynolFix boolean term issue in invariants from sygus. Minor... commit | commitdiff | tree
2016-09-01 ajreynolCleanup quantifier elimination in smt engine. commit | commitdiff | tree
2016-09-01 ajreynolUpdates to cbqi. New strategy --cbqi-nested-qe to... commit | commitdiff | tree
2016-09-01 Tim KingRelaxing the throw specifiers for the destructors for... commit | commitdiff | tree
2016-09-01 Tim KingRemoving the forward declaration of QuantInfo from... commit | commitdiff | tree
2016-08-31 Tim KingCleaning up the dead FORIT macros. commit | commitdiff | tree
2016-08-31 Tim KingRemoving the usage of typeof from theory_sets_private. commit | commitdiff | tree
2016-08-31 Tim KingBeautifying theory_model.h. commit | commitdiff | tree
2016-08-31 Tim KingRemoving BOOST_FOREACH from theory/sets/scrutinize.h. commit | commitdiff | tree
2016-08-31 Tim KingRemoving typeof from sets normal form and beautifying... commit | commitdiff | tree
2016-08-31 Tim KingRemoving typeof from command_executor_portfolio.cpp. commit | commitdiff | tree
2016-08-31 Tim KingRemoving typeof from didyoumean.cpp. commit | commitdiff | tree
2016-08-26 ajreynolBasic support for EPR+CBQI. Minor cleanup. commit | commitdiff | tree
2016-08-25 ajreynolMinor cleanup preprocessing, add ppNotifyAssertions. commit | commitdiff | tree
2016-08-25 ajreynolOptions for counterexample guided instantiation. commit | commitdiff | tree
2016-08-20 Clark BarrettFixed two bugs commit | commitdiff | tree
2016-08-19 Clark BarrettAdded fitsSignedLong and fitsUnsignedLong commit | commitdiff | tree
2016-08-16 ajreynolInitial infrastructure for ExtTheory, generalize extend... commit | commitdiff | tree
2016-08-15 ajreynolExpression sharing on demand in LFSC (replace definitio... commit | commitdiff | tree
2016-08-15 ajreynolEnable bounded set membership with --fmf-bound. Map... commit | commitdiff | tree
2016-08-12 ajreynolAdd a few more regressions. commit | commitdiff | tree
2016-08-12 ajreynolMinor fixes to model construction to take singleton... commit | commitdiff | tree
2016-08-12 guykatzzMerge pull request #90 from 4tXJ7f/fewer_preproc_holes commit | commitdiff | tree
2016-08-12 Andres NotzliAdd support for fewer preprocessing holes commit | commitdiff | tree
2016-08-11 ajreynolMinor change to strings, introduce proxy vars only... commit | commitdiff | tree
2016-08-10 ajreynolImprovements to strings: work on propagations for rever... commit | commitdiff | tree
2016-08-09 guykatzzMerge pull request #89 from 4tXJ7f/fix_proof_spaces commit | commitdiff | tree
2016-08-09 ajreynolFixes for sep star rewrite. commit | commitdiff | tree
2016-08-09 Andres NotzliFix missing/redundant spaces in proofs commit | commitdiff | tree
2016-08-06 guykatzzMerge pull request #88 from 4tXJ7f/fix_comments commit | commitdiff | tree
2016-08-05 Andres NotzliMinor: add/fix comments, remove redundant includes commit | commitdiff | tree
2016-08-03 GuyFixed an issue where arrays proofs would sometimes... commit | commitdiff | tree
2016-08-03 barrettcwMerge pull request #87 from 4tXJ7f/fix_oob_access commit | commitdiff | tree
2016-07-30 ajreynolPrioritize inferences when processing normal forms... commit | commitdiff | tree
2016-07-28 GuyThe "aggressive" optimizer for lemma L now returns... commit | commitdiff | tree
2016-07-28 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2016-07-28 GuyBug fix involving negated lemmas commit | commitdiff | tree
2016-07-28 ajreynolFix bug 749. commit | commitdiff | tree
2016-07-28 GuyAdd the negative conjunction case commit | commitdiff | tree
2016-07-28 Andres NotzliFix out-of-bounds access in ExprManager commit | commitdiff | tree
2016-07-28 GuyProper instrumentation of the preprocessing phase commit | commitdiff | tree
2016-07-28 Guyproper handling of ITEs commit | commitdiff | tree
2016-07-27 GuyProper handling of IFF lemmas in the unsat core. commit | commitdiff | tree
2016-07-27 GuyAdded an option for a more aggressive weakest implicant... commit | commitdiff | tree
2016-07-27 GuyIf we can't find a weaker implicant, fail gracefully... commit | commitdiff | tree
2016-07-27 guykatzzMerge pull request #86 from 4tXJ7f/fix_warnings commit | commitdiff | tree
2016-07-27 Andres NotzliFix warnings in src/proof commit | commitdiff | tree
2016-07-26 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2016-07-26 GuyBug fix: commit | commitdiff | tree
2016-07-26 ajreynolAdd option to minimize sygus solutions based on using... commit | commitdiff | tree
2016-07-26 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2016-07-26 GuyLetification of BV constants commit | commitdiff | tree
2016-07-26 ajreynolMinor improvements to strings related to constant split... commit | commitdiff | tree
2016-07-26 GuyAdded functionality to retrieve a lemma's "weakest... commit | commitdiff | tree
2016-07-26 GuyBug fix commit | commitdiff | tree
2016-07-26 GuyPropagate the usage of proof let maps into constant... commit | commitdiff | tree
2016-07-25 GuyBug fix commit | commitdiff | tree
2016-07-25 GuyMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2016-07-25 Guycleanup commit | commitdiff | tree
2016-07-25 GuyUse letification for the aliasing declarations as well... commit | commitdiff | tree
2016-07-25 GuyProper handling for lemmas that are conjuncts: commit | commitdiff | tree
2016-07-22 ajreynolMinor, error handling for polymorphism + sep logic. commit | commitdiff | tree
2016-07-21 ajreynolFixes for strings, explanations for constant split... commit | commitdiff | tree
next