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

Age	Commit message (Collapse)	Author
2013-06-24	Add files missing from last commit	Morgan Deters

2013-06-24	Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵	Morgan Deters
	allows linearization of div,mod,/ by a constant.
2013-06-24	Add options for symmetry breaking in uf+ss totality axiom approach, option ↵	Andrew Reynolds
	for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
2013-06-19	Merge branch '1.2.x'	Morgan Deters

2013-06-19	Workaround for suspected clang 3.0 codegen bug on Mac	Morgan Deters

2013-06-19	Fix to the "include" extended feature of the SMT-LIB parser	Morgan Deters

2013-06-19	Give a more useful parse error message for "undeclared variable -1".	Morgan Deters
	Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
2013-06-17	Java streams example I forgot to add a long time ago	Morgan Deters

2013-06-17	Make --var-elim-quant true by default. Add rewrite engine to quantifiers ↵	Andrew Reynolds
	module.
2013-06-15	Fix in SMT2 parser for parametric datatypes	Andrew Reynolds

2013-06-09	another fix for array-store-all printing	Morgan Deters

2013-06-09	Better array-store-all output for SMT-LIB.	Morgan Deters

2013-06-08	Fix typos in alttheoryskel	Morgan Deters

2013-06-08	Fixes for Boolean terms in arrays (including fix for bug 517).	Morgan Deters

2013-06-07	One more case for arrays of Boolean.	Morgan Deters

2013-06-07	Fix for bug 517.	Morgan Deters

2013-06-07	Allow disabling include-file feature	Morgan Deters

2013-06-06	small parese issue in IDL	Dejan Jovanović

2013-06-06	typo	Dejan Jovanović

2013-06-06	IDL example theory (to be used with --use-theory=idl).	Dejan Jovanović

2013-06-05	Fix bug in --fmf-fmc for producing models of functions not appearing in ↵	Andrew Reynolds
	quantified formulas.
2013-06-04	File inclusion in Smt2 parser.	Morgan Deters
	The extended command (include-file "filename") now includes file content.
2013-06-04	Add --no-condense-function-values option for explicit function models ↵	Morgan Deters
	(useful in some applications)
2013-06-04	Merge branch '1.2.x'	Morgan Deters

2013-06-04	Fix clang static initialization order issue; fixes bug 512.	Morgan Deters

2013-06-04	Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ↵	Andrew Reynolds
	bounds for bounded integers.
2013-06-03	Merge tag 'casc24'	Morgan Deters

2013-06-03	Updated CASC scripts, as provided to Geoff Sutcliffecasc24	Morgan Deters

2013-05-29	Merge branch '1.2.x'	Morgan Deters

2013-05-29	Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵	Morgan Deters
	unknown key.
2013-05-29	SMT-LIB printer updates (some missing cases).	Morgan Deters

2013-05-29	Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real ↵	Morgan Deters
	division
2013-05-28	Standardize SMT-LIBv2 set of logics to use LogicInfo.	Morgan Deters
	Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics.
2013-05-23	Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.	Andrew Reynolds

2013-05-22	Merge branch 'master' of https://github.com/CVC4/CVC4	Andrew Reynolds
	Conflicts: src/theory/arith/theory_arith_private.cpp src/theory/quantifiers_engine.cpp
2013-05-22	Significant work on bounded integer quantification to handle non-trivial ↵	Andrew Reynolds
	bounds. Refactoring of InstConstantAttribute to be internal to TermDb.
2013-05-22	Add regressions for finite model finding	Andrew Reynolds

2013-05-21	Merge branch '1.2.x'	Morgan Deters

2013-05-21	Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵	Morgan Deters
	to improper ITE removal in quantifier instantiations.
2013-05-21	Fix an error that valgrind found.	Morgan Deters

2013-05-21	Merge branch '1.2.x'	Morgan Deters

2013-05-21	Fix incremental bug in symmetry breaker.	Morgan Deters
	Thanks to Christoph Sticksel for reporting this.
2013-05-20	Merge branch '1.2.x'	Morgan Deters
	Conflicts: library_versions src/parser/parser.h
2013-05-20	Fix error reporting on use of (nonlinear) div,mod,/ symbols	Morgan Deters

2013-05-20	Update THANKS to mention David Cok's contributions.	Morgan Deters

2013-05-20	Detect multiply-defined :named annotations and issue an error.	Morgan Deters
	Thanks to David Cok for pointing out this issue. Conflicts: library_versions
2013-05-20	Fix parsing of SMT-LIBv2 \|quoted\| symbols that span newlines in interactive ↵	Morgan Deters
	mode. Thanks to David Cok for raising this issue.
2013-05-20	Compliance fixes for :named annotations: they must name closed subterms, the ↵	Morgan Deters
	names must be user-permitted names, etc. Thanks to David Cok for raising this issue.
2013-05-20	Don't allow get-model & co after a user push/pop	Morgan Deters
	This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this.
2013-05-20	As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵	Morgan Deters
	takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue.