summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-05-13Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix ↵ajreynol
for sygus.
2015-05-12Added Finn Haedicke as a contributor.Clark Barrett
2015-05-12Merge pull request #74 from finnhaedicke/namespace_minisatbarrettcw
moved Minisat namespace into CVC4
2015-05-11Allow sygus with no syntactic restrictions for LIA. Add regressions.ajreynol
2015-05-11Add missing regression.ajreynol
2015-05-11Support for arbitrary constants/variables in Sygus grammars.ajreynol
2015-05-10Minor improvements to infrastructure. Minor changes to default options. Add ↵ajreynol
tff script. Minor additions to sygus.
2015-05-08Add casc25 fnt script.ajreynol
2015-05-02Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add ↵ajreynol
competition scripts (in progress).
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-27Merge branch 'master' of https://github.com/CVC4/CVC4Clark Barrett
2015-04-27Fixed problem with private/public header clashClark Barrett
2015-04-27Disambiguate namespaces in options, fix permissionsClark Barrett
2015-04-27Updating failing unit tests.Tim King
2015-04-26Bug 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-24More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for ↵ajreynol
fmf mbqi=gen-ev for interpreted operators.
2015-04-24Fix sygus parser for non-tokenized operators, reenable regression. Fix for ↵ajreynol
--fmf-fun.
2015-04-24Fix compiler errors due to unbalanced throw specifiers.Clark Barrett
2015-04-23Merge branch 'master' into googleClark Barrett
2015-04-23Whitespace differenceClark Barrett
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
(mostly whitespace differences).
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of ↵Liana Hadarean
Morgan's proof branch).
2015-04-22Merge pull request #73 from kbansal/parser-dont-tokenizeKshitij Bansal
Parser dont tokenize
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-04-21Fix file permissionsClark Barrett
2015-04-21Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.ajreynol
2015-04-21Adding an example of a tester in SMT2.Tim King
2015-04-18Farkas 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-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-17Merge pull request #72 from kbansal/decision-requirephaseKshitij 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-17moved Minisat namespace into CVC4Finn Haedicke
This avoids conflicts when CVC4 is linked to an application that also uses plain Minisat.
2015-04-16Fix option --quant-fun-wd. Add mk_starexec script to contrib.ajreynol
2015-04-16Handle (degenerate) case of synthesis conjectures for constants. Disable ↵ajreynol
delta lemmas.
2015-04-16disable failing sygus testsKshitij Bansal
2015-04-16update commentKshitij Bansal
2015-04-15string parser builtinop changesKshitij Bansal
2015-04-15bv parserchanges cleanupKshitij Bansal
2015-04-15fp builtinop parser changesKshitij Bansal
2015-04-15fp reorder tokens to match other occurencesKshitij Bansal
2015-04-15THEORY_INTS parser changesKshitij Bansal
2015-04-15THEORY_REAL_INTS parser changesKshitij Bansal
2015-04-15array theory builtinopKshitij Bansal
2015-04-15cleanupKshitij Bansal
2015-04-15dont tokenize bv operators (normal ones)Kshitij Bansal
2015-04-15Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2Tim King
2015-04-15Fix for unconstrained bug.Clark Barrett
2015-04-15Adding an example that violates an assertion during unconstrained ↵Tim King
simplification.
2015-04-13Making CVC4::theory::quantifiers::PrenexQuantMode public for now.Tim King
2015-04-09disable string reqressions timing out after changeKshitij Bansal
2015-04-09DE requests respect requirePhaseKshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback