summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2016-03-04refactored the codePaulMeng
2016-03-01small fixes for eq rep namesPaulMeng
2016-03-01small fix for namingPaulMeng
2016-03-01fixed product rulesPaulMeng
2016-02-29adapted the solver to accept sets of built-in types (int, string, real)PaulMeng
2016-02-29Added more benchmarksPaulMeng
2016-02-28implemented a basic solving procedure for finite relations (only forPaulMeng
2016-02-17added rules for join and transpose operatorsPaulMeng
2016-02-15Merge remote-tracking branch 'origin/master'PaulMeng
2016-02-15extended smt parser for the finite relationsPaulMeng
2016-02-15Minor change to last commitajreynol
2016-02-15Eliminate most of the internal representation infrastructure for tuples and r...ajreynol
2016-02-11More aggressive conditional rewriting for quantified formulas. Bug fix set in...ajreynol
2016-02-10Fix model postprocessor for tuples, add regression.ajreynol
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-09- extend cvc4 frontend parser to accept relational operators (product,PaulMeng
2016-02-09Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to...ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-02-05Changing the way the equality engine explains disequalities.guykatzz
2016-02-05Add two optimizations for datatypes, currently disabled. Bug fix rewriter for...ajreynol
2016-02-04Fixed two more memory leaks in array_info.cppClark Barrett
2016-02-03Added --omit-dont-cares option which doesn't print model values forClark Barrett
2016-02-02Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ...Tim King
2016-02-01Removing the CVC4_PUBLIC attribute from the forward declaration of Record in ...Tim King
2016-02-01Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a simpler build p...Tim King
2016-02-01Generalizing lib/strtok_r.c so that it can always be compiled.Tim King
2016-02-01Generalizing the implementation of lib/clock_gettime.c so that it can always ...Tim King
2016-02-01Fixing a potentially malformed template expansion when Dump() is disabled.Tim King
2016-02-01Fixing a memory leak in bv_subtheory_algebraic.cpp. Also formatting the file.Tim King
2016-02-01Adding an virtual destructor to OstreamUpdate.Tim King
2016-02-01Making the ManagedOstream::defaultSource() a const function.Tim King
2016-02-01Adding a destructor to ProofOutputChannel.Tim King
2016-02-01Fixing white spaces in sat_proof.h.Tim King
2016-02-01Making the references to std more explicit in didyoumean.cpp.Tim King
2016-02-01Fixing a memory leak in array info.Tim King
2016-02-01Deleting the dead code in proof/sat_proof.cpp.Tim King
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-28Adding listeners to Options.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ...ajreynol
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
2016-01-15Type enumerators take optional argument indicating fixed cardinalities of uni...ajreynol
2016-01-15Ensure model construction for parametric sorts involving uninterpreted sorts ...ajreynol
2016-01-13Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for d...ajreynol
2016-01-08Adding a new Listener utility class. Changing the ResourceManager to use List...Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-08Disabling the RESTART command.Tim King
2016-01-06fix windows buildsKshitij Bansal
2016-01-06Fixing a SWIG ordering issue between bitvector and integer.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback