| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-06-09 | Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization ↵ | ajreynol | |
| for non-UF logics. Update SMT COMP scripts accordingly. | |||
| 2015-06-08 | make comment precise | Kshitij Bansal | |
| 2015-06-08 | move delete beyond ifdef CVC4_COMPETITION_MODE | Kshitij Bansal | |
| 2015-06-04 | Minor changes to smt comp script for quantified arith. Add option ↵ | ajreynol | |
| --cbqi-sat whether to disable sat for quantified arith. | |||
| 2015-06-03 | Refactoring of sygus parsing, properly parse Constant/Variable constructors. | ajreynol | |
| 2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol | |
| 2015-06-02 | Add casc 25 tfn script. Change tff script to output instantiations. Work ↵ | ajreynol | |
| towards parsing non-flattened sygus grammars. | |||
| 2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol | |
| 2015-05-29 | Do not enforce dt fairness when single invocation sygus. | ajreynol | |
| 2015-05-29 | changed resource step options to unsigned | lianah | |
| 2015-05-28 | added options for controlling resource step-count for various solving stages | Liana Hadarean | |
| 2015-05-27 | Merge pull request #75 from Dunedune/master | lianah | |
| Added missing LogicException to throws in method lemma. | |||
| 2015-05-25 | Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report. | ajreynol | |
| 2015-05-22 | Added throw LogicException to method lemma. | Jordy Ruiz | |
| 2015-05-15 | Fixes related to cbqi + E-matching. | ajreynol | |
| 2015-05-15 | Avoid ensureLiteral on unpreprocessed formulas in cbqi. | ajreynol | |
| 2015-05-13 | Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ↵ | ajreynol | |
| for sygus. | |||
| 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 | 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-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-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-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 | 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 | |
 |
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