cvc5.git
2016-03-24 Tim KingFixing a garbage collection issue in simplifyWithCare...
2016-03-24 Tim KingDeleting allocated NodeVecs in ITESimplifier.
2016-03-24 Tim KingFreeing CegConjecture::d_ceg_si. Also making d_ceg_si...
2016-03-24 Tim KingFixing a memory leak in CDInstMatchTrie::d_data.
2016-03-24 Tim KingFix for a memory leak in InstStrategyCegqi.
2016-03-24 Tim KingFixing a memory leak in QuantInfo::d_var_mg.
2016-03-23 guykatzzMerge pull request #82 from CVC4/master_for_merge
2016-03-23 Guysquash-merge from proof branch
2016-03-23 Tim KingFixing memory leaks in Trigger and TriggerTrie.
2016-03-23 Clark BarrettFixed help for tear-down-incremental option
2016-03-23 Tim KingFixing two garbage collection issues in Region and...
2016-03-23 Tim KingDeleting the CDInstMatchTries in QuantifiersEngine...
2016-03-23 Tim KingGarbage collecting the EqcInfo s in TheoryDatatypes...
2016-03-23 Tim KingGarbage collecting the MinisatEmptyNotify for the Eager...
2016-03-22 ajreynolBug fix for define functions + incremental. Minor work...
2016-03-22 Tim KingDeleting the contents of d_modelGlobalsCommands before...
2016-03-22 Tim KingNew version of the recursive options parsing strategy.
2016-03-18 ajreynolLimit duplicate propagating instances to avoid exponent...
2016-03-16 ajreynolChange internal representative selection for finite...
2016-03-12 ajreynolAdd options related to interleaving quantifiers and...
2016-03-10 ajreynolFaster conditional rewriting for and/or beneath quantif...
2016-03-08 ajreynolExtend synthesis solver to handle single invocation...
2016-03-07 ajreynolMinor change to F-Length inference in strings. No inter...
2016-03-03 ajreynolAdd missing code to track dependencies recursively...
2016-03-02 ajreynolWork towards complete instantiation for datatypes.
2016-03-01 ajreynolShorter explanations for strings based on tracking...
2016-02-29 ajreynolMinor options to datatypes.
2016-02-26 ajreynolRefactoring of inferences in strings. Add several options.
2016-02-25 ajreynolMinor improvement to partial qe. Add options for repres...
2016-02-24 ajreynolAdd entailment checks between length terms to reduce...
2016-02-24 Tim KingAdding the missing clause_id.h file.
2016-02-24 Tim KingUnifying the definitions of ClauseId to a single source...
2016-02-23 ajreynolFix term database for non-equal, congruent terms in...
2016-02-19 ajreynolFixes and improvements for datatypes properties and...
2016-02-19 ajreynolImplement dynamic splitting for quantified formulas...
2016-02-18 ajreynolCorrect subtyping for arrays, disable subtyping for...
2016-02-18 Kshitij Bansalfix for windows builds
2016-02-17 ajreynolRefactor quantifiers attributes. Make quantifier elimin...
2016-02-16 ajreynolPublic interface for quantifier elimination. Minor...
2016-02-16 ajreynolMore simplification to internal implementation of tuple...
2016-02-15 ajreynolMinor change to last commit
2016-02-15 ajreynolEliminate most of the internal representation infrastru...
2016-02-11 ajreynolMore aggressive conditional rewriting for quantified...
2016-02-10 ajreynolFix model postprocessor for tuples, add regression.
2016-02-09 ajreynolFix regression, minor change to output.
2016-02-09 ajreynolEager introduction of eqc, lemma cache for ground fmf...
2016-02-08 ajreynolUpdates related to finite model finding and (co)datatyp...
2016-02-06 guykatzzChanging the way the equality engine explains disequali...
2016-02-05 ajreynolAdd two optimizations for datatypes, currently disabled...
2016-02-04 Clark BarrettFixed two more memory leaks in array_info.cpp
2016-02-03 Clark BarrettAdded --omit-dont-cares option which doesn't print...
2016-02-02 Tim KingMoving dump.*, command.*, model.*, and ite_removal...
2016-02-01 Tim KingRemoving the CVC4_PUBLIC attribute from the forward...
2016-02-01 Tim KingRemoving the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard...
2016-02-01 Tim KingGeneralizing lib/strtok_r.c so that it can always be...
2016-02-01 Tim KingGeneralizing the implementation of lib/clock_gettime...
2016-02-01 Tim KingFixing a potentially malformed template expansion when...
2016-02-01 Tim KingFixing a memory leak in bv_subtheory_algebraic.cpp...
2016-02-01 Tim KingAdding an virtual destructor to OstreamUpdate.
2016-02-01 Tim KingMaking the ManagedOstream::defaultSource() a const...
2016-02-01 Tim KingAdding a destructor to ProofOutputChannel.
2016-02-01 Tim KingFixing white spaces in sat_proof.h.
2016-02-01 Tim KingMaking the references to std more explicit in didyoumea...
2016-02-01 Tim KingFixing a memory leak in array info.
2016-02-01 Tim KingDeleting the dead code in proof/sat_proof.cpp.
2016-02-01 ajreynolSimplify fmc model construction, add regression. Improv...
2016-01-28 Tim KingAdding listeners to Options.
2016-01-27 Liana HadareanMerged bit-vector and uf proof branch.
2016-01-20 ajreynolFix bug in fmc mbqi where modelscomputed for mbqi could...
2016-01-19 ajreynolBug fixes for model construction with codatatypes,...
2016-01-18 ajreynolBug fix rewriter for fun defs.
2016-01-15 ajreynolType enumerators take optional argument indicating...
2016-01-14 ajreynolEnsure model construction for parametric sorts involvin...
2016-01-13 ajreynolLemma cache datatypes. Do not send true lemma in quanti...
2016-01-09 Tim KingAdding a new Listener utility class. Changing the Resou...
2016-01-09 Tim KingRemoving StatisticsRegistry's static functions current...
2016-01-08 Tim KingDisabling the RESTART command.
2016-01-06 Kshitij Bansalfix windows builds
2016-01-06 Tim KingFixing a SWIG ordering issue between bitvector and...
2016-01-06 Tim KingImproving the documentation of the CVC command CONTINUE.
2016-01-06 Tim KingRemoving dead code. StackingMap only appeared in unit...
2016-01-06 Tim KingMoving sexpr.{cpp,h,i} from expr/ back into util/.
2016-01-06 Tim KingAdd SmtGlobals Class
2016-01-05 Tim KingAdding a new class LastExceptionBuffer for the purpose...
2016-01-01 Clark BarrettAdded propagation rule for array ext lemmas to aid...
2015-12-31 Clark BarrettModified tear-down-incremental option to take an intege...
2015-12-30 Tim KingShuffling around public vs. private headers
2015-12-29 Tim KingAdding a missing header include for cvc4_assert.h in...
2015-12-27 Clark BarrettMerged my changes from experimental branch (new array...
2015-12-24 Tim KingChanging the attribute on the forward declaration of...
2015-12-24 Tim KingAdding a missing return on the new ArrayStoreAll::opera...
2015-12-24 Tim KingMiscellaneous fixes
2015-12-23 Clark BarrettEnabled array propagation during lemma propagation...
2015-12-23 Clark BarrettAdded extract.cpp example
2015-12-22 ajreynolBug fix uf-ss-totality.
2015-12-22 ajreynolAlways split on constructor types for datatypes involvi...
2015-12-22 ajreynolBug fix for cbqi, do not use model values for terms...
2015-12-19 Tim KingModifying emptyset.h and sexpr. Adding SetLanguage.
2015-12-17 ajreynolMinor
2015-12-16 Tim KingRemoving the Record iterator from the swig interface...
next