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-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 | 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 | |
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-14 | Fix unit tests. | ajreynol | |
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. | |||
2015-02-11 | Better support for solving multiple functions with cegqi-si. Minor cleanup. | ajreynol | |
2015-02-11 | Move si solution reconstruction to own file, make more robust. Other ↵ | ajreynol | |
refactoring. | |||
2015-02-06 | Handle missing cases for single inv solution reconstruction. Minor fixes. ↵ | ajreynol | |
Refactor. | |||
2015-02-05 | Minor clean up | Tianyi Liang | |
2015-02-05 | Improved string performance, thanks to Peter's benchmarks. | Tianyi Liang | |
2015-02-05 | Working version of sygus solution reconstruction from single inv cegqi. ↵ | ajreynol | |
Heuristics to fit syntax. | |||
2015-02-04 | Initial draft of solution reconstruction into syntax for single inv cegqi. | ajreynol | |