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

Age	Commit message (Collapse)	Author
2014-10-23	Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.	Morgan Deters
	* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-23	Fixed inefficiency in bit-vector rewrite rule.	lianah

2014-10-22	Fix bug590 regression distcheck failure from last night.	Morgan Deters

2014-10-21	Fixed bug 589	Tianyi Liang

2014-10-21	Fixed bug 590, added regression test	Clark Barrett

2014-10-20	Minor cleanup in datatypes.	ajreynol

2014-10-19	Merge pull request #59 from kbansal/sets3	Kshitij Bansal
	sets type enumerator
2014-10-19	Finish sets type enumerator implementation.	Kshitij Bansal

2014-10-19	fix statistic in decision engine	Kshitij Bansal

2014-10-18	Fix assertion.	ajreynol

2014-10-18	Add dt lemma: zero size implies nullary constructor.	ajreynol

2014-10-18	Fix for bounded integers when incremental, fixes bug 588. Add option ↵	ajreynol
	--dt-binary-split.
2014-10-17	Merge branch '1.4.x'	Morgan Deters

2014-10-17	Remove a bad (unstable, timing-dependent) test.	Morgan Deters

2014-10-17	Minor change for performance according to Andy's suggestion.	Tianyi Liang

2014-10-16	Fix clang warnings	Morgan Deters

2014-10-16	Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ↵	ajreynol
	changes to options.
2014-10-16	Merge branch '1.4.x'	Morgan Deters

2014-10-16	Add Thomas Hunger to THANKS file (for having submitted patches).	Morgan Deters

2014-10-16	Use n-ary splits instead of binary splits in theory datatypes.	ajreynol

2014-10-16	Add dt.size to datatypes theory. Add option for fairness strategy used by ↵	ajreynol
	CEGQI. Improve care graph/equality status for datatypes. Only do FULL effort check in datatypes if no other theories used output channel.
2014-10-14	fix for memory leak in BVQuickCheck	lianah

2014-10-14	Merge pull request #58 from mdeters/smt-attributes	Morgan Deters
	Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.
2014-10-14	Context-dependent expr attributes are now attached to a specific SmtEngine, ↵	Morgan Deters
	and the SAT context is owned by the SmtEngine.
2014-10-14	amend prvs commit	Kshitij Bansal

2014-10-14	trace decision-node	Kshitij Bansal

2014-10-13	CEGQI uses model. Enforce fairness in CEGQI natively.	ajreynol

2014-10-13	Model building into quantifiers engine. Simplify axiom-inst mode.	ajreynol

2014-10-13	Refactor model builder from model engine to quant engine. Work on fairness ↵	ajreynol
	strategy for CEGQI. Add option for single/multi triggers. Minor cleanup.
2014-10-11	Merge branch '1.4.x'	Morgan Deters

2014-10-11	Some defensive programming at destruction time, and fix a latent dangling ↵	Morgan Deters
	pointer bug.
2014-10-10	Merge remote-tracking branch 'origin/1.4.x'	Kshitij Bansal

2014-10-10	Initial draft of CEGQI.	ajreynol

2014-10-10	Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵	Kshitij Bansal
	Rabitti for the report.
2014-10-10	Cleanup	Morgan Deters

2014-10-10	Add owner map to better manage QuantifiersModules. Initial infrastructure ↵	ajreynol
	for cegqi.
2014-10-09	Refactor quantifier prenex option. By default, do not pull quantifiers with ↵	ajreynol
	user patterns.
2014-10-08	Merge branch '1.4.x'	Morgan Deters

2014-10-08	Add unsat cores support to CVC native language.	Morgan Deters

2014-10-08	Some minor cleanup.	Morgan Deters

2014-10-08	Remove private header from public driver.	Morgan Deters

2014-10-07	Fix portoflio issues (debugging code was being called even when tag was off)	Kshitij Bansal

2014-10-07	Merge remote-tracking branch 'upstream/master' into sets-mergable	Kshitij Bansal

2014-10-07	update default Sets options	Kshitij Bansal

2014-10-07	whitespace fixes	Kshitij Bansal

2014-10-08	Cache for getInstance, thanks to Johannes Kanig for the report. Do not ↵	ajreynol
	mkRep for multi triggers.
2014-10-07	add couple of stats	Kshitij Bansal

2014-10-07	sets stronger equality propagator	Kshitij Bansal

2014-10-07	Refactor quantifiers attributes.	ajreynol

2014-10-07	define-const is an extended command, not permitted in strict mode.	Morgan Deters