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

Age	Commit message (Collapse)	Author
2017-07-10	Merge ntExt branch. Adds support for transcendental functions. Refactoring ↵	ajreynol
	of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
2017-07-10	Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵	ajreynol
	decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-05	Fix for logic info, update regressions. Update casc tfa script.	ajreynol

2017-07-05	Non-linear supported in ALL logics. Minor fixes for set logic with sygus.	ajreynol

2017-06-30	Minor change to trigger selection, fixes related to subtypes (in macros, ↵	ajreynol
	cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-06-28	Enable non-linear solve by default, update regressions.	ajreynol

2017-06-22	Fix assertion failure due to missing clause id (#180)	Andres Nötzli
	This commit fixes bug 821. As written in the description of the bug, the issue is that `id` is not being set on one of the paths in addClause(), specifically in the case where all but one literal are assigned false and the remaining literal is assigned true. In that case, we are not actually adding anything and set the `id` to `ClauseIdUndef`.
2017-06-21	Properly handle subtypes in smt2 printer.	ajreynol

2017-06-16	Merge pull request #170 from CVC4/fix_2_6_parser3	Clark Barrett
	Parse 'is', 'match' differently for non-DT input
2017-06-16	Fix segfault by making unit conflict CDMaybe	Andres Nötzli
	This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.
2017-06-16	Parse 'is', 'match' differently for non-DT input	Andres Noetzli
	In SMT 2.6, Datatypes are being introduced and they come with testers (indexed identifier of the form (_ is c)) and match expressions. This lead to failures in UFIDL benchmarks in SMT-LIB because they declare the function 'is'. This commit changes the parser s.t. it does not consider 'is' and 'match' special tokens unless the theory of datatypes is enabled.
2017-06-15	Fix for bug 639.	Clark Barrett

2017-06-15	Add regression.	ajreynol

2017-06-02	Fix regression.	ajreynol

2017-06-02	Incorporate datatypes into smt comp script, add regression.	ajreynol

2017-05-31	Fix model construction for BV with cbqi. Minor change to defaults.	ajreynol

2017-05-31	Minor change to defaults, update smt comp script, minor changes to options ↵	ajreynol
	in regressions.
2017-05-26	Checking that equalities belong to the arithmetic theory in the solve() routine.	Tim King

2017-05-20	Fix bug 812.	ajreynol

2017-05-15	Cleanup handling of division (possible fix for bugs 803, 804, 805).	ajreynol

2017-05-15	Merge pull request #158 from 4tXJ7f/fix_sets_rewriter	Andrew Reynolds
	Fix minor bug in sets rewriter
2017-05-15	Fix minor bug in sets rewriter	Andres Noetzli
	As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit.
2017-05-15	Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.	ajreynol

2017-05-10	Do not split on cardinality for string equivalence classes with non-constant ↵	ajreynol
	lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
2017-05-09	Change str.replace for empty string.	ajreynol

2017-05-05	Do not eliminate extended arithmetic symbols when finite model finding is ↵	ajreynol
	on, add regression.
2017-04-28	Minor fixes	ajreynol

2017-04-28	Fix bug for real division.	ajreynol

2017-04-28	Do not eliminate non-standard arithmetic operators in recursive function ↵	ajreynol
	definitions, add regression.
2017-04-24	Fixes and simplifications for fmf mbqi.	ajreynol

2017-04-24	Fix parsing selectors for nullary constructors in smtlib 2.6 format.	ajreynol

2017-04-23	Changing spaces to tabs in Makefile.	Tim King

2017-04-21	Disabled bug639.smt2 which still fails.	Clark Barrett

2017-04-21	Add test cases for bugs 639 and 681.	Clark Barrett

2017-04-21	Fix new relations regressions to use sets-ext.	ajreynol

2017-04-21	Handle subtypes in sets. Bug fixes for tuples with subtypes.	ajreynol

2017-04-20	Support for relational operators identity and join image	Paul Meng

2017-04-19	Fixes for handling set universe: restrict upwards rule for universe to ↵	ajreynol
	memberships into variable sets, do not variable eliminate sets during ppAssert.
2017-04-14	Actively split for upwards closusure intersection. Minor clean up, add ↵	ajreynol
	regressions.
2017-04-14	Fix for fmf-fun when the option is set by user command.	ajreynol

2017-04-07	Change option names for nl.	ajreynol

2017-04-05	Merge pull request #143 from FabianWolff/master	Clark Barrett
	Fix several spelling errors
2017-04-05	Fix bug 698.	ajreynol

2017-04-05	Caching for fun def process, add regression.	ajreynol

2017-04-05	Remove extraneous portion of an nl regression.	ajreynol

2017-04-05	Add non-linear regressions, disable nlAlgSubs, do not do rep checking for ↵	ajreynol
	NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
2017-04-05	Fix several spelling errors	Fabian Wolff

2017-04-04	Enable multi-trigger-linear by default, add option.	ajreynol

2017-04-04	Do not solve for 0-ary non-constant symbols (for which isVar returns true), ↵	ajreynol
	add regressions.
2017-04-02	Adding a model based axiom instantiation scheme for multiplication. Merge ↵	Tim King
	commit for nlAlgMaster.