Age | Commit message (Collapse) | Author | |
---|---|---|---|
2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ↵ | ajreynol | |
for sygus. | |||
2015-05-12 | Added Finn Haedicke as a contributor. | Clark Barrett | |
2015-05-12 | Merge pull request #74 from finnhaedicke/namespace_minisat | barrettcw | |
moved Minisat namespace into CVC4 | |||
2015-05-11 | Allow sygus with no syntactic restrictions for LIA. Add regressions. | ajreynol | |
2015-05-11 | Add missing regression. | ajreynol | |
2015-05-11 | Support for arbitrary constants/variables in Sygus grammars. | ajreynol | |
2015-05-10 | Minor improvements to infrastructure. Minor changes to default options. Add ↵ | ajreynol | |
tff script. Minor additions to sygus. | |||
2015-05-08 | Add casc25 fnt script. | ajreynol | |
2015-05-02 | Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add ↵ | ajreynol | |
competition scripts (in progress). | |||
2015-04-28 | Fix smt2 printing of fun-def. Simplification of mbqi interface. | ajreynol | |
2015-04-27 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Clark Barrett | |
2015-04-27 | Fixed problem with private/public header clash | Clark Barrett | |
2015-04-27 | Disambiguate namespaces in options, fix permissions | Clark Barrett | |
2015-04-27 | Updating failing unit tests. | Tim King | |
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 | Whitespace difference | 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-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-17 | moved Minisat namespace into CVC4 | Finn Haedicke | |
This avoids conflicts when CVC4 is linked to an application that also uses plain Minisat. | |||
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 | disable failing sygus tests | Kshitij Bansal | |
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 | 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 | |