cvc5.git
2012-04-04 Dejan Jovanovićsome settings in bvminisat
2012-04-04 Liana Hadareanchanged BVMinisat options to use cc_min=0 in propagate...
2012-04-04 Liana Hadareanchanged ccmin_mode in BvMinisat
2012-04-04 Liana Hadarean * added propagation as lemmas to TheoryBV:
2012-04-03 Tim KingFix for make dist.
2012-04-02 Tim KingFix for broken unit tests from the previous commit.
2012-04-02 Tim King- Merged in the branch cdlist-cleanup.
2012-04-02 Kshitij Bansalfix for cvc4_logic dump
2012-04-02 Tim KingRemoving large and unused regress2 benchmarks to decrea...
2012-03-30 Dejan Jovanovićsome more build system fixes
2012-03-30 Dejan Jovanovićfixing some build systme warnings
2012-03-29 Tim KingFix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is...
2012-03-29 Tim KingFixes a linking problem with the new SatSolverConstruct...
2012-03-29 Dejan Jovanovićbringing cryptominisat into the main branch
2012-03-28 Dejan Jovanovićenabling the --disable-arithmetic-propagation option...
2012-03-28 Morgan Detersfix swig-ignored interface name; hopefully fixes Debian...
2012-03-28 Tim KingUpdate to the ArithRewriter to remove REWRITE_AGAIN_FUL...
2012-03-28 Dejan JovanovićSome renaming and refactoring in SAT
2012-03-28 Dejan Jovanovićgetting rid of a rewrite in uf sharing, speeds things...
2012-03-28 Liana Hadareanfixed faulty bv rewrite rule
2012-03-28 Dejan Jovanovićadding an extra cache check in the rewriter, speeds...
2012-03-26 Dejan JovanovićGlobal registry of SAT solvers, where they are register...
2012-03-26 Dejan JovanovićMore cleaning up.
2012-03-26 Dejan Jovanovićmore datail from the build failure
2012-03-26 Dejan Jovanovićwith a small fix
2012-03-26 Dejan Jovanovićforgot to commit this one, fixing build errors
2012-03-25 Dejan Jovanovićmoving minisat implementation into their respective...
2012-03-25 Dejan Jovanovićsat_module.h,cpp -> sat_solver.h,cpp (as intended)
2012-03-25 Dejan Jovanovićsat.h,cpp -> theory_proxy.h,cpp (this is what it defines)
2012-03-24 Dejan Jovanovića cute script to make a video of development from the...
2012-03-23 Tim KingRemoved the variableRemovalEnabled option and d_removed...
2012-03-22 Dejan Jovanović* improving arithmetic getEqualityStatus
2012-03-22 Liana HadareanMerged updated version of the bitvector theory:
2012-03-22 Dejan Jovanovićsome improvements to the sharing mechanism/interface
2012-03-21 Morgan DetersDisable nonclausal simplification for QF_SAT benchmarks...
2012-03-09 Morgan DetersSome work on the dump infrastructure to support portfol...
2012-03-09 Morgan Detersfix a "lost command" bug and associated memory leak...
2012-03-09 Morgan DetersStrengthen minisat assertion regarding t-propagations...
2012-03-09 Morgan Detersminor fixes: to "make dist" in build directories with...
2012-03-08 Morgan Detersfix "make dist"
2012-03-08 Dejan JovanovićFixin the bug Clark found. In final check, enqueued...
2012-03-08 Dejan JovanovićRemoving QUICK_CHECK, and other unused ones, from the...
2012-03-07 François Bobotcdqueue : fix size(). Thank you Clark for spotting...
2012-03-07 Morgan Detersfix some Java compatibility-layer interface problems...
2012-03-06 Dejan Jovanovićupdating the equality engine to be able to give explana...
2012-03-03 Morgan DetersChanging the dependency checking; GMP is required ...
2012-03-02 Kshitij BansalRemove some commented out code from sat.h
2012-03-02 Tim KingThis commit merges in the changes from branches/arithme...
2012-03-02 Dejan JovanovićCDMap -> CDHashMap
2012-03-02 Morgan Deterscommitting the TNode/Node fix that was in the kind...
2012-03-02 Tim KingRenamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue...
2012-03-01 Morgan DetersPartial merge from kind-backend branch, including Minis...
2012-03-01 François Bobotcdqueue2 : cdlist that can be used like queue and can...
2012-03-01 Tim KingFixed a copy paste error where a lower bound was looked...
2012-02-29 Liana HadareanThis should fix the debian build fails:
2012-02-29 Dejan Jovanovićfixing bug310
2012-02-29 Morgan Detersconsistency in how the Dump output stream is used
2012-02-28 Tim KingThis commit merges in branches/arithmetic/internalbb...
2012-02-28 Tim KingImproves the arithmetic difference manager to delay...
2012-02-28 Morgan Detersfix theory "kinds" file documentation for allowed arity...
2012-02-28 Tim KingAdds the CDQueue class. This is a wrapper for combinin...
2012-02-28 Morgan DetersReplace the sequence of hardcoded addTheory() calls...
2012-02-27 Morgan Detersfixes to new-theory script; resolves bug #307
2012-02-25 Dejan JovanovićppAsert -> ppAssert
2012-02-25 Liana HadareanRefactored CnfStream to work with the bv theory Bitblaster:
2012-02-24 Dejan JovanovićTheory interface changes:
2012-02-23 Morgan DetersAdded ability to set a "cvc4-specific logic" in standar...
2012-02-23 Morgan Deterspcvc4 only built if --with-portfolio given to the confi...
2012-02-22 Tim KingFix for bug 305.
2012-02-22 Morgan Detersfixes to configure and boost.m4 to make certain boost...
2012-02-22 Morgan Detersanother static library unavailability issue
2012-02-22 Morgan Detersmake sure to clear out READLINE_LIBS if readline causes...
2012-02-22 Morgan DetersAdded OutputChannel::propagateAsDecision() functionalit...
2012-02-22 Morgan DetersFixes to documentation / fixes for MacOS
2012-02-22 Kshitij Bansalminor change to order fn in sat solver's ElimLt
2012-02-21 Morgan Detersadd a "--with-portfolio" configure option that makes...
2012-02-21 Morgan Detersfix src/util/hash.h to specialize GNU's hash template...
2012-02-21 Morgan Deterslanguage bindings fixes for yesterday's portfolio merge
2012-02-21 Dejan JovanovićFix for bug303. The problem was with function applicati...
2012-02-21 Morgan Detersdon't require libboost_thread (its presence is detected...
2012-02-20 Morgan Detersfix sharing issue for portfolio (full lit-to-node map...
2012-02-20 Morgan Detersfix "make dist"
2012-02-20 Morgan Deterszlib not required; remove configure's dependency on it
2012-02-20 Morgan Detersportfolio merge
2012-02-20 Morgan Detersreadline links in -ltermcap -ltinfo too (fixes breakage...
2012-02-20 Morgan DetersAdded Theory::postsolve() infrastructure as Clark reque...
2012-02-20 Morgan DetersBy default, ONLY enable symmetry breaker ONLY for QF_UF...
2012-02-16 Morgan Detersclarify wording in README, thanks for finding this...
2012-02-16 Tim KingLast commit accidentally lacked r2778 and r2779 from...
2012-02-15 Tim KingThis commit merges into trunk the branch branches/arith...
2012-02-13 François Bobotprecision in theoryskel
2012-02-13 Morgan Detersproper handling of improper get-value
2012-02-12 Morgan Deterscopyright year updated to 2012
2012-02-12 Morgan Detersseparate new-theory components into a "theoryskel"...
2012-02-11 Morgan Detersensure using bash for new-theory script
2012-02-10 Morgan Detersattempt at a fix for the local regression failure ...
2012-02-10 Morgan Detersscript to ease creating a new theory from scratch ...
2012-02-10 Morgan Deterscorrect comment typo found during today's architectural...
2012-02-09 Dejan Jovanovićfixing antoher small bug in backtracking
2012-02-08 Dejan Jovanovićfixing a bug in uf_engine application lookup backtracking
next