cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2010-10-23	Removed slack.h, and arith_activity.h. Replaced IsBasicManager with the more ↵	Tim King
	general ArithVarDenseSet. Renamed NextArithRewriter to ArithRewriter.
2010-10-02	branches/arith-indexed-variables merged into the main trunk.	Tim King

2010-07-02	re-generated comment headers of source files	Morgan Deters

2010-06-04	Don't fear the files-changed list, almost all changes are in the	Morgan Deters
	file-level documentation at the top of the sources. This is the "make bugzilla stop bugging me" bugfix commit. * Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy. Updated documentation in the file. Resolves bug #99. * Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.) moved into a separate file. Partially resolves bug #100. * Moved isAssociative(Kind) into kind.h (and into the CVC4::kind namespace) instead of metakind.h (where it was in CVC4::metakind). This clears up a warning (private #inclusion) from the SMT and SMT2 parsers, and maybe makes more sense anyways, since this is based on the kind (and not the metakind) of an operator. * Documentation improvement; doxygen top-level \file gestures, \brief gestures for files, etc. Changed contrib/update-copyright.pl for this change, and post-processed to add \brief. Resolves bug #98. * Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind). They no longer made sense. Resolves bug #91.
2010-05-19	Significant revision to theory/arith. The new draft has a lot of small bug ↵	Tim King
	fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.
2010-04-28	Merging the arithmetic theory draft (lra-init) back into the main trunk. ↵	Tim King
	This should not affect other parts of the system. This code is untested, and is volatile. It is going to be improved in the future so don't pick on it too much. I am merging this code in its current state back into the main trunk because it was getting unruly to keep merging the updated trunk back into the branch.