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

Age	Commit message (Collapse)	Author
2012-12-01	drastic simplification of quantifiers code regarding equality queries, ↵	Andrew Reynolds
	instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
2012-11-30	quantifiers now uses master equality engine, preparation work to cleanup code	Andrew Reynolds

2012-11-02	more minor updates to inst gen and representative selection, clean up of ↵	Andrew Reynolds
	equality query
2012-10-31	cleaning up some of the equality query stuff, implemented a new ↵	Andrew Reynolds
	representative selection strategy for quantifier instantiation
2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-22	Separate public-facing and internal-facing interfaces to Statistics.	Morgan Deters
	The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry). The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it). This is part of the ongoing effort to clean up the public interface. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-07-31	Moving some instantiation-related stuff from src/theory to ↵	Morgan Deters
	src/theory/quantifiers and src/theory/rewriterules. This unclutters the src/theory directory somewhat. The namespaces weren't changed, only the file locations.
2012-07-27	Merge quantifiers2-trunk:	François Bobot
	- new syntax for rewrite rules - better rewrite rules theory - remove the rewriting with rewrite rules during ppRewrite temporarily - theory can define their own candidate generator - define a general candidate generator (inefficient ask to every theory) - split inst_match between the pattern matching used for quantifiers (inst_match.) and the one used for rewrite rules (rr_inst_match.): - the pattern matching is less exhaustive for quantifiers, - the one for rewrite rules can use efficient-e-matching.
2012-07-12	merged fmf-devel branch, includes support for SMT2 command get-value and ↵	Andrew Reynolds
	(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
2012-06-11	Merge from quantifiers2-trunkmerge branch.	Morgan Deters
	Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.