cvc5.git
2012-05-15 Liana Hadareanrenamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaste...
2012-05-15 Morgan Detersremoving all extended commands (as inspired by the...
2012-05-15 Morgan DetersFix QF_AUFLIA (resolves bug #331).
2012-05-15 Dejan Jovanovićfixing warnings, grr
2012-05-15 Liana Hadareanseveral bug fixes: in TheoryBV::NotifyClass missing...
2012-05-14 Dejan Jovanovićfixes for shared term registration. previously the...
2012-05-14 Clark BarrettFixed assertion failures in array theory
2012-05-14 Morgan Detersin debug builds, -d can be used for trace tags that...
2012-05-14 Dejan Jovanovićfixing up preregistration again
2012-05-13 Dejan Jovanovićfixing build warnings
2012-05-11 Morgan Detersfix regex in Debug_tags and Trace_tags generation for...
2012-05-11 Morgan Detersfix typo in sed line
2012-05-11 Morgan Detersoutput a warning message when a function type (or datat...
2012-05-11 Clark BarrettDisabled arith-rewrite-equalities by default unless...
2012-05-11 Clark BarrettAdded some ITE rewrites,
2012-05-11 Tim KingPartially fixes something-like-a-problem with TheoryAri...
2012-05-10 Tim KingRemoving now unneeded (as of r3425) typenames from...
2012-05-09 Morgan Detersfix an issue which breaks language bindings (so this...
2012-05-09 Morgan Deters--disable-tracing at configure time now disables Trace...
2012-05-09 Dejan Jovanović* simplifying equality engine interface
2012-05-09 Kshitij Bansalrm something for a future merge that sneaked in
2012-05-09 Kshitij BansalMerge from decision branch (ITE support)
2012-05-09 Dejan JovanovićFixing the debug tags generation and related methods...
2012-05-08 Liana HadareanMerging in bvprop branch, with proper bit-vector propag...
2012-05-07 Tim KingFixing a bug with TheoryArith::ppAssert() and shared...
2012-05-07 Tim KingFixes a sign bug in the DioSolver.
2012-05-04 Clark BarrettGuard for expensive Debug trace
2012-05-04 François Bobotoptions: fail if the debug or trace tag specified doesn...
2012-05-04 François Bobotfix: getNumTraceTags, getNumDebugTags
2012-05-04 Tim King- This fixes a problem where simplex produced the same...
2012-05-03 Dejan JovanovićSome cleanup starting off from trying to understand...
2012-05-02 Clark BarrettChanging d_sharedTermsExist to logicInfo.isSharingEnabled()
2012-04-30 Clark BarrettAdded map from skolem variables to new ite formulas...
2012-04-28 Morgan DetersNew LogicInfo functionality.
2012-04-28 Morgan Detersrequire boost library (but not the threading support...
2012-04-28 Morgan Detersundo, again
2012-04-28 Morgan Detersadding THEORY_QUANTIFIERS and THEORY_REWRITERULES to...
2012-04-27 Morgan Detersundo previous commit (as it will break a number of...
2012-04-27 Morgan Detersadding THEORY_QUANTIFIERS and THEORY_REWRITERULES to...
2012-04-27 Morgan Detersfix parser logic-handling oversights: QF_UFBV should...
2012-04-27 Morgan Detersbreak dependence on zlib-dev for now
2012-04-27 Clark BarrettFixed warning in decision_engine.h, minor tweak to...
2012-04-27 Tim KingThis merges in the branch cvc4/branches/arithmetic...
2012-04-25 Kshitij Bansalportfolio driver: respect parseOnly option
2012-04-25 Kshitij Bansalfix for de+lemmas
2012-04-24 Tim KingThis commit merges in the branch branches/arithmetic...
2012-04-23 Kshitij BansalMerge from decision branch -- partially working justifi...
2012-04-20 Clark BarrettUpdates to array theory - much more lazy about introduc...
2012-04-19 Tim KingIn the constructor of DecisionEngine, there were 2...
2012-04-18 Kshitij Bansaladd the missing BINARY variable in some test/regress...
2012-04-18 Kshitij Bansalcout -> warning. Happening in portfolio
2012-04-18 Dejan Jovanovićdisabling the problematic pragma in node_manager.h...
2012-04-17 Dejan JovanovićFix for thos annoying "array index" warnings in product...
2012-04-17 Kshitij BansalA dummy decision engine. Expected performance impact...
2012-04-17 Tim KingMerges branches/arithmetic/atom-database r2979 through...
2012-04-14 Clark BarrettFixed bug in sharing with arrays of different types
2012-04-13 Morgan DetersFix SExpr name qualification for swig, and #include...
2012-04-12 Morgan Deterssvn ignore Makefile.in for aufbv regression directory
2012-04-12 Tim KingAdds an operator<< to SExpr::SexprTypes. This fixes...
2012-04-11 Morgan Detersmerge from arrays-clark branch
2012-04-06 François Bobot* Smt2 printer for datatypes
2012-04-06 Morgan Deters* Fix ITEs and functions in CVC language printer.
2012-04-06 Morgan Detersfix distributed builds (and therefore the Debian nightl...
2012-04-06 Dejan Jovanovićprocessing assertions in bit-vectors even when in fullc...
2012-04-05 Morgan DetersSupport to test the "dumper" mechanism in regressions...
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...
next