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

Age	Commit message (Collapse)	Author
2019-03-26	Update copyright headers.	Aina Niemetz

2018-12-10	BoolToBV modes (off, ite, all) (#2530)	makaimann

2018-10-02	Make registration of preprocessing passes explicit (#2564)	Andres Noetzli
	As it turns out, self-registering types are problematic with static linkage [0]. Instead of fixing the issue with linker flags, which seems possible but also brittle (e.g. the flags may be different for different linkers), this commit adds an explicit registration of each preprocessing pass. [0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
2018-10-01	Refactor preprocessing pass registration (#2468)	Andres Noetzli
	This commit refactors how preprocessing pass registration works, inspired by LLVM's approach [0]. The basic idea is that every preprocessing pass declares a static variable of type `RegisterPass` in its source file that registers the pass with the `PreprocessingPassRegistry` when starting the program. The registry is a singleton that keeps track of all the available passes and allows other code to create instances of the passes (note: previously the registry itself was owning the passes but this is no longer the case). One of the advantages of this solution is that we have a list of available passes directly at the beginning of the program, which is useful for example when parsing options. As a side effect, this commit also fixes the SortInference pass, which was expecting arguments other than the preprocessing pass context in its constructor. This commit is required for fixing dumping pre/post preprocessing passes. It is also the ground work for allowing the user to specify a preprocessing pipeline using command-line arguments. [0] https://llvm.org/docs/WritingAnLLVMPass.html
2018-08-01	Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251)	Mathias Preiner

2018-06-25	Updated copyright headers.	Aina Niemetz

2018-05-21	Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)	makaimann

2018-04-25	Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)	yoni206