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

Age	Commit message (Collapse)	Author
2015-04-21	Fix file permissions	Clark Barrett

2015-04-21	Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.	ajreynol

2015-04-21	Adding an example of a tester in SMT2.	Tim King

2015-04-18	Farkas proof coefficients.	Tim King
	This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear real arithmetic when proofs are enabled. There could be some performance changes due to subtly different search paths being taken. Additional bug fixes: - Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor. To prevent future problems, Monomials should now be made via one of the mkMonomial functions. - Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets(). There was a way to use a row twice in the construction of the conflicts. This was violating an assumption in the Tableau when constructing the intermediate rows. Constraints: - To enable proofs, all conflicts and propagations are designed to go through the Constraint system before they are converted to externally understandable conflicts and propagations in the form of Node. - Constraints must now be given a reason for marking them as true that corresponds to a proof. - Constraints should now be marked as being true by one of the impliedbyX functions. - Each impliedByX function has an ArithProofType associated with it. - Each call to an impliedByX function stores a context dependent ConstraintRule object to track the proof. - After marking the node as true the caller should either try to propagate the constraint or raise a conflict. - There are no more special cases for marking a node as being true when its negation has a proof vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag to the impliedByX (and similar functions). For example,this is now longer both: void setAssertedToTheTheory(TNode witness); void setAssertedToTheTheoryWithNegationTrue(TNode witness); There is just: void setAssertedToTheTheory(TNode witness, bool inConflict);
2015-04-17	Patch for Kshitij's fix on requriePhase	Tianyi Liang

2015-04-17	Merge pull request #72 from kbansal/decision-requirephase	Kshitij Bansal
	https://www.starexec.org/starexec/secure/details/job.jsp?id=6972 The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.
2015-04-16	Fix option --quant-fun-wd. Add mk_starexec script to contrib.	ajreynol

2015-04-16	Handle (degenerate) case of synthesis conjectures for constants. Disable ↵	ajreynol
	delta lemmas.
2015-04-15	Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2	Tim King

2015-04-15	Fix for unconstrained bug.	Clark Barrett

2015-04-15	Adding an example that violates an assertion during unconstrained ↵	Tim King
	simplification.
2015-04-13	Making CVC4::theory::quantifiers::PrenexQuantMode public for now.	Tim King

2015-04-09	disable string reqressions timing out after change	Kshitij Bansal

2015-04-09	DE requests respect requirePhase	Kshitij Bansal

2015-04-09	Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, ↵	ajreynol
	and strings preprocessing. Minor fix for conjecture generation for finite types.
2015-04-09	Fix performance issue with variable triggers + instantiation restrictions.	ajreynol

2015-04-09	Bug fix negative contains cache.	ajreynol

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-04-07	Removing the reference to THEORY_BOOL from the equality engine. This theory	Dejan Jovanovic
	id was used as an internal marker in a set of theories tagging reasons of a propagated disequalities. Replaced it with THEORY_LAST which is not completely kosher but is safe in the context being used.
2015-04-07	Minor fixes for cegqi.	ajreynol

2015-04-02	Merge pull request #71 from kbansal/const-are-triggers	Kshitij Bansal
	change const are triggers from false to true in equality engines Performance comparison: https://www.starexec.org/starexec/secure/details/job.jsp?id=6941 Bug opened for testcase that became much worse: http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621
2015-04-01	Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with ↵	ajreynol
	fun-def. Add skolemization options.
2015-03-31	fix no return value warning	Kshitij Bansal

2015-03-31	fix echo command in --tear-down-incremental	Kshitij Bansal

2015-03-28	printer change for string smtlib2	Tianyi Liang

2015-03-25	change const are triggers from false to true in equality engines	Kshitij Bansal

2015-03-23	Parsing support for define-fun-rec/define-funs-rec.	ajreynol

2015-03-23	Decouple counter-example guided quantifier instantiation from Sygus.	ajreynol

2015-03-16	Add requirePhase len(x) = 0.	Tianyi Liang

2015-03-16	Fixed proof unitialized memory and minor memory leaks.	Liana Hadarean

2015-03-14	Bug fix for BV	Tianyi Liang

2015-03-14	Patches for 32-bit ARM	Tianyi Liang

2015-03-14	Updating resize for occurence lists to properly resize the whole state.	Dejan Jovanovic

2015-03-11	Strings split on constant lengths, add length=0 to split lemma for empty string.	ajreynol

2015-03-11	Minor fixes and improvements to cegqi-si for linear arithmetic.	ajreynol

2015-03-10	CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵	ajreynol
	signature. Add regressions.
2015-03-05	Minor fixes. Extend cegqi-si to real arithmetic.	ajreynol

2015-03-04	More work on arithmetic single invocation synthesis conjectures.	ajreynol

2015-02-27	Revert "dummy commit to force nightly builds"	Kshitij Bansal
	This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.
2015-02-26	Robust strategy for single invocation LIA synthesis conjectures. Add ↵	ajreynol
	regressions.
2015-02-25	Switch back to eager loop temporarily.	Tianyi Liang

2015-02-24	minor fix for internal string print	Tianyi Liang

2015-02-22	New trigger options. --inst-no-entail on by default. Misc cleanup.	ajreynol

2015-02-18	dummy commit to force nightly builds	Kshitij Bansal

2015-02-16	Merge branch 'master' of https://github.com/CVC4/CVC4	Kshitij Bansal

2015-02-16	webget: curl follow redirect	Kshitij Bansal

2015-02-14	Fix unit tests.	ajreynol

2015-02-14	attempt to fix win32 builds	Kshitij Bansal

2015-02-13	Minor cleanup, remove unused files.	ajreynol

2015-02-13	Handle recursive singleton case for codatatypes, add regression. Simplify ↵	ajreynol
	implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.