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

Age	Commit message (Collapse)	Author
2014-06-09	Merge pull request #29 from kbansal/alternatefix	Kshitij Bansal
	Fix for emptyset in smt2 parser, sets translator to quantified logic, misc
2014-06-08	parseErrorHelper : factor out whole word matching	Kshitij Bansal
	catches some corner cases, more readable too
2014-06-08	Previous "repeat" fix required extra lookahead (leading to assert-fails). ↵	Morgan Deters
	Fixed, at the cost of an antlr warning that's safe to ignore for now.
2014-06-08	smt2 parser: tokenize emptyset only if theory enabled	Kshitij Bansal

2014-06-08	Better error when there are \backslashes in \|quoted symbols\|.	Morgan Deters

2014-06-08	Allow 'repeat' as an SMT-LIB user symbol name (UFNIA/vcc-havoc does this).	Morgan Deters

2014-06-06	Sets translate, and other short fixes	Kshitij Bansal
	- $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine
2014-06-04	Add operator support (resolves bug #563).	Morgan Deters

2014-06-04	SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, ↵	Morgan Deters
	bvor, and bvxor.
2014-05-13	Reject native extended ASCII characters. It requires user to use escaped ↵	Tianyi Liang
	sequence for an extended ASCII character.
2014-04-29	Fix for --force-logic to extend its reach to the parser.	Morgan Deters

2014-04-29	fix was compiler warning in antlr_input, crashing test case with the old fix	Kshitij Bansal

2014-04-29	Revert a compiler warning fix from ea6a5a6.	Morgan Deters

2014-04-29	fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr	Tianyi Liang

2014-04-28	Merge remote-tracking branch 'upstream/master' into sets	Kshitij Bansal

2014-04-27	attempt to improve CVC4's "parse error" message	Kshitij Bansal

2014-04-24	Add --inst-max-level=N option for Kshitij. Support define-const command in ↵	Andrew Reynolds
	Smt2.
2014-04-14	Add initial support for co-datatypes.	Andrew Reynolds

2014-04-10	Expand definitions in theory datatypes, now has the expected semantics for ↵	Andrew Reynolds
	incorrectly applied selector terms.
2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
2014-04-09	Handle fmf.card as input from user, add support in SMT2 parser, as requested ↵	Andrew Reynolds
	by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.
2014-04-04	For security, add --no-filesystem-access option, which disables SMT-LIB ↵	Morgan Deters
	script access to filesystem.
2014-03-31	add str to u16/u32, and u16/u32 to str	Tianyi Liang

2014-03-27	adds new feature: re.loop	Tianyi Liang

2014-03-19	Minor usability fixes related to SMT-LIB compliance.	Morgan Deters

2014-03-14	SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). ↵	Morgan Deters
	Thanks to David Cok for the bug report.
2014-03-05	Don't tokenize SET_THEORY operators in smt2 parser	Kshitij Bansal

2014-02-28	add re.nostr for the empty regular expression; add re.allchar for the ↵	Tianyi Liang
	regular expresssion containing all charactors
2014-02-28	a new regular expression engine for solving both positive and negative ↵	Tianyi Liang
	membership constraints
2014-02-28	rename kind::IN to kind::MEMBER (fixes some windows build conflicts)	Kshitij Bansal

2014-02-26	smt-lib syntax change: str.contain -> str.contains; add some prefix syntax ↵	Tianyi Liang
	for cvc format
2014-02-25	Minor code clean up in parser.	Morgan Deters

2014-02-21	add new theory (sets)	Kshitij Bansal
	Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2014-02-20	add negative int2str	Tianyi Liang

2014-02-20	String parsing example in CVC parser	Morgan Deters

2014-02-17	type conversion	Tianyi Liang

2014-02-11	lexer fix: disable smt-lib conversion for string literals	Tianyi Liang

2014-02-06	Minor fix for previous commit	Morgan Deters

2014-02-06	Oops.. premature push on lexer fix (remove debugging output)	Morgan Deters

2014-02-06	Fixes for escape-handling for string literals in SMT-LIBv2 lexer	Morgan Deters

2014-01-29	add prefixof, suffixof	Tianyi Liang

2014-01-09	add constant replace, indexof	Tianyi Liang

2014-01-02	Merge branch '1.3.x'	Morgan Deters

2014-01-02	Update copyright year.	Morgan Deters

2013-12-27	minor fix	Tianyi Liang

2013-12-27	Merge branch '1.3.x'	Morgan Deters

2013-12-27	Fix for ANTLR warning.	Morgan Deters

2013-12-26	new functions in strings	Tianyi Liang

2013-12-24	Better get-value parse error message for common user error.	Morgan Deters

2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters