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

Age	Commit message (Collapse)	Author
2015-05-11	Allow sygus with no syntactic restrictions for LIA. Add regressions.	ajreynol

2015-05-11	Support for arbitrary constants/variables in Sygus grammars.	ajreynol

2015-04-24	More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for ↵	ajreynol
	fmf mbqi=gen-ev for interpreted operators.
2015-04-24	Fix sygus parser for non-tokenized operators, reenable regression. Fix for ↵	ajreynol
	--fmf-fun.
2015-04-23	Added option for --check-unsat-cores and various core bug fixes (merge of ↵	Liana Hadarean
	Morgan's proof branch).
2015-04-22	Merge pull request #73 from kbansal/parser-dont-tokenize	Kshitij Bansal
	Parser dont tokenize
2015-04-16	Handle (degenerate) case of synthesis conjectures for constants. Disable ↵	ajreynol
	delta lemmas.
2015-04-16	update comment	Kshitij Bansal

2015-04-15	string parser builtinop changes	Kshitij Bansal

2015-04-15	bv parserchanges cleanup	Kshitij Bansal

2015-04-15	fp builtinop parser changes	Kshitij Bansal

2015-04-15	fp reorder tokens to match other occurences	Kshitij Bansal

2015-04-15	THEORY_INTS parser changes	Kshitij Bansal

2015-04-15	THEORY_REAL_INTS parser changes	Kshitij Bansal

2015-04-15	array theory builtinop	Kshitij Bansal

2015-04-15	cleanup	Kshitij Bansal

2015-04-15	dont tokenize bv operators (normal ones)	Kshitij Bansal

2015-04-08	Make fun-def quantifiers carry the function app they define, make fun-def ↵	ajreynol
	utilities more robust. Fix bug in conjecture generation for non-parameterized operators.
2015-03-23	Parsing support for define-fun-rec/define-funs-rec.	ajreynol

2015-03-05	Minor fixes. Extend cegqi-si to real arithmetic.	ajreynol

2015-02-06	Handle missing cases for single inv solution reconstruction. Minor fixes. ↵	ajreynol
	Refactor.
2015-01-26	Output solutions for synthesis conjectures with --dump-synth. Minor ↵	ajreynol
	refactor of previous commit.
2015-01-23	Rework inst-closure.	ajreynol

2015-01-22	Add option --lte-partial-inst. Remove inst-closure.	ajreynol

2015-01-21	Initial work on sygusNormalForm.	ajreynol

2015-01-20	Mark datatypes as sygus. Add option to normalize sygus terms in search. ↵	ajreynol
	Add sygus regressions.
2015-01-20	Handle miniscoping of conjunctions in synthesis properties. Refactor ↵	ajreynol
	construction of sygus datatypes. Expand define-fun in evaluators.
2015-01-17	Avoid name conflicts for multiple synth-fun.	ajreynol

2015-01-16	Linearize multiplication by constants in sygus grammars. Handle unary minus ↵	ajreynol
	integer numerals. Refactor to smt2.cpp.
2015-01-16	Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding ↵	ajreynol
	declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.
2015-01-16	Minor: Ensure indexed terms are in EE. Add support for bv constants in ↵	ajreynol
	sygus parser.
2015-01-14	sygus input language and benchmark	Morgan Deters

2015-01-13	Fix typo.	Morgan Deters

2015-01-09	blocked unprintable characters in string literals;	Tianyi Liang
	disabled string literal test case for smtlib v2.5
2014-12-03	Floating point infrastructure.	Martin Brain
	Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-25	Fix bug in --term-db-mode=relevant with variable triggers. Support ↵	ajreynol
	inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
2014-11-12	Fix tokenization of "reset" in SMT-LIB v2.0. It's a reserved word only in 2.5.	Morgan Deters

2014-10-28	Preprocessing step for finding finite runs of well-defined function ↵	ajreynol
	definitions using FMF.
2014-10-28	Initial infrastructure for function definition quantifiers, internal parsing ↵	ajreynol
	format for Smt2.
2014-10-24	Minor parser performance fix.	Morgan Deters

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-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-10	Add owner map to better manage QuantifiersModules. Initial infrastructure ↵	ajreynol
	for cegqi.
2014-10-07	Refactor quantifiers attributes.	ajreynol

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

2014-10-03	More array constants and parsing: better error messages, extend to CVC ↵	Morgan Deters
	presentation language.
2014-10-03	SMT-LIB parser support for array constants (Z3 syntax).	Morgan Deters

2014-09-23	Support :no-pattern.	ajreynol

2014-09-17	Merge branch '1.4.x'	Kshitij Bansal

2014-09-17	Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.	Kshitij Bansal