summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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
2015-04-09Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, ↵ajreynol
and strings preprocessing. Minor fix for conjecture generation for finite types.
2015-04-09Fix performance issue with variable triggers + instantiation restrictions.ajreynol
2015-04-09Bug fix negative contains cache.ajreynol
2015-04-08Make 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-07Removing the reference to THEORY_BOOL from the equality engine. This theoryDejan 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-07Minor fixes for cegqi.ajreynol
2015-04-02Merge pull request #71 from kbansal/const-are-triggersKshitij 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-01Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with ↵ajreynol
fun-def. Add skolemization options.
2015-03-31fix no return value warningKshitij Bansal
2015-03-31fix echo command in --tear-down-incrementalKshitij Bansal
2015-03-28printer change for string smtlib2Tianyi Liang
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2015-03-23Parsing support for define-fun-rec/define-funs-rec.ajreynol
2015-03-23Decouple counter-example guided quantifier instantiation from Sygus.ajreynol
2015-03-16Add requirePhase len(x) = 0.Tianyi Liang
2015-03-16Fixed proof unitialized memory and minor memory leaks.Liana Hadarean
2015-03-14Bug fix for BVTianyi Liang
2015-03-14Patches for 32-bit ARMTianyi Liang
2015-03-14Updating resize for occurence lists to properly resize the whole state.Dejan Jovanovic
2015-03-11Strings split on constant lengths, add length=0 to split lemma for empty string.ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ajreynol
signature. Add regressions.
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-27Revert "dummy commit to force nightly builds"Kshitij Bansal
This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add ↵ajreynol
regressions.
2015-02-25Switch back to eager loop temporarily.Tianyi Liang
2015-02-24minor fix for internal string printTianyi Liang
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-02-18dummy commit to force nightly buildsKshitij Bansal
2015-02-16Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2015-02-16webget: curl follow redirectKshitij Bansal
2015-02-14Fix unit tests.ajreynol
2015-02-14attempt to fix win32 buildsKshitij Bansal
2015-02-13Minor cleanup, remove unused files.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify ↵ajreynol
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
2015-02-12try curl before wget, workaround for issue with FTP PASVKshitij Bansal
2015-02-12Changing CXXFLAGS for custom cln installation in configure.ac.Tim King
Making sure the CVC4 flags do not get overwritten after being set.
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other ↵ajreynol
refactoring.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback