cvc5.git
2012-06-09 Morgan DetersCleanup and comments for the dag-ifier. Also some...
2012-06-09 Morgan DetersDagification of output expressions.
2012-06-08 Morgan DetersThe option --arith-presolve-lemmas had previously been...
2012-06-08 Morgan DetersExtend Printer infrastructure also to the "Result"...
2012-06-08 Morgan Detersminor fixes, for Mac OS
2012-06-08 Dejan Jovanovićvery small fast example for the bv fail
2012-06-08 Morgan DetersFix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri...
2012-06-08 Kshitij Bansalhandle BitVectorSignExtend in pickler
2012-06-08 Kshitij Bansalthreadlocal
2012-06-08 Kshitij BansalMerge from decision branch (till r3663)
2012-06-08 Dejan Jovanovićsmall fuzz examples where bv fails
2012-06-07 Dejan Jovanovićfixing the wrong results. arrays equality adaptor had...
2012-06-07 Morgan DetersLogicInfo locking implemented, and some initialization...
2012-06-07 Clark BarrettFixed performance issue with ite_simplifier on some...
2012-06-07 Morgan DetersAdding EchoCommand and associated printer and parser...
2012-06-07 Dejan Jovanovićcleaning up the expample for the future
2012-06-07 Clark BarrettAdded small test case for diseq propagation
2012-06-07 Dejan Jovanovićfixing some bugs in propagation of disequalities
2012-06-06 Clark BarrettDon't ever call nonclausalSimplify if simplificationMod...
2012-06-06 Clark BarrettFixed assertion failures
2012-06-06 Morgan Detersremoving std::cout from trunk
2012-06-06 Morgan Detersalso remove now-incorrect comment from makefile
2012-06-06 Clark BarrettFixed broken test case, removed one that is a mistake
2012-06-06 Morgan Detersunconstrained regressions are now run with "make check...
2012-06-06 Morgan DetersFixing numerous issues with tests and "make dist":
2012-06-06 Dejan Jovanovićdisabling a super-expensive assertions to speed up...
2012-06-06 Dejan JovanovićChanges to the combination mechanism, lots of details...
2012-06-06 Clark BarrettFixed problem causing crash at destruction time
2012-06-05 Clark BarrettMore clean-up
2012-06-05 Clark BarrettFixed a performance issue with unconstrained simplifier
2012-06-05 Clark BarrettAdding missing files...
2012-06-04 Clark BarrettAdded preprocessing pass that propagates unconstrained...
2012-06-01 Morgan Detersadd a global user-context push/pop in smt engine, just...
2012-05-31 Clark BarrettFixed bug in bv: one more case where non-shared equalit...
2012-05-31 Morgan Deterssvn:ignore a parallel-tests driver file that automake...
2012-05-31 Morgan Deterspass JAVA_CPPFLAGS properly
2012-05-30 Clark BarrettAdded BitwiseEq bitvector rewrite
2012-05-30 Clark BarrettFixed problem with array queue growing too large
2012-05-30 Morgan Detersremove unused/broken check build target
2012-05-29 Morgan Detersremoving now-unused TheoryEngine::setLogic() interface...
2012-05-29 Clark BarrettEnabled SolveEq bv rewrite
2012-05-28 Clark BarrettAdded some BV rewrites, fixed bugs in array theory...
2012-05-27 Dejan Jovanovićsome reordering to keep invariants
2012-05-27 Dejan JovanovićCommitting the work on equality engine, I need to see...
2012-05-27 Clark BarrettAnother expensive function call in a Debug trace
2012-05-27 Clark BarrettAnother expensive function call in a Debug line
2012-05-25 Kshitij Bansalinit bug fix
2012-05-25 Clark BarrettChecking in fix for bug 340 - somehow didn't get checke...
2012-05-24 Dejan JovanovićSeparating the subtheory implementations in the bitvect...
2012-05-24 Dejan JovanovićSignificant changes to the internals of the equality...
2012-05-22 Tim KingThis commit merges in the branch arithmetic/cprop.
2012-05-21 Dejan JovanovićUpdating equality manager to handle tagged trigger...
2012-05-21 Morgan Detersmain() no longer catches non-CVC4 exceptions. This...
2012-05-19 Tim KingAdding regress test for bug 341.
2012-05-19 Tim King- The array type rules were fixed to use isSubtypeOf.
2012-05-18 Tim KingThis commit adds TypeNode::leastCommonTypeNode(). ...
2012-05-18 Tim KingThis commit removes the dead psuedoboolean code.
2012-05-18 Tim KingRemoving long unsigned operator+ from CDList's const_it...
2012-05-18 Dejan Jovanovićremoving failing regression
2012-05-17 Tim KingThis fixes a fascinating segfault. This is the sequenc...
2012-05-17 Morgan DetersFixing an issue with LogicInfo::isPure() that turned...
2012-05-17 Liana HadareanFixed bug 338:
2012-05-17 Tim KingAdding failing regression for ite type computation.
2012-05-17 Dejan JovanovićQueueing up asserted literals in the proxy instead...
2012-05-16 Dejan Jovanovićadding simple-minded handling of (dis-)equalities where...
2012-05-16 Morgan DetersFixing C compatibility library (it still had a referenc...
2012-05-16 Dejan Jovanovićtestcase for bug 337
2012-05-16 Dejan JovanovićChanges to SAT solver:
2012-05-16 Dejan Jovanovićequality status for bitvectors can now look into the...
2012-05-16 Dejan Jovanovićremoving duplicate literals in explanations of propagations
2012-05-16 Liana Hadareanrefactored TheoryBV bitblaster and equality engine...
2012-05-15 Liana Hadareanfixed QF_BV performance problem due to using CDList...
2012-05-15 Dejan Jovanović(no commit message)
2012-05-15 Dejan Jovanovićtest cases
2012-05-15 Tim KingFix to shared terms visitor.
2012-05-15 Morgan DetersImplement TypeNode::isComparableTo() and add a unit...
2012-05-15 Clark BarrettFixed several bugs in shared terms database
2012-05-15 Tim KingThis commit removes the CONST_INTEGER kind from nodes...
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)
next