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

Age	Commit message (Collapse)	Author
2020-12-02	Update copyright headers.	Aina Niemetz

2020-12-01	Fix issues related to model declarations (#5560)	Andrew Reynolds
	This corrects two issues related to model declarations: (1) model declaration terms were mistaken not cleared, (2) the model needs to be explicitly destructed before the node manager because it contains references to Node. Fixes #5540
2020-11-26	Removing infrastructure related to SMT model (#5527)	Andrew Reynolds
	Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine. The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
2020-11-23	Add declare model symbol methods to SymbolManager and Model (#5480)	Andrew Reynolds
	This is in preparation for the symbol manager determining which symbols are printed in the model.
2020-10-16	Refactor SMT-level model object (#5277)	Andrew Reynolds
	This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary. Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only. This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-02	Introduce an internal version of Commands. (#4988)	Abdalrhman Mohamed
	This PR is a step towards the migration of Commands to the public API. Node versions of some Commands are introduced for internal use (as necessary). The DumpManager is refactored to make use of those commands.
2020-08-03	Split dump manager from SmtEngine (#4824)	Andrew Reynolds
	Towards splitting SmtEngine. This moves utilities related to managing information for dumping to its own utility, DumpManager. Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.
2020-06-16	Update copyright headers.	Aina Niemetz

2019-11-13	Distinguish unknown status for model printing (#3454)	Andrew Reynolds

2019-03-26	Update copyright headers.	Aina Niemetz

2018-06-25	Updated copyright headers.	Aina Niemetz

2017-08-14	Move function defns from smt_engine_scope.h to cpp (#216)	Andres Noetzli
	Additionally, this commit removes unnecessary includes, adds includes to smt_engine.h in files that require it and removes s_smtEngine_current from smt_engine_scope.h.
2017-07-07	Update copyright headers.	Mathias Preiner

2016-04-20	update from the master	PaulMeng

2016-02-02	Moving dump., command., model., and ite_removal. from smt_util/ to smt/. ↵	Tim King
	Breaking an edge between the sat solver and command.h.