| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-04-26 | Bug fixes and improvements for mbqi with theory symbols, TheoryModel ↵ | ajreynol | |
| fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions. | |||
| 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-24 | Fix compiler errors due to unbalanced throw specifiers. | Clark Barrett | |
| 2015-04-23 | Merge branch 'master' into google | Clark Barrett | |
| 2015-04-23 | A few more minor updates to match google repository with CVC4 repository | Clark Barrett | |
| (mostly whitespace differences). | |||
| 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-21 | Changes needed to compile at Google, plus some bug fixes from Google. | Clark Barrett | |
| 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-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-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-15 | Fix for unconstrained bug. | Clark Barrett | |
| 2015-04-13 | Making CVC4::theory::quantifiers::PrenexQuantMode public for now. | Tim King | |
| 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 | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback