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

Age	Commit message (Collapse)	Author
2010-08-17	Merge from "cc" branch:	Morgan Deters
	CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes.
2010-07-06	add regressions from bug reports	Morgan Deters

2010-07-04	make dist && make distcheck functional, other fixes	Morgan Deters

2010-06-17	fix some minor annoyances in the regression test Makefiles; add some ↵	Morgan Deters
	documentation
2010-04-04	* Node::isAtomic() now looks at an "atomic" attribute of arguments	Morgan Deters
	instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup.
2010-03-30	Removing unnecessary .gitignores	Christopher L. Conway

2010-03-30	Merging from branches/antlr3 (r246:354)	Christopher L. Conway

2010-02-08	Fixing the test case, it had a unary or. The cnf converter should be adapted ↵	Dejan Jovanović
	to handle cases like this.
2010-02-04	assign expected-status to regressions	Morgan Deters

2010-02-04	build system for multi-level regressions	Morgan Deters

2010-02-04	Moved regressions into various levels based on running time.	Tim King

2010-02-04	test infrastructure updated for multiple-level regressions	Morgan Deters