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

Age	Commit message (Collapse)	Author
2010-02-04	minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵	Morgan Deters
	regenerated configure script
2010-02-04	Added theory output channel interfaces and "Interrupted" exception.	Morgan Deters
	Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs. Updated copyright year. Added a new "bool" theory (right now just to hold a kind.h contribution). Added "kinds" files to UF and the new "bool" theory.
2010-02-04	Fixes to the cnf converter. Also a barebones utility for printing out a ↵	Tim King
	satisifying model.
2010-02-03	adding an option to minisat to not do any debug checks/output	Dejan Jovanović

2010-02-03	Fixing bad commit	Christopher L. Conway

2010-02-03	Adding functions/predicates to SMT grammar	Christopher L. Conway

2010-02-03	Addressed many of the concerns of bug 10 (build system code review).	Morgan Deters
	Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested.
2010-02-03	ELSEIF support and parser debugging with '-d parser'	Dejan Jovanović

2010-02-03	simple ITE parsing	Dejan Jovanović

2010-02-03	By popular demand, I also added a printAst to Expr.	Tim King

2010-02-03	I hacked in a temporary way to restart minisat for multiple queries.	Tim King

2010-02-03	Within node I added printAst(..) for general purpose debugging use ↵	Tim King
	throughout the code. I also added debugPrint() to Node for use within gdb.
2010-02-02	(no commit message)	Dejan Jovanović

2010-02-02	Fixed bug in context code	Clark Barrett

2010-02-02	for tim	Dejan Jovanović

2010-02-02	beginings of test for CDO. one fail	Dejan Jovanović

2010-02-02	Rethrow rewrite in antlr_parser. Taking LT(0) to locate the error causes the ↵	Dejan Jovanović
	build to break on 64-bit machines. Changed to LT(1), it works now, but i'll ask around how this actually works.
2010-02-02	Switched cnf conversion to go through CnfStream.	Tim King

2010-02-02	Minor changes to parser	Christopher L. Conway

2010-02-02	Adding support for escapes in string literals (strings like "\n\t\"")	Dejan Jovanović

2010-02-02	Fixed compile errors	Clark Barrett

2010-02-02	Updates to context:	Clark Barrett
	Use vector instead of linked list for Scopes Added CDO and CDList templates
2010-02-01	Fixing the CVC grammar for parsing Boolean expressions. All the ↵	Dejan Jovanović
	associativity stufff is now in the grammar. All the parser tests pass now.
2010-02-01	fix node manager code (bugzilla #15, comment #2) in case where there's a ↵	Morgan Deters
	hash collision for distinct objects
2010-01-30	cnf conversion (variable-introducing), cleanups, fixes to minisat calling ↵	Morgan Deters
	for multiple-query cases
2010-01-29	fixing the last context build problem, it compiles now	Dejan Jovanović

2010-01-29	one more bug	Clark Barrett

2010-01-29	Fixed compile errors	Clark Barrett

2010-01-29	Adding Makefile.in to svn:ignore	Christopher L. Conway

2010-01-29	Fixing boolean operator precedences	Christopher L. Conway

2010-01-29	Update of context module	Clark Barrett

2010-01-29	fixed CNF conversion, and more modular; CNF conversion command line option; ↵	Morgan Deters
	various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
2010-01-28	Removing Makefile.in's	Christopher L. Conway

2010-01-26	cnf conversion	Morgan Deters

2010-01-26	fixes to build structure, util classes, lots of fixes to Node and ↵	Morgan Deters
	NodeBuilder. outstanding SEGVs fixed
2010-01-25	minor fixes to scoped-context node manager	Morgan Deters

2010-01-25	scoped node managers	Morgan Deters

2010-01-19	minor changes to Theory	Morgan Deters

2009-12-18	More fixes fot the parser tests.	Dejan Jovanović

2009-12-18	Changing some deatils on the parser. Now we know we are done if command is ↵	Dejan Jovanović
	null, or expression is null.
2009-12-18	More fixes	Dejan Jovanović

2009-12-18	numerous fixes to nodes; more coming	Morgan Deters

2009-12-18	more build system fix-ups	Morgan Deters

2009-12-18	Lots of parser changes to make Chris happy. Yet more to come later.	Dejan Jovanović

2009-12-17	more build system fix-ups	Morgan Deters

2009-12-17	update-copyright.pl now retrieves and incorporates author information from ↵	Morgan Deters
	repository history; re-ran update-copyright.pl; cleaned up some things with make
2009-12-17	Adding more parser tests	Christopher L. Conway

2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-17	CvcParserBlack and supporting Makefile changes	Christopher L. Conway

2009-12-17	+ test infrastructure fixes	Morgan Deters
	+ regenerate configure script + add CVC4::Message output class + add some IllegalArgument() assertion things + rename NodeManager::mkExpr() to mkNode()