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

Age	Commit message (Collapse)	Author
2011-04-01	This commit is a merge from the "betterstats" branch, which:	Morgan Deters
	* Makes Options an "omnipresent thread-local global" (like the notion of the "current NodeManager" was already). Options::current() accesses this structure. * Removes Options from constructors and data structures everywhere (this cleans up a lot of things). * No longer uses StatisticsRegistry statically. An instance of the registry is created and linked to a NodeManager. * StatisticsRegistry::current() is similar to Options::current(), but the pointer is stowed in the NodeManager (rather than stored) * The static functions of StatisticsRegistry have been left, for backward compatibility; they now use the "current" statistics registry. * SmtEngine::getStatisticsRegistry() is a public accessor for the registry; this is needed by main() to reach in and get the registry, for flushing statistics at the end.
2010-08-13	Adding the changes to the original copy	Dejan Jovanović

2010-08-13	Removing old version of MiniSat for proper vendor import	Christopher L. Conway

2010-04-15	Adding info in the minisat README	Dejan Jovanović

2010-02-09	Changes to the CNF conversion and the SAT solver. All regression pass now, ↵	Dejan Jovanović
	and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.